summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-02-24 16:08:14 -0500
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-02-24 16:08:14 -0500
commit0d05a92e260650352ad72af1af3b1218d5102822 (patch)
treec6814ba9a48630106013bdd778370dea14587bed /src
parentd4452116d68b41b3c829d830f3fa9f2a275e36ec (diff)
Coq formalization uses TDisjoint
Diffstat (limited to 'src')
-rw-r--r--src/coq/Name.v46
-rw-r--r--src/coq/Semantics.v84
-rw-r--r--src/coq/Syntax.v16
3 files changed, 17 insertions, 129 deletions
diff --git a/src/coq/Name.v b/src/coq/Name.v
index bc6df1c1..6dedae6a 100644
--- a/src/coq/Name.v
+++ b/src/coq/Name.v
@@ -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 --git a/src/coq/Semantics.v b/src/coq/Semantics.v
index 2a12df72..39fb534a 100644
--- a/src/coq/Semantics.v
+++ b/src/coq/Semantics.v
@@ -48,13 +48,11 @@ Fixpoint kDen (k : kind) : Type :=
| 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 @@ Fixpoint cDen k (c : con kDen k) {struct c} : kDen k :=
| 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 @@ Theorem subs_correct : forall k1 (c1 : con kDen k1) k2 (c2 : _ -> con kDen k2) c
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 @@ Ltac deq_disj_correct scm :=
| [ |- 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 @@ Qed.
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 @@ Fixpoint eDen t (e : exp dvar tDen t) {struct e} : tDen t :=
| _ => 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 --git a/src/coq/Syntax.v b/src/coq/Syntax.v
index 2378037e..03f8d82e 100644
--- a/src/coq/Syntax.v
+++ b/src/coq/Syntax.v
@@ -54,7 +54,7 @@ Section vars.
| 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 @@ Section vars.
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 @@ Section vars.
-> 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 @@ Section vars.
| 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.