2
$\begingroup$

I want to mimic natural deduction proofs in coq ; for instance the proof I made for "A /\ B -> B /\ A" is for now

Theorem commute_and : A /\ B -> B /\ A.
Proof.
    intro hAB.
    elim hAB.
    split.
    auto.
    auto.
Qed.

I am trying to obtain something more close to the operators elimination and introduction axioms.

1/ First part of the attempt : create functions for introduction and elimination of the operator 'and'

I tried :

Definition elim_and_r ( C : Prop) : Prop:=
    match C with
    |  A /\ B => A
end.  

But Coq doesn't understand the pattern "A /\ B" (I also tried " A && B" and "and A B" and I also added "Require Import Coq.Init.Logic." at the beginning of the code).

2/ Second part :

I tried to use the theorem proj1 of the library Coq.Init.Logic with

Theorem commute_and_V2 : A /\ B -> B /\ A.
Proof.
    intro hAB.
    apply proj1.

but it gives to me "Unable to find an instance for the variable B." (if I try "apply proj1 hAB", an error occurs as well).

If I can fix the step one, I would like to use apply elim_and_r hAB. but is hAB even of type Prop ?

You can see that I am a bit lost at deferent levels... It is true I'm beginning in Coq, so, sorry if it is dumb questions.

$\endgroup$
7
  • 1
    $\begingroup$ I’m not sure I understand what your question is. $\endgroup$
    – Jason Rute
    Aug 27 at 13:41
  • $\begingroup$ Also your function elim_and_r isn’t going to give you what you think it is. By returning a Prop you are returning something which could be true or false, and there is no logical connection between the input Prop and output Prop. $\endgroup$
    – Jason Rute
    Aug 27 at 13:48
  • $\begingroup$ Maybe look at the term proofs generated with Show Proof.. Or (and I hate to point you to another system, but) Section 3.3 of Theorem proving in Lean focuses on term proofs for propositional logic, and you can easily see the connection to natural deduction-style elim and intro rules. (I imagine there is a similar Coq reference, but I don’t know it.) $\endgroup$
    – Jason Rute
    Aug 27 at 13:52
  • $\begingroup$ @JasonRute I already did it with Lean ; in fact I am working in translating Latex proof into proof assistants one. Since I could do with Lean, I wanted to do it with Coq, and see the differences $\endgroup$
    – Netchaiev
    Aug 27 at 13:54
  • $\begingroup$ @JasonRute Basically, I have a tree with nodes (Vector_of_propositions, intro/elim_operator) and I want to convert it automatically in Coq $\endgroup$
    – Netchaiev
    Aug 27 at 13:57

1 Answer 1

5
$\begingroup$

(Based on our chat, I've figured out what you are asking for.)

Since you know natural deduction and Lean, you already know what the natural deduction rules look like in Lean, e.g. here are the and elimination rules in Lean:

theorem and.elim_left {a b : Prop} (h : a ∧ b) : a
theorem and.elim_right {a b : Prop} (h : a ∧ b) : b

The and.intro rule is automatically generated as:

constructor and.intro : ∀ {a b : Prop}, a → b → a ∧ b

The corresponding rules in Coq are in Coq.Init.Logic:

Inductive and (A B:Prop) : Prop := conj : A -> B -> A /\ B
Section Conjunction.
  Variables A B : Prop.
  Theorem proj1 : A /\ B -> A.
  Theorem proj2 : A /\ B -> B.
End Conjunction.

Notice the right-and-elimination-rule proj2 doesn't look anything like your elim_and_r.

Here is a tactic proof of your theorem using these rules. Your mistake is that you forgot to apply the intro rule conj where you needed to.

Variables A B : Prop.
Theorem commute_and_V2 : A /\ B -> B /\ A.
Proof.
    intro hAB.
    apply conj.           (* and intro rule *)
    - apply (proj2 hAB).  (* and elim right*)
    - apply (proj1 hAB).  (* and elim left *)
Qed.

Also, by using Show Proof. we can see the term proof:

(fun hAB : A /\ B => conj (proj2 hAB) (proj1 hAB))
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.