Kind vs Teoria dos Conjuntos

O núcleo lógico do Coq, o Cálculo das Construções Indutivas, difere de algumas maneiras importantes de outros sistemas formais que são usados pelos matemáticos para escrever provas precisas e rigorosas. Por exemplo, na fundação mais popular para a matemática em papel e lápis convencional, a Teoria dos Conjuntos de Zermelo-Fraenkel (ZFC), um objeto matemático pode potencialmente ser membro de muitos conjuntos diferentes; um termo na lógica de Kind, por outro lado, é membro de no máximo um tipo. Essa diferença muitas vezes leva a formas ligeiramente diferentes de capturar conceitos matemáticos informais, mas estes são, em grande parte, bastante naturais e fáceis de trabalhar. Por exemplo, em vez de dizer que um número natural n pertence ao conjunto de números pares, diríamos em Kind que ev n é verdadeiro, onde ev: Nat -> Tipo é uma propriedade que descreve os números pares.

No entanto, há alguns casos em que traduzir o raciocínio matemático padrão para Kind pode ser tanto trabalhoso quanto, às vezes, até impossível, a menos que enriqueçamos a lógica central com axiomas adicionais. Concluímos este capítulo com uma breve discussão de algumas das diferenças mais significativas entre os dois mundos.

Extensão Funcional.

As afirmações de igualdade que vimos até agora dizem principalmente respeito a elementos de tipos indutivos (Nat, Bool, etc.). Mas como o operador de igualdade de Kind é polimórfico, essas não são as únicas possibilidades - em particular, podemos escrever proposições que afirmam que duas funções são iguais uma à outra:

#![allow(unused)]
fn main() {
Function_equality_ex1 : Equal (Nat.succ 3n) (Nat.succ (Nat.pred 4n))
Function_equality_ex1 = Equal.refl
}

Na prática matemática comum, duas funções f e g são consideradas iguais se produzem as mesmas saídas:

(∀𝑥, 𝑓(𝑥) = 𝑔(𝑥)) → 𝑓 = 𝑔

Isto é conhecido como o princípio da extensão funcional.

De forma informal, uma "propriedade extensional" é aquela que diz respeito ao comportamento observável de um objeto. Assim, a extensão funcional significa simplesmente que a identidade de uma função é completamente determinada pelo que podemos observar a partir dela - isto é, em termos de Kind, os resultados que obtemos após aplicá-la.

A extensão funcional não faz parte dos axiomas básicos do Kind. Isso significa que algumas proposições "razoáveis" não são prováveis.

#![allow(unused)]
fn main() {
Function_equality_ex2 : Equal ((x: Nat) => Nat.add x 1n) ((x: Nat) => Nat.add 1n x)
Function_equality_ex2 = ?
}

No entanto, podemos declarar um teorema e pular a sua prova ou usar um buraco

#![allow(unused)]
fn main() {
Functional_extensionality <a><b> (f: a -> b) (g: a -> b) (e: (x: a) -> Equal (f x) (g x)) : Equal f g
}

Agora podemos invocar a extensionalidade funcional em provas:

#![allow(unused)]
fn main() {
Function_equality_ex2 : Equal ((x: Nat) => Nat.add x 1n) ((x: Nat) => Nat.add 1n x)
Function_equality_ex2 =
  Functional_extensionality ((x: Nat) => Nat.add x 1n) ((x: Nat) => Nat.add 1n x) (x => Plus_comm x 1n)
}

Naturalmente, devemos ter cuidado ao adicionar novos axiomas à lógica do Kind, pois eles podem torná-la inconsistente - ou seja, podem tornar possível provar todas as proposições, incluindo Void!

Infelizmente, não há uma maneira simples de saber se um axioma é seguro para adicionar: geralmente é necessário um trabalho árduo para estabelecer a consistência de qualquer combinação particular de axiomas.

No entanto, sabe-se que adicionar a extensionalidade funcional, em particular, é consistente.

Tr_rev

Um problema com a definição da função de reversão de lista "rev" que temos é que ela realiza uma chamada a "++" a cada passo. Executar "++" leva tempo assintoticamente linear no tamanho da lista, o que significa que "rev" tem tempo de execução quadrático. Podemos melhorar isso com a seguinte definição:

#![allow(unused)]
fn main() {
Rev_append <x> (l1: List x) (l2: List x)  : List x
Rev_append x List.nil l2                  = l2
Rev_append x (List.cons xs.h xs.t) l2     = Rev_append xs.t (List.cons xs.h l2)

Tr_rev <x> (l: List x) : List x
Tr_rev x l = Rev_append x l List.nil1
}

