Exercícios adicionais

Nostutter

Formular definições indutivas de propriedades é uma habilidade importante que você precisará neste curso. Tente resolver este exercício sem qualquer ajuda.

Dizemos que uma lista "gagueja" se ela repete o mesmo elemento consecutivamente. A propriedade "Nostutter minha_lista" significa que minha_lista não gagueja. Formule uma definição indutiva para Nostutter. (Isso é diferente da propriedade NoDup no exercício abaixo; a sequência [1,4,1] se repete, mas não gagueja).

type Nostutter <t> (l: List t) {
  RemoveMe : Nostutter []
}

Certifique-se de que cada um desses testes seja bem-sucedido, mas sinta-se à vontade para alterar a prova sugerida (em comentários) se ela não funcionar para você. Sua definição pode ser diferente da nossa e ainda estar correta, nesse caso, os exemplos podem precisar de uma prova diferente. (Você vai perceber que as provas sugeridas usam várias táticas sobre as quais não falamos, para torná-las mais robustas em relação às diferentes formas possíveis de definir Nostutter. Provavelmente, você pode apenas descomentá-las e usá-las como estão, mas também pode provar cada exemplo com táticas mais básicas.)

Test_nostutter_1 : Nostutter [3n,1n,4n,1n,5n,6n]
Test_nostutter_1 = ?
// Prova. repita o construtor; aplique beq_nat_false_iff; auto.

Test_nostutter_2 : Nostutter []
Test_nostutter_2 = ?
// Prova. repita o construtor; aplique beq_nat_false_iff; auto.

Test_nostutter_3 : Nostutter [5n]
Test_nostutter_3 = ?
// Prova. repita o construtor; aplique beq_nat_false; auto. Qed.

Test_nostutter_4 : Not (Nostutter [3n,1n,1n,4n])
Test_nostutter_4 = ?
// Prova. intro.
// repetir correspondência de metas com
// h: nostutter _ |- _ => inversão h; limpar h; subst
// end.
// contradição H1; auto.

Filter_challenge

Vamos provar que nossa definição de filter do capítulo Poly corresponde a uma especificação abstrata. Aqui está a especificação, escrita informalmente em inglês:

Uma lista l é uma "mescla em ordem" de l1 e l2 se ela contém todos os mesmos elementos de l1 e l2, na mesma ordem de l1 e l2, mas possivelmente intercalados. Por exemplo,

[1n,4n,6n,2n,3n]

é uma mescla em ordem de

[1n,6n,2n]

e

[4n,3n].

Agora, suponha que temos um conjunto t, uma função test: t -> Bool e uma lista l do tipo List t. Suponha ainda que l é uma mescla em ordem de duas listas, l1 e l2, de modo que cada item em l1 satisfaça test e nenhum item em l2 satisfaça test. Então, filter test l = l1.

Traduza esta especificação em um teorema em Kind e prove-o. (Você precisará começar definindo o que significa uma lista ser uma mescla de outras duas. Faça isso com um tipo de dados indutivo, não uma função.)

Filter_challenge_2

Uma maneira diferente de caracterizar o comportamento do filter é a seguinte: Entre todas as subsequências de l com a propriedade de que test avalia como Verdadeiro para todos os seus elementos, o filter test l é o mais longo. Formalize essa afirmação e prove-a.

Palindromes

Um palíndromo é uma sequência que é lida da mesma forma de trás para frente.

  • Defina uma proposição indutiva Pal sobre List t que capture o que significa ser um palíndromo. (Dica: você precisará de três casos. Sua definição deve ser baseada na estrutura da lista; ter apenas um único construtor como

    C <t> (l : List t)  (rev: Equal l (Rev l)) : Pal l

    pode parecer óbvio, mas não funcionará muito bem.)

  • Prove (pal_app_rev) que

    (l : List t) : Pal (List.concat l (Rev l))

  • Prove (pal_rev) que

      (l : List t) (p: Pal l) : Equal l (Rev l)

Palindrome_converse

Novamente, a direção contrária é significativamente mais difícil, devido à falta de evidência. Usando sua definição de Pal do exercício anterior, prove que

(l : List t) ( Equal l (Rev l)) Pal l

NoDup

Lembre-se da definição da propriedade In do capítulo Lógica, que afirma que um valor x aparece pelo menos uma vez em uma lista l:

In <t> (x : t) (l : List t) : Type
In x List.nil = Empty
In x (List.concat xs.h xs.t) = Either (Equal x xs.h)  (In x xs)

Sua primeira tarefa é usar In para definir uma proposição Disjoint <t> l1 l2, que deve ser comprovável exatamente quando l1 e l2 são listas (com elementos do tipo t) que não têm elementos em comum.

Em seguida, use In para definir uma proposição indutiva NoDup <t> l, que deve ser comprovável exatamente quando l é uma lista (com elementos do tipo t) em que cada membro é diferente de todos os outros. Por exemplo, NoDup U60 [1,2,3,4] e NoDup Bool [] devem ser comprováveis, enquanto NoDup Nat [1,2,1] e NoDup Bool [True,True] não devem ser.

Por fim, declare e prove um ou mais teoremas interessantes que relacionam Disjoint, NoDup e List.

Pigeonhole principle

O princípio da gaiola de pombos afirma um fato básico sobre contagem: se distribuirmos mais do que n itens em n gaiolas de pombos, alguma gaiola de pombos deve conter pelo menos dois itens. Como frequentemente acontece, esse fato aparentemente trivial sobre números requer uma máquina não trivial para provar, mas agora temos o suficiente... Primeiro, prove um lema fácil e útil.

In_split 
  <t> 
  <x: t> 
  <l: List t> 
  (i: In x l) 
  : ([l1] -> [l2] -> ((Equal l (List.concat l1  (List.cons x  l2)))))
In_split i = ?

Agora defina uma propriedade Repeats de forma que Repeats <t> l afirme que l contém pelo menos um elemento repetido (do tipo t).

type  Repeats <t> (l: List t) {
  -- PREENCHA AQUI
  RemoveMe' : Repeats [] -- necessário para verificação de tipo, os dados não devem estar vazios
}

Essa prova é muito mais fácil se você usar a hipótese excluded_middle para mostrar que In é decidível, ou seja, Either (In x l) (Not (In x l)). No entanto, também é possível fazer a prova sem assumir que In é decidível; se você conseguir fazer isso, não precisará da hipótese excluded_middle.

Aqui está uma maneira de formalizar o princípio da gaiola de pombos. Suponha que a lista l2 represente uma lista de rótulos de gaiolas de pombos, e a lista l1 represente os rótulos atribuídos a uma lista de itens. Se houver mais itens do que rótulos, pelo menos dois itens devem ter o mesmo rótulo - ou seja, a lista l1 deve conter repetições.

Pigeonhole_principle <t> (x: t) 
	(l1: Data.List t) 
	(l2: Data.List t) 
	(i1: In x l1) 
	(i2: In x l2) 
	(lt: Lt (Data.List.length l1) (Data.List.length l2)) 
	: Repeats l1
Pigeonhole_principle t x l1 l2 i2 i2 lt = ?

Excluded_middle : (p : Type) : Either p (Not p)