Semantics for ordered rows only

3 files changed, 164 insertions, 128 deletions

diff --git a/src/coq/Axioms.v b/src/coq/Axioms.v
new file mode 100644
index 00000000..f89bc1e8
--- /dev/null
+++ b/src/coq/Axioms.v
@@ -0,0 +1,49 @@
+(* Copyright (c) 2009, Adam Chlipala
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ *
+ * - Redistributions of source code must retain the above copyright notice,
+ *   this list of conditions and the following disclaimer.
+ * - Redistributions in binary form must reproduce the above copyright notice,
+ *   this list of conditions and the following disclaimer in the documentation
+ *   and/or other materials provided with the distribution.
+ * - The names of contributors may not be used to endorse or promote products
+ *   derived from this software without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+ * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+ * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+ * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
+ * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR 
+ * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
+ * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
+ * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
+ * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
+ * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+ * POSSIBILITY OF SUCH DAMAGE.
+ *)
+
+Require Import Syntax.
+
+Set Implicit Arguments.
+
+
+Axiom ext_eq : forall dom ran (f g : forall x : dom, ran x),
+  (forall x, f x = g x)
+  -> f = g.
+
+Theorem ext_eq_forall : forall dom (f g : forall x : dom, Type),
+  (forall x, f x = g x)
+  -> (forall x, f x) = (forall x, g x).
+  intros.
+  rewrite (ext_eq _ f g H); reflexivity.
+Qed.
+
+Theorem ext_eq_forallS : forall dom (f g : forall x : dom, Set),
+  (forall x, f x = g x)
+  -> (forall x, f x) = (forall x, g x).
+  intros.
+  rewrite (ext_eq _ f g H); reflexivity.
+Qed.
diff --git a/src/coq/Semantics.v b/src/coq/Semantics.v
index c3e99b5d..a60ae102 100644
--- a/src/coq/Semantics.v
+++ b/src/coq/Semantics.v
@@ -25,33 +25,21 @@
  * POSSIBILITY OF SUCH DAMAGE.
  *)
 
-Require Import Arith List Omega TheoryList.
+Require Import Arith List TheoryList.
 
+Require Import Axioms.
 Require Import Syntax.
 
 Set Implicit Arguments.
 
 
-Section row'.
-  Variable A : Type.
+Definition row (T : Type) := list (name * T).
 
-  Inductive row' : list name -> Type :=
-  | Nil : row' nil
-  | Cons : forall n ls, A -> AllS (lt n) ls -> row' ls -> row' (n :: ls).
-End row'.
-
-Implicit Arguments Nil [A].
-
-Record row (A : Type) : Type := Row {
-  keys : list name;
-  data : row' A keys
-}.
-
-Inductive record' : forall ls, row' Set ls -> Set :=
-| RNil : record' Nil
-| RCons : forall n ls (T : Set) (pf : AllS (lt n) ls) r, T -> record' r -> record' (Cons T pf r).
-
-Definition record (r : row Set) := record' (data r).
+Fixpoint record (r : row Set) : Set :=
+  match r with
+    | nil => unit
+    | (_, T) :: r' => T * record r'
+  end%type.
 
 Fixpoint kDen (k : kind) : Type :=
   match k with
@@ -61,82 +49,10 @@ Fixpoint kDen (k : kind) : Type :=
     | KRecord k1 => row (kDen k1)
   end.
 
