Proof by Simplification
Now that we have defined some data types and functions, let's start proving properties of their behaviors. In fact, we have already been doing this: each function in the previous sections that starts with Test makes a precise assertion about the behavior of some function for specific inputs. The proofs of these assertions were always the same: use Equal.refl to check that both sides are indeed identical.
The same type of "proof by simplification" can be used to prove more interesting properties. For example, the fact that Nat.zero is a "neutral element" on the left-hand side of addition can be proven simply by observing that Plus Nat.zero n reduces to n, regardless of what n is, a fact that can be read directly from the definition of Plus.
Plus_Z_n (n: Nat) : Equal Nat (Plus Nat.zero n) n
Plus_Z_n n = Equal.reflOther similar theorems can be proven in a similar way.
Plus_1_l (n: Nat) : Equal Nat (Plus (Nat.succ Nat.zero) n) (Nat.succ n)
Plus_1_l n = Equal.refl
Mult_0_l (n: Nat) : Equal Nat (Mult Nat.zero n) Nat.zero
Mult_0_l n = Equal.refl The _l indicates that the proof involves the value on the left-hand side. For example: the proof of adding 1 on the left-hand side (Plus_1_l) or the proof of multiplying by zero on the left-hand side (Mult_0_l).
Although simplification is powerful enough to prove some general facts, there are several statements that cannot be demonstrated with simplification alone. For example, we cannot use it to prove that Nat.zero is a neutral element for addition on the right-hand side.
Plus_n_Z (n: Nat) : Equal Nat n (Plus n Nat.zero)
Plus_n_Z n = Equal.refl- ERROR Type mismatch
• Got : Equal Nat n n
• Expected : Equal Nat n (Plus n 0n)
• Context:
• n : Nat
Plus_n_Z n = Equal.refl
┬─────────
└Here!
(Can you explain why this is?)
The next chapter will introduce the concept of induction, a powerful technique that can be used to demonstrate this theorem. For now, however, let's see some more simple types of proof.