Some simple proofs

First declare the following variables : P, Q, R, S of sort Prop.
Then prove the following theorems, using only the tactics assumption, intros, and apply.

 Lemma id_P : P -> P.

 Lemma id_PP : (P->P)->(P->P).

 Lemma imp_trans : (P->Q)->(Q->R)->P->R.

 Lemma imp_perm : (P->Q->R)->(Q->P->R).

 Lemma ignore_Q : (P->R)->P->Q->R.

 Lemma delta_imp  : (P->P->Q)->P->Q.

 Lemma delta_impR : (P->Q)->(P->P->Q).

 Lemma diamond : (P->Q)->(P->R)->(Q->R->S)->P->S.

 Lemma weak_peirce : ((((P->Q)->P)->P)->Q)->Q.

Solution (without tacticals)
Solution (using some tacticals)

Note

All these theorems can be proved with a simple call to Auto.

Going home

Pierre Castéran