Mercurial > urweb

annotate src/coq/Semantics.v @ 620:d828b143e147

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Finish semantics for Featherweight Ur
author Adam Chlipala <adamc@hcoop.net>
date Sat, 21 Feb 2009 14:10:06 -0500
parents f38e009009bb
children 75c7a69354d6
rev   line source
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@620 51 Fixpoint kDefault (k : kind) : kDen k :=
adamc@620 52 match k return kDen k with
adamc@620 53 | KType => unit
adamc@620 54 | KName => defaultName
adamc@620 55 | KArrow _ k2 => fun _ => kDefault k2
adamc@620 56 | KRecord _ => fun _ => None
adamc@620 57 end.
adamc@620 58
adamc@615 59 Fixpoint cDen k (c : con kDen k) {struct c} : kDen k :=
adamc@615 60 match c in con _ k return kDen k with
adamc@615 61 | CVar _ x => x
adamc@615 62 | Arrow c1 c2 => cDen c1 -> cDen c2
adamc@615 63 | Poly _ c1 => forall x, cDen (c1 x)
adamc@615 64 | CAbs _ _ c1 => fun x => cDen (c1 x)
adamc@615 65 | CApp _ _ c1 c2 => (cDen c1) (cDen c2)
adamc@615 66 | Name n => n
adamc@615 67 | TRecord c1 => record (cDen c1)
adamc@617 68 | CEmpty _ => fun _ => None
adamc@617 69 | CSingle _ c1 c2 => fun n => if name_eq_dec n (cDen c1) then Some (cDen c2) else None
adamc@617 70 | CConcat _ c1 c2 => fun n => match (cDen c1) n with
adamc@617 71 | None => (cDen c2) n
adamc@617 72 | v => v
adamc@617 73 end
adamc@617 74 | CMap k1 k2 => fun f r n => match r n with
adamc@617 75 | None => None
adamc@617 76 | Some T => Some (f T)
adamc@617 77 end
adamc@620 78 | CGuarded _ _ c1 c2 c =>
adamc@620 79 if badName (fun n => match (cDen c1) n, (cDen c2) n with
adamc@620 80 | Some _, Some _ => false
adamc@620 81 | _, _ => true
adamc@620 82 end)
adamc@620 83 then kDefault _
adamc@620 84 else cDen c
adamc@615 85 end.
adamc@616 86
adamc@616 87 Theorem subs_correct : forall k1 (c1 : con kDen k1) k2 (c2 : _ -> con kDen k2) c2',
adamc@616 88 subs c1 c2 c2'
adamc@616 89 -> cDen (c2 (cDen c1)) = cDen c2'.
adamc@616 90 induction 1; simpl; intuition; try (apply ext_eq_forallS || apply ext_eq);
adamc@616 91 repeat match goal with
adamc@616 92 | [ H : _ |- _ ] => rewrite H
adamc@616 93 end; intuition.
adamc@616 94 Qed.
adamc@616 95
adamc@616 96 Definition disjoint T (r1 r2 : row T) :=
adamc@617 97 forall n, match r1 n, r2 n with
adamc@617 98 | Some _, Some _ => False
adamc@617 99 | _, _ => True
adamc@617 100 end.
adamc@616 101 Definition dvar k (c1 c2 : con kDen (KRecord k)) :=
adamc@616 102 disjoint (cDen c1) (cDen c2).
adamc@616 103
adamc@620 104 Theorem known_badName : forall T (r1 r2 : row T) T' (v1 v2 : T'),
adamc@620 105 disjoint r1 r2
adamc@620 106 -> (if badName (fun n => match r1 n, r2 n with
adamc@620 107 | Some _, Some _ => false
adamc@620 108 | _, _ => true
adamc@620 109 end)
adamc@620 110 then v1
adamc@620 111 else v2) = v2.
adamc@620 112 intros; match goal with
adamc@620 113 | [ |- context[if ?E then _ else _] ] => destruct E
adamc@620 114 end; firstorder;
adamc@620 115 match goal with
adamc@620 116 | [ H : disjoint _ _, x : name |- _ ] =>
adamc@620 117 generalize (H x);
adamc@620 118 repeat match goal with
adamc@620 119 | [ |- context[match ?E with None => _ | Some _ => _ end] ] => destruct E
adamc@620 120 end; tauto || congruence
adamc@620 121 end.
adamc@620 122 Qed.
adamc@620 123
adamc@620 124 Hint Rewrite known_badName using solve [ auto ] : Semantics.
adamc@620 125
adamc@616 126 Scheme deq_mut := Minimality for deq Sort Prop
adamc@616 127 with disj_mut := Minimality for disj Sort Prop.
adamc@616 128
adamc@618 129 Ltac deq_disj_correct scm :=
adamc@620 130 let t := repeat progress (simpl; intuition; subst; autorewrite with Semantics) in
adamc@617 131
adamc@618 132 let rec use_disjoint' notDone E :=
adamc@617 133 match goal with
adamc@617 134 | [ H : disjoint _ _ |- _ ] =>
adamc@617 135 notDone H; generalize (H E); use_disjoint'
adamc@617 136 ltac:(fun H' =>
adamc@617 137 match H' with
adamc@617 138 | H => fail 1
adamc@617 139 | _ => notDone H'
adamc@617 140 end) E
adamc@617 141 | _ => idtac
adamc@618 142 end in
adamc@618 143 let use_disjoint := use_disjoint' ltac:(fun _ => idtac) in
adamc@616 144
adamc@618 145 apply (scm _ dvar
adamc@616 146 (fun k (c1 c2 : con kDen k) =>
adamc@616 147 cDen c1 = cDen c2)
adamc@616 148 (fun k (c1 c2 : con kDen (KRecord k)) =>
adamc@617 149 disjoint (cDen c1) (cDen c2))); t;
adamc@617 150 repeat ((unfold row; apply ext_eq)
adamc@617 151 || (match goal with
adamc@620 152 | [ H : _ |- _ ] => rewrite H; []
adamc@617 153 | [ H : subs _ _ _ |- _ ] => rewrite <- (subs_correct H)
adamc@617 154 end); t);
adamc@617 155 unfold disjoint; t;
adamc@616 156 repeat (match goal with
adamc@617 157 | [ |- context[match cDen ?C ?E with Some _ => _ | None => _ end] ] =>
adamc@617 158 use_disjoint E; destruct (cDen C E)
adamc@617 159 | [ |- context[if name_eq_dec ?N1 ?N2 then _ else _] ] =>
adamc@617 160 use_disjoint N1; use_disjoint N2; destruct (name_eq_dec N1 N2)
adamc@617 161 | [ _ : context[match cDen ?C ?E with Some _ => _ | None => _ end] |- _ ] =>
adamc@617 162 use_disjoint E; destruct (cDen C E)
adamc@620 163 | [ |- context[if ?E then _ else _] ] => destruct E
adamc@617 164 end; t).
adamc@618 165
adamc@620 166 Lemma bool_disjoint : forall T (r1 r2 : row T),
adamc@620 167 (forall nm : name,
adamc@620 168 match r1 nm with
adamc@620 169 | Some _ => match r2 nm with
adamc@620 170 | Some _ => false
adamc@620 171 | None => true
adamc@620 172 end
adamc@620 173 | None => true
adamc@620 174 end = true)
adamc@620 175 -> disjoint r1 r2.
adamc@620 176 intros; intro;
adamc@620 177 match goal with
adamc@620 178 | [ H : _, n : name |- _ ] => generalize (H n)
adamc@620 179 end;
adamc@620 180 repeat match goal with
adamc@620 181 | [ |- context[match ?E with Some _ => _ | None => _ end] ] => destruct E
adamc@620 182 end; tauto || discriminate.
adamc@620 183 Qed.
adamc@620 184
adamc@620 185 Implicit Arguments bool_disjoint [T r1 r2].
adamc@620 186
adamc@620 187 Hint Resolve bool_disjoint.
adamc@620 188 Hint Unfold dvar.
adamc@620 189
adamc@618 190 Theorem deq_correct : forall k (c1 c2 : con kDen k),
adamc@618 191 deq dvar c1 c2
adamc@618 192 -> cDen c1 = cDen c2.
adamc@618 193 deq_disj_correct deq_mut.
adamc@616 194 Qed.
adamc@618 195
adamc@618 196 Theorem disj_correct : forall k (c1 c2 : con kDen (KRecord k)),
adamc@618 197 disj dvar c1 c2
adamc@618 198 -> disjoint (cDen c1) (cDen c2).
adamc@618 199 deq_disj_correct disj_mut.
adamc@618 200 Qed.
adamc@618 201
adamc@618 202 Definition tDen (t : con kDen KType) : Set := cDen t.
adamc@618 203
adamc@618 204 Theorem name_eq_dec_refl : forall n, name_eq_dec n n = left _ (refl_equal n).
adamc@618 205 intros; destruct (name_eq_dec n n); intuition; [
adamc@618 206 match goal with
adamc@618 207 | [ e : _ = _ |- _ ] => rewrite (UIP_refl _ _ e); reflexivity
adamc@618 208 end
adamc@618 209 | elimtype False; tauto
adamc@618 210 ].
adamc@618 211 Qed.
adamc@618 212
adamc@618 213 Theorem cut_disjoint : forall n1 v r,
adamc@618 214 disjoint (fun n => if name_eq_dec n n1 then Some v else None) r
adamc@618 215 -> unit = match r n1 with
adamc@618 216 | Some T => T
adamc@618 217 | None => unit
adamc@618 218 end.
adamc@618 219 intros;
adamc@618 220 match goal with
adamc@618 221 | [ H : disjoint _ _ |- _ ] => generalize (H n1)
adamc@618 222 end; rewrite name_eq_dec_refl;
adamc@618 223 destruct (r n1); intuition.
adamc@618 224 Qed.
adamc@618 225
adamc@618 226 Implicit Arguments cut_disjoint [v r].
adamc@618 227
adamc@620 228 Set Printing All.
adamc@620 229
adamc@618 230 Fixpoint eDen t (e : exp dvar tDen t) {struct e} : tDen t :=
adamc@618 231 match e in exp _ _ t return tDen t with
adamc@618 232 | Var _ x => x
adamc@618 233 | App _ _ e1 e2 => (eDen e1) (eDen e2)
adamc@618 234 | Abs _ _ e1 => fun x => eDen (e1 x)
adamc@618 235 | ECApp _ c _ _ e1 Hsub => match subs_correct Hsub in _ = T return T with
adamc@618 236 | refl_equal => (eDen e1) (cDen c)
adamc@618 237 end
adamc@618 238 | ECAbs _ _ e1 => fun X => eDen (e1 X)
adamc@618 239 | Cast _ _ Heq e1 => match deq_correct Heq in _ = T return T with
adamc@618 240 | refl_equal => eDen e1
adamc@618 241 end
adamc@618 242 | Empty => fun _ => tt
adamc@618 243 | Single c _ e1 => fun n => if name_eq_dec n (cDen c) as B
adamc@618 244 return (match (match (if B then _ else _) with Some _ => if B then _ else _ | None => _ end)
adamc@618 245 with Some _ => _ | None => unit end)
adamc@618 246 then eDen e1 else tt
adamc@618 247 | Proj c _ _ e1 =>
adamc@618 248 match name_eq_dec_refl (cDen c) in _ = B
adamc@618 249 return (match (match (if B then _ else _) with
adamc@618 250 | Some _ => if B then _ else _
adamc@618 251 | None => _ end)
adamc@618 252 return Set
adamc@618 253 with Some _ => _ | None => _ end) with
adamc@618 254 | refl_equal => (eDen e1) (cDen c)
adamc@618 255 end
adamc@618 256 | Cut c _ c' Hdisj e1 => fun n =>
adamc@618 257 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 258 with Some T => T | None => unit end
adamc@618 259 -> match (cDen c') n with
adamc@618 260 | None => unit
adamc@618 261 | Some T => T
adamc@618 262 end) with
adamc@618 263 | left Heq => fun _ =>
adamc@618 264 match sym_eq Heq in _ = n' return match cDen c' n' return Set with Some _ => _ | None => _ end with
adamc@618 265 | refl_equal =>
adamc@618 266 match cut_disjoint _ (disj_correct Hdisj) in _ = T return T with
adamc@618 267 | refl_equal => tt
adamc@618 268 end
adamc@618 269 end
adamc@618 270 | right _ => fun x => x
adamc@618 271 end ((eDen e1) n)
adamc@618 272
adamc@619 273 | Concat c1 c2 e1 e2 => fun n =>
adamc@619 274 match (cDen c1) n as D return match D with
adamc@619 275 | None => unit
adamc@619 276 | Some T => T
adamc@619 277 end
adamc@619 278 -> match (match D with
adamc@619 279 | None => (cDen c2) n
adamc@619 280 | v => v
adamc@619 281 end) with
adamc@619 282 | None => unit
adamc@619 283 | Some T => T
adamc@619 284 end with
adamc@619 285 | None => fun _ => (eDen e2) n
adamc@619 286 | _ => fun x => x
adamc@619 287 end ((eDen e1) n)
adamc@619 288
adamc@620 289 | Guarded _ c1 c2 _ e1 =>
adamc@620 290 match badName (fun n => match (cDen c1) n, (cDen c2) n with
adamc@620 291 | Some _, Some _ => false
adamc@620 292 | _, _ => true
adamc@620 293 end)
adamc@620 294 as BN return (if BN return Set then _ else _) with
adamc@620 295 | inleft _ => tt
adamc@620 296 | inright pf => eDen (e1 (bool_disjoint pf))
adamc@620 297 end
adamc@618 298 end.