Esta versão é dita ser tail-recursive, porque a chamada recursiva à função é a última operação que precisa ser executada (ou seja, não precisamos executar ++ após a chamada recursiva); um compilador decente irá gerar um código muito eficiente neste caso. Prove que as duas definições são realmente equivalentes.

#![allow(unused)]
fn main() {
Tr_rev_correct <a> (xs: List a) : Equal (Tr_rev xs) (Rev xs)
Tr_rev_correct a xs = ?
}

Proposições e Booleans.

Vimos duas maneiras diferentes de codificar fatos lógicos em Kind: com booleanos (do tipo Bool) e com proposições (do tipo Type). Por exemplo, para afirmar que um número n é par, podemos dizer que • (1) evenb n retorna True, ou • (2) existe um k tal que n = double k. De fato, essas duas noções de paridade são equivalentes, como pode ser facilmente mostrado com um par de lemas auxiliares. Muitas vezes dizemos que o booleano evenb n reflete a proposição (n => Equal n (double k)).

#![allow(unused)]
fn main() {
Evenb_double (k: Nat)     : Equal (Nat.is_even (Nat.double k)) Bool.true
Evenb_double Nat.zero     = Equal.refl
Evenb_double (Nat.succ k) = Evenb_double k
}

Evenb_double_conv

#![allow(unused)]
fn main() {
Evenb_double_conv (n: Nat):
  Sigma Nat (k => (Equal n (Bool.if (Evenb n) (Nat.double k) (Nat.succ (Nat.double k)))))
Evenb_double_conv n = ?
}

TODO: terminar even_bool_prop

#![allow(unused)]
fn main() {
Even_bool_prop (n: Nat): 
  Equivalence (Equal (Evenb n) Bool.true) (Sigma Nat (k => Equal n (Nat.double k)))
}

Da mesma forma, para afirmar que dois números n e m são iguais, podemos dizer (1) que n == m retorna Bool.true ou (2) que n = m. Essas duas noções são equivalentes.

#![allow(unused)]
fn main() {
Beq_nat_true_equiv (n1: Nat) (n2: Nat) : Equivalence (Equal (Nat.equal n1 n2) Bool.true) (Equal n1 n2)
Beq_nat_true_equiv n1 n2 = Equivalence.new (x => To_beq_nat_true n1 n2 x) (y => Fro_beq_nat_true n1 n2 y)

To_beq_nat_true (n1: Nat) (n2: Nat) (e: Equal (Nat.equal n1 n2) Bool.true) : Equal n1 n2  
To_beq_nat_true Nat.zero Nat.zero Equal.refl = Equal.refl
To_beq_nat_true Nat.zero (Nat.succ n2) e = 
  let emp = (Equal.rewrite e 
    (x => match Bool x {
      true  => Empty
      false => Unit
    })
    (Unit.new))
  Empty.absurd emp
To_beq_nat_true (Nat.succ n1) Nat.zero e = 
  let emp = (Equal.rewrite e 
    (x => match Bool x {
      true  => Empty
      false => Unit
    })
    (Unit.new))
  Empty.absurd emp
To_beq_nat_true (Nat.succ n1) (Nat.succ n2) e = Equal.apply (x => Nat.succ x) (Extract_equal n1 n2 e)

Fro_beq_nat_true (n1: Nat) (n2: Nat) (e: Equal  n1 n2) : Equal (Nat.equal n1 n2) Bool.true
Fro_beq_nat_true Nat.zero Nat.zero Equal.refl = Equal.refl
Fro_beq_nat_true Nat.zero (Nat.succ n2) e = 
  let emp = (Equal.rewrite e 
    (x => match Nat x {
      zero => Unit
      succ => Empty
    })
    (Unit.new))
  Empty.absurd emp
Fro_beq_nat_true (Nat.succ n1) Nat.zero e = 
  let emp = (Equal.rewrite e 
    (x => match Nat x {
      zero => Empty
      succ => Unit
    })
    (Unit.new))
  Empty.absurd emp
Fro_beq_nat_true (Nat.succ n1) (Nat.succ n2) e =
  let e2  = Succ_n1_n2 n1 n2 e
  let ind = Fro_beq_nat_true n1 n2 e2
  ind

  Succ_n1_n2 (n1: Nat) (n2: Nat) (e : (Equal Nat (Nat.succ n1) (Nat.succ n2))) : Equal Nat n1 n2
Succ_n1_n2 Nat.zero Nat.zero e            = Equal.refl
Succ_n1_n2 (Nat.succ n1) Nat.zero e       = Equal.apply (x => Nat.pred x) e
Succ_n1_n2 Nat.zero (Nat.succ n2) e       = Equal.apply (x => Nat.pred x) e
Succ_n1_n2 (Nat.succ n1) (Nat.succ n2) e  = Equal.apply (x => Nat.pred x) e

Extract_equal (n1: Nat) (n2: Nat) (e: Equal (Nat.equal n1 n2) Bool.true) : Equal n1 n2
Extract_equal Nat.zero Nat.zero (Equal.refl) = Equal.refl
Extract_equal Nat.zero (Nat.succ n2) (e) = 
  let emp = (Equal.rewrite e 
    (x => match Bool x {
      true  => Empty
      false => Unit
    })
    (Unit.new))
  Empty.absurd emp
Extract_equal (Nat.succ n1) Nat.zero (e) = 
  let emp = (Equal.rewrite e 
    (x => match Bool x {
      true  => Empty
      false => Unit
    })
    (Unit.new))
  Empty.absurd emp
Extract_equal (Nat.succ n1) (Nat.succ n2) e = Equal.apply (x => Nat.succ x) (Extract_equal n1 n2 e)
}

