Prova por Reescrita

Esse teorema é um pouco mais interessante que anteriores:

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

Assim como mostrado anteriormente, essa é uma prova que dentro de seus argumentos temos uma outra prova, ou hipótese: no caso, temos Equal n m - ou seja, n e m são iguais.

Como n e m são números arbitrários, não podemos só usar simplificação para demonstrar o teorema. Em vez disso, nós observando que, já que assumimos Equal n m, poderíamos substituir n por m no objetivo e os dois lados ficarão iguais. A função que usamos para fazer essa substituição é a Equal.rewrite.

Como não podemos reescrever diretamente no objetivo, nós usamos uma outra igualdade e fazemos ela ser igual ao objetivo. No nosso caso, usaremos um Equal.apply em e para conseguir essa igualdade.

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!

Esse app será do tipo Equal (Plus n n) (Plus m n), como mostrado no comentário. Com isso feito, precisamos trocar o n por m no lado direito da igualdade, e pra isso usamos o 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

O retorno da operação Equal.rewrite já será a prova que precisamos, então só retornamos direto o resultado da função.

Plus_id_exercise

Prove que:

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 = ?