Raciocínio sobre listas

Assim como os números, fatos simples sobre funções de processamento de lista podem às vezes ser provado inteiramente por simplificação. Por exemplo, a simplificação realizada por Equal.refl é suficiente para este teorema...

`List.nil`_app (xs: List Nat) : Equal (Concat (List.nil Nat) xs) xs
`List.nil`_app xs = Equal.refl

... isso porque o Kind "vê" o List.nil e já reduz automaticamente a igualdade da mesma forma que ocorre com os números naturais, com o Nat.zero

Além disso, como acontece com os números, às vezes é útil realizar uma análise de caso no possíveis formas (vazias ou não vazias) de uma lista desconhecida

Tl_length_pred (xs: List Nat)         : Equal Nat (Pred (Length xs)) (Length (Tail xs))
Tl_length_pred List.nil               = Equal.refl
Tl_length_pred (List.cons head tail)  = Equal.refl

Caso o usuário não abra os casos e use direto o Equal.refl, o Kind retorna um erro de tipo:

- ERROR  Type mismatch

   • Got      : Equal Nat (Nat.pred (Length xs)) (Nat.pred (Length xs)) 
   • Expected : Equal Nat (Nat.pred (Length xs)) (Length (Tail xs)) 

   • Context: 
   •   xs : (List Nat) 

   Tl_length_pred xs = Equal.refl
                       ┬─────────
                       └Here!

Da mesma forma, alguns teoremas precisam de indução para suas provas.

Micro-Sermão. Simplesmente ler scripts de prova de exemplo não o levará muito longe! É importante trabalhar os detalhes de cada um, usando Kind e pensando no que cada passo alcança. Caso contrário, é mais ou menos garantido que os exercícios não farão sentido quando você chegar a eles. ( ಠ ʖ̯ ಠ)

Indução em Listas

Provas por indução sobre tipos de dados como List são um pouco menos familiares do que a indução de números naturais padrão, mas a ideia é igualmente simples. Cada declaração de dados define um conjunto de valores de dados que podem ser construídos usando os construtores declarados: um booleano pode ser True ou False; um número pode ser Zero ou Succ aplicado a outro número; uma lista de naturais pode ser List.nil ou List.cons aplicado a um número e uma lista.

Além disso, as aplicações dos construtores declarados entre si são as únicas possíveis formas que os elementos de um conjunto definido indutivamente podem ter, e este fato diretamente dá origem a uma maneira de raciocinar sobre conjuntos indutivamente definidos: um número é Zero ou então é Succ aplicado a um número menor; uma lista é List.nil ou então é um List.cons aplicado a algum número e a alguma lista menor; etc. Então, se tivermos e mente alguma proposição p que menciona uma lista l e queremos argumentar que p vale para todas as listas, podemos raciocinar da seguinte forma:

Primeiro, mostre que p é verdadeiro para l quando l é List.nil.
Então mostre que p é verdadeiro para l quando l é List.cons n l para algum número n e alguma lista menor l, assumindo que p é verdadeiro para l.

Como listas maiores só podem ser construídas a partir de listas menores, eventualmente chegando a List.nil, esses dois argumentos juntos estabelecem a verdade de p para todas as listas l. Aqui está um exemplo concreto:

Concat_assoc (xs: List Nat) (ys: List Nat) (zs: List Nat) : Equal (Concat (Concat xs ys) zs) (Concat xs (Concat ys zs))
Concat_assoc List.nil                               ys zs = Equal.refl
Concat_assoc (List.cons Nat xs.head xs.tail)        ys zs = 
  let ind = Concat_assoc xs.tail ys zs
  let app = Equal.apply (x => (List.cons xs.head x)) ind
  app

Nós recebemos três listas xs, ys e zs e verificamos se a concatenação da de xs e ys com zs é igual a de xs com a de ys com zs Para isso nós verificamos para o caso de xs ser uma lista vazia, então recebemos uma reflexão da concatenação é entre ys e zs e basta dar um *Equal*.**refl**

Em seguida nós "abrimos" o xs para obter o xs.tail para a nossa indução, e recebemos como objetivo:

 • Expected: Equal (List Nat) (List.cons Nat xs.head (Concat (Concat xs.tail ys) zs)) (List.cons Nat xs.head (Concat xs.tail (Concat ys zs)))

