Prova por aplicação

A nossa primeira ferramenta para resolver provas que não são reduzíveis de cara será a aplicação dos dois lados. Para isso, usaremos a função Equal.apply, que recebe uma igualdade (um Equal) e uma função, e aplica essa função dos dois lados da igualdade, gerando uma nova igualdade.

Por exemplo:

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

O que exatamente temos aqui? Temos uma prova que recebe como argumento uma outra prova/igualdade. Isso quer dizer que vamos realizar a nossa prova supondo que a prova dada como argumento também é verdadeira. Então, lendo a declaração da prova, temos que: "Dados dois naturais, m e n, e uma prova de que eles são iguais, provar que Nat.succ m e Nat.succ n também são iguais".

Nós aprendemos, nas nossas aulas de matemática, que aplicar uma função dos dois lados de uma igualdade mantém a igualdade (x/2 = 3 -> 2*x/2 = 2*3), e podemos ver que para provar o que a gente quer, precisamos aplicar a função Nat.succ nos dois lados de e, usando 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!

Como o Equal.apply funciona: Ele recebe como primeiro argumento a função a ser aplicada dos dois lados, e como segundo argumento a igualdade aonde aplicar a função. Se você não entendeu muito bem a passagem da função de argumento (x => Nat.succ x), ela é o que chamamos de função lambda, e é também conhecida como função anônima. Funções lambda são identificadas pela sua seta =>, sendo que do lado esquerdo da seta fica o nome do argumento da função - use o nome que quiser - e do lado direito fica o corpo da função: o que ela retorna. A nossa função lambda atual é uma função que recebe um x qualquer e retorna Nat.succ x.

Podemos ver o resultado disso dando check no arquivo:

+ 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!

Como e_apply é uma igualdade do tipo Equal Nat (Nat.succ m) (Nat.succ n), a prova que procuramos, é só retornar ele e concluiremos a nossa prova.

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.