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.