diff options
Diffstat (limited to 'pw12.v')
| -rw-r--r-- | pw12.v | 90 |
1 files changed, 62 insertions, 28 deletions
@@ -70,34 +70,49 @@ Eval compute in (polyid nat O). Lemma exercise2 : forall a:Prop, a -> ~~a. Proof. -(*! proof *) - +intros a H H0. +apply H0. +exact H. Qed. Lemma exercise3: forall a:Prop, ~~~a -> ~a. Proof. -(*! proof *) - +intros a H H0. +apply H. +apply exercise2. +exact H0. Qed. Lemma exercise4: forall a:Prop, ~~(~~a -> a). Proof. -(*! proof *) - +intros a H. +apply H. +intro. +elimtype False. +apply H0. +intro. +apply H. +intro. +exact H1. Qed. (* exercises with full intuitionistic prop2 *) Lemma exercise5 : forall a:Prop, (exists b:Prop, a) -> a. Proof. -(*! proof *) - +intros a H. +elim H. +intros b Ha. +exact Ha. Qed. Lemma exercise6 : forall a:Prop, exists b:Prop, ((a -> b) \/ (b -> a)). Proof. -(*! proof *) - +intro. +exists a. +left. +intro. +assumption. Qed. (* exercise with classical prop2 *) @@ -106,8 +121,13 @@ 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. +assert (a \/ ~a). +apply em'. +inversion_clear H. +right. intro. assumption. +left. intro. elimtype False. apply H0. assumption. Qed. (* expressibility of prop2 *) @@ -119,22 +139,25 @@ Definition new_false := forall a:Prop, a. (* False implies new_false *) Lemma exercise8 : False -> new_false. Proof. -(*! proof *) - +intro. +elimtype False. +exact H. Qed. (* new_false implies False *) Lemma exercise9 : new_false -> False. Proof. -(*! proof *) - +unfold new_false. +intro. +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. (* definition of and *) @@ -145,8 +168,13 @@ Definition new_and (a b : Prop) := forall c : Prop, (a -> b -> c) -> c. (* and implies new_and *) Lemma exercise11 : forall a b : Prop,a /\ b -> new_and a b. Proof. -(*! proof *) - +unfold new_and. +intros a b H c H'. +elim H. +intros Ha Hb. +apply H'. +apply Ha. +apply Hb. Qed. @@ -154,8 +182,9 @@ Qed. Lemma exercise12 : forall a b : Prop , new_and a b -> a /\ b. Proof. -(*! proof *) - +unfold new_and. +intros a b H. +split ; apply H ; intros Ha Hb ; assumption. Qed. (* exercise 13 *) @@ -170,14 +199,20 @@ Definition new_or (a b : Prop) := forall c : Prop, (a -> c) -> (b -> c) -> c. Lemma exercise14 : forall a b , a \/ b -> new_or a b. Proof. -(*! proof *) - +unfold new_or. +intros a b H c Hac Hbc. +inversion_clear H. +apply Hac. assumption. +apply Hbc. assumption. Qed. Lemma exercise15 : forall a b , new_or a b -> a \/ b. Proof. -(*! proof *) - +unfold new_or. +intros a b H. +apply H. +intro. left. assumption. +intro. right. assumption. Qed. (* exercise 16 *) @@ -185,7 +220,6 @@ Qed. (* give an inhabitant of new_or A B with A and B in Prop *) Parameter Q:A. -Check (*! term *) - . +Check (fun (c : Prop) (Ha : A -> c) (Hb : B -> c) => Ha Q) : new_or A B. |