Equal.chain and Equal.mirror

In this section we will not discuss any inherently new tool, but rather some proof utilities to make use of the previous tools easier.

Consider the example:

Example_mirror (a: Nat) (b: Nat) (e: Equal Nat a b) : Equal Nat b a

It seems like a trivial example. If a is equal to b, then b is equal to a, right? Although correct, the type checker of Kind does not recognize this equality, because for it, the order is important. For such situations, we have the function Equal.mirror, which simply swaps the sides of an equality.

Example_mirror (a: Nat) (b: Nat) (e: Equal Nat a b) : Equal Nat b a
Example_mirror a b e = 
   let mir = Equal.mirror e
   mir

+ INFO  Inspection.

   • Expected: Equal Nat b a 

   • Context: 
   •   a   : Nat 
   •   b   : Nat 
   •   e   : Equal Nat a b
   •   mir : Equal Nat b a 
   •   mir = Equal.mirror Nat a b e

Although it may not seem very useful at the moment, this operation is very useful for our second utility: Equal.chain. Equal.chain is a specific case of Equal.rewrite, in which you rewrite an entire side of an equality using another.

Example_chain (a: Nat) (b: Nat) (c: Nat) (e1: Equal Nat b (Plus a a)) (e2 : Equal Nat c (Plus a a)) : Equal Nat b c

Since we already know Equal.rewrite, we could use it to solve this theorem, but instead we will use Equal.chain.Equal.chain works by "chaining" two equalities that have the same expression on the right side of the first equality and on the left side of the second, "gluing" these equalities together by the common expression, generating a new equality with the other two expressions (Equal.chain (a = b) (b = c) = (a = c)). For example, in our example, the right side of the two equalities is equal. If we use Equal.mirror on one of them, we can then use Equal.chain on them:

Example_chain (a: Nat) (b: Nat) (c: Nat) (e1: Equal Nat b (Plus a a)) (e2 : Equal Nat c (Plus a a)) : Equal Nat b c
Example_chain a b c e1 e2 =
  let e3 = Equal.mirror e2
  let chn = Equal.chain e1 e3

+ INFO  Inspection.

   • Expected: Equal Nat b c

   • Context: 
   •   a   : Nat 
   •   b   : Nat 
   •   c   : Nat 
   •   e1  : Equal Nat b (Plus a a) 
   •   e2  : Equal Nat c (Plus a a) 
   •   e3  : Equal Nat (Plus a a) c
   •   e3  = Equal.mirror Nat c (Plus a a) e2
   •   chn : Equal Nat b c
   •   chn = Equal.chain Nat b (Plus a a) c e1 e3