IndProp

Slide 0

Good afternoon!

Slide 1

For the previous lectures, we have seen many ways to define propositions like equations, implications, AND, OR, FORALL and EXISTS.
Today, we are going to define propositions in a more general way, called inductive definition.

Slide 2

We have seen two ways to say a number n is even:

by showing that evenb n is true, or
by showing that n is the double of some number k.
We can also define the evenness of numbers inductively.
The base case says that 0 is even.
The induction case says that if n is even, then n+2 is also even.

Slide 3

We can write the definition in another way:
There is a bar which is annotated by the name of the rule.
The propositions above the bar are the hypothesis.
Those below are the conclusions.
We can read it like this:
ev_0 takes no hypothesis, and infers that 0 is even.
ev_SS takes the evidence that n is even, and infers that n+2 is even.
We can take the conclusion of one inference to satisfy the hypothesis of another inference.
By joining these inferences, we can construct proofs in a tree structure.
Here is how we prove that 4 is even:
By ev_0, we know that 0 is even.
We take the evenness of 0 to satisfy the hypothesis of ev_SS, and infer that 2 is even.
We do it again, so 4 is even. QED.

Slide 4

Let's see how to write it in Coq.
We are using Inductive again, just like how we define inductive data types like natural numbers.
Remember we define nat with two constructors, O and S.
It says, O is a nat, and S takes a nat and to construct another nat.
For ev, it is a proposition that takes a natural number.
You can also read it as a property of natural numbers.
The two constructors are, ev_0 that constructs the evidence for ev 0, and ev_SS that takes the evidence that n is even and constructs the evidence n+2 as even.
As we define this inductive proposition, we also get two "primitive theorems".
If you look at the two constructors ev_0 and ev_SS, their type is actually a theorem.
We will cover more about the relation between types and theorems in our next chapter, called ProofObjects, so for now,

Slide 5

Let's see how to use these "constructor theorems" to prove something else.
(Proof General)
We want to show that 4 is even.
From the proof tree we just seen, we know that the evenness of 4 is based on the evenness of 2 and the theorem ev_SS.
Let's check the type of ev_SS.
It is forall n, ev n -> ev (n+2).
Remember what apply tactic does?
When you do apply ev_SS. our target changes to the evenness of 2.
We apply ev_SS again, and now we need to show that 0 is even.
This comes from ev_0.
Thus, Qed.
We can also treat the constructor theorems as functions, and simply apply this stuff.
Let's try another one.
We hope to show that for all n, if n is even, then 4+n is even.
We first do intros and simpl.
Apply ev_SS twice.
Now we need to show that n is even, which comes from the hypothesis.
If you draw the proof tree, it will be ev n at the top, then ev (n+2) by using inference rule ev_SS, and then ev (n+4) by using ev_SS again.
Any questions?
Let's try some exercises.

Slide 6

ev 0
Answer: One

Slide 7

ev 1
Answer: Zero

Slide 8

ev 2
Answer: One

Slide 9

ev n
Answer: At most one

Slide 10

Add ev_PP
Answer: Finite or infinitely many
For example, in order to show that 0 is even, we can either use ev_0 directly, or apply ev_PP to some evidence that 2 is even.
To show that 2 is even, we can use either apply ev_SS to some evidence that 0 is even, or apply ev_PP to some evidence that 4 is even.
Similarly, for all even numbers, you always have two approaches to prove it, and each approach, except for ev_0, is based on some evidence that another number is even.
Therefore, for all even numbers, there are infinite many proofs for its evenness.
For odd numbers, we still cannot construct a proof for its evenness.
Therefore, adding this rule does not change the semantics of our definition.

Slide 11

Remove ev_0
Answer: Zero
The reason is that we don't have a base case.
In order to prove some natural number is even, we can only apply the remaining two constructors to some evidence that another natural number is even, thus leads to an infinite loop.

Slide 12

Remove ev_0
forall n, ev n -> ev (4 + n)
Answer: Infinitely many
The reason is that our proof does not require ev_0.

Slide 13

So much for the exercises.
We have learnt how to construct a proof that shows a natural number is even.
Let's try to prove some more interesting theorems that have inductive propositions like evenness.
The inductive definition of evenness tells us how to build evidence that some number is even.
It also tells us that the two constructors ev_0 and ev_SS are the only ways to build evidence that numbers of even in the sense of ev.

Slide 14

So once we have an evidence E that says n is even, we know that E must have one of the two shapes:

E is ev_0 and n is 0, or
E is ev_SS applied to n-2 and some evidence that n-2 is even.
Remember that we could do induction and case analysis for natural numbers and lists.
Now we can do the same on evenness.

Slide 15

When we do inversion on a natural number n, we get two cases, n is constructed by either O or S applied to some n'.
When we do inversion on the evidence that n is even, we also get two cases: the evidence is constructed by either ev_0, which tells us that n is 0, or ev_SS applied to n-2, which tells us that n-2 is even.

Slide 16

Let's prove this theorem that if n is even, then n-2 is even.
(Proof General)
In the previous chapter, we have proven the equivalence of evenness in terms of evenb n = true and n is equal to the double some k.
Let's try to show that the ev property is semantically equivalent to our previous definitions.

Slide 17

(Proof General)

Slide 18

Let's try the proof again and see what would happen if we do induction on E.
(Proof General)

Slide 19

Evenness is a single-argument proposition, in other words, a property of natural numbers.
We can also define propositions that take multiple arguments, also known as relations.
For instance, we can define "the less than or equal to" relation with two constructors:

le_n says that any natural number is less than or equal to itself
le_S says that if we have evidence that n is less than or equal to m, then we know that n is less than or equal to m+1
The notation for it is the same as many programming languages like C and Java.

Slide 20

Let's do some sanity checks for the relation we defined to see if it makes sense.
(Proof General)

Slide 21

Once we defined "less than or equal to", we can define "less than" easily.
n is less than m if n+1 is less than or equal to m.
Here are some more examples of relation on numbers, that define a number is the square of another, a number is the next nat of another, and a number is the next even number of another.
As you can see, for these relations, we can also write a function that takes the two numbers and returns a Boolean that says whether they have such relation.
These two styles of defining relations are both used in practice.
The functional definition is decidable, and we can run checking on it.
The inductive definition is usually easier for reasoning and writing proofs.
In order to utilize the benefit of both styles of definitions, we can write them both, and prove that they are equivalent.
So whenever we need to prove one style of definition, we can prove it in the other style instead, and use the equivalence to transform the definition.
Any questions?
So this is a good point for us to wrap up.
For the next lecture, we are going to discuss regular expressions.
If you don't know what regular expressions are, I would suggest that you fill yourself with these knowledge.
See you next week.