Mais exercícios

Boolean_functions

Use os conhecimentos ensinados até aqui para resolver o teorema:

Identity_fn_applied_twice (f: Bool -> Bool) (e: (x: Bool) -> Equal Bool (f x) x) (b : Bool) : Equal Bool (f (f b)) b
Identity_fn_applied_twice f e b = ?

Depois, resolva o teorema negation_fn_applied_twice, que é o mesmo que o anterior, mas mudando a hipótese para Equal (f x) (Not x)

Andb_eq_orb

Prove o seguinte teorema (Lembre-se que voce pode provar teoremas intermediários separadamente)

Andb_eq_orb (b: Bool) (c: Bool) (e: Equal Bool (Andb b c) (Orb b c)) : Equal Bool b c
Andb_eq_orb b c prf = ?

Binary

Considere uma representação diferente de números naturais, usando um sistema binário ao invés de unário. Ou seja, ao invés de termos apenas zero ou um sucessor de um número, nós podemos ter:

  • zero;
  • o dobro de um número;
  • o dobro de um número mais 1.
  1. Primeiro, escreva uma definição indutiva desse tipo, chamando-o de Bin. (Lembre-se que, no fundo, a própria definição de Nat como zero ou succ n não tem sentido intrínseco. Ela só diz que um elemento de Nat pode ser um zero ou um succ n se n também for Nat. A interpretação disso como um sistema de valores 0, 1, 2, etc, vem de como nós trabalhamos com esse tipo Nat. A sua definição de Bin idealmente também será tão simples quanto. Serão as funções que você fizer sobre Bin que darão sentido matemático a ele).
  2. Então, escreva uma função Incr para incrementar um Bin, e uma função Bin_to_nat para converter de Bin para Nat.
  3. Escreva cinco provas que testam suas funções de incremento e de conversão. Note que incrementar um binário e então convertê-lo deve ser chegar no mesmo resultado que convertê-lo primeiro e então incrementar o Nat.