e a nossa variável ind é:

 • ind: Equal (List Nat) (Concat (Concat xs.tail ys) zs) (Concat xs.tail (Concat ys zs))

bastando apenas aplicar um List.cons xs.head em ambos os lados da igualdade para ter o objetivo final e é isso o que fazemos no app:

 • app : Equal (List Nat) (List.cons Nat xs.head (Concat (Concat xs.tail ys) zs)) (List.cons Nat xs.head (Concat xs.tail (Concat ys zs)))

OBSERVAÇÃO O Type Check nos retorna tipos t2, t3 e outros gerados no mesmo estilo e podemos ignorar e até mesmo apagar na hora de comparar o retorno das variáveis como vemos no seguinte caso:

 • Expected: Equal (List Nat) (List.cons Nat xs.head (Concat (Concat xs.tail ys) zs)) (List.cons Nat xs.head (Concat xs.tail (Concat ys zs))) 
 •   app   : Equal (List Nat) (List.cons Nat xs.head (Concat (Concat xs.tail ys) zs)) (List.cons Nat xs.head (Concat xs.tail (Concat ys zs)))

Dessa forma fica mais fácil perceber que o app e o Expected são idênticos, então não é necessário se assustar ao ver esses tipos gerados

Invertendo uma lista

Para um exemplo um pouco mais complicado de prova indutiva sobre listas, suponha que usamos Concat para definir uma função de reversão de lista Rev:

Rev (xs: List Nat)        : List Nat
Rev List.nil              = List.nil Nat
Rev (List.cons head tail) = Concat (Rev tail) [head]

Test_rev1 : Equal (List Nat) (Rev [1n,2n,3n]) [3n,2n,1n]
Test_rev1 = Equal.refl

Test_rev2 : Equal (Rev List.nil) List.nil
Test_rev2 = Equal.refl

Propriedades da Rev

Agora vamos provar alguns teoremas sobre o rev que acabamos de definir. Para algo um pouco mais desafiador do que vimos, vamos provar que inverter uma lista não altera seu comprimento. Nossa primeira tentativa fica presa o caso sucessor...

Rev_length_firsttry (xs: List Nat)              : Equal Nat (Length (Rev xs)) (Length xs)
Rev_length_firsttry List.nil                    = Equal.refl
Rev_length_firsttry (List.cons xs.head xs.tail) =
   let ind = Rev_length_firsttry xs.tail
   ?

O Type Check nos retorna o seguinte objetivo e contexto:

+ INFO  Inspection.

   • Expected: Equal Nat (Length (Concat (Rev tail) (List.cons Nat head (List.nil Nat)))) (Nat.succ (Length tail)) 

   • Context: 
   •   head : Nat 
   •   tail : (List Nat) 
   •   ind  : Equal Nat (Length (Rev tail)) (Length tail)
   •   ind  = (Rev_length_firsttry tail) 

   let ind = Rev_length_firsttry tail
      ?
      ┬
      └Here!

Agora nós temos que provar que o tamanho da concatenação do reverso do tail da lista e a head dela é igual ao sucessor do tamanho da tail, então precisaremos usar algumas outras provas, uma dela é que o tamanho da concatenação de duas listas é o mesmo da soma do tamanho das de cada uma delas:

Concat_length (xs: List Nat) (ys: List Nat)  : Equal Nat (Length (Concat xs ys)) (Plus (Length xs) (Length ys))
Concat_length List.nil ys                    = Equal.refl
Concat_length (List.cons xs.head xs.tail) ys =
   let ind = Concat_length xs.tail ys
   let app = Equal.apply (x => (Nat.succ x)) ind
   app

Além dessa prova, usaremos outras já provadas nos capítulos anteriores:

Plus_n_z (n: Nat)     : Equal Nat n (Plus n Nat.zero)
Plus_n_sn (n: Nat) (m: Nat) : Equal Nat (Nat.succ (Plus n m)) (Plus n (Nat.succ m))
Plus_comm (n: Nat) (m: Nat) : Equal Nat (Plus n m) (Plus m n)

E agora é possível provar o nosso teorema:

Rev_length (xs: List Nat)               : Equal Nat (Length (Rev xs)) (Length xs)
Rev_length List.nil                     = Equal.refl
Rev_length (List.cons Nat head tail)  =
   let ind   = Rev_length tail
   ?