No entanto, enquanto as formulações booleanas e proposicionais de uma afirmação são equivalentes do ponto de vista puramente lógico, elas não precisam ser equivalentes operacionalmente. A igualdade fornece um exemplo extremo: saber que n == m = Verdadeiro geralmente é de pouca ajuda direta no meio de uma prova envolvendo n e m; no entanto, se convertermos a declaração para a forma equivalente n = m, podemos reescrevê-la.

O caso dos números pares também é interessante. Lembre-se de que, ao provar a direção inversa de even_bool_prop (ou seja, evenb_double, indo da afirmação proposicional para a booleana), usamos uma indução simples em k. Por outro lado, a conversa (o exercício evenb_double_conv) exigiu uma generalização inteligente, uma vez que não podemos provar diretamente (k => Equal n (Nat.double k)) = Bool.true

Para esses exemplos, as afirmações proposicionais são mais úteis do que suas contrapartes booleanas, mas nem sempre é o caso. Por exemplo, não podemos testar se uma proposição geral é verdadeira ou não em uma definição de função; como consequência, o seguinte trecho de código é rejeitado:

#![allow(unused)]
fn main() {
Is_even_prime : Nat -> Bool
Is_even_prime = (n: Nat) => Bool.if (Equal n 2n) Bool.true Bool.false
}

O Kind reclama que n = 2 tem o tipo Type, enquanto espera um elemento de Bool (ou algum outro tipo indutivo com dois elementos). A razão para esta mensagem de erro tem a ver com a natureza computacional da linguagem central de Kind, que é projetada de forma que cada função que ela possa expressar seja computável e total. Uma razão para isso é permitir a extração de programas executáveis a partir dos desenvolvimentos de Kind. Como consequência, em Kind, Type não tem uma operação de análise de caso universal que diga se uma dada proposição é verdadeira ou falsa, já que tal operação permitiria escrever funções não computáveis.

Embora propriedades gerais não computáveis não possam ser formuladas como computações booleanas, vale ressaltar que muitas propriedades computáveis ​​são mais fáceis de expressar usando Type do que Bool, já que definições de funções recursivas estão sujeitas a restrições significativas em Kind. Por exemplo, o próximo capítulo mostra como definir a propriedade de que uma expressão regular corresponde a uma determinada string usando Type. Fazer o mesmo com Bool seria equivalente a escrever um verificador de expressão regular, o que seria mais complicado, mais difícil de entender e mais difícil de raciocinar.

Por outro lado, um importante benefício adicional de afirmar fatos usando booleanos é habilitar alguma automação de prova por meio de computação com termos em Kind, uma técnica conhecida como prova por reflexão. Considere a seguinte afirmação:

#![allow(unused)]
fn main() {
Even_1000 : Sigma Nat (k => Equal 1000n (Nat.double k))
}

A prova mais direta desse fato é fornecer o valor de k explicitamente.

#![allow(unused)]
fn main() {
Even_1000 = $ 500n Equal.refl
}

