1 files changed, 146 insertions, 0 deletions
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.
+
+