Add templates for exercises 8-12

5 files changed, 1104 insertions, 0 deletions

diff --git a/pw08.v b/pw08.v
new file mode 100644
index 0000000..c8237d6
--- /dev/null
+++ b/pw08.v
@@ -0,0 +1,136 @@
+(* cf antwoorden voor laatste opgave *)
+
+Section proplogic.
+Parameters A B C : Prop.
+
+(* exercise 1 *)
+(* complete the following simply typed lambda terms *)
+
+Definition prop1 := (*! term *)
+(* fun (x : ?) (y : ?) (z : ?) => x z (y z). *)
+  .
+
+Definition prop2 := (*! term *)
+(* fun (x : ?) (y : ?) (z : ?) => x (y z) z. *)
+  .
+
+Definition prop3 := (*! term *)
+(* fun (x : ?) (y : ?) => x (fun z : A => y) y. *)
+  .
+
+Definition prop4 := (*! term *)
+(* fun (x : ?) (y : ?) (z : ?) => x (y x) (z x). *)
+  .
+
+End proplogic.
+
+Section deptypes.
+
+(* exercise 2 *)
+(* complete the following dependently typed lambda terms *)
+
+Definition pred1 := (*! term *)
+(* fun (l : Set -> Set) (A : ?) (B : ?) (f : l A -> l B) (x : ?) => f x. *)
+  .
+
+Definition pred2 := (*! term *)
+(* fun (e : nat -> nat -> ?) (n : ?) => forall m : ?, e n m. *)
+  .
+
+End deptypes.
+
+
+
+Section drinker.
+
+(* we will prove (twice) the drinker's paradox:
+   in a non-empty domain there is someone such that
+   if he drinks then everyone drinks *)
+
+(* use the following *)
+Parameter D : Set.
+Parameter d : D.
+Parameter drinks : D -> Prop.
+
+(* law of excluded middle *)
+Parameter em: forall p:Prop, p \/ ~p.
+
+(* double negation law *)
+Parameter dn: forall p:Prop, ~~p -> p.
+
+(* first proof *)
+
+(* exercise 3 *)
+(* prove the following auxiliary lemma
+   use dn twice, first time quite soon *)
+Lemma aux : (~ forall x:D, drinks x) -> (exists x:D, ~drinks x).
+Proof.
+(*! proof *)
+
+Qed.
+
+
+(* exercise 4 *)
+(* prove the drinker's paradox *)
+(* first step: use em to distinguish two cases: everyone drinks or not *)
+(* for the second case, use aux *)
+
+Theorem drinker : exists x:D, (drinks x) -> (forall y:D, drinks y).
+Proof.
+(*! proof *)
+
+Qed.
+
+
+(* second proof *)
+
+(* exercise 5 *)
+(* give another proof of the drinker
+   using dn in the first step and then yet another time *)
+Theorem drinker2 : exists x:D, (drinks x) -> (forall y:D, drinks y).
+Proof.
+(*! proof *)
+
+Qed.
+
+End drinker.
+
+Section barber.
+
+(* the barber's paradox:
+   it is not the case that
+   there is someone who shaves exactly everyone who does not shave himself *)
+
+(* setting *)
+Parameter V : Set.
+Parameter v : V.
+Parameter shaves : V -> V -> Prop.
+
+(* the barber's paradox *)
+(* exercise 6: prove the barber's paradox
+   use inversion twice,
+   and distinguish cases using em: x shaves himself or not *)
+Theorem barber : ~ exists x : V ,
+  (forall y:V, (shaves x y -> ~ shaves y y))
+   /\
+  (forall y:V, (~ shaves y y -> shaves x y)).
+Proof.
+(*! proof *)
+
+Qed.
+
+
+(* possible additional exercise:
+   prove the more elegant formulation of the barber's paradox
+   with the forall inside the /\ *)
+
+Theorem barber2 : (*! term *)
+  .
+Proof.
+(*! proof *)
+
+Qed.
+
+End barber.
+
+
diff --git a/pw09.v b/pw09.v
new file mode 100644
index 0000000..753a592
--- /dev/null
+++ b/pw09.v
@@ -0,0 +1,146 @@
+(* ************************************************* *)
+(* 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 *)
+(* give inhabitants of the following types: *)
+(* forall a : Prop, a -> a *)
+(* forall a b : Prop, (a -> b) -> a -> b *)
+(* forall a : Prop, a -> forall b : Prop, (a -> b) ->  b*)
+
+
+
+(* exercises with negation *)
+
+(* exercise 2 *)
+Lemma exercise2 : forall a:Prop, a -> ~~a.
+Proof.
+(*! proof *)
+
+Qed.
+
+Lemma exercise3: forall a:Prop, ~~~a -> ~a.
+Proof.
+(*! proof *)
+
+Qed.
+
+Lemma exercise4: forall a:Prop, ~~(~~a -> a).
+Proof.
+(*! proof *)
+
+Qed.
+
+
+(* exercises with full intuitionistic prop2 *)
+
+Lemma exercise5 : forall a:Prop, (exists b:Prop, a) -> a.
+Proof.
+(*! proof *)
+
+Qed.
+
+Lemma exercise6 : forall a:Prop, exists b:Prop, ((a -> b) \/ (b -> a)).
+Proof.
+(*! proof *)
+
+Qed.
+
+
+
+(* exercise with classical prop2 *)
+
+Definition em:= forall a:Prop, a \/ ~a.
+
+Lemma exercise7: em -> forall a b:Prop, ((a -> b) \/ (b -> a)).
+Proof.
+(*! proof *)
+
+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.
+(*! proof *)
+
+Qed.
+
+(* new_false implies False *)
+Lemma exercise9 : new_false -> False.
+Proof.
+(*! proof *)
+
+Qed.
+
+(* from new_false we can prove anything *)
+Lemma exercise10 : forall a:Prop, new_false -> a.
+Proof.
+(*! proof *)
+
+Qed.
+
+
diff --git a/pw10.v b/pw10.v
new file mode 100644
index 0000000..823c297
--- /dev/null
+++ b/pw10.v
@@ -0,0 +1,313 @@
+(* ************************************************* *)
+(* introduction and examples                         *)
+(* ************************************************* *)
+
+
+(* example of a polymorphic function: identity *)
+
+(* first the identity on natural numbers *)
+Definition natid : nat -> nat :=
+  fun n : nat => n.
+Check (natid O).
+Eval compute in (natid O).
+
+(* then the identity on booleans *)
+Definition boolid: bool -> bool :=
+  fun b : bool => b.
+Check (boolid true).
+Eval compute in (boolid true).
+
+(* now the polymorphic identity *)
+Definition polyid : forall A : Set, A -> A :=
+  fun (A : Set) => fun (a : A) => a.
+Check polyid.
+
+Check (polyid nat).
+Check (polyid nat O).
+Eval compute in (polyid nat O).
+Check (polyid _ O).
+
+Check (polyid bool).
+Check (polyid bool true).
+Eval compute in (polyid bool true).
+Check (polyid _ true).
+
+(* the following does not work:
+Check (polyid _).
+because Coq cannot infer what should be on the place of _ *)
+
+(* notation *)
+Notation id := (polyid _).
+Check (id O).
+Eval compute in (id O).
+Check (id true).
+Eval compute in (id true).
+
+
+
+(* example of a polymorphic inductive definition: polylists *)
+
+(* first the lists of natural numbers *)
+Inductive natlist : Set :=
+  natnil : natlist
+| natcons : nat -> natlist -> natlist.
+
+(* the list 2;1;0 *)
+Check (natcons 2 (natcons 1 (natcons 0 natnil))).
+
+(* then the lists of booleans *)
+Inductive boollist : Set :=
+  boolnil : boollist
+| boolcons : bool -> boollist -> boollist.
+
+(* now the polymorphic lists *)
+Inductive polylist (X : Set) : Set :=
+    polynil  : polylist X
+  | polycons : X -> polylist X -> polylist X.
+
+Check polylist.
+Check (polylist nat).
+Check (polylist bool).
+
+Check polynil.
+Check (polynil nat).
+Check (polynil bool).
+Check polycons.
+Check (polycons nat).
+Check (polycons bool).
+
+(* again the list 2;1;0 *)
+Check (polycons nat 2 (polycons nat 1 (polycons nat 0 (polynil nat)))).
+
+(* we introduce some handy notation *)
+Notation ni := (polynil _).
+Notation co := (polycons _).
+(* and write the list 2;1;0 again *)
+Check (co 2 (co 1 (co 0 ni))).
+Check (co true (co false ni)).
+
+(* induction principle for polymorphic lists;
+   more about this later *)
+Check polylist_ind.
+
+(* length of lists of natural numbers *)
+Fixpoint natlength (l:natlist) {struct l} : nat :=
+  match l with
+    natnil => O
+  | natcons h t => S (natlength t)
+  end.
+
+Eval compute in (natlength (natcons 2 (natcons 1 (natcons 0 natnil)))).
+
+(* length of polymorphic lists *)
+Fixpoint polylength (A:Set)(l:(polylist A)){struct l} : nat :=
+  match l with
+    polynil => O
+  | polycons h t => S (polylength A t)
+  end.
+
+(* NB: in the recursive definition,
+   polynil and polycons do _not_ get an argument A left of =>;
+   they do get such arguments right of => *)
+
+Eval compute in (polylength nat (polycons nat 2 (polycons nat 1 (polycons nat 0 (polynil nat))))).
+Eval compute in (polylength nat (co 2 (co 1 (co 0 ni)))).
+
+Eval compute in (polylength bool (polycons bool true (polycons bool false (polynil bool)))).
+Eval compute in (polylength bool (co true (co false ni))).
+
+(* remark1 about Coq notation:
+   In the definition of polylist
+   we use a parameter declaration (X:Set).
+   Alternatively, we could define a type Set -> Type
+   as follows: *)
+Inductive polylistb : Set -> Type :=
+  polynilb : forall X:Set, polylistb X
+| polyconsb: forall X:Set, X -> polylistb X -> polylistb X.
+
+(* but then we get a quite strange induction predicate *)
+Check polylistb_ind.
+
+(* so we usually take the first definition *)
+
+
+
+
+(* ************************************************* *)
+(*        start of the  exercises                    *)
+(* ************************************************* *)
+
+(*        exercises about polymorphic lists          *)
+(*        see pw04 for similar exercises on natlists *)
+
+(* exercise 1 *)
+(* give the definition of polyappend for polymorphic lists *)
+(* test it using Eval compute on an example *)
+
+Fixpoint polyappend (X:Set) (k l : polylist X) {struct k} : (polylist X) :=
+    (*! term *)
+  .
+
+Eval compute in (*! term *)
+  .
+
+(* prove the following lemma, to be used later*)
+Lemma append_nil :
+  forall X:Set, forall l: polylist X,
+  polyappend X l (polynil X) = l.
+Proof.
+(*! proof *)
+
+Qed.
+
+
+(* exercise 3 *)
+(* prove the following lemma, to be used later *)
+Lemma append_assoc : forall X, forall k l m,
+  (polyappend X (polyappend X k l) m) = (polyappend X k (polyappend X l m)).
+Proof.
+(*! proof *)
+
+Qed.
+
+
+(* exercise 4 *)
+(* prove the following lemma *)
+Lemma length_append :
+ forall X:Set, forall k l : (polylist X),
+  polylength X (polyappend X k l) = plus (polylength X k) (polylength X l).
+Proof.
+(*! proof *)
+
+Qed.
+
+
+(* exercise 5 *)
+(* give the definition of polyreverse for polymorphic lists *)
+(* test it using Eval compute on an example *)
+
+Fixpoint polyreverse (X:Set) (l : polylist X) {struct l} :(polylist X) :=
+    (*! term *)
+  .
+
+
+(* exercise 6 *)
+(* prove the following lemma *)
+Lemma reverse_append :
+  forall X:Set, forall k l: (polylist X),
+  polyreverse X (polyappend X k l) =
+  polyappend X (polyreverse X l) (polyreverse X k).
+Proof.
+(*! proof *)
+
+Qed.
+
+
+(* exercise 7 *)
+(* prove the following lemma *)
+(* this does not correspond to a lemma in pw04 *)
+Lemma rev_cons_app :
+  forall X:Set, forall k l : (polylist X), forall x:X,
+  polyappend X (polyreverse X (polycons X x k)) l =
+  polyappend X (polyreverse X k) (polycons X x l).
+Proof.
+(*! proof *)
+
+Qed.
+
+
+
+(*        exercises about polymorphic pairs         *)
+
+
+
+(* definition of pairs of natural numbers *)
+Inductive natprod : Set :=
+| natpair : nat -> nat -> natprod.
+
+Check natpair.
+Check natpair 1.
+Check (natpair 1 2).
+
+Check natprod_ind.
+
+(* we define the first and second projection *)
+
+Definition natprodfirst (p : natprod) : nat :=
+match p with
+| natpair x y => x
+end.
+Eval compute in (natprodfirst (natpair 1 2)).
+
+Definition natprodsecond (p : natprod) : nat :=
+match p with
+| natpair x y => y
+end.
+Eval compute in (natprodsecond (natpair 1 2)).
+
+(* exercise 8 *)
+(* give a definition prod of polymorphic pairs
+   where the first element comes from a set X
+   and the second element comes from a set Y    *)
+
+Inductive prod (X Y :Set) : Set := (*! term *)
+  .
+
+(* exercise 9 *)
+(* give definitions of the first and second projection *)
+
+Definition fst (X Y : Set) (p: prod X Y) : X := (*! term *)
+  .
+
+Definition snd (X Y : Set) (p : prod X Y) : Y := (*! term *)
+  .
+
+
+(*        exercises about polymorphic trees       *)
+
+
+
+(* definition of natbintrees
+   with labels on the nodes  *)
+Inductive natbintree : Set :=
+    natleaf : natbintree
+  | natnode : nat -> natbintree -> natbintree -> natbintree.
+
+Check natleaf.
+Check (natnode 1 natleaf natleaf).
+Check (natnode 2 (natnode 1 natleaf natleaf) (natnode 3 natleaf natleaf)).
+
+(* the last is the tree
+               2
+              / \
+             1   3
+*)
+
+(* exercise 10 *)
+(* give the definition polybintree with constructors polyleaf and polynode
+   of polymorphic binary trees
+   with labels on the nodes
+   you may introduce handy notation *)
+
+Inductive polybintree (X : Set) : Set := (*! term *)
+  .
+
+
+
+(* exercise 11 *)
+(* complete the definition of polyflatten
+   polyflatten puts the labels of a polybintree from left to right in a polylist *)
+
+Fixpoint polyflatten (X:Set) (t:polybintree X) {struct t} : (polylist X) :=
+  (*! term *)
+(*
+match t with
+| polyleaf =>
+| polynode x l r =>
+end
+*)
+  .
+
+(* perform some tests using the trees above *)
+
+
diff --git a/pw11.v b/pw11.v
new file mode 100644
index 0000000..b3e0896
--- /dev/null
+++ b/pw11.v
@@ -0,0 +1,318 @@
+(* ************************************************* *)
+(* prop1 and simply typed lambda calculus *)
+(* ************************************************* *)
+
+Section prop1.
+
+Parameters A B C : Prop.
+
+(* exercise 1 *)
+(* prove the following three lemma's *)
+(* also use Print to see the proof-term *)
+Lemma one1 : ((A -> B -> A) -> A) -> A.
+Proof.
+(*! proof *)
+
+Qed.
+
+Lemma one2 : (A -> B -> C) -> (A -> B) -> A -> C.
+Proof.
+(*! proof *)
+
+Qed.
+
+Lemma one3 : (B -> (A -> B) -> C) -> B -> C.
+Proof.
+(*! proof *)
+
+Qed.
+
+
+
+(* exercise 2 *)
+(* give of each of the following three types an inhabitant *)
+Definition two1 : (A -> A -> B) -> (C -> A) -> C -> B := (*! term *)
+  .
+
+Definition two2 : (A -> A -> B) -> A -> B := (*! term *)
+  .
+
+Definition two3 : (A -> B -> C) -> B -> A -> C := (*! term *)
+  .
+
+
+
+(* exercise 3 *)
+(* complete the following four simply typed lambda terms *)
+Definition three1 := (*! term *)
+(* fun (x : ?) (y : ?) (z : ?) => x z (y z) *)
+  .
+
+Definition three2 := (*! term *)
+(* fun (x : ?) (y : ?) (z : ?) => x (y z) z *)
+  .
+
+Definition three3 := (*! term *)
+(* fun (x : ?) (y : ?) => x (fun z : ? => y) y *)
+  .
+
+Definition three4 := (*! term *)
+(* fun (x : ?) (y : ?) (z : ?) => x (y x) (z x) *)
+  .
+
+
+
+(* exercise 4 *)
+(* prove the following two lemma's *)
+Lemma four1 : (~A \/ B) -> (A -> B).
+Proof.
+(*! proof *)
+
+Qed.
+
+Lemma four2 : (A \/ ~ A) -> ~~A -> A.
+Proof.
+(*! proof *)
+
+Qed.
+
+
+
+End prop1.
+
+(* ************************************************* *)
+(* pred1 and lambda P *)
+(* ************************************************* *)
+
+Section pred1.
+
+Parameter Terms : Set.
+Parameters M N : Terms.
+Parameters P Q : Terms -> Prop.
+Parameters R : Terms -> Terms -> Prop.
+
+
+
+(* exercise 5 *)
+(* prove the following three lemma's *)
+(* use Print to see the proof-term *)
+(* see practical work 7 *)
+Lemma five1 : (forall x:Terms, ~ (P x)) -> ~ (exists x:Terms, P x).
+Proof.
+(*! proof *)
+
+Qed.
+
+Lemma five2 : forall x:Terms, (P x -> ~ (forall y:Terms, ~(P y))).
+Proof.
+(*! proof *)
+
+Qed.
+
+Lemma five3 :
+  (forall x y :Terms, R x y -> ~ (R y x)) ->
+  (forall x:Terms, ~ (R x x)).
+Proof.
+(*! proof *)
+
+Qed.
+
+
+   
+(* exercise 6 *)
+(* give inhabitants of the following two types *)
+
+Definition six1 : 
+  (forall x y:Terms, R x y -> R y x) ->
+  (forall x : Terms, R x M -> R M x) := (*! term *)
+  .
+
+Definition six2 :
+  (forall x y z : Terms, R x y -> R y z -> R x z) ->
+  R M N ->
+  R N M ->
+  R M M := (*! term *)
+  .
+
+
+  
+(* exercise 7 *)
+(* complete the following two lambda-terms *)
+
+Definition seven1 := (*! term *)
+(*
+  fun (H : forall x:Terms, P x -> Q x) =>
+  fun (I : ?) =>
+  H M I
+*)
+  .
+
+Definition seven2 := (*! term *)
+(*
+  fun (H : forall x y : Terms, R x y -> R y x) =>
+  fun (I : ?) =>
+  H M N I
+*)
+  .
+
+Definition seven3 := (*! term *)
+(*
+  fun (H : ?) =>
+  fun (I : forall x, P x -> Q x) =>
+  I M (H M)
+*)
+  .
+
+End pred1.
+
+
+
+(* ************************************************* *)
+(* prop2 and polymorphic lambda calculus *)
+(* ************************************************* *)
+
+Section prop2.
+
+(* exercise 8 *)
+(* prove the following two lemma's *)
+Lemma eight1 : forall a:Prop, a -> forall b:Prop, b -> a. 
+Proof.
+(*! proof *)
+
+Qed.
+
+Lemma eight2 : (forall a:Prop, a) -> 
+  forall b:Prop, forall c:Prop, ((b->c)->b)->b.
+Proof.
+(*! proof *)
+
+Qed.
+
+
+
+(* exercise 9 *)
+(* find inhabitants of the following two types *)
+Definition nine1 : forall a:Prop, (forall b:Prop, b) -> a := (*! term *)
+  .
+
+Definition nine2 : forall a:Prop, a -> (forall b:Prop, ((a -> b) -> b)) :=
+    (*! term *)
+  .
+
+
+
+(* exercise 10 *)
+(* complete the following lambda terms *)
+
+Definition ten1 := (*! term *)
+(*
+  fun (a:?) =>
+  fun (x: forall b:Prop, b) =>
+  x a
+*)
+  .
+
+Definition ten2 := (*! term *)
+(*
+  fun (a:?) =>
+  fun (x:a) =>
+  fun (b:?) =>
+  fun (y:b) =>
+  x
+*)
+  .
+ 
+
+
+End prop2.
+
+
+
+
+(* ************************************************* *)
+(* inductive datatypes and predicates *)
+(* ************************************************* *)
+
+Section inductivetypes.
+
+(* given *)
+Fixpoint plus (n m : nat) {struct n} : nat :=
+  match n with
+  | O => m
+  | S p => S (plus p m)
+  end.
+
+
+
+(* exercise 11 *)
+(* prove the following three lemma's *)
+Lemma plus_n_O : forall n : nat, n = plus n 0.
+Proof.
+(*! proof *)
+
+Qed.
+
+Lemma plus_n_S : forall n m : nat, S (plus n m) = plus n (S m).
+Proof.
+(*! proof *)
+
+Qed.
+
+Lemma com : forall n m : nat, plus n m = plus m n.
+Proof.
+(*! proof *)
+
+Qed.
+
+
+
+(* given *)
+Inductive polybintree (X : Set) : Set :=
+    polyleaf : X -> polybintree X
+  | polynode : polybintree X -> polybintree X -> polybintree X.
+
+
+
+(* exercise 12 *)
+(* give a definition counttree that counts the number of leafs *)
+
+Fixpoint counttree (X : Set) (b : polybintree X) {struct b} : nat :=
+    (*! term *)
+  .
+
+
+
+(* exercise 13 *)
+(* give a definition sum that adds the values on the leafs
+   for a tree with natural numbers on the leafs *)
+
+Fixpoint sum (b:polybintree nat) {struct b} : nat := (*! term *)
+  .
+
+
+(* given *)
+Definition ifb (b1 b2 b3:bool) : bool :=
+  match b1 with
+  | true => b2
+  | false => b3
+  end.
+
+(* given *)
+Definition andb (b1 b2:bool) : bool := ifb b1 b2 false.
+
+
+
+(* exercise 14 *)
+(* give a definition and that computes the conjunction
+   of the values of all leafs where all leafs have a 
+   boolean label 
+   use andb for conjunction on booleans *)
+
+Fixpoint conjunction (t : polybintree bool) {struct t} : bool := (*! term *)
+  .
+
+
+
+End inductivetypes.
+
+
diff --git a/pw12.v b/pw12.v
new file mode 100644
index 0000000..977f4f6
--- /dev/null
+++ b/pw12.v
@@ -0,0 +1,191 @@
+(* first part: prop2 and lambda2 and their connection *)
+(* via the Curry-Howard-De Bruijn isomorphism         *)
+
+(* the paradigmatic example: the polymorphic identity *)
+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.
+*)
+
+(* the polymorphic identity *)
+Definition polyid : forall a:Set, forall x:a, a := 
+                    fun a:Set =>  fun x:a =>  x.
+(* instantiation by application *)
+(* Check gives the types *)
+Check polyid.
+Check polyid nat.
+Check polyid nat O.
+(* Eval compute computes normal forms *)
+Eval compute in (polyid nat).
+Eval compute in (polyid nat O).
+
+(* exercise 1 *)
+(* give inhabitants of the following types *)
+
+(* forall a : Prop, a -> a *)
+(* forall a b : Prop, (a -> b) -> a -> b *)
+(* forall a : Prop, a -> forall b : Prop, (a -> b) ->  b*)
+
+(* exercises with negation *)
+
+Lemma exercise2 : forall a:Prop, a -> ~~a.
+Proof.
+(*! proof *)
+
+Qed.
+
+Lemma exercise3: forall a:Prop, ~~~a -> ~a.
+Proof.
+(*! proof *)
+
+Qed.
+
+Lemma exercise4: forall a:Prop, ~~(~~a -> a).
+Proof.
+(*! proof *)
+
+Qed.
+
+(* exercises with full intuitionistic prop2 *)
+
+Lemma exercise5 : forall a:Prop, (exists b:Prop, a) -> a.
+Proof.
+(*! proof *)
+
+Qed.
+
+Lemma exercise6 : forall a:Prop, exists b:Prop, ((a -> b) \/ (b -> a)).
+Proof.
+(*! proof *)
+
+Qed.
+
+(* exercise with classical prop2 *)
+
+Definition em:= forall a:Prop, a \/ ~a.
+
+Lemma exercise7 : em -> forall a b:Prop, ((a -> b) \/ (b -> a)).
+Proof.
+(*! proof *)
+
+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.
+(*! proof *)
+
+Qed.
+
+(* new_false implies False *)
+Lemma exercise9 : new_false -> False.
+Proof.
+(*! proof *)
+
+Qed.
+
+(* from new_false we can prove anything *)
+Lemma exercise10 : forall a:Prop, new_false -> a.
+Proof.
+(*! proof *)
+
+Qed.
+
+(*  definition of and *)
+(* "a and b" is valid is everything that can be
+   derived from {a,b} is valid *)
+Definition new_and (a b : Prop) := forall c : Prop, (a -> b -> c) -> c.
+
+(* and implies new_and *)
+Lemma exercise11 : forall a b : Prop,a /\ b -> new_and a b.
+Proof.
+(*! proof *)
+
+Qed.
+
+
+(* new_and implies and *)
+Lemma exercise12 : forall a b : Prop ,
+                   new_and a b -> a /\ b.
+Proof.
+(*! proof *)
+
+Qed.
+
+(* exercise 13 *)
+(* assume an inhabitant P of new_and A B with A and B in Prop *)
+(* give an inhabitant of A and an inhabitant of B *)
+Parameters A B : Prop.
+Parameter P : new_and A B.
+
+(* "a or b" is valid if everything that follows form
+   {a} and follows from {b} is valid *)
+Definition new_or (a b : Prop) := forall c : Prop, (a -> c) -> (b -> c) -> c.
+
+Lemma exercise14 : forall a b , a \/ b -> new_or a b.
+Proof.
+(*! proof *)
+
+Qed.
+
+Lemma exercise15 : forall a b , new_or a b -> a \/ b.
+Proof.
+(*! proof *)
+
+Qed.
+
+(* exercise 16 *)
+(* given an inhabitant Q:A *)
+(* give an inhabitant of new_or A B with A and B in Prop *)
+Parameter Q:A.
+
+Check (*! term *)
+  .
+
+