(* Assignment 7 *)

(* Exercise 7.1 (Proof terms and scripts) *)
Proposition a_exact : forall P Q : Prop, (P -> P -> Q) -> ((P -> Q) -> P) -> Q.

Proposition a_script : forall P Q : Prop, (P -> P -> Q) -> ((P -> Q) -> P) -> Q.

Proposition b_exact : forall P Q R S T : Prop, (Q -> R -> T) -> (P->Q) -> P -> R-> T.

Proposition b_script : forall P Q R S T : Prop, (Q -> R -> T) -> (P->Q) -> P -> R-> T.

Proposition c_exact : forall P Q R : Prop, (P -> Q) -> (Q -> R)-> P -> R.

Proposition c_script : forall P Q R : Prop, (P -> Q) -> (Q -> R)-> P -> R.

Proposition d_exact : forall P Q : Prop, P -> (P -> forall R, R) -> Q.

Proposition d_script : forall P Q : Prop, P -> (P -> forall R, R) -> Q.

(* Exercise 7.2 (Conjunction) *)
Inductive and (X Y : Prop) : Prop :=
| and_I : X -> Y -> and X Y.

Proposition conji_exact : forall X Y : Prop, X -> Y -> and X Y.

Proposition conji_script : forall X Y : Prop, X -> Y -> and X Y.

Proposition conjii_exact : forall X Y : Prop, and X Y -> X.

Proposition conjii_script : forall X Y : Prop, and X Y -> X.

(* Exercise 7.3 (Disjunction) *)
Inductive or (X Y: Prop) : Prop :=
| or_L : X -> or X Y
| or_R : Y -> or X Y.

Proposition disji_exact : forall X Y : Prop, X -> or X Y.

Proposition disji_script : forall X Y : Prop, X -> or X Y.

Proposition disjii_exact : forall X Y Z: Prop, or X Y -> (X -> Z) -> (Y -> Z) -> Z.

Proposition disjii_script : forall X Y Z: Prop, or X Y -> (X -> Z) -> (Y -> Z) -> Z.

(* Exercise 7.4 (Classical tautologies) *)
Definition DN := forall P: Prop, ~~P -> P.
Definition Contra := forall P Q : Prop, (~P -> ~Q) -> Q -> P.
Definition Peirce := forall P Q :  Prop, ((P -> Q) -> P) -> P.

Proposition dn2contra : DN -> Contra.

Proposition dn2peirce : DN -> Peirce.

Proposition contra2dn : Contra -> DN. 

Proposition contra2peirce : Contra -> Peirce.

Proposition peirce2dn : Peirce -> DN. 

Proposition peirce2contra : Peirce -> Contra.