adamc@615
|
1 (* Copyright (c) 2009, Adam Chlipala
|
adamc@615
|
2 * All rights reserved.
|
adamc@615
|
3 *
|
adamc@615
|
4 * Redistribution and use in source and binary forms, with or without
|
adamc@615
|
5 * modification, are permitted provided that the following conditions are met:
|
adamc@615
|
6 *
|
adamc@615
|
7 * - Redistributions of source code must retain the above copyright notice,
|
adamc@615
|
8 * this list of conditions and the following disclaimer.
|
adamc@615
|
9 * - Redistributions in binary form must reproduce the above copyright notice,
|
adamc@615
|
10 * this list of conditions and the following disclaimer in the documentation
|
adamc@615
|
11 * and/or other materials provided with the distribution.
|
adamc@615
|
12 * - The names of contributors may not be used to endorse or promote products
|
adamc@615
|
13 * derived from this software without specific prior written permission.
|
adamc@615
|
14 *
|
adamc@615
|
15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
|
adamc@615
|
16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
|
adamc@615
|
17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
|
adamc@615
|
18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
|
adamc@615
|
19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
|
adamc@615
|
20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
|
adamc@615
|
21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
|
adamc@615
|
22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
|
adamc@615
|
23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
|
adamc@615
|
24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
|
adamc@615
|
25 * POSSIBILITY OF SUCH DAMAGE.
|
adamc@615
|
26 *)
|
adamc@615
|
27
|
adamc@618
|
28 Require Import Eqdep.
|
adamc@618
|
29
|
adamc@616
|
30 Require Import Axioms.
|
adamc@615
|
31 Require Import Syntax.
|
adamc@615
|
32
|
adamc@615
|
33 Set Implicit Arguments.
|
adamc@615
|
34
|
adamc@615
|
35
|
adamc@617
|
36 Definition row (A : Type) : Type := name -> option A.
|
adamc@615
|
37
|
adamc@617
|
38 Definition record (r : row Set) := forall n, match r n with
|
adamc@617
|
39 | None => unit
|
adamc@617
|
40 | Some T => T
|
adamc@617
|
41 end.
|
adamc@615
|
42
|
adamc@615
|
43 Fixpoint kDen (k : kind) : Type :=
|
adamc@615
|
44 match k with
|
adamc@615
|
45 | KType => Set
|
adamc@615
|
46 | KName => name
|
adamc@615
|
47 | KArrow k1 k2 => kDen k1 -> kDen k2
|
adamc@615
|
48 | KRecord k1 => row (kDen k1)
|
adamc@615
|
49 end.
|
adamc@615
|
50
|
adamc@615
|
51 Fixpoint cDen k (c : con kDen k) {struct c} : kDen k :=
|
adamc@615
|
52 match c in con _ k return kDen k with
|
adamc@615
|
53 | CVar _ x => x
|
adamc@615
|
54 | Arrow c1 c2 => cDen c1 -> cDen c2
|
adamc@615
|
55 | Poly _ c1 => forall x, cDen (c1 x)
|
adamc@615
|
56 | CAbs _ _ c1 => fun x => cDen (c1 x)
|
adamc@615
|
57 | CApp _ _ c1 c2 => (cDen c1) (cDen c2)
|
adamc@615
|
58 | Name n => n
|
adamc@615
|
59 | TRecord c1 => record (cDen c1)
|
adamc@617
|
60 | CEmpty _ => fun _ => None
|
adamc@617
|
61 | CSingle _ c1 c2 => fun n => if name_eq_dec n (cDen c1) then Some (cDen c2) else None
|
adamc@617
|
62 | CConcat _ c1 c2 => fun n => match (cDen c1) n with
|
adamc@617
|
63 | None => (cDen c2) n
|
adamc@617
|
64 | v => v
|
adamc@617
|
65 end
|
adamc@617
|
66 | CMap k1 k2 => fun f r n => match r n with
|
adamc@617
|
67 | None => None
|
adamc@617
|
68 | Some T => Some (f T)
|
adamc@617
|
69 end
|
adamc@615
|
70 | CGuarded _ _ _ _ c => cDen c
|
adamc@615
|
71 end.
|
adamc@616
|
72
|
adamc@616
|
73 Theorem subs_correct : forall k1 (c1 : con kDen k1) k2 (c2 : _ -> con kDen k2) c2',
|
adamc@616
|
74 subs c1 c2 c2'
|
adamc@616
|
75 -> cDen (c2 (cDen c1)) = cDen c2'.
|
adamc@616
|
76 induction 1; simpl; intuition; try (apply ext_eq_forallS || apply ext_eq);
|
adamc@616
|
77 repeat match goal with
|
adamc@616
|
78 | [ H : _ |- _ ] => rewrite H
|
adamc@616
|
79 end; intuition.
|
adamc@616
|
80 Qed.
|
adamc@616
|
81
|
adamc@616
|
82 Definition disjoint T (r1 r2 : row T) :=
|
adamc@617
|
83 forall n, match r1 n, r2 n with
|
adamc@617
|
84 | Some _, Some _ => False
|
adamc@617
|
85 | _, _ => True
|
adamc@617
|
86 end.
|
adamc@616
|
87 Definition dvar k (c1 c2 : con kDen (KRecord k)) :=
|
adamc@616
|
88 disjoint (cDen c1) (cDen c2).
|
adamc@616
|
89
|
adamc@616
|
90 Scheme deq_mut := Minimality for deq Sort Prop
|
adamc@616
|
91 with disj_mut := Minimality for disj Sort Prop.
|
adamc@616
|
92
|
adamc@618
|
93 Ltac deq_disj_correct scm :=
|
adamc@618
|
94 let t := repeat progress (simpl; intuition; subst) in
|
adamc@617
|
95
|
adamc@618
|
96 let rec use_disjoint' notDone E :=
|
adamc@617
|
97 match goal with
|
adamc@617
|
98 | [ H : disjoint _ _ |- _ ] =>
|
adamc@617
|
99 notDone H; generalize (H E); use_disjoint'
|
adamc@617
|
100 ltac:(fun H' =>
|
adamc@617
|
101 match H' with
|
adamc@617
|
102 | H => fail 1
|
adamc@617
|
103 | _ => notDone H'
|
adamc@617
|
104 end) E
|
adamc@617
|
105 | _ => idtac
|
adamc@618
|
106 end in
|
adamc@618
|
107 let use_disjoint := use_disjoint' ltac:(fun _ => idtac) in
|
adamc@616
|
108
|
adamc@618
|
109 apply (scm _ dvar
|
adamc@616
|
110 (fun k (c1 c2 : con kDen k) =>
|
adamc@616
|
111 cDen c1 = cDen c2)
|
adamc@616
|
112 (fun k (c1 c2 : con kDen (KRecord k)) =>
|
adamc@617
|
113 disjoint (cDen c1) (cDen c2))); t;
|
adamc@617
|
114 repeat ((unfold row; apply ext_eq)
|
adamc@617
|
115 || (match goal with
|
adamc@617
|
116 | [ H : _ |- _ ] => rewrite H
|
adamc@617
|
117 | [ H : subs _ _ _ |- _ ] => rewrite <- (subs_correct H)
|
adamc@617
|
118 end); t);
|
adamc@617
|
119 unfold disjoint; t;
|
adamc@616
|
120 repeat (match goal with
|
adamc@617
|
121 | [ |- context[match cDen ?C ?E with Some _ => _ | None => _ end] ] =>
|
adamc@617
|
122 use_disjoint E; destruct (cDen C E)
|
adamc@617
|
123 | [ |- context[if name_eq_dec ?N1 ?N2 then _ else _] ] =>
|
adamc@617
|
124 use_disjoint N1; use_disjoint N2; destruct (name_eq_dec N1 N2)
|
adamc@617
|
125 | [ _ : context[match cDen ?C ?E with Some _ => _ | None => _ end] |- _ ] =>
|
adamc@617
|
126 use_disjoint E; destruct (cDen C E)
|
adamc@617
|
127 end; t).
|
adamc@618
|
128
|
adamc@618
|
129 Theorem deq_correct : forall k (c1 c2 : con kDen k),
|
adamc@618
|
130 deq dvar c1 c2
|
adamc@618
|
131 -> cDen c1 = cDen c2.
|
adamc@618
|
132 deq_disj_correct deq_mut.
|
adamc@616
|
133 Qed.
|
adamc@618
|
134
|
adamc@618
|
135 Theorem disj_correct : forall k (c1 c2 : con kDen (KRecord k)),
|
adamc@618
|
136 disj dvar c1 c2
|
adamc@618
|
137 -> disjoint (cDen c1) (cDen c2).
|
adamc@618
|
138 deq_disj_correct disj_mut.
|
adamc@618
|
139 Qed.
|
adamc@618
|
140
|
adamc@618
|
141 Axiom cheat : forall T, T.
|
adamc@618
|
142
|
adamc@618
|
143 Definition tDen (t : con kDen KType) : Set := cDen t.
|
adamc@618
|
144
|
adamc@618
|
145 Theorem name_eq_dec_refl : forall n, name_eq_dec n n = left _ (refl_equal n).
|
adamc@618
|
146 intros; destruct (name_eq_dec n n); intuition; [
|
adamc@618
|
147 match goal with
|
adamc@618
|
148 | [ e : _ = _ |- _ ] => rewrite (UIP_refl _ _ e); reflexivity
|
adamc@618
|
149 end
|
adamc@618
|
150 | elimtype False; tauto
|
adamc@618
|
151 ].
|
adamc@618
|
152 Qed.
|
adamc@618
|
153
|
adamc@618
|
154 Theorem cut_disjoint : forall n1 v r,
|
adamc@618
|
155 disjoint (fun n => if name_eq_dec n n1 then Some v else None) r
|
adamc@618
|
156 -> unit = match r n1 with
|
adamc@618
|
157 | Some T => T
|
adamc@618
|
158 | None => unit
|
adamc@618
|
159 end.
|
adamc@618
|
160 intros;
|
adamc@618
|
161 match goal with
|
adamc@618
|
162 | [ H : disjoint _ _ |- _ ] => generalize (H n1)
|
adamc@618
|
163 end; rewrite name_eq_dec_refl;
|
adamc@618
|
164 destruct (r n1); intuition.
|
adamc@618
|
165 Qed.
|
adamc@618
|
166
|
adamc@618
|
167 Implicit Arguments cut_disjoint [v r].
|
adamc@618
|
168
|
adamc@618
|
169 Fixpoint eDen t (e : exp dvar tDen t) {struct e} : tDen t :=
|
adamc@618
|
170 match e in exp _ _ t return tDen t with
|
adamc@618
|
171 | Var _ x => x
|
adamc@618
|
172 | App _ _ e1 e2 => (eDen e1) (eDen e2)
|
adamc@618
|
173 | Abs _ _ e1 => fun x => eDen (e1 x)
|
adamc@618
|
174 | ECApp _ c _ _ e1 Hsub => match subs_correct Hsub in _ = T return T with
|
adamc@618
|
175 | refl_equal => (eDen e1) (cDen c)
|
adamc@618
|
176 end
|
adamc@618
|
177 | ECAbs _ _ e1 => fun X => eDen (e1 X)
|
adamc@618
|
178 | Cast _ _ Heq e1 => match deq_correct Heq in _ = T return T with
|
adamc@618
|
179 | refl_equal => eDen e1
|
adamc@618
|
180 end
|
adamc@618
|
181 | Empty => fun _ => tt
|
adamc@618
|
182 | Single c _ e1 => fun n => if name_eq_dec n (cDen c) as B
|
adamc@618
|
183 return (match (match (if B then _ else _) with Some _ => if B then _ else _ | None => _ end)
|
adamc@618
|
184 with Some _ => _ | None => unit end)
|
adamc@618
|
185 then eDen e1 else tt
|
adamc@618
|
186 | Proj c _ _ e1 =>
|
adamc@618
|
187 match name_eq_dec_refl (cDen c) in _ = B
|
adamc@618
|
188 return (match (match (if B then _ else _) with
|
adamc@618
|
189 | Some _ => if B then _ else _
|
adamc@618
|
190 | None => _ end)
|
adamc@618
|
191 return Set
|
adamc@618
|
192 with Some _ => _ | None => _ end) with
|
adamc@618
|
193 | refl_equal => (eDen e1) (cDen c)
|
adamc@618
|
194 end
|
adamc@618
|
195 | Cut c _ c' Hdisj e1 => fun n =>
|
adamc@618
|
196 match name_eq_dec n (cDen c) as B return (match (match (if B then Some _ else None) with Some _ => if B then _ else _ | None => (cDen c') n end)
|
adamc@618
|
197 with Some T => T | None => unit end
|
adamc@618
|
198 -> match (cDen c') n with
|
adamc@618
|
199 | None => unit
|
adamc@618
|
200 | Some T => T
|
adamc@618
|
201 end) with
|
adamc@618
|
202 | left Heq => fun _ =>
|
adamc@618
|
203 match sym_eq Heq in _ = n' return match cDen c' n' return Set with Some _ => _ | None => _ end with
|
adamc@618
|
204 | refl_equal =>
|
adamc@618
|
205 match cut_disjoint _ (disj_correct Hdisj) in _ = T return T with
|
adamc@618
|
206 | refl_equal => tt
|
adamc@618
|
207 end
|
adamc@618
|
208 end
|
adamc@618
|
209 | right _ => fun x => x
|
adamc@618
|
210 end ((eDen e1) n)
|
adamc@618
|
211
|
adamc@619
|
212 | Concat c1 c2 e1 e2 => fun n =>
|
adamc@619
|
213 match (cDen c1) n as D return match D with
|
adamc@619
|
214 | None => unit
|
adamc@619
|
215 | Some T => T
|
adamc@619
|
216 end
|
adamc@619
|
217 -> match (match D with
|
adamc@619
|
218 | None => (cDen c2) n
|
adamc@619
|
219 | v => v
|
adamc@619
|
220 end) with
|
adamc@619
|
221 | None => unit
|
adamc@619
|
222 | Some T => T
|
adamc@619
|
223 end with
|
adamc@619
|
224 | None => fun _ => (eDen e2) n
|
adamc@619
|
225 | _ => fun x => x
|
adamc@619
|
226 end ((eDen e1) n)
|
adamc@619
|
227
|
adamc@618
|
228 | _ => cheat _
|
adamc@618
|
229 end.
|