Proof by Case Analysis

The next tool for formal proofs will be case analysis, which means using pattern matching in the proof. For example, let's prove that the logical AND of anything and False is always False:

Example_case_analysis (b: Bool/) : Equal/ Bool/ (Andb b1 Bool/false) Bool/false
Example_case_analysis b = ?

Although it may seem like a proof that could be solved simply with Equal/refl, it's not the case. This is because the Andb function pattern matches on the first argument, and we don't have its value in the proof, so it remains "stuck".

To give a value to it and show that the proof is correct for both Bool values, we pattern match in the proof, creating two different proofs: one for when b is Bool/true and one for when it's Bool/false.

Example_case_analysis (b: Bool/) : Equal/ Bool/ (Andb b Bool/false) Bool/false
Example_case_analysis Bool/true  = ?
Example_case_analysis Bool/false = ?

And both of these proofs are directly solvable with Equal/refl, since the type checker can reduce both of them to Equal Bool.false Bool.false directly.

Example_case_analysis (b: Bool/) : Equal/ Bool/ (Andb b Bool/false) Bool/false
Example_case_analysis Bool/true  = Equal/refl
Example_case_analysis Bool/false = Equal/refl