summaryrefslogtreecommitdiff
path: root/src/coq
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-02-18 09:32:17 -0500
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-02-18 09:32:17 -0500
commit2bfa859812bcf33fa05372d668ac363d17bc8892 (patch)
treeb871da721d32333e117c07c177c42f8b80ab4d41 /src/coq
parent9caa49973b2ea034d985bcee1c991804d2176bf5 (diff)
Semantics for ordered rows only
Diffstat (limited to 'src/coq')
-rw-r--r--src/coq/Axioms.v49
-rw-r--r--src/coq/Semantics.v212
-rw-r--r--src/coq/Syntax.v31
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.