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.

logic coq 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

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.
- A eliminação da dupla negação é um desses axiomas:
```
Axiom dne : forall P:Prop, ~~P -> P.
```
- A lei de Peirce é outro exemplo:
```
Axiom peirce : forall P Q:Prop, ((P -> Q) -> P) -> P.
```
- Ou use uma das leis de De Morgan :
```
Axiom de_morgan_and : forall P Q:Prop, ~(~P /\ ~Q) -> P \/ Q.
```

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

Provando tautologia com coq

Respostas: