Mercurial > urweb

comparison src/coq/Syntax.v @ 635:75c7a69354d6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Coq formalization uses TDisjoint
author Adam Chlipala <adamc@hcoop.net>
date Tue, 24 Feb 2009 16:08:14 -0500
parents d828b143e147
children
comparison
equal deleted inserted replaced
634:6302b10dbe0e 635:75c7a69354d6
52 | TRecord : con (KRecord KType) -> con KType 52 | TRecord : con (KRecord KType) -> con KType
53 | CEmpty : forall k, con (KRecord k) 53 | CEmpty : forall k, con (KRecord k)
54 | CSingle : forall k, con KName -> con k -> con (KRecord k) 54 | CSingle : forall k, con KName -> con k -> con (KRecord k)
55 | CConcat : forall k, con (KRecord k) -> con (KRecord k) -> con (KRecord k) 55 | CConcat : forall k, con (KRecord k) -> con (KRecord k) -> con (KRecord k)
56 | CMap : forall k1 k2, con (KArrow (KArrow k1 k2) (KArrow (KRecord k1) (KRecord k2))) 56 | CMap : forall k1 k2, con (KArrow (KArrow k1 k2) (KArrow (KRecord k1) (KRecord k2)))
57 | CGuarded : forall k1 k2, con (KRecord k1) -> con (KRecord k1) -> con k2 -> con k2. 57 | TGuarded : forall k, con (KRecord k) -> con (KRecord k) -> con KType -> con KType.
58 58
59 Variable dvar : forall k, con (KRecord k) -> con (KRecord k) -> Type. 59 Variable dvar : forall k, con (KRecord k) -> con (KRecord k) -> Type.
60 60
61 Section subs. 61 Section subs.
62 Variable k1 : kind. 62 Variable k1 : kind.
89 -> subs (fun x => CSingle (c2 x) (c3 x)) (CSingle c2' c3') 89 -> subs (fun x => CSingle (c2 x) (c3 x)) (CSingle c2' c3')
90 | S_CConcat : forall k2 (c2 c3 : _ -> con (KRecord k2)) c2' c3', 90 | S_CConcat : forall k2 (c2 c3 : _ -> con (KRecord k2)) c2' c3',
91 subs c2 c2' 91 subs c2 c2'
92 -> subs c3 c3' 92 -> subs c3 c3'
93 -> subs (fun x => CConcat (c2 x) (c3 x)) (CConcat c2' c3') 93 -> subs (fun x => CConcat (c2 x) (c3 x)) (CConcat c2' c3')
94 | S_CGuarded : forall k2 k3 (c2 c3 : _ -> con (KRecord k2)) (c4 : _ -> con k3) c2' c3' c4', 94 | S_TGuarded : forall k2 (c2 c3 : _ -> con (KRecord k2)) c4 c2' c3' c4',
95 subs c2 c2' 95 subs c2 c2'
96 -> subs c3 c3' 96 -> subs c3 c3'
97 -> subs c4 c4' 97 -> subs c4 c4'
98 -> subs (fun x => CGuarded (c2 x) (c3 x) (c4 x)) (CGuarded c2' c3' c4'). 98 -> subs (fun x => TGuarded (c2 x) (c3 x) (c4 x)) (TGuarded c2' c3' c4').
99 End subs. 99 End subs.
100 100
101 Inductive disj : forall k, con (KRecord k) -> con (KRecord k) -> Prop := 101 Inductive disj : forall k, con (KRecord k) -> con (KRecord k) -> Prop :=
102 | DVar : forall k (c1 c2 : con (KRecord k)), 102 | DVar : forall k (c1 c2 : con (KRecord k)),
103 dvar c1 c2 -> disj c1 c2 103 dvar c1 c2 -> disj c1 c2
155 | Eq_Map_Cons : forall k1 k2 f c1 c2 c3, 155 | Eq_Map_Cons : forall k1 k2 f c1 c2 c3,
156 disj (CSingle c1 c2) c3 156 disj (CSingle c1 c2) c3
157 -> deq (CApp (CApp (CMap k1 k2) f) (CConcat (CSingle c1 c2) c3)) 157 -> deq (CApp (CApp (CMap k1 k2) f) (CConcat (CSingle c1 c2) c3))
158 (CConcat (CSingle c1 (CApp f c2)) (CApp (CApp (CMap k1 k2) f) c3)) 158 (CConcat (CSingle c1 (CApp f c2)) (CApp (CApp (CMap k1 k2) f) c3))
159 159
160 | Eq_Guarded_Remove : forall k1 k2 (c1 c2 : con (KRecord k1)) (c : con k2),
161 disj c1 c2
162 -> deq (CGuarded c1 c2 c) c
163 | Eq_Guarded_Cong : forall k1 k2 (c1 c2 : con (KRecord k1)) (c c' : con k2),
164 (dvar c1 c2 -> deq c c')
165 -> deq (CGuarded c1 c2 c) (CGuarded c1 c2 c')
166
167 | Eq_Map_Ident : forall k c, 160 | Eq_Map_Ident : forall k c,
168 deq (CApp (CApp (CMap k k) (CAbs (fun x => CVar x))) c) c 161 deq (CApp (CApp (CMap k k) (CAbs (fun x => CVar x))) c) c
169 | Eq_Map_Dist : forall k1 k2 f c1 c2, 162 | Eq_Map_Dist : forall k1 k2 f c1 c2,
170 deq (CApp (CApp (CMap k1 k2) f) (CConcat c1 c2)) 163 deq (CApp (CApp (CMap k1 k2) f) (CConcat c1 c2))
171 (CConcat (CApp (CApp (CMap k1 k2) f) c1) (CApp (CApp (CMap k1 k2) f) c2)) 164 (CConcat (CApp (CApp (CMap k1 k2) f) c1) (CApp (CApp (CMap k1 k2) f) c2))
186 | Empty : exp (TRecord (CEmpty _)) 179 | Empty : exp (TRecord (CEmpty _))
187 | Single : forall c t, exp t -> exp (TRecord (CConcat (CSingle c t) (CEmpty _))) 180 | Single : forall c t, exp t -> exp (TRecord (CConcat (CSingle c t) (CEmpty _)))
188 | Proj : forall c t c', exp (TRecord (CConcat (CSingle c t) c')) -> exp t 181 | Proj : forall c t c', exp (TRecord (CConcat (CSingle c t) c')) -> exp t
189 | Cut : forall c t c', disj (CSingle c t) c' -> exp (TRecord (CConcat (CSingle c t) c')) -> exp (TRecord c') 182 | Cut : forall c t c', disj (CSingle c t) c' -> exp (TRecord (CConcat (CSingle c t) c')) -> exp (TRecord c')
190 | Concat : forall c1 c2, exp (TRecord c1) -> exp (TRecord c2) -> exp (TRecord (CConcat c1 c2)) 183 | Concat : forall c1 c2, exp (TRecord c1) -> exp (TRecord c2) -> exp (TRecord (CConcat c1 c2))
191 | Guarded : forall k (c1 c2 : con (KRecord k)) c, (dvar c1 c2 -> exp c) -> exp (CGuarded c1 c2 c). 184 | Guarded : forall k (c1 c2 : con (KRecord k)) c, (dvar c1 c2 -> exp c) -> exp (TGuarded c1 c2 c)
185 | GuardedApp : forall k (c1 c2 : con (KRecord k)) t, exp (TGuarded c1 c2 t) -> disj c1 c2 -> exp t.
192 End vars. 186 End vars.