Por outro lado, a prova da correspondente afirmação booleana é ainda mais simples:

#![allow(unused)]
fn main() {
Even_1000a : Equal (Evenb 1000n) Bool.true
Even_1000a = Equal.refl
}

O interessante é que, como as duas noções são equivalentes, podemos usar a formulação booleana para provar a outra sem mencionar explicitamente o valor 500:

#![allow(unused)]
fn main() {
Even_1000b : Sigma Nat (k => Equal 1000n (Nat.double k))
Even_1000b = ? //TODO: Terminar aqui
}

Embora não tenhamos ganhado muito em termos de tamanho de prova neste caso, provas maiores podem ser consideravelmente simplificadas pelo uso da reflexão. Como um exemplo extremo, a prova do teorema dos 4 cores em Coq usa reflexão para reduzir a análise de centenas de casos diferentes a uma computação booleana. Não abordaremos a reflexão em grande detalhe, mas ela serve como um bom exemplo que mostra as forças complementares dos booleanos e proposições gerais.

Logical_connectives

Os seguintes lemas relacionam os conectivos proposicionais estudados neste capítulo com as operações booleanas correspondentes.

#![allow(unused)]
fn main() {
Andb_true_equiv 
  (b1: Bool) 
  (b2: Bool) : Equivalence (Equal (Bool.and b1 b2) Bool.true) (Pair (Equal b1 Bool.true) (Equal b2 Bool.true))
Andb_true_equiv b1 b2 = ?


Orb_true_equiv 
  (b1: Bool) 
  (b2: Bool): Equivalence (Equal (Bool.or b1 b2) Bool.true) (Either (Equal b1 Bool.true) (Equal b2 Bool.true))
Orb_true_equiv b1 b2 = ?
}

Beq_nat_false_equiv

O teorema a seguir é uma formulação alternativa "negativa" de beq_nat_true_equiv que é mais conveniente em certas situações (veremos exemplos em capítulos posteriores).

#![allow(unused)]
fn main() {
Beq_nat_false_equiv (n1: Nat) (n2: Nat) : Equivalence (Equal (Nat.equal n1 n2) Bool.false) (Not (Equal n1 n2))
Beq_nat_false_equiv n1 n2 = ?
}

Beq_list

Dado um operador booleano beq para testar a igualdade de elementos de algum tipo a, podemos definir uma função beq_list beq para testar a igualdade de listas com elementos em a. Complete a definição da função beq_list abaixo. Para garantir que sua definição está correta, prove o lema beq_list_true_equiv.

#![allow(unused)]
fn main() {
Beq_list <a> (beq: a -> a -> Bool) (xs: List a) (ys: List a) : Bool
Beq_list a beq  xs ys = ?

Beq_list_true_equiv <a> 
  (beq: a -> a -> Bool) 
  (a1: a) 
  (a2: a) 
  (e: Equivalence (Equal (beq a1 a2) Bool.true) (Equal a1 a2))
  (xs: List a)
  (ys: List a): Equivalence (Equal (Beq_list beq xs ys) Bool.true) (Equal xs ys)
Beq_list_true_equiv a beq a1 a2 e xs ys = ?
}

All_forallb

#![allow(unused)]
fn main() {
Forallb <x> (t: x -> Bool) (xs: List x) : Bool
Forallb x t List.nil = Bool.true
Forallb x t (List.cons xs.h xs.t) = Bool.and (t xs.h) (Forallb t xs.t)

}

Prove o teorema abaixo, que relaciona forallb à propriedade All do exercício acima.

#![allow(unused)]
fn main() {
Forallb_true_equiv <x> 
  (t: x -> Bool) 
  (xs: List x) : 
  Equivalence (Equal (Forallb t xs) Bool.true) ((All ((k: x) => Equal (t k) Bool.true) xs))
Forallb_true_equiv x t xs = ?
}

Existem alguma propriedades importantes da função forallb que não são capturadas por esta especificação?

Lógica Clássica vs. Lógica Construtiva.

Vimos que não é possível testar se uma proposição p é verdadeira ou não ao definir uma função Kind. Você pode se surpreender ao descobrir que uma restrição semelhante se aplica às provas! Em outras palavras, o seguinte princípio de raciocínio intuitivo não é derivável em Kind:

#![allow(unused)]
fn main() {
Excluded_middle <p>: Either p (Not p)
}

