pw10

1 files changed, 77 insertions, 37 deletions

diff --git a/pw10.v b/pw10.v
index 823c297..713e798 100644
--- a/pw10.v
+++ b/pw10.v
@@ -102,8 +102,8 @@ Eval compute in (natlength (natcons 2 (natcons 1 (natcons 0 natnil)))).
 (* length of polymorphic lists *)
 Fixpoint polylength (A:Set)(l:(polylist A)){struct l} : nat :=
   match l with
-    polynil => O
-  | polycons h t => S (polylength A t)
+    polynil _ => O
+  | polycons _ h t => S (polylength A t)
   end.
 
 (* NB: in the recursive definition,
@@ -145,19 +145,25 @@ Check polylistb_ind.
 (* test it using Eval compute on an example *)
 
 Fixpoint polyappend (X:Set) (k l : polylist X) {struct k} : (polylist X) :=
-    (*! term *)
-  .
+  match k with
+    polynil _ => l
+  | polycons _ x xs => co x (polyappend X xs l)
+  end.
 
-Eval compute in (*! term *)
-  .
+Eval compute in polyappend nat (co 1 (co 2 ni)) (co 3 (co 4 ni)).
 
 (* prove the following lemma, to be used later*)
 Lemma append_nil :
   forall X:Set, forall l: polylist X,
   polyappend X l (polynil X) = l.
 Proof.
-(*! proof *)
-
+intros X l.
+induction l.
+simpl.
+reflexivity.
+simpl.
+rewrite IHl.
+reflexivity.
 Qed.
 
 
@@ -166,19 +172,28 @@ Qed.
 Lemma append_assoc : forall X, forall k l m,
   (polyappend X (polyappend X k l) m) = (polyappend X k (polyappend X l m)).
 Proof.
-(*! proof *)
-
+intros X k l m.
+induction k.
+simpl.
+reflexivity.
+simpl.
+rewrite IHk.
+reflexivity.
 Qed.
 
-
 (* exercise 4 *)
 (* prove the following lemma *)
 Lemma length_append :
  forall X:Set, forall k l : (polylist X),
   polylength X (polyappend X k l) = plus (polylength X k) (polylength X l).
 Proof.
-(*! proof *)
-
+intros X k l.
+induction k.
+simpl.
+reflexivity.
+simpl.
+rewrite IHk.
+reflexivity.
 Qed.
 
 
@@ -187,9 +202,12 @@ Qed.
 (* test it using Eval compute on an example *)
 
 Fixpoint polyreverse (X:Set) (l : polylist X) {struct l} :(polylist X) :=
-    (*! term *)
-  .
+  match l with
+    polynil _ => ni
+  | polycons _ x xs => polyappend X (polyreverse X xs) (co x ni)
+  end.
 
+Eval compute in polyreverse nat (co 1 (co 2 (co 3 ni))).
 
 (* exercise 6 *)
 (* prove the following lemma *)
@@ -198,8 +216,15 @@ Lemma reverse_append :
   polyreverse X (polyappend X k l) =
   polyappend X (polyreverse X l) (polyreverse X k).
 Proof.
-(*! proof *)
-
+intros X k l.
+induction k.
+simpl.
+rewrite append_nil.
+reflexivity.
+simpl.
+rewrite IHk.
+rewrite append_assoc.
+reflexivity.
 Qed.
 
 
@@ -211,8 +236,21 @@ Lemma rev_cons_app :
   polyappend X (polyreverse X (polycons X x k)) l =
   polyappend X (polyreverse X k) (polycons X x l).
 Proof.
-(*! proof *)
-
+intros X k l x.
+simpl.
+(* Coq accepts, but prover does not accept:
+apply append_assoc.
+   This proves the proposition immediately.
+*)
+induction k. (* Not actually induction, but this is cleaner than elim *)
+simpl.
+reflexivity.
+simpl.
+rewrite append_assoc.
+rewrite append_assoc.
+rewrite append_assoc.
+simpl.
+reflexivity.
 Qed.
 
 
@@ -250,17 +288,21 @@ Eval compute in (natprodsecond (natpair 1 2)).
    where the first element comes from a set X
    and the second element comes from a set Y    *)
 
-Inductive prod (X Y :Set) : Set := (*! term *)
-  .
+Inductive prod (X Y :Set) : Set :=
+  | pair : X -> Y -> prod X Y.
 
 (* exercise 9 *)
 (* give definitions of the first and second projection *)
 
-Definition fst (X Y : Set) (p: prod X Y) : X := (*! term *)
-  .
+Definition fst (X Y : Set) (p: prod X Y) : X :=
+  match p with
+    pair _ _ x _ => x
+  end.
 
-Definition snd (X Y : Set) (p : prod X Y) : Y := (*! term *)
-  .
+Definition snd (X Y : Set) (p : prod X Y) : Y :=
+  match p with
+    pair _ _ _ y => y
+  end.
 
 
 (*        exercises about polymorphic trees       *)
@@ -289,8 +331,9 @@ Check (natnode 2 (natnode 1 natleaf natleaf) (natnode 3 natleaf natleaf)).
    with labels on the nodes
    you may introduce handy notation *)
 
-Inductive polybintree (X : Set) : Set := (*! term *)
-  .
+Inductive polybintree (X : Set) : Set :=
+    polyleaf : polybintree X
+  | polynode : X -> polybintree X -> polybintree X -> polybintree X.
 
 
 
@@ -299,15 +342,12 @@ Inductive polybintree (X : Set) : Set := (*! term *)
    polyflatten puts the labels of a polybintree from left to right in a polylist *)
 
 Fixpoint polyflatten (X:Set) (t:polybintree X) {struct t} : (polylist X) :=
-  (*! term *)
-(*
-match t with
-| polyleaf =>
-| polynode x l r =>
-end
-*)
-  .
+  match t with
+  | polyleaf _ => ni
+  | polynode _ x l r => polyappend X (polyflatten X l) (co x (polyflatten X r))
+  end.
 
 (* perform some tests using the trees above *)
-
-
+Eval compute in polyflatten nat (polyleaf nat).
+Eval compute in polyflatten nat (polynode nat 1 (polyleaf nat) (polyleaf nat)).
+Eval compute in polyflatten nat (polynode nat 1 (polynode nat 2 (polyleaf nat) (polyleaf nat)) (polynode nat 3 (polyleaf nat) (polyleaf nat))).
\ No newline at end of file