Prova por Simplificação

Agora que definimos alguns tipos de dados e funções, vamos começar a provar propriedades de seus comportamentos. Na verdade, já estamos fazendo isso: cada função das seções anteriores que começa com Test, faz uma afirmação precisa sobre o comportamento de alguma função para algumas entradas especificas. As provas dessas afirmações foram sempre a mesma: use Equal.refl para checar que ambos os lados são de fato idênticos.

O mesmo tipo de "prova por simplificação" pode ser usada para provar propriedades mais interessantes. Por exemplo, o fato que o Nat.zero é um "elemento neutro" no lado esquerdo da adição pode ser provado apenas observando que Plus Nat.zero n reduz para n, independente do que é n, fato que pode ser lido diretamente na definição do Plus.

Plus_Z_n (n: Nat) : Equal Nat (Plus Nat.zero n) n
Plus_Z_n n = Equal.refl

Outros teoremas parecidos podem ser provados de forma parecida.

Plus_1_l (n: Nat) : Equal Nat (Plus (Nat.succ Nat.zero) n) (Nat.succ n)
Plus_1_l n = Equal.refl

Mult_0_l (n: Nat) : Equal Nat (Mult Nat.zero n) Nat.zero
Mult_0_l n = Equal.refl 

O _l indica que a prova envolve o valor no lado esquerdo. Por exemplo: A prova da soma por 1 no lado esquerdo (Plus_1_l) ou a prova da multiplicação por zero no lado esquerdo (Mult_0_l)

Embora a simplificação seja poderosa o suficiente para provar alguns fatos gerais, existem várias declarações que não podem ser demonstradas só com simplificação. Por exemplo, não podemos usá-la para provar que Nat.zero é um elemento neutro para adição no lado direito.

Plus_n_Z (n: Nat) : Equal Nat n (Plus n Nat.zero)
Plus_n_Z n = Equal.refl

- ERROR Type mismatch  

   • Got      : Equal Nat n n
   • Expected : Equal Nat n (Plus n 0n)

   • Context: 
   •   n : Nat 

   Plus_n_Z n = Equal.refl
                ┬─────────
                └Here!

(Você consegue explicar por que isso acontece?)

O próximo capítulo vai introduzir o conceito de indução, uma técnica poderosa que pode ser usada para demonstrar esse teorema. Por agora, no entanto, vamos ver mais alguns tipos simples de prova.