-Axiom cheat : forall T, T.
-
-Fixpoint cinsert (n : name) (ls : list name) {struct ls} : list name :=
-  match ls with
-    | nil => n :: nil
-    | n' :: ls' =>
-      if eq_nat_dec n n'
-        then ls
-        else if le_lt_dec n n'
-          then n :: ls
-          else n' :: cinsert n ls'
-  end.
-
-Hint Constructors AllS.
-Hint Extern 1 (_ < _) => omega.
-
-Lemma insert_front' : forall n n',
-  n <> n'
-  -> n <= n'
-  -> forall ls, AllS (lt n') ls
-    -> AllS (lt n) ls.
-  induction 3; auto.
-Qed.
-
-Lemma insert_front : forall n n',
-  n <> n'
-  -> n <= n'
-  -> forall ls, AllS (lt n') ls
-    -> AllS (lt n) (n' :: ls).
-  Hint Resolve insert_front'.
-  eauto.
-Qed.
-
-Lemma insert_continue : forall n n',
-  n <> n'
-  -> n' < n
-  -> forall ls, AllS (lt n') ls
-    -> AllS (lt n') (cinsert n ls).
-  induction 3; simpl; auto;
-    repeat (match goal with
-              | [ |- context[if ?E then _ else _] ] => destruct E
-            end; auto).
-Qed.
-
-Fixpoint insert T (n : name) (v : T) ls (r : row' T ls) {struct r} : row' T (cinsert n ls) :=
-  match r in row' _ ls return row' T (cinsert n ls) with
-    | Nil => Cons (n := n) v (allS_nil _) Nil
-    | Cons n' ls' v' pf r' =>
-      match eq_nat_dec n n' as END
-        return row' _ (if END then _ else _) with
-        | left _ => Cons (n := n') v' pf r'
-        | right pfNe =>
-          match le_lt_dec n n' as LLD
-            return row' _ (if LLD then _ else _) with
-            | left pfLe => Cons (n := n) v (insert_front pfNe pfLe pf) (Cons (n := n') v' pf r')
-            | right pfLt => Cons (n := n') v' (insert_continue pfNe pfLt pf) (insert n v r')
-          end
-      end
-  end.
-
-Fixpoint cconcat (ls1 ls2 : list name) {struct ls1} : list name :=
-  match ls1 with
-    | nil => ls2
-    | n :: ls1' => cinsert n (cconcat ls1' ls2)
-  end.
-
-Fixpoint concat T ls1 ls2 (r1 : row' T ls1) (r2 : row' T ls2) {struct r1} : row' T (cconcat ls1 ls2) :=
-  match r1 in row' _ ls1 return row' _ (cconcat ls1 _) with
-    | Nil => r2
-    | Cons n _ v _ r1' => insert n v (concat r1' r2)
-  end.
-
-Fixpoint cfold T T' (f : name -> T -> T' -> T') (i : T') ls (r : row' T ls) {struct r} : T' :=
+Fixpoint cfold T T' (f : name -> T -> T' -> T') (i : T') (r : row T) {struct r} : T' :=
   match r with
-    | Nil => i
-    | Cons n _ v _ r' => f n v (cfold f i r')
+    | nil => i
+    | (n, v) :: r' => f n v (cfold f i r')
   end.
 
 Fixpoint cDen k (c : con kDen k) {struct c} : kDen k :=
@@ -148,9 +64,107 @@ Fixpoint cDen k (c : con kDen k) {struct c} : kDen k :=
     | CApp _ _ c1 c2 => (cDen c1) (cDen c2)
     | Name n => n
     | TRecord c1 => record (cDen c1)
-    | CEmpty _ => Row Nil
-    | CSingle _ c1 c2 => Row (Cons (n := cDen c1) (cDen c2) (allS_nil _) Nil)
-    | CConcat _ c1 c2 => Row (concat (data (cDen c1)) (data (cDen c2)))
-    | CFold k1 k2 => fun f i r => cfold f i (data r)
+    | CEmpty _ => nil
+    | CSingle _ c1 c2 => (cDen c1, cDen c2) :: nil
+    | CConcat _ c1 c2 => cDen c1 ++ cDen c2
+    | CFold k1 k2 => @cfold _ _
     | CGuarded _ _ _ _ c => cDen c
   end.
+
+Theorem subs_correct : forall k1 (c1 : con kDen k1) k2 (c2 : _ -> con kDen k2) c2',
+  subs c1 c2 c2'
+  -> cDen (c2 (cDen c1)) = cDen c2'.
+  induction 1; simpl; intuition; try (apply ext_eq_forallS || apply ext_eq);
+    repeat match goal with
+             | [ H : _ |- _ ] => rewrite H
+           end; intuition.
+Qed.
+
+Definition disjoint T (r1 r2 : row T) :=
+  AllS (fun p1 => AllS (fun p2 => fst p1 <> fst p2) r2) r1.
+Definition dvar k (c1 c2 : con kDen (KRecord k)) :=
+  disjoint (cDen c1) (cDen c2).
+
+Lemma AllS_app : forall T P (ls2 : list T),
+  AllS P ls2
+  -> forall ls1, AllS P ls1
+    -> AllS P (ls1 ++ ls2).
+  induction 2; simpl; intuition.
+Qed.
+
+Lemma AllS_weaken : forall T (P P' : T -> Prop),
+  (forall x, P x -> P' x)
+  -> forall ls,
+    AllS P ls
+    -> AllS P' ls.
+  induction 2; simpl; intuition.
+Qed.
+
+Theorem disjoint_symm : forall T (r1 r2 : row T),
+  disjoint r1 r2
+  -> disjoint r2 r1.
+  Hint Constructors AllS.
+  Hint Resolve AllS_weaken.
+  
+  unfold disjoint; induction r2; simpl; intuition.
+  constructor.
+  eapply AllS_weaken; eauto.
+  intuition.
+  inversion H0; auto.
+
+  apply IHr2.
+  eapply AllS_weaken; eauto.
+  intuition.
+  inversion H0; auto.
+Qed.  
+
+Lemma map_id : forall k (r : row k),
+  cfold (fun x x0 (x1 : row _) => (x, x0) :: x1) nil r = r.
+  induction r; simpl; intuition;
+    match goal with
+      | [ H : _ |- _ ] => rewrite H
+    end; intuition.
+Qed.
+
+Lemma map_dist : forall T1 T2 (f : T1 -> T2) (r2 r1 : row T1),
+  cfold (fun x x0 (x1 : row _) => (x, f x0) :: x1) nil (r1 ++ r2)
+  = cfold (fun x x0 (x1 : row _) => (x, f x0) :: x1) nil r1
+  ++ cfold (fun x x0 (x1 : row _) => (x, f x0) :: x1) nil r2.
+  induction r1; simpl; intuition;
+    match goal with
+      | [ H : _ |- _ ] => rewrite H
+    end; intuition.
+Qed.
+
+Lemma fold_fuse : forall T1 T2 T3 (f : name -> T1 -> T2 -> T2) (i : T2) (f' : T3 -> T1) (c : row T3),
+  cfold f i (cfold (fun x x0 (x1 : row _) => (x, f' x0) :: x1) nil c)
+  = cfold (fun x x0 => f x (f' x0)) i c.
+  induction c; simpl; intuition;
+    match goal with
+      | [ H : _ |- _ ] => rewrite <- H
+    end; intuition.
+Qed.
+
+Scheme deq_mut := Minimality for deq Sort Prop
+with disj_mut := Minimality for disj Sort Prop.
+
+Theorem deq_correct : forall k (c1 c2 : con kDen k),
+  deq dvar c1 c2
+  -> cDen c1 = cDen c2.
+  Hint Resolve map_id map_dist fold_fuse AllS_app disjoint_symm.
+  Hint Extern 1 (_ = _) => unfold row; symmetry; apply app_ass.
+
+  apply (deq_mut (dvar := dvar)
+    (fun k (c1 c2 : con kDen k) =>
+      cDen c1 = cDen c2)
+    (fun k (c1 c2 : con kDen (KRecord k)) =>
+      disjoint (cDen c1) (cDen c2)));
+  simpl; intuition;
+    repeat (match goal with
+              | [ H : _ |- _ ] => rewrite H
+              | [ H : subs _ _ _ |- _ ] => rewrite <- (subs_correct H)
+            end; simpl; intuition); try congruence; unfold disjoint in *; intuition;
+    fold kDen in *; repeat match goal with
+                             | [ H : AllS _ (_ :: _) |- _ ] => inversion H; clear H; subst; simpl in *
+                           end; auto.
+Qed.
diff --git a/src/coq/Syntax.v b/src/coq/Syntax.v
index 786751d0..d73f5361 100644
--- a/src/coq/Syntax.v
+++ b/src/coq/Syntax.v
@@ -145,15 +145,14 @@ Section vars.
 
   | Eq_Concat_Empty : forall k c,
     deq (CConcat (CEmpty k) c) c
-  | Eq_Concat_Comm : forall k (c1 c2 : con (KRecord k)),
-    deq (CConcat c1 c2) (CConcat c2 c1)
   | Eq_Concat_Assoc : forall k (c1 c2 c3 : con (KRecord k)),
     deq (CConcat c1 (CConcat c2 c3)) (CConcat (CConcat c1 c2) c3)
 
   | Eq_Fold_Empty : forall k1 k2 f i,
     deq (CApp (CApp (CApp (CFold k1 k2) f) i) (CEmpty _)) i
   | Eq_Fold_Cons : forall k1 k2 f i c1 c2 c3,
-    deq (CApp (CApp (CApp (CFold k1 k2) f) i) (CConcat (CSingle c1 c2) c3))
+    disj (CSingle c1 c2) c3
+    -> deq (CApp (CApp (CApp (CFold k1 k2) f) i) (CConcat (CSingle c1 c2) c3))
     (CApp (CApp (CApp f c1) c2) (CApp (CApp (CApp (CFold k1 k2) f) i) c3))
 
   | Eq_Guarded : forall k1 k2 (c1 c2 : con (KRecord k1)) (c : con k2),
@@ -184,30 +183,4 @@ Section vars.
     (CApp (CApp (CApp (CFold k3 k2)
       (CAbs (fun x1 => CAbs (fun x2 => CApp (CApp f (CVar x1)) (CApp f' (CVar x2))))))
       i) c).
-
-  Inductive wf : forall k, con k -> Type :=
-  | HK_CVar : forall k (x : cvar k),
-    wf (CVar x)
-  | HK_Arrow : forall c1 c2,
-    wf c1 -> wf c2 -> wf (Arrow c1 c2)
-  | HK_Poly : forall k (c1 : cvar k -> _),
-    (forall x, wf (c1 x)) -> wf (Poly c1)
-  | HK_CAbs : forall k1 k2 (c1 : cvar k1 -> con k2),
-    (forall x, wf (c1 x)) -> wf (CAbs c1)
-  | HK_CApp : forall k1 k2 (c1 : con (KArrow k1 k2)) c2,
-    wf c1 -> wf c2 -> wf (CApp c1 c2)
-  | HK_Name : forall X,
-    wf (Name X)
-  | HK_TRecord : forall c,
-    wf c -> wf (TRecord c)
-  | HK_CEmpty : forall k,
-    wf (CEmpty k)
-  | HK_CSingle : forall k c1 (c2 : con k),
-    wf c1 -> wf c2 -> wf (CSingle c1 c2)
-  | HK_CConcat : forall k (c1 c2 : con (KRecord k)),
-    wf c2 -> wf c2 -> disj c1 c2 -> wf (CConcat c1 c2)
-  | HK_CFold : forall k1 k2,
-    wf (CFold k1 k2)
-  | HK_CGuarded : forall k1 k2 (c1 c2 : con (KRecord k1)) (c : con k2),
-    wf c1 -> wf c2 -> (disj c1 c2 -> wf c) -> wf (CGuarded c1 c2 c).
 End vars.