Exercises

Prove the following using induction. You may need previously proven results.

Mult_0_r (n: Nat/) : Equal/ Nat/ (Mult n Nat/zero) Nat/zero
Mult_0_r n = ?

Plus_n_sm (n: Nat/) (m: Nat/) : Equal/ Nat/ (Nat/succ (Plus n m)) (Plus n (Nat/succ m))
Plus_n_sm n m = ?

Plus_comm (n: Nat/) (m: Nat/) : Equal/ Nat/ (Plus n m) (Plus m n)
Plus_comm n m = ?

Add_0_r (n: Nat/) : Equal/ Nat/ (Plus n Nat/zero) n
Add_0_r n = ?

Plus_assoc (n: Nat/) (m: Nat/) (p: Nat/) : Equal/ Nat/ (Plus n (Plus m p)) (Plus (Plus n m) p)
Plus_assoc n m p = ?

Consider the following function that doubles its input.

Double (n: Nat/)     : Nat/
Double Nat/zero     = Nat/zero
Double (Nat/succ n) = Nat/succ (Nat/succ (Double n))

Use induction to prove the following theorems about Double:

Double_plus (n: Nat/) : Equal/ Nat/ (Double n) (Plus n n)
Double_plus n = ?

Some theorems require analyzing the best way to prove them, for example, to prove that a number is even, we could prove it for its successor, but that would require us to prove it for the successor of the successor, making the proof of Evenb more difficult by induction. So it's important to realize when it is necessary and when it is not.

Evenb_s (n: Nat/) : Equal/ Bool/ (Evenb (Nat/succ n)) (Notb  (Evenb n))
Evenb_s n = ?

Another case

Let's verify if the equality n +(m + 1) = 1 + (n + m) is true.

First, our problem:

Problems.t2 (n: Nat/) (m: Nat/) : Equal/ Nat/ (Plus n (Nat/succ m)) (Nat/succ (Plus n m))

We verify the base case, when n is zero:

Problems.t2 Nat/zero m = Equal/refl

and move on to the next case

Problems.t2 (Nat/succ n) m = ?

and our current goal becomes:

• Expected: Prop.Equal Data.Nat (Data.Nat.succ (Plus n (Data.Nat.succ m))) (Data.Nat.succ (Data.Nat.succ (Plus n m)))

Translating, the successor of the addition of n and the successor of m is equal to the successor of the successor of the addition of n and m. To solve this problem, we will invoke induction:

let ind = Problems.t2 n m

and our current goal is to prove that:

• Expected: Prop.Equal Data.Nat (Data.Nat.succ (Plus n (Data.Nat.succ m))) (Data.Nat.succ (Data.Nat.succ (Plus n m)))

Again, translating, that the successor of the addition of n and the successor of m is equal to the successor of the successor of the addition of n and m.

But now we have a very useful tool, our variable ind which is:

Equal/ Nat/ (Plus n (Nat/succ m)) (Nat/succ (Plus n m))

Now, analyzing our goal and our variable ind, we can see that it is enough to add Nat.succ to both sides of the induction, and it will be exactly the same as our goal. To do this, we will use a lambda function:

let app = Equal/apply (x => (Nat/succ x)) ind

And our variable app will return our goal:

Equal/ Nat/ (Nat/succ (Plus n (Nat/succ m))) (Nat/succ (Nat/succ (Plus n m)))

Just return app and Kind will give us the coveted All terms check.

Using other theorems

In Kind, as in informal mathematics, large proofs are often divided into a sequence of theorems, with later proofs referring to earlier theorems. But sometimes a proof will require some varied fact that is too trivial and of too little general interest to give it its own higher-level name. In these cases, it is convenient to be able to simply state and prove the necessary "sub-theorem" exactly at the point where it is used.

Let's analyze the following addition commutation theorem:

Problems.t3 (n: Nat/) (m: Nat/) : Equal/ Nat/ (Plus n  m) (Plus m n)

In the first case, for n and m equal to zero we have a reflection:

Problems.t3 Nat/zero Nat/zero = Equal/refl

So we move on to the next case:

Problems.t3 (Nat/succ n) m = ?

And here it seems that we have a new problem:

Expected: Prop.Equal Data.Nat (Data.Nat.succ (Plus n m)) (Plus m (Data.Nat.succ n))

Analyzing the problem, we realize that there is a theorem already proven within it, that the successor of the addition of two numbers is equal to the addition of one number with its successor, so we can use that to our advantage.

We will start by applying a Nat.succ to our original problem:

let ind_a = Equal/apply (x => (Nat/succ x)) (Problems.t3 n m )

Then we invoke our already solved problem, Problems.t2:

let ind_b = Problems.t2 m n

When we give the Type Check, the terminal returns:

+ INFO  Inspection.

   • Expected: (Equal Nat (Nat.succ (Plus n m)) (Plus m (Nat.succ n))) 

   • Context: 
   •   n     : Nat 
   •   m     : Nat 
   •   ind_a : (Equal Nat (Nat.succ (Plus n m)) (Nat.succ (Plus m n))) 
   •   ind_a = (Equal.apply Nat Nat (Plus n m) (Plus m n) (x => (Nat.succ x)) (Problems.t3 n m)) 
   •   ind_b : (Equal Nat (Plus m (Nat.succ n)) (Nat.succ (Plus m n))) 
   •   ind_b = (Problems.t2 m n) 
 
   let ind_b = Problems.t2 m n
     ?
     ┬
     └Here!

Now we can see that the first part of ind_a is the inverse of the first part of our goal and the first part of ind_b is equal to the second part of the goal, we just need to organize and join the necessary parts. To do this, we will use Equal.mirror and Equal.chain.

let ind_c = Equal/chain ind_b Equal/mirror ind_a

And ind_c returns a value similar to the desired one:

• Expected: Prop.Equal Data.Nat (Data.Nat.succ (Plus n m)) (Plus m (Data.Nat.succ n))
•   ind_c : Prop.Equal Data.Nat (Plus m (Data.Nat.succ n)) (Data.Nat.succ (Plus n m))

We can see that one is the other mirrored, to make them equal, we will use Equal.mirror again:

let app = Equal/mirror ind_c

When we call app, the Type Check returns the message All terms checked and thus we prove, through induction and using another proof, the commutation of addition, that the sum of n and m is equal to the sum of m and n.