Para entender operacionalmente por que esse é o caso, lembre-se de que, para provar uma declaração da forma Either p q, usamos as correspondências de padrão Left e Right, que exigem saber qual lado da disjunção é verdadeiro. Mas a proposição p universalmente quantificada em Excluded_middle é uma proposição arbitrária, sobre a qual não sabemos nada. Não temos informações suficientes para escolher qual de Left ou Right aplicar, assim como Kind não tem informações suficientes para decidir mecanicamente se p é verdadeira ou não dentro de uma função.

No entanto, se soubermos que p é refletida em algum termo booleano b, saber se ela é verdadeira ou não é trivial: basta verificar o valor de b.

#![allow(unused)]
fn main() {
Restricted_excluded_middle <p> <q> (b: Bool)(e: Equivalence p (Equal b Bool.true)) : Either p (Not p) 
Restricted_excluded_middle p q Bool.true  (Equivalence.new pb bp) = Either.left (bp Equal.refl)
Restricted_excluded_middle p q Bool.false (Equivalence.new pb bp) = Either.right (Empty.absurd (Not_implies_our_not pb))
}

Em particular, o terceiro excluído é válido para equações n = m, entre números naturais n e m.

#![allow(unused)]
fn main() {
//TODO: Terminar aqui
Restricted_excluded_middle_eq (n: Nat) (m: Nat) : Either (Equal n m) (Not (Equal n m))
Restricted_excluded_middle_eq n m = ?

To_reme (n: Nat) (m: Nat) (e: Equal n m) : Equal (Nat.equal n m) Bool.true
To_reme Nat.zero Nat.zero e         = Equal.refl
To_reme Nat.zero (Nat.succ m) e     = Empty.absurd (Not_implies_our_not e)
To_reme (Nat.succ n) Nat.zero e     = Empty.absurd (Not_implies_our_not e)
To_reme (Nat.succ n) (Nat.succ m) e = To_reme n m (Succ_injective n m e)

From_reme (n: Nat) (m: Nat) (e: Equal (Nat.equal n m) Bool.true) : Equal n m
From_reme Nat.zero Nat.zero e         = Equal.refl
From_reme Nat.zero (Nat.succ m) e     = Empty.absurd (Not_implies_our_not e)
From_reme (Nat.succ n) Nat.zero e     = Empty.absurd (Not_implies_our_not e)
From_reme (Nat.succ n) (Nat.succ m) e = Equal.apply (x => Nat.succ x) (From_reme n m e)
}

Pode parecer estranho que o princípio do terceiro excluído não esteja disponível por padrão no Kind; afinal, qualquer afirmação deve ser verdadeira ou falsa. No entanto, há uma vantagem em não assumir o princípio do terceiro excluído: as declarações no Kind podem fazer afirmações mais fortes do que as declarações análogas na matemática padrão.

Pode parecer estranho que o princípio do terceiro excluído não esteja disponível por padrão no Kind; afinal, qualquer afirmação deve ser verdadeira ou falsa. No entanto, há uma vantagem em não assumir o princípio do terceiro excluído: as declarações no Kind podem fazer afirmações mais fortes do que as declarações análogas na matemática padrão. Notavelmente, se houver uma prova no Kind de (Sigma a (x => (p x))), é possível exibir explicitamente um valor de x para o qual podemos provar p x - em outras palavras, toda prova de existência é necessariamente construtiva. Lógicas como a do Kind, que não assumem o princípio do terceiro excluído, são referidas como lógicas construtivas. Sistemas lógicos mais convencionais, como o ZFC, nos quais o princípio do terceiro excluído é válido para proposições arbitrárias, são referidos como clássicos.

O exemplo a seguir ilustra por que assumir o princípio do terceiro excluído pode levar a provas não construtivas:

Afirmação: Existem números irracionais a e b, tais que a^b é racional.

Prova: Não é difícil mostrar que a raiz quadrada de 2 é irracional. Se a raiz quadrada de 2 ^ raiz quadrada de 2 é racional, basta tomar a = b = raiz quadrada de 2 e estamos prontos. Caso contrário, se a raiz quadrada de 2 ^ raiz quadrada de 2 for irracional, podemos tomar a = raiz quadrada de 2 ^ raiz quadrada de 2 e b = raiz quadrada de 2, já que a ^ b = raiz quadrada de 2 ^ (raiz quadrada de 2 * raiz quadrada de 2) = raiz quadrada de 2 ^ 2 = 2.

