(* ************************************************* *)
(* prop2                                             *)
(* ************************************************* *)



(* the paradigmatic example corresponding to           *)
(* the polymorphic identity                            *)
(* we already print the inhabitant although we did not *)
(* yet discuss lambda2                                 *)

Lemma example1a : forall a:Prop, a->a.

Proof.
intro a.
intro x.
exact x.
Qed.
Print example1a.
(* \a:Prop. \x:a. x *)



Lemma example1b : forall a:Set, a -> a.

Proof.
intro a.
intro x.
exact x.
Qed.
Print example1b.
(* \a:Set. \x:a. x *)



(* another example from the course *)
Lemma example2: forall a:Prop, a -> (forall b:Prop, ((a -> b) -> b)).

Proof.
intro a.
intro x.
intro b.
intro y.
apply y.
exact x.
Qed.
Print example2.
(* \a:Prop. \x:a. \b:Prop. \y:a->b. (y x) *)


(* the following "lemma" is not valid *)
(*
Lemma example_wrong : forall a:Prop, a -> (forall b:Prop, b).

Proof.
intro a.
intro x.
intro b.
Abort.
*)


(* exercise 1 *)

(* (* Not checked by proofweb *)
Definition term_1
  : forall a : Prop, a -> a
  := fun (a : Prop) (x : a) => x.
Definition term_2
  : forall a b : Prop, (a -> b) -> a -> b
  := fun (a : Prop) (b : Prop) (x : a -> b) => x.
Definition term_3
  : forall a : Prop, a -> forall b : Prop, (a -> b) ->  b
  := fun (a : Prop) (x : a) (b : Prop) (f : a -> b) => f x.
*)

(* exercises with negation *)

(* exercise 2 *)
Lemma exercise2 : forall a:Prop, a -> ~~a.
Proof.
intros a H.
intro H'.
apply H'.
exact H.
Qed.

Lemma exercise3: forall a:Prop, ~~~a -> ~a.
Proof.
intros a H H'.
assert (~~a).
apply exercise2 ; exact H'.
apply H.
exact H0.
Qed.

Lemma exercise4: forall a:Prop, ~~(~~a -> a).
Proof.
intros a H.
apply H.
intro.
induction H0.
intro.
apply H.
intro.
exact H0.
Qed.
Print exercise4.

(* exercises with full intuitionistic prop2 *)

Lemma exercise5 : forall a:Prop, (exists b:Prop, a) -> a.
Proof.
intros a H.
elim H.
intros H0 H1.
exact H1.
Qed.

Lemma exercise6 : forall a:Prop, exists b:Prop, ((a -> b) \/ (b -> a)).
Proof.
intro a.
exists False.
right.
intro.
elimtype False.
assumption.
Qed.



(* exercise with classical prop2 *)

Definition em:= forall a:Prop, a \/ ~a.

Lemma exercise7: em -> forall a b:Prop, ((a -> b) \/ (b -> a)).
Proof.
unfold em.
intros em' a b.
elim em' with a.

intro. right. intro. assumption.
intro H. left. intro. elimtype False. apply H. assumption.
Qed.

(* expressibility of prop2 *)
(* we will represent logical connectives in prop2 *)

(* definition of false *)
Definition new_false := forall a:Prop, a.

(* False implies new_false *)
Lemma exercise8 : False -> new_false.
Proof.
intro.
elimtype False.
assumption.
Qed.

(* new_false implies False *)
Lemma exercise9 : new_false -> False.
Proof.
unfold new_false.
intro H.
assert (~False).
unfold not. intro. assumption.
apply H.
Qed.

(* from new_false we can prove anything *)
Lemma exercise10 : forall a:Prop, new_false -> a.
Proof.
unfold new_false.
intros a H.
apply H.
Qed.