Natural deduction with coq assistant prover

Question

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.

Answer 1

(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))