Finish all proofweb exercises

2 files changed, 179 insertions, 121 deletions

diff --git a/pw11.v b/pw11.v
index b3e0896..b942a0e 100644
--- a/pw11.v
+++ b/pw11.v
@@ -11,54 +11,60 @@ Parameters A B C : Prop.
 (* also use Print to see the proof-term *)
 Lemma one1 : ((A -> B -> A) -> A) -> A.
 Proof.
-(*! proof *)
-
+intro.
+apply H.
+intros a b.
+exact a.
 Qed.
+Print one1.
 
 Lemma one2 : (A -> B -> C) -> (A -> B) -> A -> C.
 Proof.
-(*! proof *)
-
+intros H H' a.
+apply H.
+assumption.
+apply H'.
+assumption.
 Qed.
 
 Lemma one3 : (B -> (A -> B) -> C) -> B -> C.
 Proof.
-(*! proof *)
-
+intros H b.
+apply H.
+exact b.
+intro.
+exact b.
 Qed.
 
 
 
 (* exercise 2 *)
 (* give of each of the following three types an inhabitant *)
-Definition two1 : (A -> A -> B) -> (C -> A) -> C -> B := (*! term *)
-  .
+Definition two1
+  : (A -> A -> B) -> (C -> A) -> C -> B
+  := fun (f : A -> A -> B) (g : C -> A) (c : C) => f (g c) (g c).
 
-Definition two2 : (A -> A -> B) -> A -> B := (*! term *)
-  .
+Definition two2
+  : (A -> A -> B) -> A -> B
+  := fun (f : A -> A -> B) (x : A) => f x x.
 
-Definition two3 : (A -> B -> C) -> B -> A -> C := (*! term *)
-  .
+Definition two3
+  : (A -> B -> C) -> B -> A -> C
+  := fun (f : A -> B -> C) (x : B) (y : A) => f y x.
 
 
 
 (* exercise 3 *)
 (* complete the following four simply typed lambda terms *)
-Definition three1 := (*! term *)
-(* fun (x : ?) (y : ?) (z : ?) => x z (y z) *)
-  .
+Definition three1 := fun (x : C -> B -> A) (y : C -> B) (z : C) => x z (y z).
 
-Definition three2 := (*! term *)
-(* fun (x : ?) (y : ?) (z : ?) => x (y z) z *)
-  .
+Definition three2 := fun (x : B -> C -> A) (y : C -> B) (z : C) => x (y z) z.
 
-Definition three3 := (*! term *)
-(* fun (x : ?) (y : ?) => x (fun z : ? => y) y *)
-  .
+Definition three3 := fun (x : (C -> B) -> B -> A) (y : B) => x (fun z : C => y) y.
 
-Definition three4 := (*! term *)
-(* fun (x : ?) (y : ?) (z : ?) => x (y x) (z x) *)
-  .
+Definition three4
+  := fun (x : B -> C -> A) (y : (B -> C -> A) -> B) (z : (B -> C -> A) -> C)
+  => x (y x) (z x).
 
 
 
