# HG changeset patch # User Adam Chlipala # Date 1235509694 18000 # Node ID 75c7a69354d6984440202f0674bc4f80d1e50fca # Parent 6302b10dbe0eceee6aa553e43c377c3ddefbc8b6 Coq formalization uses TDisjoint diff -r 6302b10dbe0e -r 75c7a69354d6 src/coq/Name.v --- a/src/coq/Name.v Tue Feb 24 15:54:05 2009 -0500 +++ b/src/coq/Name.v Tue Feb 24 16:08:14 2009 -0500 @@ -25,47 +25,7 @@ * POSSIBILITY OF SUCH DAMAGE. *) -Set Implicit Arguments. +Require Import String. - -Fixpoint name' (n : nat) : Type := - match n with - | O => Empty_set - | S n' => option (name' n') - end. - -Definition name'_eq_dec : forall n (x y : name' n), {x = y} + {x <> y}. - Hint Extern 1 (_ = _ -> False) => congruence. - - induction n; simpl; intuition; - repeat match goal with - | [ x : Empty_set |- _ ] => destruct x - | [ x : option _ |- _ ] => destruct x - end; intuition; - match goal with - | [ IH : _, n1 : name' _, n2 : name' _ |- _ ] => - destruct (IHn n1 n0); subst; intuition - end. -Qed. - -Definition badName' n (P : name' n -> bool) : - {nm : _ | P nm = false} + {forall nm, P nm = true}. - Hint Constructors sig. - Hint Extern 1 (_ = true) => - match goal with - | [ nm : option _ |- _ ] => destruct nm - end; auto. - - induction n; simpl; intuition; - match goal with - | [ IH : forall P : _ -> _,_ |- _ ] => - case_eq (P None); - destruct (IH (fun nm => P (Some nm))); firstorder eauto - end. -Qed. - -Parameter numNames : nat. -Definition name := name' (S numNames). -Definition name_eq_dec : forall (x y : name), {x = y} + {x <> y} := @name'_eq_dec _. -Definition badName : forall P : name -> bool, {nm : _ | P nm = false} + {forall nm, P nm = true} := @badName' _. -Definition defaultName : name := None. +Definition name := string. +Definition name_eq_dec : forall x y : name, {x = y} + {x <> y} := string_dec. diff -r 6302b10dbe0e -r 75c7a69354d6 src/coq/Semantics.v --- a/src/coq/Semantics.v Tue Feb 24 15:54:05 2009 -0500 +++ b/src/coq/Semantics.v Tue Feb 24 16:08:14 2009 -0500 @@ -48,13 +48,11 @@ | KRecord k1 => row (kDen k1) end. -Fixpoint kDefault (k : kind) : kDen k := - match k return kDen k with - | KType => unit - | KName => defaultName - | KArrow _ k2 => fun _ => kDefault k2 - | KRecord _ => fun _ => None - end. +Definition disjoint T (r1 r2 : row T) := + forall n, match r1 n, r2 n with + | Some _, Some _ => False + | _, _ => True + end. Fixpoint cDen k (c : con kDen k) {struct c} : kDen k := match c in con _ k return kDen k with @@ -75,13 +73,7 @@ | None => None | Some T => Some (f T) end - | CGuarded _ _ c1 c2 c => - if badName (fun n => match (cDen c1) n, (cDen c2) n with - | Some _, Some _ => false - | _, _ => true - end) - then kDefault _ - else cDen c + | TGuarded _ c1 c2 t => disjoint (cDen c1) (cDen c2) -> cDen t end. Theorem subs_correct : forall k1 (c1 : con kDen k1) k2 (c2 : _ -> con kDen k2) c2', @@ -93,41 +85,14 @@ end; intuition. Qed. -Definition disjoint T (r1 r2 : row T) := - forall n, match r1 n, r2 n with - | Some _, Some _ => False - | _, _ => True - end. Definition dvar k (c1 c2 : con kDen (KRecord k)) := disjoint (cDen c1) (cDen c2). -Theorem known_badName : forall T (r1 r2 : row T) T' (v1 v2 : T'), - disjoint r1 r2 - -> (if badName (fun n => match r1 n, r2 n with - | Some _, Some _ => false - | _, _ => true - end) - then v1 - else v2) = v2. - intros; match goal with - | [ |- context[if ?E then _ else _] ] => destruct E - end; firstorder; - match goal with - | [ H : disjoint _ _, x : name |- _ ] => - generalize (H x); - repeat match goal with - | [ |- context[match ?E with None => _ | Some _ => _ end] ] => destruct E - end; tauto || congruence - end. -Qed. - -Hint Rewrite known_badName using solve [ auto ] : Semantics. - Scheme deq_mut := Minimality for deq Sort Prop with disj_mut := Minimality for disj Sort Prop. Ltac deq_disj_correct scm := - let t := repeat progress (simpl; intuition; subst; autorewrite with Semantics) in + let t := repeat progress (simpl; intuition; subst) in let rec use_disjoint' notDone E := match goal with @@ -163,28 +128,6 @@ | [ |- context[if ?E then _ else _] ] => destruct E end; t). -Lemma bool_disjoint : forall T (r1 r2 : row T), - (forall nm : name, - match r1 nm with - | Some _ => match r2 nm with - | Some _ => false - | None => true - end - | None => true - end = true) - -> disjoint r1 r2. - intros; intro; - match goal with - | [ H : _, n : name |- _ ] => generalize (H n) - end; - repeat match goal with - | [ |- context[match ?E with Some _ => _ | None => _ end] ] => destruct E - end; tauto || discriminate. -Qed. - -Implicit Arguments bool_disjoint [T r1 r2]. - -Hint Resolve bool_disjoint. Hint Unfold dvar. Theorem deq_correct : forall k (c1 c2 : con kDen k), @@ -225,8 +168,6 @@ Implicit Arguments cut_disjoint [v r]. -Set Printing All. - Fixpoint eDen t (e : exp dvar tDen t) {struct e} : tDen t := match e in exp _ _ t return tDen t with | Var _ x => x @@ -286,13 +227,6 @@ | _ => fun x => x end ((eDen e1) n) - | Guarded _ c1 c2 _ e1 => - match badName (fun n => match (cDen c1) n, (cDen c2) n with - | Some _, Some _ => false - | _, _ => true - end) - as BN return (if BN return Set then _ else _) with - | inleft _ => tt - | inright pf => eDen (e1 (bool_disjoint pf)) - end + | Guarded _ _ _ _ e1 => fun pf => eDen (e1 pf) + | GuardedApp _ _ _ _ e1 Hdisj => (eDen e1) (disj_correct Hdisj) end. diff -r 6302b10dbe0e -r 75c7a69354d6 src/coq/Syntax.v --- a/src/coq/Syntax.v Tue Feb 24 15:54:05 2009 -0500 +++ b/src/coq/Syntax.v Tue Feb 24 16:08:14 2009 -0500 @@ -54,7 +54,7 @@ | CSingle : forall k, con KName -> con k -> con (KRecord k) | CConcat : forall k, con (KRecord k) -> con (KRecord k) -> con (KRecord k) | CMap : forall k1 k2, con (KArrow (KArrow k1 k2) (KArrow (KRecord k1) (KRecord k2))) - | CGuarded : forall k1 k2, con (KRecord k1) -> con (KRecord k1) -> con k2 -> con k2. + | TGuarded : forall k, con (KRecord k) -> con (KRecord k) -> con KType -> con KType. Variable dvar : forall k, con (KRecord k) -> con (KRecord k) -> Type. @@ -91,11 +91,11 @@ subs c2 c2' -> subs c3 c3' -> subs (fun x => CConcat (c2 x) (c3 x)) (CConcat c2' c3') - | S_CGuarded : forall k2 k3 (c2 c3 : _ -> con (KRecord k2)) (c4 : _ -> con k3) c2' c3' c4', + | S_TGuarded : forall k2 (c2 c3 : _ -> con (KRecord k2)) c4 c2' c3' c4', subs c2 c2' -> subs c3 c3' -> subs c4 c4' - -> subs (fun x => CGuarded (c2 x) (c3 x) (c4 x)) (CGuarded c2' c3' c4'). + -> subs (fun x => TGuarded (c2 x) (c3 x) (c4 x)) (TGuarded c2' c3' c4'). End subs. Inductive disj : forall k, con (KRecord k) -> con (KRecord k) -> Prop := @@ -157,13 +157,6 @@ -> deq (CApp (CApp (CMap k1 k2) f) (CConcat (CSingle c1 c2) c3)) (CConcat (CSingle c1 (CApp f c2)) (CApp (CApp (CMap k1 k2) f) c3)) - | Eq_Guarded_Remove : forall k1 k2 (c1 c2 : con (KRecord k1)) (c : con k2), - disj c1 c2 - -> deq (CGuarded c1 c2 c) c - | Eq_Guarded_Cong : forall k1 k2 (c1 c2 : con (KRecord k1)) (c c' : con k2), - (dvar c1 c2 -> deq c c') - -> deq (CGuarded c1 c2 c) (CGuarded c1 c2 c') - | Eq_Map_Ident : forall k c, deq (CApp (CApp (CMap k k) (CAbs (fun x => CVar x))) c) c | Eq_Map_Dist : forall k1 k2 f c1 c2, @@ -188,5 +181,6 @@ | Proj : forall c t c', exp (TRecord (CConcat (CSingle c t) c')) -> exp t | Cut : forall c t c', disj (CSingle c t) c' -> exp (TRecord (CConcat (CSingle c t) c')) -> exp (TRecord c') | Concat : forall c1 c2, exp (TRecord c1) -> exp (TRecord c2) -> exp (TRecord (CConcat c1 c2)) - | Guarded : forall k (c1 c2 : con (KRecord k)) c, (dvar c1 c2 -> exp c) -> exp (CGuarded c1 c2 c). + | Guarded : forall k (c1 c2 : con (KRecord k)) c, (dvar c1 c2 -> exp c) -> exp (TGuarded c1 c2 c) + | GuardedApp : forall k (c1 c2 : con (KRecord k)) t, exp (TGuarded c1 c2 t) -> disj c1 c2 -> exp t. End vars.