Exercícios

Prove o seguinte usando indução. Você pode precisar de resultados previamente comprovados.

Mult_0_r (n: Nat) : Equal Nat (Mult n Nat.zero) Nat.zero
Mult_0_r n = ?

Plus_n_sm (n: Nat) (m: Nat) : Equal Nat (Nat.succ (Plus n m)) (Plus n (Nat.succ m))
Plus_n_sm n m = ?

Plus_comm (n: Nat) (m: Nat) : Equal Nat (Plus n m) (Plus m n)
Plus_comm n m = ?

Add_0_r (n: Nat) : Equal Nat (Plus n Nat.zero) n
Add_0_r n = ?

Plus_assoc (n: Nat) (m: Nat) (p: Nat) : Equal Nat (Plus n (Plus m p)) (Plus (Plus n m) p)
Plus_assoc n m p = ?

Considere a seguinte função que dobra o argumento recebido

Double (n: Nat)     : Nat
Double Nat.zero     = Nat.zero
Double (Nat.succ n) = Nat.succ (Nat.succ (Double n))

Use indução para provar esses seguintes teoremas sobre Double:

Double_plus (n: Nat) : Equal Nat (Double n) (Plus n n)
Double_plus n = ?

Alguns teoremas é necessário analisar a melhor forma de se provar, por exemplo, para provar que um numero é par, poderíamos provar pelo sucessor dele, mas isso nos faria ter que provar para o sucessor do sucessor dele, isso faz com a que a prova de Evenb ser mais difícil por indução, então é importante perceber quando é necessário e quando não é.

Evenb_s (n: Nat) : Equal Bool (Evenb (Nat.succ n)) (Notb  (Evenb n))
Evenb_s n = ?

Outro caso

Vamos verificar se a a igualdade "n +(m + 1) = 1 + (n + m)" é verdadeira

Primeiro, o nosso problema:

Problems.t2 (n: Nat) (m: Nat) : Equal Nat (Plus n (Nat.succ m)) (Nat.succ(Plus n m))

Verificamos o primeiro caso, quando n é zero:

Problems.t2 Nat.zero m = Equal.refl

e partimos para o caso seguinte

Problems.t2 (Nat.succ n) m = ?

e o nosso objetivo atual vira:

• Expected: Equal Nat (Nat.succ (Plus n (Nat.succ m))) (Nat.succ (Nat.succ (Plus n m)))

Traduzindo, o sucessor da adição de n e o sucessor de m é igual ao sucessor do sucessor da adição de n e m. Para resolver esse problema, invocaremos a indução:

let ind = Problems.t2 n m

e o nosso objetivo atual é provar que:

• Expected: Equal Nat (Nat.succ (Plus n (Nat.succ m))) (Nat.succ (Nat.succ (Plus n m)))

Traduzindo novamente, que o sucessor da adição de n e o sucessor de m é igual ao sucessor do sucessor da adição de n e m.

mas agora nós temos uma ferramenta muito útil, a nossa variável ind que é:

Equal Nat (Plus n (Nat.succ m)) (Nat.succ (Plus n m))

Ora, analisando o nosso objetivo e a nossa variável ind, podemos perceber que basta dar um Nat.succ em ambos os lados da indução e ela ficará exatamente igual ao nosso objetivo, para isso usaremos uma função lambda:

let app = Equal.apply (x => (Nat.succ x)) ind

E a nossa variável app retornará o nosso objetivo:

Equal Nat (Nat.succ (Plus n (Nat.succ m))) (Nat.succ (Nat.succ (Plus n m)))

Bastando apenas retornar o app para e o Kind nos retornará o tão almejado All terms check.

Usando outros teoremas

Em Kind, como na matemática informal, grandes provas são frequentemente divididas em uma sequência de teoremas, com provas posteriores referindo-se a teoremas anteriores. Mas às vezes uma prova exigirá algum fato variado que é muito trivial e de muito pouco geral interesse em dar-lhe o seu próprio nome de nível superior. Nesses casos, é conveniente ser capaz de simplesmente enunciar e provar o “sub-teorema” necessário exatamente no ponto onde é usado.

Analisemos o seguinte teorema da comutação da adição:

Problems.t3 (n: Nat) (m: Nat) : Equal Nat (Plus n  m) (Plus m n)

No primeiro caso, para n e m igual a zero nós temos uma reflexão:

Problems.t3 Nat.zero Nat.zero = Equal.refl

Então partimos para o próximo caso:

Problems.t3 (Nat.succ n) m = ?

E aqui parece que temos um novo problema:

Expected: Equal Nat (Nat.succ (Plus n m)) (Plus m (Nat.succ n))

Ao analisar o problema, percebemos que dentro dele há um teorema já provado, de que o sucessor da adição de dois números é igual a adição de um número com o sucessor dele, então podemos usar isso ao nosso favor.

Começaremos aplicando um Nat.succ no nosso problema original:

let ind_a = Equal.apply (x => (Nat.succ x)) (Problems.t3 n m )

Depois invocaremos nosso problema já resolvido, o Problems.t2:

let ind_b = Problems.t2 m n

Ao dar o Type Check, o terminal nos retorna:

+ INFO  Inspection.

   • Expected: (Equal Nat (Nat.succ (Plus n m)) (Plus m (Nat.succ n))) 

   • Context: 
   •   n     : Nat 
   •   m     : Nat 
   •   ind_a : (Equal Nat (Nat.succ (Plus n m)) (Nat.succ (Plus m n))) 
   •   ind_a = (Equal.apply Nat Nat (Plus n m) (Plus m n) (x => (Nat.succ x)) (Problems.t3 n m)) 
   •   ind_b : (Equal Nat (Plus m (Nat.succ n)) (Nat.succ (Plus m n))) 
   •   ind_b = (Problems.t2 m n) 
 
   let ind_b = Problems.t2 m n
     ?
     ┬
     └Here!

Agora podemos perceber que a primeira parte da ind_a é igual ao inverso da primeira parte do nosso objetivo e a primeira parte da ind_b é igual a segunda do objetivo, basta apenas organizar e juntar as partes necessárias. Para isso usaremos a Equal.mirror e a Equal.chain.

let ind_c = Equal.chain ind_b Equal.mirror ind_a

E o ind_c nos retorna um valor similar ao desejado:

• Expected: Equal Nat (Nat.succ (Plus n m)) (Plus m (Nat.succ n))
•   ind_c : Equal Nat (Plus m (Nat.succ n)) (Nat.succ (Plus n m))

Podemos perceber que um é o outro espelhado, para torná-los iguais, usaremos o Equal.mirror novamente:

let app = Equal.mirror ind_c

Ao chamar o app o Type Check nos retorna a mensagem All terms checked e desta forma provamos, por meio da indução e usando uma outra prova, a comutação da adição, ou seja, que a soma de n e m é igual a soma de m e n.