Proof by Rewriting

This theorem is a bit more interesting than the previous ones:

Plus_id_example (n: Nat) (m: Nat) (e: Equal/ Nat n m) : Equal/ Nat (Plus n n) (Plus m m)

As shown before, this is a proof that has another proof or hypothesis within its arguments: in this case, we have Equal n m - meaning, n and m are equal.

Since n and m are arbitrary numbers, we can't just use simplification to prove the theorem. Instead, we observe that, since we assume Equal n m, we could substitute n for m in the goal and both sides will be equal. The function we use to perform this substitution is Equal.rewrite.

Since we can't rewrite directly in the goal, we use another equality and make it equal to the goal. In our case, we will use an Equal.apply on e to obtain this equality.

Plus_id_example (n: Nat) (m: Nat) (e: Equal/ Nat n m) : Equal/ Nat (Plus n n) (Plus m m)

Plus_id_example n m e =
  let app = Equal/apply (k => Plus k n) e
  ? 

+ INFO  Inspection.

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

   • Context: 
   •   n   : Nat 
   •   m   : Nat 
   •   e   : Equal Nat n m 
   •   app : Equal Nat (Plus n n) (Plus m n) 
   •   app = Equal.apply Nat Nat n m (k => (Plus k n)) e
    
   let app = Equal.apply (k => Plus k n) e
      ?
      ┬
      └Here!

This app will be of type Equal (Plus n n) (Plus m n), as shown in the comment. With this done, we need to replace n with m on the right-hand side of the equality, and for that we use rewrite:

Plus_id_example (n: Nat) (m: Nat) (e: Equal/ Nat n m) : Equal/ Nat (Plus n n) (Plus m m)
Plus_id_example n m e =
  let app = Equal/apply (k => Plus k n) e
  let rrt = Equal/rewrite e (x => Equal/ (Plus n n) (Plus m x)) app
  rrt

+ INFO  Inspection.

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

   • Context: 
   •   n   : Nat 
   •   m   : Nat 
   •   e   : Equal Nat n m 
   •   app : Equal Nat (Plus n n) (Plus m n) 
   •   app = Equal.apply Nat Nat n m (k => (Plus k n)) e 
   •   rrt : Equal Nat (Plus n n) (Plus m m) 
   •   rrt = Equal.rewrite Nat n m e (x => Equal Nat (Plus n n) (Plus m x)) app

The return value of the Equal.rewrite operation will be the proof we need, so we just return the result directly from the function.

Plus_id_exercise

Prove that:

Plus_id_exercise (n: Nat) (m: Nat) (o: Nat) (e1: Equal/ Nat n m) (e2: Equal/ Nat m o) : Equal/ Nat (Plus n m) (Plus m o)
Plus_id_exercise n m o e1 e2 = ?