Equal.chain e Equal.mirror

Nessa parte não falaremos de nenhuma ferramenta inerentemente nova, mas sim de alguns utilitários de provas para facilitar o uso das ferramentas anteriores.

Imagine o exemplo:

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

Parece um exemplo trivial. Se a é igual a b, b é igual a a, correto? Apesar de correto, o type checker do Kind não reconhece essa igualdade, pois para ele, a ordem é importante. Para esse tipo de situação, temos a função Equal.mirror, que simplesmente troca os lados de uma igualdade.

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

Apesar de não parecer muito útil no momento, essa operação é muito útil para nosso segundo utilitário: Equal.chain. Equal.chain é um caso específico do Equal.rewrite, no qual você reescreve um lado inteiro de uma igualdade usando outra.

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

Como nós já conhecemos o Equal.rewrite, poderíamos usar ele para resolver esse teorema, mas ao invés disso vamos usar o Equal.chain. Equal.chain funciona "encadeando" duas igualdades que tenham a mesma expressão no lado direito da primeira igualdade e no lado esquerdo da segunda, "grudando" essas igualdades pela expressão em comum, gerando uma nova igualdade com as outras duas expressões (Equal.chain (a=b) (b=c) = (a=c)). Por exemplo, no nosso exemplo, o lado direito das duas igualdades é igual. Se usarmos Equal.mirror em uma delas, podemos dar Equal.chain nelas:

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