Estrutura de dados

Listas: trabalhando com dados estruturados

A partir de agora, veremos dados estruturados, em especial as listas e pares, e que podem conter elementos de diversos tipos. Na definição do tipo, já mostraremos eles com tipos polimórficos, mas não se assombre, veremos sobre isso no próximo capítulo, apenas vamos ignorar o tipo e acompanhar a explicação, fará mais sentido ao decorrer do nosso estudo.

Pares de Números

Em uma definição de tipo indutivo, cada construtor pode receber qualquer número de argumentos -- nenhum como o Bool, Empty ou um como o *Nat* -- e temos o Pair que recebe dois argumentos (podendo ser até mesmo outros dois pares) e retorna um tipo:

record Pair (a) (b) 

Os dois argumentos recebidos são transformados no primeiro componente, o fst, e o segundo, o snd.

record Pair (a) (b) {
  fst : a
  snd : b
} 

A forma de construir um par de Nat é a seguinte:

Pair.new Nat Nat a b  : (Pair a b)

Aqui estão duas funções simples para extrair o primeiro e o segundo componentes de um par. As definições também ilustram como fazer a correspondência de padrões em dois argumentos construtores.

Fst (pair: Pair Nat Nat) : Nat
Fst (Pair.new Nat Nat fst snd) = fst

Exemplo 1: (Fst Nat (List Nat) (Pair 2n [1n,2n,3n])) -> 2n

Snd (pair: Pair Nat Nat) : Nat
Snd (Pair.new Nat Nat fst snd) = snd

Exemplo 2: (Snd Nat (List Nat) (Pair 2n [1n,2n,3n])) -> [1n,2n,3n]

Algumas provas

Vamos tentar provar alguns fatos simples sobre pares. Se declararmos as coisas de uma maneira particular (e ligeiramente peculiar), podemos completar provas com apenas reflexividade:

Surjective_pairing (p: Pair Nat Nat) : Equal (Pair Nat Nat) p (Pair.new (Fst p) (Snd p))
Surjective_pairing (Pair.new Nat Nat fst snd) = Equal.refl

Mas *Equal.*refl não é suficiente caso a declaração seja:

Surjective_pairing (Pair.new Nat Nat fst snd) = Equal.refl

Já que o Kind espera

Equal (Pair Nat Nat) p (Pair.new (Fst p) (Snd p))

E recebeu

Equal p p

Nós devemos "expor" a estrutura interna do par para que o Type Checker possa verificar se p é realmente igual a Pair.new (Fst p) (Snd p)

Snd_fst_is_swap

Snd_fst_is_swap (p: Pair Nat Nat ) : Equal (Pair Nat Nat) (Pair.swap Nat Nat (Pair.swap Nat Nat p) p)
Snd_fst_is_swap (Pair.new Nat Nat fst snd) = ? 

Fst_swap_is_snd

Fst_swap_is_inverse (p: Pair Nat Nat) (a: Nat) (b: Nat) : Equal (Pair Nat Nat) (Pair.swap Nat Nat (Pair.new a b) (Pair.new b a))
Fst_swap_is_inverse p a b = ?