Você percebeu o que aconteceu aqui? Usamos o princípio do terceiro excluído para considerar separadamente os casos em que a raiz quadrada de 2 ^ raiz quadrada de 2 é racional e onde não é, sem saber qual deles é verdadeiro! Por causa disso, sabemos que tais a e b existem, mas não podemos determinar quais são seus valores reais (pelo menos, usando essa linha de argumento).

Por útil que seja a lógica construtiva, ela tem suas limitações: há muitas declarações que podem ser facilmente provadas na lógica clássica, mas que têm provas construtivas muito mais complicadas, e há algumas que não se sabe ter prova construtiva alguma! Felizmente, assim como a extensão funcionalidade, o princípio do terceiro excluído é conhecido por ser compatível com a lógica do Kind, permitindo-nos adicioná-lo com segurança como um axioma. No entanto, não precisaremos fazer isso neste livro: os resultados que cobrimos podem ser desenvolvidos inteiramente dentro da lógica construtiva a um custo extra negligenciável.

Leva um pouco de prática para entender quais técnicas de prova devem ser evitadas no raciocínio construtivo, mas os argumentos por contradição, em particular, são infames por levar a provas não construtivas. Aqui está um exemplo típico: suponha que queremos mostrar que existe um x com alguma propriedade p, isto é, tal que p x. Começamos assumindo que nossa conclusão é falsa; isto é Not (Sigma a (x => (p x))). A partir desta premissa, não é difícil deduzir (x: a) -> Not (p x). Se conseguirmos mostrar que esse fato intermediário resulta em uma contradição, chegamos a uma prova de existência sem nunca exibir um valor de x para o qual p x seja verdadeiro!

A falha técnica aqui, do ponto de vista construtivo, é que afirmamos provar Sigma a (x => (p x)) usando uma prova de Not (Not (Sigma a (x =>(p x)))). Permitir-nos remover duplas negações de afirmações arbitrárias é equivalente a assumir o terceiro excluído, como mostrado em um dos exercícios abaixo. Assim, essa linha de raciocínio não pode ser codificada em Kind sem assumir axiomas adicionais.

Excluded_middle_irrefutable

A consistência do Kind com o axioma geral do terceiro excluído requer raciocínios complicados que não podem ser realizados dentro do próprio Kind. No entanto, o seguinte teorema implica que é sempre seguro assumir um axioma de decidibilidade (ou seja, uma instância do terceiro excluído) para qualquer tipo específico p. Por quê? Porque não podemos provar a negação de tal axioma; se pudéssemos, teríamos tanto Not (Either p (Not p)) quanto Not (Not (Either p (Not p))), o que é uma contradição.

#![allow(unused)]
fn main() {
Excluded_middle_irrefutable <p> : Not (Not (Either p (Not p)))
Excluded_middle_irrefutable p = ?
}

Not_exists_dist

É um teorema da lógica clássica que as seguintes duas afirmações são equivalentes:

#![allow(unused)]
fn main() {
Not (Sigma a (k => Not (p k))))
(x : a) -> p x
}

O teorema dist_not_exists acima prova um lado dessa equivalência. Curiosamente, a outra direção não pode ser provada na lógica construtiva. Sua tarefa é mostrar que ela é implicada pelo terceiro excluído.

#![allow(unused)]
fn main() {
Not_exists_dist <a> (p: a -> Type) (s: Not (Sigma a (k => Not (p k)))) : (x: a) -> p x
Not_exists_dist a p s = ?
}

sendo que

#![allow(unused)]
fn main() {
Excluded_middle <p>: Either p (Not p)
// Excluded_middle p = Confia 
}

Classical_axioms

Para aqueles que gostam de um desafio, aqui está um exercício retirado do livro Coq'Art de Bertot e Casteran (p. 123). Cada uma das seguintes quatro afirmações, juntamente com excluded_middle, pode ser considerada como caracterizando a lógica clássica. Não podemos provar nenhum deles em Kind, mas podemos adicionar consistentemente qualquer um deles como um axioma se quisermos trabalhar na lógica clássica.

Prove que todas as cinco proposições (essas quatro mais excluded_middle) são equivalentes.

#![allow(unused)]
fn main() {
Peirce <p> <q>(pq: (p -> q) -> p) : p

Double_negation_elimination <p> (np: Not (Not p)) : p

De_morgan_not_not <p> <q> (np: Pair (Not p) (Not q)) : Either p q

Implies_to_or <p> <q> (pq: p -> q) : Either (Not p) q
}