Proof by Application

Our first tool for proving non-trivial theorems will be applying functions to both sides of an equality. For this, we will use the function Equal.apply, which takes an equality (Equal) and a function, and applies this function to both sides of the equality, generating a new equality.

For example:

Example_apply (n: Nat) (m: Nat) (e: Equal/ Nat m n) : Equal/ Nat (Nat.succ m) (Nat.succ n)
Example_apply n m e = ?

What do we have here? We have a proof that takes another proof/equality as argument. This means that we will carry out our proof assuming that the proof given as argument is also true. So, reading the statement of the proof, we have: "Given two naturals, m and n, and a proof that they are equal, prove that Nat.succ m and Nat.succ n are also equal".

We learned in our math classes that applying a function to both sides of an equality preserves the equality (x/2 = 3 -> 2x/2 = 23), and we can see that to prove what we want, we need to apply the function Nat.succ to both sides of e, using Equal.apply.

+ INFO  Inspection.

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

  • Context: 
  •   n : Nat 
  •   m : Nat 
  •   e : (Equal Nat m n) 

  Example_apply n m e = ?
                        ┬
                        └Here!

How does Equal.apply work: It takes as first argument the function to be applied to both sides, and as second argument the equality to which to apply the function. If you didn't understand the passage of the argument function (x => Nat.succ x), it is what we call a lambda function, and is also known as an anonymous function. Lambda functions are identified by their arrow =>, where on the left side of the arrow is the name of the function argument - use any name you want - and on the right side is the body of the function: what it returns. Our current lambda function is a function that takes any x and returns Nat.succ x.

We can see the result of this by check the file:

+ INFO  Inspection.

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

  • Context: 
  •   n : Nat 
  •   m : Nat 
  •   e       : (Equal Nat m n) 
  •   e_apply : (Equal Nat (Nat.succ m) (Nat.succ n)) 
  •   e_apply = (Equal.apply Nat Nat m n (x => (Nat.succ x)) e) 

  let e_apply = Equal.apply (x => Nat.succ x) e
      ?
      ┬
      └Here!

As e_apply is an equality of type Equal/ Nat (Nat.succ m) (Nat.succ n), the proof we are looking for is simply to return it, and we will have concluded our proof.

Example_apply (n: Nat) (m: Nat) (e: Equal/ Nat m n) : Equal/ Nat (Nat.succ m) (Nat.succ n)
Example_apply n m e =
  let e_apply = Equal/apply (x => Nat.succ x) e
  e_apply

  All terms checked.