@@ -66,14 +72,20 @@ Definition three4 := (*! term *)
 (* prove the following two lemma's *)
 Lemma four1 : (~A \/ B) -> (A -> B).
 Proof.
-(*! proof *)
-
+intro.
+inversion_clear H.
+intro. elimtype False. apply H0. exact H.
+intro. exact H0.
 Qed.
 
 Lemma four2 : (A \/ ~ A) -> ~~A -> A.
 Proof.
-(*! proof *)
-
+intros H H'.
+inversion_clear H.
+assumption.
+elimtype False.
+apply H'.
+exact H0.
 Qed.
 
 
@@ -99,69 +111,66 @@ Parameters R : Terms -> Terms -> Prop.
 (* see practical work 7 *)
 Lemma five1 : (forall x:Terms, ~ (P x)) -> ~ (exists x:Terms, P x).
 Proof.
-(*! proof *)
-
+intros F E.
+elim E.
+intros x H.
+apply F with x.
+exact H.
 Qed.
 
 Lemma five2 : forall x:Terms, (P x -> ~ (forall y:Terms, ~(P y))).
 Proof.
-(*! proof *)
-
+intros x H F.
+apply F with x.
+exact H.
 Qed.
 
 Lemma five3 :
   (forall x y :Terms, R x y -> ~ (R y x)) ->
   (forall x:Terms, ~ (R x x)).
 Proof.
-(*! proof *)
-
+intros H x HR.
+apply H with x x ; exact HR.
 Qed.
 
 
-   
 (* exercise 6 *)
 (* give inhabitants of the following two types *)
 
 Definition six1 : 
   (forall x y:Terms, R x y -> R y x) ->
-  (forall x : Terms, R x M -> R M x) := (*! term *)
-  .
+  (forall x : Terms, R x M -> R M x) :=
+  fun (f : forall x y:Terms, R x y -> R y x) (X : Terms) (r : R X M) => f X M r.
 
 Definition six2 :
   (forall x y z : Terms, R x y -> R y z -> R x z) ->
   R M N ->
   R N M ->
-  R M M := (*! term *)
-  .
+  R M M :=
+  fun
+    (f : forall x y z : Terms, R x y -> R y z -> R x z)
+    (ra : R M N)
+    (rb : R N M) =>
+    f M N M ra rb.
 
 
-  
 (* exercise 7 *)
 (* complete the following two lambda-terms *)
 
-Definition seven1 := (*! term *)
-(*
+Definition seven1 :=
   fun (H : forall x:Terms, P x -> Q x) =>
-  fun (I : ?) =>
-  H M I
-*)
-  .
+  fun (I : P M) =>
+  H M I.
 
-Definition seven2 := (*! term *)
-(*
+Definition seven2 :=
   fun (H : forall x y : Terms, R x y -> R y x) =>
-  fun (I : ?) =>
-  H M N I
-*)
-  .
-
-Definition seven3 := (*! term *)
-(*
-  fun (H : ?) =>
+  fun (I : R M N) =>
+  H M N I.
+
+Definition seven3 :=
+  fun (H : forall x, P x) =>
   fun (I : forall x, P x -> Q x) =>
-  I M (H M)
-*)
-  .
+  I M (H M).
 
 End pred1.
 
@@ -177,51 +186,43 @@ Section prop2.
 (* prove the following two lemma's *)
 Lemma eight1 : forall a:Prop, a -> forall b:Prop, b -> a. 
 Proof.
-(*! proof *)
-
+intros a Ha b Hb.
+exact Ha.
 Qed.
 
 Lemma eight2 : (forall a:Prop, a) -> 
   forall b:Prop, forall c:Prop, ((b->c)->b)->b.
 Proof.
-(*! proof *)
-
+intros H b c H'.
+apply H.
 Qed.
 
 
 
 (* exercise 9 *)
 (* find inhabitants of the following two types *)
-Definition nine1 : forall a:Prop, (forall b:Prop, b) -> a := (*! term *)
-  .
+Definition nine1 : forall a:Prop, (forall b:Prop, b) -> a :=
+  fun (a : Prop) (f : forall b:Prop, b) => f a.
 
 Definition nine2 : forall a:Prop, a -> (forall b:Prop, ((a -> b) -> b)) :=
-    (*! term *)
-  .
+  fun (a : Prop) (H : a) (b : Prop) (H' : a -> b) => H' H.
 
 
 
 (* exercise 10 *)
 (* complete the following lambda terms *)
 
-Definition ten1 := (*! term *)
-(*
-  fun (a:?) =>
+Definition ten1 :=
+  fun (a: Prop) =>
   fun (x: forall b:Prop, b) =>
-  x a
-*)
-  .
+  x a.
 
-Definition ten2 := (*! term *)
-(*
-  fun (a:?) =>
+Definition ten2 :=
+  fun (a:Prop) =>
   fun (x:a) =>
-  fun (b:?) =>
+  fun (b:Prop) =>
   fun (y:b) =>
-  x
-*)
-  .
- 
+  x.
 
 
 End prop2.
@@ -248,20 +249,35 @@ Fixpoint plus (n m : nat) {struct n} : nat :=
 (* prove the following three lemma's *)
 Lemma plus_n_O : forall n : nat, n = plus n 0.
 Proof.
-(*! proof *)
-
+intro n.
+induction n.
+simpl.
+reflexivity.
+simpl.
+rewrite <- IHn.
+reflexivity.
 Qed.
 
 Lemma plus_n_S : forall n m : nat, S (plus n m) = plus n (S m).
 Proof.
-(*! proof *)
-
+intros n m.
+induction n.
+simpl.
+reflexivity.
+simpl.
+rewrite IHn.
+reflexivity.
 Qed.
 
 Lemma com : forall n m : nat, plus n m = plus m n.
 Proof.
-(*! proof *)
-
+intros n m.
+induction n.
+simpl.
+apply plus_n_O.
+simpl.
+rewrite IHn.
+apply plus_n_S.
 Qed.
 
 
@@ -277,8 +293,10 @@ Inductive polybintree (X : Set) : Set :=
 (* give a definition counttree that counts the number of leafs *)
 
 Fixpoint counttree (X : Set) (b : polybintree X) {struct b} : nat :=
-    (*! term *)
-  .
+  match b with
+  | polyleaf _ _ => 0
+  | polynode _ l r => plus (counttree X l) (counttree X r)
+  end.
 
 
 
@@ -286,8 +304,11 @@ Fixpoint counttree (X : Set) (b : polybintree X) {struct b} : nat :=
 (* give a definition sum that adds the values on the leafs
    for a tree with natural numbers on the leafs *)
 
-Fixpoint sum (b:polybintree nat) {struct b} : nat := (*! term *)
-  .
+Fixpoint sum (b:polybintree nat) {struct b} : nat :=
+  match b with
+  | polyleaf _ n => n
+  | polynode _ l r => plus (sum l) (sum r)
+  end.
 
 
 (* given *)
@@ -308,8 +329,11 @@ Definition andb (b1 b2:bool) : bool := ifb b1 b2 false.
    boolean label 
    use andb for conjunction on booleans *)
 
-Fixpoint conjunction (t : polybintree bool) {struct t} : bool := (*! term *)
-  .
+Fixpoint conjunction (t : polybintree bool) {struct t} : bool :=
+  match t with
+  | polyleaf _ b => b
+  | polynode _ l r => andb (conjunction l) (conjunction r)
+  end.
 
 
 
diff --git a/pw12.v b/pw12.v
index 977f4f6..17f7501 100644
--- a/pw12.v
+++ b/pw12.v
@@ -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.