More exercises

You can use rewrite or chain in this proof, choose whichever you find easiest.

Plus_swap (n: Nat) (m: Nat) (p: Nat) : Equal Nat (Plus n (Plus m p)) (Plus m (Plus n p))
Plus_swap n m p = ?

Now prove the commutativity of multiplication. (You will probably need to define and prove a separate auxiliary theorem to be used in the proof of this. You may find Plus_swap useful.)

Mult_comm (n: Nat) (m: Nat) : Equal Nat (Mult n m) (Mult m n)
Mult_comm n m = ?

Take a piece of paper. For each of the following theorems, first think whether (a) it can be proven using just simplification and rewriting, (b) also requires case analysis (destruction), or (c) also requires induction. Write down your prediction.

Then, fill in the proof. (There is no need to submit your piece of paper; this is just to encourage you to reflect before hacking!)

Lte_refl (n: Nat) : Equal Bool Bool.true (Lte n n)
Lte_refl n = ?

Zero_nbeq_s (n: Nat) : Equal Bool (Eql (Nat.zero) (Nat.succ n)) Bool.false
Zero_nbeq_s n = ?

And_false_r (b: Bool) : Equal Bool (Andb b Bool.false) Bool.false
And_false b = ?

S_nbeq_0 (n: Nat) : Equal Bool (Eql (Nat.succ n) Nat.zero) Bool.false

Mult_1_l (n: Nat) : Equal Nat (Mult (Nat.succ Nat.zero) n) n
Mult_1_l n = ?

All3_spec (b: Bool) (c: Bool) : Equal Bool (Orb (Orb (Andb b c) (Notb  b)) (Notb  c)) Bool.true
All3_spec b c = ?

Mult_plus_distr_r (n: Nat) (m: Nat) (p: Nat) : Equal Nat (Mult (Plus n m) p) (Plus (Mult n p) (Mult m p))
Mult_plus_distr_r n m p = ?

Mult_assoc (n: Nat) (m: Nat) (p: Nat) : Equal Nat (Mult (Mult m p)) (Mult (Mult n m) p)
Mult_assoc n m p = ?