make StrongAlt a parameter rather than field in StrongCaseBranch and ProofCaseBranch

[coq-hetmet.git] / src / General.v

diff --git a/src/General.v b/src/General.v
index ffd0d29..2a1a398 100644 (file)
--- a/src/General.v
+++ b/src/General.v
@@ -52,7 +52,7 @@ Fixpoint mapOptionTree {a b:Type}(f:a->b)(t:@Tree ??a) : @Tree ??b :=
   match t with 
     | T_Leaf None     => T_Leaf None
     | T_Leaf (Some x) => T_Leaf (Some (f x))
-    | T_Branch l r => T_Branch (mapOptionTree f l) (mapOptionTree f r)
+    | T_Branch l r    => T_Branch (mapOptionTree f l) (mapOptionTree f r)
   end.
 Fixpoint mapTreeAndFlatten {a b:Type}(f:a->@Tree b)(t:@Tree a) : @Tree b :=
   match t with 
@@ -129,6 +129,14 @@ Lemma mapOptionTree_compose : forall A B C (f:A->B)(g:B->C)(l:Tree ??A),
     reflexivity.
     Qed.
 
+Lemma mapOptionTree_extensional {A}{B}(f g:A->B) : (forall a, f a = g a) -> (forall t, mapOptionTree f t = mapOptionTree g t).
+  intros.
+  induction t.
+  destruct a; auto.
+  simpl; rewrite H; auto.
+  simpl; rewrite IHt1; rewrite IHt2; auto.
+  Qed.
+
 Open Scope string_scope.
 Fixpoint treeToString {T}{TT:ToString T}(t:Tree ??T) : string :=
 match t with
@@ -223,6 +231,17 @@ Lemma mapOptionTree_comp a b c (f:a->b) (g:b->c) q : (mapOptionTree g (mapOption
     reflexivity.
   Qed.
 
+Lemma leaves_unleaves {T}(t:list T) : leaves (unleaves t) = t.
+  induction t; auto.
+  simpl.
+  rewrite IHt; auto.
+  Qed.
+
+Lemma mapleaves' {T:Type}(t:list T){Q}{f:T->Q} : unleaves (map f t) = mapOptionTree f (unleaves t).
+  induction t; simpl in *; auto.
+  rewrite IHt; auto.
+  Qed.
+
 (* handy facts: map preserves the length of a list *)
 Lemma map_on_nil : forall A B (s1:list A) (f:A->B), nil = map f s1 -> s1=nil.
   intros.
@@ -301,6 +320,16 @@ Fixpoint unleaves'' {A:Type}(l:list ??A) : Tree ??A :=
     | (a::b) => (unleaves'' b),,(T_Leaf a)
   end.
 
+Lemma mapleaves {T:Type}(t:Tree ??T){Q}{f:T->Q} : leaves (mapOptionTree f t) = map f (leaves t).
+  induction t.
+  destruct a; auto.
+  simpl.
+  rewrite IHt1.
+  rewrite IHt2.
+  rewrite map_app.
+  auto.
+  Qed.
+
 Fixpoint filter {T:Type}(l:list ??T) : list T :=
   match l with
     | nil => nil
@@ -312,6 +341,50 @@ Inductive distinct {T:Type} : list T -> Prop :=
 | distinct_nil  : distinct nil
 | distinct_cons : forall a ax, (@In _ a ax -> False) -> distinct ax -> distinct (a::ax).
 
+Lemma in_decidable {VV:Type}{eqdVV:EqDecidable VV} : forall (v:VV)(lv:list VV), sumbool (In v lv) (not (In v lv)).
+  intros.
+  induction lv.
+  right.
+  unfold not.
+  intros.
+  inversion H.
+  destruct IHlv.
+  left.
+  simpl.
+  auto.
+  set (eqd_dec v a) as dec.
+  destruct dec.
+  subst.
+  left; simpl; auto.
+  right.
+  unfold not; intros.
+  destruct H.
+  subst.
+  apply n0; auto.
+  apply n.
+  apply H.
+  Defined.
+
+Lemma distinct_decidable {VV:Type}{eqdVV:EqDecidable VV} : forall (lv:list VV), sumbool (distinct lv) (not (distinct lv)).
+  intros.
+  induction lv.
+  left; apply distinct_nil.
+  destruct IHlv.
+  set (in_decidable a lv) as dec.
+  destruct dec.
+  right; unfold not; intros.
+  inversion H.
+  subst.
+  apply H2; auto.
+  left.
+  apply distinct_cons; auto.
+  right.
+  unfold not; intros.
+  inversion H.
+  subst.
+  apply n; auto.
+  Defined.
+
 Lemma map_preserves_length {A}{B}(f:A->B)(l:list A) : (length l) = (length (map f l)).
   induction l; auto.
   simpl.
@@ -782,4 +855,46 @@ Notation "'failM'  x" := (uniqM (fun _ => Error x)) (at level 100).
 
 
 
+
+
+Record FreshMonad {T:Type} :=
+{ FMT       :  Type -> Type
+; FMT_Monad :> Monad FMT
+; FMT_fresh :  forall tl:list T, FMT { t:T & @In _ t tl -> False }
+}.
+Implicit Arguments FreshMonad [ ].
+Coercion FMT       : FreshMonad >-> Funclass.
+
+
+
 Variable Prelude_error : forall {A}, string -> A.   Extract Inlined Constant Prelude_error => "Prelude.error".
+
+
+
+
+Ltac eqd_dec_refl X :=
+  destruct (eqd_dec X X) as [eqd_dec1 | eqd_dec2];
+    [ clear eqd_dec1 | set (eqd_dec2 (refl_equal _)) as eqd_dec2'; inversion eqd_dec2' ].
+
+Lemma unleaves_injective : forall T (t1 t2:list T), unleaves t1 = unleaves t2 -> t1 = t2.
+  intros T.
+  induction t1; intros.
+  destruct t2.
+  auto.
+  inversion H.
+  destruct t2.
+  inversion H.
+  simpl in H.
+  inversion H.
+  set (IHt1 _ H2) as q.
+  rewrite q.
+  reflexivity.
+  Qed.
+
+Lemma fst_zip : forall T Q n (v1:vec T n)(v2:vec Q n), vec_map (@fst _ _) (vec_zip v1 v2) = v1.
+  admit.
+  Defined.
+
+Lemma snd_zip : forall T Q n (v1:vec T n)(v2:vec Q n), vec_map (@snd _ _) (vec_zip v1 v2) = v2.
+  admit.
+  Defined.