Menu
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?
726
To prove a goal that involves a conjunction, we use the split tactic, that generates two subgoals, one for each operand of the conjunction. split. We can use destruct for the conjunctive hypothesis P ∧ Q, in order to get both P and Q as hypotheses.
The name coq means "rooster" in French and stems from a French tradition of naming research development tools after animals. Up until 1991, Coquand was implementing a language called the Calculus of Constructions and it was simply called CoC at this time.
Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
Coq supports mutual and nested inductive types and coinductive types natively. Lean 3's frontend supports mutual and nested inductives via encoding, but some definitional equalities may be lost. Lean 4 supports mutual inductives natively.
Coq's kernel verifies the correctness of proof terms when it exits proof mode by checking that the proof term is well-typed and that its type is the same as the theorem statement. After a proof is completed, Print <theorem_name> shows the proof term and its type.
Show Existentials. Coq's kernel verifies the correctness of proof terms when it exits proof mode by checking that the proof term is well-typed and that its type is the same as the theorem statement. After a proof is completed, Print <theorem_name> shows the proof term and its type.
Coq enters proof mode when you begin a proof, such as with the Theorem command. It exits proof mode when you complete a proof, such as with the Qed command. Tactics, which are available only in proof mode, incrementally transform incomplete proofs to eventually generate a complete proof.
When you run Coq interactively, such as through CoqIDE, Proof General or coqtop, Coq shows the current proof state (the incomplete proof) as you enter tactics. This information isn't shown when you run Coq in batch mode with coqc.
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.
58
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With
