diff options
| -rw-r--r-- | pw09.v | 78 |
1 files changed, 55 insertions, 23 deletions
@@ -61,47 +61,70 @@ 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*) - +(* (* Not checked by proofweb *) +Definition term_1 + : forall a : Prop, a -> a + := fun (a : Prop) (x : a) => x. +Definition term_2 + : forall a b : Prop, (a -> b) -> a -> b + := fun (a : Prop) (b : Prop) (x : a -> b) => x. +Definition term_3 + : forall a : Prop, a -> forall b : Prop, (a -> b) -> b + := fun (a : Prop) (x : a) (b : Prop) (f : a -> b) => f x. +*) (* exercises with negation *) (* exercise 2 *) Lemma exercise2 : forall a:Prop, a -> ~~a. Proof. -(*! proof *) - +intros a H. +intro H'. +apply H'. +exact H. Qed. Lemma exercise3: forall a:Prop, ~~~a -> ~a. Proof. -(*! proof *) - +intros a H H'. +assert (~~a). +apply exercise2 ; exact H'. +apply H. +exact H0. Qed. Lemma exercise4: forall a:Prop, ~~(~~a -> a). Proof. -(*! proof *) - +intros a H. +apply H. +intro. +induction H0. +intro. +apply H. +intro. +exact H0. Qed. - +Print exercise4. (* exercises with full intuitionistic prop2 *) Lemma exercise5 : forall a:Prop, (exists b:Prop, a) -> a. Proof. -(*! proof *) - +intros a H. +elim H. +intros H0 H1. +exact H1. Qed. Lemma exercise6 : forall a:Prop, exists b:Prop, ((a -> b) \/ (b -> a)). Proof. -(*! proof *) - +intro a. +exists False. +right. +intro. +elimtype False. +assumption. Qed. @@ -112,8 +135,12 @@ Definition em:= forall a:Prop, a \/ ~a. Lemma exercise7: em -> forall a b:Prop, ((a -> b) \/ (b -> a)). Proof. -(*! proof *) +unfold em. +intros em' a b. +elim em' with a. +intro. right. intro. assumption. +intro H. left. intro. elimtype False. apply H. assumption. Qed. (* expressibility of prop2 *) @@ -125,22 +152,27 @@ Definition new_false := forall a:Prop, a. (* False implies new_false *) Lemma exercise8 : False -> new_false. Proof. -(*! proof *) - +intro. +elimtype False. +assumption. Qed. (* new_false implies False *) Lemma exercise9 : new_false -> False. Proof. -(*! proof *) - +unfold new_false. +intro H. +assert (~False). +unfold not. intro. assumption. +apply H. Qed. (* from new_false we can prove anything *) Lemma exercise10 : forall a:Prop, new_false -> a. Proof. -(*! proof *) - +unfold new_false. +intros a H. +apply H. Qed. |