Provando tautologia com coq

12

Atualmente, tenho que aprender Coq e não sei como lidar com or:

Como exemplo, por mais simples que seja, não vejo como provar:

Theorem T0: x \/ ~x.

Eu realmente aprecio isso, se alguém puder me ajudar.

Para referência, eu uso esta folha de dicas .

Também um exemplo de uma prova que tenho em mente: Aqui para dupla negação:

Require Import Classical_Prop.

Parameters x: Prop.

Theorem T7: (~~x) -> x. 
intro H. 
apply NNPP. 
exact H. 
Qed.
Imago
fonte
NNPPO tipo é forall p:Prop, ~ ~ p -> p., então é trapaceiro usá-lo para provar T7. Quando você importa, Classical_Propvocê recebeAxiom classic : forall P:Prop, P \/ ~ P.
Anton Trunov
Então, apply classic.resolve seu objetivo T0.
Anton Trunov

Respostas:

14

Você não pode provar isso em Coq "baunilha", porque é baseado na lógica intuicionista :

De uma perspectiva teórica da prova, a lógica intuicionista é uma restrição da lógica clássica, na qual a lei da eliminação excluída da média e da dupla negação não são regras lógicas válidas.

Existem várias maneiras de lidar com uma situação como essa.

  • Introduzir a lei do meio excluído como um axioma:

    Axiom excluded_middle : forall P:Prop, P \/ ~ P.
    

    Não há mais necessidade de provar nada após esse ponto.

  • Introduzir algum axioma equivalente à lei do meio excluído e provar sua equivalência. Aqui estão apenas alguns exemplos.

Anton Trunov
fonte
Muito obrigado até agora. Não estou familiarizado com tudo o que você escreveu, mas irá verificar. Eu uso o coqIde e, de fato, também tenho uma prova de dupla negação. Adicionei-o à descrição do problema para obter mais clareza posteriormente. Eu esperava que houvesse uma maneira análoga para o problema mencionado acima. Talvez eu devesse ter incluído um exemplo.
Imago
1
@AntonTrunov, você precisa adicionar alguns parênteses ao seu Axiom peirce: do jeito que está, não é a lei de Peirce (e de fato é trivialpara provar).
Gallais
@ galais Obrigado por descobrir isso! Fixo.
Anton Trunov
6

Como outros informaram, sua tautologia não é uma tautologia, a menos que você assuma a lógica clássica. Mas como você está praticando tautologias sobre valores de verdade decidíveis, você pode usar em boolvez de Prop. Então sua tautologia vale:

Require Import Bool.

Lemma how_about_bool: forall (p : bool), Is_true (p || negb p).
Proof.
  now intros [|].
Qed.
Andrej Bauer
fonte