+ INFO  Inspection.

   • Expected: Equal Nat (Length (Concat (Rev tail) (List.cons Nat head (List.nil Nat)))) (Nat.succ (Length tail)) 

   • Context: 
   •   head : Nat 
   •   tail : (List Nat) 
   •   ind  : Equal Nat (Length (Rev tail)) (Length tail) 
   •   ind  = (Rev_length tail) 

   let ind   = Rev_length tail
      ?
      ┬
      └Here!

Nós criamos uma variável com nossa auxiliar Concat_length:

Rev_length (xs: List Nat)             : Equal Nat (Length (Rev xs)) (Length xs)
Rev_length List.nil                   = Equal.refl
Rev_length (List.cons Nat head tail)  =
   let ind  = Rev_length tail
   let aux1 = Concat_length (Rev xs.tail) [xs.head]
   ?

Recebemos um novo contexto para nos auxiliar, o

 • aux1: Equal Nat (Length (Concat (Rev tail) (List.cons Nat head (List.nil Nat)))) (Plus (Length (Rev tail)) 1n)

A aux1 é igual ao lado esquerdo do nosso Expected, então metade do trabalho já foi resolvido, basta o outro lado da igualdade e para isso nós criamos uma nova variável, a aux2:

let aux2 = Plus_comm (Length (Rev xs.tail)) (1n)

Agora nosso contexto está ainda melhor:

 • aux2: Equal Nat (Plus (Length (Rev tail)) 1n) (Nat.succ (Length (Rev tail)))

Como estamos progredindo nas provas formais, é possível perceber que o lado esquerdo da aux2 é igual ao direito da aux1 e podemos encadear um no outro com o Equal.chain:

let chn = Equal.chain aux1 aux2

Ao dar o Type Check, vemos nosso novo contexto:

 • chn : Equal Nat (Length (Concat (Rev tail) (List.cons Nat head (List.nil Nat)))) (Nat.succ (Length (Rev tail)))

Nossa variável chn é praticamente idêntica ao nosso Expected só diferindo na parte final, pois Expected espera um Nat.succ (Length xs.tail) e o chn nos dá Nat.succ (Length (Rev xs.tail)), mas nós temos a variável ind que nos retorna essa igualdade. Vamos relembrar:

 • ind: Equal Nat (Length (Rev tail)) (Length tail)

Incrível, não é? Ela nos retorna exatamente o que precisamos, que o tamanho do reverso da tail é igual ao tamanho da tail, então basta reescrever a variável ind na nossa chn:

let rrt = Equal.rewrite ind (x => Equal Nat (Length (Concat (Rev tail) (List.cons head (List.nil)))) (Nat.succ x )) chn

Vamos ver nosso novo contexto, apenas ocultando os tipos para uma leitura mais fácil:

+ INFO  Inspection.

   • Expected: Equal Nat (Length (Concat (Rev tail) (List.cons _ head (List.nil _)))) (Nat.succ (Length tail)) 

   • Context: 
   •   head : Nat 
   •   tail : (List Nat) 
   •   ind  : Equal Nat (Length (Rev tail)) (Length tail) 
   •   ind  = (Rev_length tail) 
   •   aux1 : Equal Nat (Length (Concat (Rev tail) (List.cons Nat head (List.nil Nat)))) (Plus (Length (Rev tail)) 1n) 
   •   aux1 = (Concat_length (Rev tail) (List.cons Nat head (List.nil Nat))) 
   •   aux2 : Equal Nat (Plus (Length (Rev tail)) 1n) (Nat.succ (Length (Rev tail))) 
   •   aux2 = (Plus_comm (Length (Rev tail)) 1n) 
   •   chn  : Equal Nat (Length (Concat (Rev tail) (List.cons Nat head (List.nil Nat)))) (Nat.succ (Length (Rev tail)))
   •   chn  = Equal.chain Nat (Length (Concat (Rev tail) (List.cons Nat head (List.nil Nat)))) (Plus (Length (Rev tail)) 1n) (Nat.succ (Length (Rev tail))) aux1 aux2 
   •   rrt  : Equal Nat (Length (Concat (Rev tail) (List.cons Nat head (List.nil Nat)))) (Nat.succ (Length tail)) 
   •   rrt  = Equal.rewrite Nat (Length (Rev tail)) (Length tail) ind (x => Equal Nat (Length (Concat (Rev tail) (List.cons Nat head (List.nil Nat)))) (Nat.succ x))) chn

