Switching to hlist_aux in abstract to define n-dimensional space; alm…

…ost done but for a few wrinkles in hlist_aux.v

darcs-hash:20100307132516-20b81-8d469bf46a8bb0649a45db9d0b24e68587043ee1.gz

abstract.v

@@ -74,7 +74,7 @@ Section contents.
     Next Obligation.
       split; crunch.
     Qed.
-  
+
     Definition prod_space: Space := Build_Space _ _
       (NoDup_ExhaustivePairList (NoDup_regions ap) (NoDup_regions ap'))
       in_region_mor regions_cover_prod.
@@ -120,14 +120,13 @@ Section contents.
 
     Obligation Tactic := program_simpl; auto with typeclass_instances.
 
+    Hint Resolve NoDup_regions.
+
     Program Definition hyper_space : Space := @Build_Space (Regions aps) _ _ _ 
       (@in_region_aux aps) in_region_aux_morph (@regions_cover_aux aps).
     Next Obligation.
-    Admitted.
-    Next Obligation.
-    Admitted.
-    Next Obligation.
-    Admitted.
+      set (w := NoDup_ExhaustiveHList). simpl in w. apply w. auto.
+    Qed.
 
   End hyper_space.
 

hlist.v

@@ -195,23 +195,6 @@ Section HList_prods.
     induction all_x; crunch.
   Qed.
 
-  Ltac NoDup_simpl :=
-    repeat
-      match goal with
-      | |- NoDup (_ ++ _) => apply NoDup_app
-      | |- NoDup (map _ _) => apply NoDup_map
-      | H : NoDup (_::_) |- _ => inversion H; clear H
-      end.
-
-  Ltac list_simpl :=
-    repeat 
-      match goal with
-      | H : In _ (?l ++ ?m) |- _ => 
-          destruct (in_app_or l m _ H); clear H
-      | H : In _ (map _ _) |- _ => 
-          destruct (proj1 (in_map_iff _ _ _) H); clear H
-      end.
-
   Lemma hlist_combine_hd a lt (x : hlist (a :: lt)) xs ys :
     In x (hlist_combine xs ys) ->
     In (hhd x) xs.

hlist_aux.v

@@ -1,4 +1,6 @@
 Require Export hybrid.tactics.
+Require Export hybrid.util.
+Require Import hybrid.list_util.
 Require Export Coq.Lists.List.
 Require Export Coq.Program.Program.
 
@@ -26,11 +28,15 @@ Section hlists_def.
 
 End hlists_def.
 
+Notation "'hnil'" := (HNil (H:=refl_equal _)).
 Notation "x ::: xs" := (HCons (H:=@nil_cons _ _ _) x xs) (at level 60).
 
 Section hlists_funs.
 
+(* FIXME, use context when switching to 8.3
   Context `{B : A -> Type, l : list A, a : A}.
+*)
+  Variable (A : Type) (B : A -> Type) (l : list A) (a : A).
 
   Program Definition hhd (hl : hlist (a::l)) : B a :=
     match hl with
@@ -44,4 +50,170 @@ Section hlists_funs.
     | HCons _ x xs => xs
     end.
 
+  (** [hsingleton x] is a [HList] with only one element [x] *)
+  Definition hsingleton (t : A) (x : B t) : hlist [t] := x:::hnil.
+
+  Variable f : forall x, B x.
+
+  (** [hbuild [t_1; ... t_n] = [f t_1; ... f t_n]] *)
+  Fixpoint hbuild (lt : list A) : hlist lt :=
+    match lt with
+    | nil => hnil
+    | x::lt' => f x ::: hbuild lt'
+    end.
+
 End hlists_funs.
+
+Ltac hlist_simpl :=
+  repeat 
+    match goal with
+    | hl : hlist [] |- _ => dep_destruct hl
+    | hl : hlist (_::_) |- _ => dep_destruct hl
+    | H : _:::_ = _:::_ |- _ => inversion H; clear H
+    end.
+
+(** Decidability of Leibniz equality on [hlist]s (given deecidable 
+    equality on all types of its elements). *)
+Section hlist_eqdec.
+
+  Context `{B : A -> Type, lt : list A}.
+  Variable EltsEqDec : forall x, In x lt -> EqDec (B x) eq.
+
+  Lemma hlist_eq_fst_eq a lt (x y : B a) (xs ys : hlist lt) :
+    x:::xs === y:::ys ->
+    x === y.
+  Proof.
+    inversion 1; dep_subst; intuition.
+  Qed.
+
+  Lemma hlist_eq_snd_eq a lt (x y : B a) (xs ys : hlist lt) :
+    x:::xs === y:::ys ->
+    xs === ys.
+  Proof.
+    inversion 1; dep_subst; intuition.
+  Qed.
+
+  Global Hint Resolve hlist_eq_fst_eq hlist_eq_snd_eq.
+
+  Global Program Instance hlist_EqDec : EqDec (hlist (B:=B) lt) eq.
+  Next Obligation.
+(*
+    revert x y; induction lt; intros; hlist_simpl; crunch;
+      match goal with
+      | EQ : forall x, ?a = x \/ In x ?l -> _, x : B ?a, y : B ?a 
+          |- context [?x:::_ === ?y:::_] =>
+          let a_al0 := fresh "a_al0" in
+          assert (a_al0 : In a (a :: l)) by intuition;
+          destruct (EQ a a_al0 x y)
+      end;
+      match goal with
+      | IH : (forall x, In x ?l -> EqDec (?B x) eq) -> forall x y, {x === y} + {x =/= y} 
+          |- context [_:::?xs === _:::?ys] =>
+          let IHpre := fresh "IHpre" in
+          assert (IHpre : forall x, In x l -> EqDec (B x) eq) by intuition;
+          destruct (IH IHpre xs ys)
+      end;
+      simpl_eqs; crunch; compute; crunch.
+*)
+  Admitted.
+
+End hlist_eqdec.
+
+Section HList_prods.
+
+  Context `{B : A -> Type}.
+
+  (* [hlist_combine [x_1; ... x_n] [ys_1; ... ys_n] = 
+     [x_1::ys_1; ... x_n::ys_n; x_2::ys_1 ... x_n::ys_n]] *)
+  Fixpoint hlist_combine t (lt : list A) 
+    (xl : list (B t)) (ys : list (hlist lt)) : list (hlist (t::lt)) :=
+    match xl with
+    | [] => []
+    | x::xs => map (fun y_i => x:::y_i) ys ++ hlist_combine xs ys
+    end.
+
+  Lemma hlist_combine_In a lt (x : B a) (ys : hlist lt) all_x all_ys : 
+    In x all_x -> In ys all_ys ->
+    In (x:::ys) (hlist_combine all_x all_ys).
+  Proof.
+    induction all_x; crunch.
+  Qed.
+
+  Lemma hlist_combine_hd a lt (x : hlist (a :: lt)) xs ys :
+    In x (hlist_combine xs ys) ->
+    In (hhd x) xs.
+  Proof.
+    induction xs; repeat (hlist_simpl; crunch; list_simpl).
+  Qed.
+
+  Lemma map_In_head a lt (x : hlist (a::lt)) (el : B a) xs :
+    In x (map (fun tail => el ::: tail) xs) ->
+    hhd x = el.
+  Proof.
+    repeat (list_simpl; crunch).
+  Qed.
+
+  Hint Resolve hlist_combine_hd map_In_head.
+
+  Lemma hlist_combine_NoDup (a : A) lt all_x all_ys : 
+    NoDup all_x -> NoDup all_ys ->
+    NoDup (hlist_combine (t:=a)(lt:=lt) all_x all_ys).
+  Proof.
+    induction all_x; 
+      repeat progress
+        (crunch; hlist_simpl; NoDup_simpl;
+         try
+           match goal with
+           | H : In ?x (map (fun _ => ?elt ::: _) _) |- _ =>
+               assert (hhd x = elt) by crunch
+           end
+        ).
+  Qed.
+
+  Program Fixpoint hlist_prod_tuple (lt : list A) (l : hlist (B := fun T => list (B T)) lt) :
+    list (hlist (B:=B) lt) :=
+    match lt with
+    | [] => [hnil]
+    | t::ts => 
+        match l with
+        | HNil _ => !
+        | HCons _ x xs =>
+            let w := @hlist_prod_tuple _ xs in _
+        end
+    end.
+   (* FIXME, this is akward... get rid of the obligation *)
+  Next Obligation.
+  Proof.
+    exact (@hlist_combine t ts x (hlist_prod_tuple _ xs)).
+  Defined.
+
+End HList_prods.
+
+About hlist_prod_tuple.
+About hbuild.
+Section ExhaustiveHList.
+
+  Variable A : Type.
+  Variable B : A -> Type.
+  Variable l : list A.
+
+  Context {EL : forall x, ExhaustiveList (B x)}.
+
+  Global Program Instance ExhaustiveHList : ExhaustiveList (hlist l) :=
+    { exhaustive_list := 
+        hlist_prod_tuple (hbuild _ (fun x => @exhaustive_list _ (EL x)) l)
+    }.
+  Next Obligation.
+  Admitted.
+
+  Variable NoDup_EL : forall x, NoDup (EL x).
+
+  Hint Constructors NoDup.
+  Hint Resolve @hlist_combine_NoDup.
+
+  Lemma NoDup_ExhaustiveHList : NoDup ExhaustiveHList.
+  Proof.
+    simpl; induction l; crunch.
+  Qed.
+
+End ExhaustiveHList.

list_util.v

@@ -455,4 +455,21 @@ End List_prods.
 (*
 Eval vm_compute in list_combine [1; 2] [[3;4]; [5;6]].
 Eval vm_compute in list_prod_tuple [[1;2]; [3;4]; [5;6]].
-*)
+*)
+
+Ltac NoDup_simpl :=
+  repeat
+    match goal with
+    | |- NoDup (_ ++ _) => apply NoDup_app
+    | |- NoDup (map _ _) => apply NoDup_map
+    | H : NoDup (_::_) |- _ => inversion H; clear H
+    end.
+
+Ltac list_simpl :=
+  repeat 
+    match goal with
+    | H : In _ (?l ++ ?m) |- _ => 
+        destruct (in_app_or l m _ H); clear H
+    | H : In _ (map _ _) |- _ => 
+        destruct (proj1 (in_map_iff _ _ _) H); clear H
+    end.