Falsidade e Negação

Até agora, nos preocupamos principalmente em provar que certas coisas são verdadeiras – adição é comutativa, anexação de listas é associativa, etc. Claro, também podemos estar interessados em resultados negativos, mostrando que certas proposições não são verdadeiras. Em Kind, tais declarações negativas são expressas com a função de nível de tipo de negação Not.

Para ver como a negação funciona, relembre a discussão do princípio da explosão do capítulo anterior; ela afirma que, se assumirmos uma contradição, então qualquer outra proposição pode ser derivada. Seguindo essa intuição, poderíamos definir Not p como q -> (p -> q). Kind realmente faz uma escolha ligeiramente diferente, definindo Not como p -> Empty, onde Empty é uma proposição contraditória específica definida na biblioteca padrão como um tipo de dados sem construtores.

Empty: Type

Not <p: Type>: Type
Not p = p -> Empty

Como Empty é uma proposição contraditória, o princípio da explosão também se aplica a ela. Se obtivermos Empty no contexto de prova, podemos chamá-lo de Empty ou absurd para completar qualquer objetivo:

Ex_falso_quodlibet <p> : Empty -> p
Ex_falso_quodlibet p   = e => Empty.absurd e

O latim ex falso quodlibet significa, literalmente, “da falsidade segue o que você quiser”; este é outro nome comum para o princípio da explosão.

Not_implies_our_not

Mostre que a definição da negação em Kind implica a intuitiva mencionada acima:

Not_implies_our_not <p> <q> (e: Not p) : q -> (p -> q)
Not_implies_our_not p q e = ?

É assim que usamos Not para afirmar que 0 e 1 são elementos diferentes de Nat:

Zero_not_one : Not (Equal Nat.zero (Nat.succ Nat.zero))
Zero_not_one = 
  (emp => 
    let app = Equal.apply (x => Nat.is_zero x) emp
    Equal.rewrite app (e => if e {Nat} else {Empty}) Nat.zero)

É preciso um pouco de prática para se acostumar a trabalhar com a negação em Kind. Mesmo que você possa ver perfeitamente por que uma afirmação envolvendo negação é verdadeira, pode ser um pouco complicado no começo colocar as coisas na configuração certa para que Kind possa entender! Aqui estão as provas de alguns fatos familiares para você se aquecer:

Not_false : Not Empty
Not_false = e => Empty.absurd e

Contradiction_implies_anythig <p> <q> (a: Pair p (Not p)) : q
Contradiction_implies_anythig p q (Pair.new fst snd) =
  let app = snd fst
  Empty.absurd app

Double_neg_inf

Escreva uma prova informal de Double_neg: Teorema: Se p, então (não (não p)), para qualquer proposição p.

Contrapositive

Contrapositive <p> <q> (f: p -> q) : (Not q -> Not p)
Contrapositive p q f = ?

Not_both_true_and_false

Not_both_true_and_false <p> : Not (Pair p (Not p))
Not_both_true_and_false p = ?

Da mesma forma, já que a desigualdade envolve uma negação, é preciso um pouco de prática para trabalhar com ela de forma fluente. Aqui está um truque útil. Se você estiver tentando provar uma meta que é absurda (por exemplo, o estado final é Bool.false == Bool.true), aplique Empty.absurd para mudar a meta para Empty. Isso facilita o uso de pressupostos do tipo (Not p) que podem estar disponíveis no contexto - em particular, pressupostos do tipo Not (x == y).

Not_true_is_false (b: Bool) (e: Not (Equal Bool b Bool.true)) : Equal Bool b Bool.false
Not_true_is_false Bool.false e = Equal.refl
Not_true_is_false Bool.true e = Empty.absurd (e Equal.refl)