Polymorphic minimal propositional logic in Coq from Coq Art

ex5_1.v

(* exercise 5.1 from Coq Art *)

Lemma id_P :
  forall P : Prop, P -> P.
Proof.
  intros P H.
  assumption.
Qed.

Lemma id_PP :
  forall P : Prop, (P -> P) -> P -> P.
Proof.
  intros P H H0.
  apply H0.
Qed.

Lemma imp_trans :
  forall P Q R : Prop, (P -> Q) -> (Q -> R) -> P -> R.
Proof.
  intros P Q R H H0 p.
  apply H0; apply H; assumption.
Qed.

Lemma imp_perm :
  forall P Q R : Prop, (P -> Q -> R) -> Q -> P -> R.
Proof.
  intros P Q R H q p.
  apply H; assumption.
Qed.

Lemma ignore_Q :
  forall P Q R : Prop, (P -> R) -> P -> Q -> R.
Proof.
  intros P _ R H p _.
  apply H; assumption.
Qed.

Lemma delta_imp :
  forall P Q : Prop,(P -> P -> Q) -> P -> Q.
Proof.
  intros P Q H p.
  apply H; assumption.
Qed.

Lemma delta_impR :
  forall P Q : Prop, (P -> Q) -> P -> P -> Q.
Proof.
  intros P Q H _.
  apply H.
Qed.

Lemma diamond :
  forall P Q R T : Prop,
    (P -> Q) -> (P -> R) -> (Q -> R -> T) -> P -> T.
Proof.
  intros P Q R T H H0 H1 p.
  apply H1.
  - apply H; assumption.
  - apply H0; assumption.
Qed.

Lemma weak_peirce :
  forall P Q : Prop, ((((P -> Q) -> P) -> P) -> Q) -> Q.
Proof.
  intros P Q H; apply H; intro H0.
  apply H0.
  intro p; apply H.
  intro H1; assumption.
Qed.