Solve exercise 8

1 files changed, 120 insertions, 31 deletions

diff --git a/pw08.v b/pw08.v
index c8237d6..847729a 100644
--- a/pw08.v
+++ b/pw08.v
@@ -6,21 +6,13 @@ 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 prop1 := fun (x : C -> B -> A) (y : C -> B) (z : C) => x z (y z).
 
-Definition prop2 := (*! term *)
-(* fun (x : ?) (y : ?) (z : ?) => x (y z) z. *)
-  .
+Definition prop2 := fun (x : B -> C -> A) (y : C -> B) (z : C) => x (y z) z.
 
-Definition prop3 := (*! term *)
-(* fun (x : ?) (y : ?) => x (fun z : A => y) y. *)
-  .
+Definition prop3 := fun (x : (A -> B) -> B -> C) (y : B) => x (fun z : A => y) y.
 
-Definition prop4 := (*! term *)
-(* fun (x : ?) (y : ?) (z : ?) => x (y x) (z x). *)
-  .
+Definition prop4 := fun (x : A -> B -> C) (y : (A -> B -> C) -> A) (z : (A -> B -> C) -> B) => x (y x) (z x).
 
 End proplogic.
 
@@ -29,13 +21,9 @@ 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 pred1 := fun (l : Set -> Set) (A : Set) (B : Set) (f : l A -> l B) (x : l A) => f x.
 
-Definition pred2 := (*! term *)
-(* fun (e : nat -> nat -> ?) (n : ?) => forall m : ?, e n m. *)
-  .
+Definition pred2 := fun (e : nat -> nat -> Set) (n : nat) => forall m : nat, e n m.
 
 End deptypes.
 
@@ -63,13 +51,24 @@ Parameter dn: forall p:Prop, ~~p -> p.
 (* exercise 3 *)
 (* prove the following auxiliary lemma
    use dn twice, first time quite soon *)
+(* With help: https://stackoverflow.com/a/4418135/1544337 *)
 Lemma aux : (~ forall x:D, drinks x) -> (exists x:D, ~drinks x).
 Proof.
-(*! proof *)
-
+intro F.
+apply dn.
+intro E.
+apply F.
+intro x.
+assert (drinks x \/ ~drinks x).
+apply em.
+inversion_clear H.
+exact H0.
+elimtype False.
+apply E.
+exists x.
+exact H0.
 Qed.
 
-
 (* exercise 4 *)
 (* prove the drinker's paradox *)
 (* first step: use em to distinguish two cases: everyone drinks or not *)
@@ -77,11 +76,24 @@ Qed.
 
 Theorem drinker : exists x:D, (drinks x) -> (forall y:D, drinks y).
 Proof.
-(*! proof *)
-
+assert ((forall x:D, drinks x) \/ ~(forall x:D, drinks x)).
+apply em.
+inversion_clear H.
+exists d.
+intro.
+exact H0.
+assert (exists x:D, ~drinks x).
+apply aux.
+exact H0.
+elim H.
+intros x H'.
+exists x.
+intro.
+elimtype False.
+apply H'.
+exact H1.
 Qed.
 
-
 (* second proof *)
 
 (* exercise 5 *)
@@ -89,8 +101,37 @@ Qed.
    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 *)
-
+apply dn.
+intro.
+(*assert (forall x:D, ~(drinks x -> forall y:D, drinks y)).*)
+assert (forall x:D, drinks x /\ ~(forall y:D, drinks y)).
+intro x.
+split.
+assert (drinks x \/ ~drinks x).
+apply em.
+inversion_clear H0.
+exact H1.
+elim H.
+exists x.
+intro.
+elimtype False.
+apply H1.
+exact H0.
+intro.
+apply H.
+exists x.
+intro.
+exact H0.
+elim H0 with d.
+intro.
+intro.
+apply H2.
+(* Coq accepts, but prover rejects 'apply H0' here *)
+intro.
+elim H0 with y.
+intro.
+intro.
+exact H3.
 Qed.
 
 End drinker.
@@ -115,8 +156,24 @@ Theorem barber : ~ exists x : V ,
    /\
   (forall y:V, (~ shaves y y -> shaves x y)).
 Proof.
-(*! proof *)
-
+intro.
+inversion_clear H.
+inversion_clear H0.
+assert (shaves x x \/ ~shaves x x).
+apply em.
+inversion_clear H0.
+
+assert (~shaves x x).
+apply H.
+exact H2.
+apply H0.
+exact H2.
+
+assert (shaves x x).
+apply H1.
+exact H2.
+apply H2.
+exact H0.
 Qed.
 
 
@@ -124,11 +181,43 @@ Qed.
    prove the more elegant formulation of the barber's paradox
    with the forall inside the /\ *)
 
-Theorem barber2 : (*! term *)
-  .
+Theorem barber2 : ~exists x:V,
+  (forall y:V, (shaves x y -> ~shaves y y) /\ (~shaves y y -> shaves x y)).
 Proof.
-(*! proof *)
+intro.
+inversion_clear H.
+assert (shaves x x \/ ~shaves x x).
+apply em.
+inversion_clear H.
+
+assert (~shaves x x).
+apply H0.
+exact H1.
+contradiction.
+
+assert (shaves x x).
+apply H0.
+exact H1.
+contradiction.
+Qed.
 
+(* version accepted by the prover: *)
+
+Theorem barber3 : ~exists x:V,
+  (forall y:V, (shaves x y -> ~shaves y y) /\ (~shaves y y -> shaves x y)).
+Proof.
+intro.
+inversion_clear H.
+elim H0 with x.
+intro.
+intro.
+
+assert (shaves x x \/ ~shaves x x).
+apply em.
+inversion_clear H2.
+
+apply H. exact H3. exact H3.
+apply H3. apply H1. exact H3.
 Qed.
 
 End barber.