Some Propositional Logic in Coq

I’ve been told the best way to learn is to do so let’s do some propositional logic with Coq. I got these exercises from the first two sessions of “The Incredible Proof Machine“.

I’m not sure how to translate contexts in sequent calculus other than making everything above the bar an input and everything below the bar an output so some of the exercises did not have analogs (like flipping the order of the premises). I either skipped those or made a best effort translation.

First let’s start a section and define some propositions

Section Logic.
Variables A B C D : Prop.

Now we can start proving.

A -> A

Lemma id : A -> A.
Proof.
intro. trivial.
Qed.

A -> B -> A

Lemma proj_fst : A -> B -> A.
Proof.
intro. trivial.
Qed.

A -> B -> B

Lemma proj_snd : A -> B -> B.
Proof.
intros ha hb. exact hb.
Qed.

A -> B -> A /\ B

Lemma and_intro : A -> B -> A /\ B.
Proof.
intros ha hb. exact (conj ha hb).
Qed.

A -> A /\ A

Lemma and_id : A -> A /\ A.
Proof.
intro ha. exact (conj ha ha).
Qed.

A /\ B -> A

Lemma and_elim_fst : A /\ B -> A.
Proof.
intro hab. elim hab. clear hab. intro ha. trivial.
Qed.

A /\ B -> B

Lemma and_elim_snd : A /\ B -> B.
Proof.
intro hab. elim hab. clear hab. intros _ hb. exact hb.
Qed.

A /\ B -> A -> B

Lemma and_curry : A /\ B -> A -> B.
Proof.
intro hab. elim hab. clear hab. trivial.
Qed.

A /\ B -> B /\ A

Lemma and_comm : A /\ B -> B /\ A.
Proof.
intro hab. elim hab. clear hab. intros ha hb. exact (conj hb ha).
Qed.

(A /\ B) /\ C -> A /\ (B /\ C)

Lemma and_assoc : (A /\ B) /\ C -> A /\ (B /\ C).
Proof.
intro habc. elim habc. clear habc. intro hab. elim hab. clear hab.
intros ha hb hc. exact (conj ha (conj hb hc)).
Qed.

A -> (A -> B) -> B

Lemma modus_ponens : A -> (A -> B) -> B.
Proof.
intros ha hab. exact (hab ha).
Qed.

Modus ponens is a good place to stop. I’m working my way up to quantifiers so I’ll post a few of those when I get around to them.

End Logic.