CODEWITHSUNDEEP
coqproof
Germán Faller
Germán Faller

Reputation: 574

Understanding COQ proof on Show Proof.

Im new in COQ and Im trying to proof the counterexample theorem.

Variable A B:Prop.

Hypothesis R1: ~A->B.
Hypothesis R2: ~B.

Theorem ej: A.

When we studied logics, we learn the RAA thechnic but in COQ this doesn't add a new Hypothesis, and now we are stuck.

So then we try:

Proof.
tauto.
Show Proof.

With the following output, but we don't have any idea what does it mean.

(NNPP A
   (fun H : ~ A => let H0 : B := R1 H in let H1 : False := R2 H0 in False_ind False H1))

Can anybody help us to understand the COQ Show Proof output?

Upvotes: 5

Views: 1003

Answers (1)

Arthur Azevedo De Amorim
Arthur Azevedo De Amorim

Reputation: 23612

Coq represents proofs as programs of a functional programming language, following the Curry-Howard correspondence. These programs are written by combining the primitives of Coq's logic with axioms and theorems proved by the user. The output that you see is a "program" that invokes the axiom NNPP on two arguments, the proposition A and the anonymous function fun H : ~ A => .... The axiom NNPP is the principle of dougle-negation elimination usually used in proofs by contradiction. If you type Check NNPP., Coq tells you that its type is forall P : Prop, ~ ~ P -> P, which means that, given any proposition P and any proof H of ~ ~ P, NNPP P H is a proof of P. The functional term that Coq built above, fun H : ~ A => ..., is precisely a Coq proof of ~ ~ A that uses the hypothesis you declared.

I don't know how much prior experience you have with Coq and functional programming, but it might be useful to have a look at the Software Foundations book series, which gives a comprehensive introduction to Coq. In particular, the Proof Objects chapter describes how Coq proofs are represented.

Upvotes: 6

Related Questions