diff options
| -rw-r--r-- | pw08.v | 151 |
1 files changed, 120 insertions, 31 deletions
@@ -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. |