Add templates for exercises 8-12

1 files changed, 136 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.
+
+