Section Minimal_Logic.
Variables P Q R S T: Prop.

Lemma general:
P -> Q.
Proof.
intro p.


Lemma id:
P -> P.
Proof.
intro p.
exact p.
Qed.
Print id.

Lemma proj:
P -> (Q -> P).
Proof.
intro p.
intro q.
exact p.
Qed.
Print proj.

Lemma double:
P -> ((P->Q) -> Q).
Proof.
intro p.
intro f.
apply f.
exact p.
Qed.
Print double.

Theorem imp_perm:
(P -> Q -> R) -> (Q -> P ->R).
Proof.
intro b.
intro q.
intro p.
apply b.
exact p.
exact q.
Qed.
Print imp_perm.

Lemma imp_trans: 
(P -> Q) -> (Q -> R) -> (P -> R).
Proof.
intro f.
intro g.
intro p.
apply g.
apply f.
exact p.
Qed.
Print imp_trans.


Theorem imp_triple:
(((P -> Q) -> Q) -> Q) -> (P -> Q).
Proof.
intro H.
intro p.
apply H.
intro f.
apply f.
exact p.
Qed.
Print imp_triple.

Theorem imp_diamond:
(P -> Q) -> (P ->R) -> (Q->R->T) -> (P->T).
Proof.
intro f.
intro g.
intro b.
intro p.
apply b.
apply f.
exact p.
apply g.
exact p.
Qed.
Print imp_diamond.

Theorem weak_pearce:
( ( ( (P->Q) -> P) -> P) -> Q) -> Q.
Proof.
intro H.
apply H.
Qed.
Print weak_pearce.

End Minimal_Logic.