Agora é muito mais fácil perceber que nosso rrt é exatamente o nosso Expected, então nossa prova fica assim:

Rev_length (xs: List Nat)            : Equal Nat (Length (Rev xs)) (Length xs)
Rev_length List.nil                  = Equal.refl
Rev_length (List.cons Nat head tail) =
   let ind   = Rev_length tail
   let aux1  = Concat_length (Rev tail) [head]
   let aux2  = Plus_comm (Length (Rev tail)) (1n)
   let chn   = Equal.chain aux1 aux2
   let rrt = Equal.rewrite ind (x => Equal Nat (Length (Concat (Rev tail) [head])) (Nat.succ x)) chn
   rrt

Exercícios de Listas, parte 1

List_exercises

Vamos praticar um pouco mais com as listas:

Concat_nil_r (xs: List Nat) : Equal (Concat xs List.nil) xs
Concat_nil_r xs = ?

Concat_assoc (xs: List Nat) (ys: List Nat) (zs: List Nat) : Equal (Concat (Concat xs ys) zs) (Concat xs (Concat ys zs))
Concat_assoc xs ys zs = ?

Rev_app_distr (xs: List Nat) (ys: List Nat) : Equal (Rev (Concat xs ys)) (Concat (Rev ys) (Rev xs))
Rev_app_distr xs ys = ?

Rev_involutive (xs: List Nat) : Equal (Rev (Rev xs)) xs
Rev_involutive xs = ?

Há uma solução curta para a próxima. Se você estiver achando muito difícil ou começar a ficar longo demais, recue e tente procurar uma maneira mais simples.

Concat_assoc4 (l1: List Nat) (l2: List Nat) (l3: List Nat) (l4: List Nat) : Equal (List Nat) (Concat l1 (Concat l2 (Concat l3 l4))) (Concat (Concat (Concat l1 l2) l3) l4)
Concat_assoc4 l1 l2 l3 l4 = ?

Um exercício sobre sua implementação de Nonzeros:

Nonzeros_app (xs: List Nat) (ys: List Nat) : Equal (List Nat) (Nonzeros (Concat xs ys)) (Concat (Nonzeros xs) (Nonzeros ys))
Nonzeros_app xs ys = ?

Beq_NatList

Preencha a definição de beq_NatList, que compara listas de números para igualdade. Prove que beq_NatList xs ys produz Bool.true para cada lista.

Beq_NatList (xs: List Nat) (ys: List Nat) : Bool
Beq_NatList xs ys = ? 

Test_beq_natlist1 : Equal Bool (Beq_list List.nil List.nil) Bool.true
Test_beq_natlist1 = ?

Test_beq_natlist2 : Equal Bool (Beq_list [1n,2n,3n] [1n,2n,3n]) Bool.true
Test_beq_natlist2 = ?

Test_beq_natlist3 : Equal Bool (Beq_list [1n,2n,3n] [1n,2n,4n]) Bool.false
Test_beq_natlist3 = ?

Beq_natlist_refl (xs: List Nat) : Equal Bool Bool.true (Beq_list xs xs)
Beq_natlist_refl xs = ?

Exercícios de Listas, parte 2

Proofs

Prove o seguinte teorema, ele ajudará você na prova seguinte

Ble_n_succ_n (n: Nat) : Equal Bool (Lte n (Nat.succ n)) Bool.true
Ble_n_succ_n n = ?

Aqui estão mais alguns pequenos teoremas para provar sobre suas definições sobre listas.

Count_member_nonzero (xs: List Nat) : Equal Bool (Lte 1n (Count 1n (List.cons 1n xs))) Bool.true
Count_member_nonzero xs = ?

Rev_injective

Prove que a função Rev é injetiva - isto é

Rev_injective (xs: List Nat) (ys: List Nat) (e: Equal (List Nat) (Rev xs) (Rev ys)) :tail Equal (List Nat) xs ys
Rev_injective xs ys e = ?

Opcional: Count_sum

Escreva um teorema interessante sobre Listas envolvendo as funções count e sum, e prova-o. (Você pode encontrar que a dificuldade da prova depende de como você definiu o count!)

Count_sum : ?