Programação com proposições

As conectivas lógicas que vimos fornecem um vocabulário rico para definir proposições complexas a partir de proposições mais simples. Para ilustrar, vamos ver como expressar a afirmação de que um elemento x ocorre em uma lista l. Observe que essa propriedade tem uma estrutura recursiva simples:

  • Se l for a lista vazia, então x não pode ocorrer nela, portanto, a propriedade "x aparece em l" é simplesmente falsa.
  • Caso contrário, l tem a forma List.cons xh xt. Nesse caso, x ocorre em l se ele é igual a xh ou se ocorre em xt.

Podemos traduzir isso diretamente em uma função recursiva simples que recebe um elemento e uma lista e retorna uma proposição:

In <a> (x: a) (l: List a)    : Type
In a x List.nil              = Empty
In a x (List.cons head tail) = Either (Equal a x head) (In a x tail)

Quando In é aplicado a uma lista concreta, ele se expande em uma sequência concreta de disjunções aninhadas.

In_example_1 : In 4n [1n, 2n, 3n, 4n, 5n]
In_example_1 = (Either.right (Either.right (Either.right (Either.left Equal.refl))))

In_example_2 (n: Nat) (i: In n [2n, 4n]) : Sigma Nat (m => Equal Nat n (Nat.mul 2n m))
In_example_2 n (Either.left e)                                  = $ 1n e
In_example_2 n (Either.right l (Either rl rr) (Either.left e))  = $ 2n e
In_example_2 n (Either.right l (Either rl rr) (Either.right e)) = Empty.absurd e

Também podemos provar lemas mais genéricos e de nível superior sobre In. Observe, no próximo exemplo, como In começa sendo aplicado a uma variável e só é expandido quando fazemos análise de casos nessa variável:

In_map <a> <b> (f: a -> b) (l: List a) (x: a) (i: In x l) : In (f x) (List.map l f) 
In_map a b f (List.nil) x i = Empty.absurd i
In_map a b f (List.cons head tail) x (Either.right e) = Either.right (In_map f tail x e)
In_map a b f (List.cons head tail) x (Either.left e)  = 
    (Equal.rewrite e 
    (y => (Either (Equal (f x) (f y)) (In (f x) (List.map tail f)))) 
    (Either.left Equal.refl))

Essa forma de definir proposições recursivamente, embora conveniente em alguns casos, também tem algumas desvantagens. Em particular, está sujeita às restrições usuais do Kind em relação à definição de funções recursivas, por exemplo, o requisito de que elas sejam "obviamente terminantes". No próximo capítulo, veremos como definir proposições indutivamente, uma técnica diferente com seu próprio conjunto de pontos fortes e limitações.

In_map_equiv

In_map_equiv <a> <b> (f: a -> b) (l: List a) (y: b) :
   Equivalence (In y (List.map l f)) (Sigma a (x => (Pair (Equal (f x) y) (In x l))))
In_map_equiv a b f l y = ?

In_app_equiv

In_app_equiv <a> (x: a) (l1: List a) (l2: List a) :
  (Equivalence (In x (List.concat l1 l2)) (Either (In x l1) (In x l2)))
In_app_equiv a x l1 l2 = ?

All

Lembre-se de que funções que retornam proposições podem ser vistas como propriedades de seus argumentos. Por exemplo, se p tem o tipo Nat -> Type, então p n afirma que a propriedade p é verdadeira para n.

Inspirado em In, escreva uma função recursiva All afirmando que alguma propriedade p é verdadeira para todos os elementos de uma lista l. Para garantir que sua definição esteja correta, prove o lema All_In abaixo. (É claro que sua definição não deve apenas repetir o lado esquerdo de All_In.)

All <t> (p: t -> Type) (l: List t)  : Type
All t p l = ?

All_in <t> (p: t -> Type) (l: List t) : Equivalence ((x: t) -> (i: In x l) -> p x) (All p l)
All_in t p l = ?

Combine_odd_even

Complete a definição da função combine_odd_even abaixo. Ela recebe como argumentos duas propriedades de números, podd e peven, e deve retornar uma propriedade p tal que p n é equivalente a podd n quando n é ímpar e equivalente a peven n caso contrário.

Combine_odd_even (podd: Nat -> Type) (peven: Nat -> Type) : Nat -> Type
Combine_odd_even podd peven = ?

Para testar sua definição, prove os seguintes teoremas:

Combine_odd_even_intro
  (n: Nat)
  (podd:  Nat -> Type)
  (peven: Nat -> Type)
  (p1: (Equal (Nat.is_odd n) Bool.true)  -> podd  n)
  (p2: (Equal (Nat.is_odd n) Bool.false) -> peven n) : (Combine_odd_even (podd) (peven)) n
Combine_odd_even_intro n podd peven p1 p2 = ?

Combine_odd_even_elim_odd
  (n: Nat)
  (podd:  Nat -> Type)
  (peven: Nat -> Type)
  (p: (Combine_odd_even podd peven) n)
  (e: Equal (Nat.is_odd n) Bool.true) : podd n
Combine_odd_even_elim_odd n podd peven p e = ?

Combine_odd_elim_even
  (n: Nat)
  (podd: Nat -> Type)
  (peven: Nat -> Type)
  (p: (Combine_odd_even podd peven) n)
  (e: Equal (Nat.is_odd n) Bool.false) : peven n
Combine_odd_elim_even n podd peven p e = ?