Mercurial > urweb

annotate src/coq/Semantics.v @ 1344:660a2715e2bd

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Clarify that you aren't supposed to be able to create new XML tags
author Adam Chlipala <adam@chlipala.net>
date Thu, 16 Dec 2010 10:23:37 -0500
parents 75c7a69354d6
children 705cb41ac7d0
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@635 51 Definition disjoint T (r1 r2 : row T) :=
adamc@635 52 forall n, match r1 n, r2 n with
adamc@635 53 | Some _, Some _ => False
adamc@635 54 | _, _ => True
adamc@635 55 end.
adamc@620 56
adamc@615 57 Fixpoint cDen k (c : con kDen k) {struct c} : kDen k :=
adamc@615 58 match c in con _ k return kDen k with
adamc@615 59 | CVar _ x => x
adamc@615 60 | Arrow c1 c2 => cDen c1 -> cDen c2
adamc@615 61 | Poly _ c1 => forall x, cDen (c1 x)
adamc@615 62 | CAbs _ _ c1 => fun x => cDen (c1 x)
adamc@615 63 | CApp _ _ c1 c2 => (cDen c1) (cDen c2)
adamc@615 64 | Name n => n
adamc@615 65 | TRecord c1 => record (cDen c1)
adamc@617 66 | CEmpty _ => fun _ => None
adamc@617 67 | CSingle _ c1 c2 => fun n => if name_eq_dec n (cDen c1) then Some (cDen c2) else None
adamc@617 68 | CConcat _ c1 c2 => fun n => match (cDen c1) n with
adamc@617 69 | None => (cDen c2) n
adamc@617 70 | v => v
adamc@617 71 end
adamc@617 72 | CMap k1 k2 => fun f r n => match r n with
adamc@617 73 | None => None
adamc@617 74 | Some T => Some (f T)
adamc@617 75 end
adamc@635 76 | TGuarded _ c1 c2 t => disjoint (cDen c1) (cDen c2) -> cDen t
adamc@615 77 end.
adamc@616 78
adamc@616 79 Theorem subs_correct : forall k1 (c1 : con kDen k1) k2 (c2 : _ -> con kDen k2) c2',
adamc@616 80 subs c1 c2 c2'
adamc@616 81 -> cDen (c2 (cDen c1)) = cDen c2'.
adamc@616 82 induction 1; simpl; intuition; try (apply ext_eq_forallS || apply ext_eq);
adamc@616 83 repeat match goal with
adamc@616 84 | [ H : _ |- _ ] => rewrite H
adamc@616 85 end; intuition.
adamc@616 86 Qed.
adamc@616 87
adamc@616 88 Definition dvar k (c1 c2 : con kDen (KRecord k)) :=
adamc@616 89 disjoint (cDen c1) (cDen c2).
adamc@616 90
adamc@616 91 Scheme deq_mut := Minimality for deq Sort Prop
adamc@616 92 with disj_mut := Minimality for disj Sort Prop.
adamc@616 93
adamc@618 94 Ltac deq_disj_correct scm :=
adamc@635 95 let t := repeat progress (simpl; intuition; subst) in
adamc@617 96
adamc@618 97 let rec use_disjoint' notDone E :=
adamc@617 98 match goal with
adamc@617 99 | [ H : disjoint _ _ |- _ ] =>
adamc@617 100 notDone H; generalize (H E); use_disjoint'
adamc@617 101 ltac:(fun H' =>
adamc@617 102 match H' with
adamc@617 103 | H => fail 1
adamc@617 104 | _ => notDone H'
adamc@617 105 end) E
adamc@617 106 | _ => idtac
adamc@618 107 end in
adamc@618 108 let use_disjoint := use_disjoint' ltac:(fun _ => idtac) in
adamc@616 109
adamc@618 110 apply (scm _ dvar
adamc@616 111 (fun k (c1 c2 : con kDen k) =>
adamc@616 112 cDen c1 = cDen c2)
adamc@616 113 (fun k (c1 c2 : con kDen (KRecord k)) =>
adamc@617 114 disjoint (cDen c1) (cDen c2))); t;
adamc@617 115 repeat ((unfold row; apply ext_eq)
adamc@617 116 || (match goal with
adamc@620 117 | [ H : _ |- _ ] => rewrite H; []
adamc@617 118 | [ H : subs _ _ _ |- _ ] => rewrite <- (subs_correct H)
adamc@617 119 end); t);
adamc@617 120 unfold disjoint; t;
adamc@616 121 repeat (match goal with
adamc@617 122 | [ |- context[match cDen ?C ?E with Some _ => _ | None => _ end] ] =>
adamc@617 123 use_disjoint E; destruct (cDen C E)
adamc@617 124 | [ |- context[if name_eq_dec ?N1 ?N2 then _ else _] ] =>
adamc@617 125 use_disjoint N1; use_disjoint N2; destruct (name_eq_dec N1 N2)
adamc@617 126 | [ _ : context[match cDen ?C ?E with Some _ => _ | None => _ end] |- _ ] =>
adamc@617 127 use_disjoint E; destruct (cDen C E)
adamc@620 128 | [ |- context[if ?E then _ else _] ] => destruct E
adamc@617 129 end; t).
adamc@618 130
adamc@620 131 Hint Unfold dvar.
adamc@620 132
adamc@618 133 Theorem deq_correct : forall k (c1 c2 : con kDen k),
adamc@618 134 deq dvar c1 c2
adamc@618 135 -> cDen c1 = cDen c2.
adamc@618 136 deq_disj_correct deq_mut.
adamc@616 137 Qed.
adamc@618 138
adamc@618 139 Theorem disj_correct : forall k (c1 c2 : con kDen (KRecord k)),
adamc@618 140 disj dvar c1 c2
adamc@618 141 -> disjoint (cDen c1) (cDen c2).
adamc@618 142 deq_disj_correct disj_mut.
adamc@618 143 Qed.
adamc@618 144
adamc@618 145 Definition tDen (t : con kDen KType) : Set := cDen t.
adamc@618 146
adamc@618 147 Theorem name_eq_dec_refl : forall n, name_eq_dec n n = left _ (refl_equal n).
adamc@618 148 intros; destruct (name_eq_dec n n); intuition; [
adamc@618 149 match goal with
adamc@618 150 | [ e : _ = _ |- _ ] => rewrite (UIP_refl _ _ e); reflexivity
adamc@618 151 end
adamc@618 152 | elimtype False; tauto
adamc@618 153 ].
adamc@618 154 Qed.
adamc@618 155
adamc@618 156 Theorem cut_disjoint : forall n1 v r,
adamc@618 157 disjoint (fun n => if name_eq_dec n n1 then Some v else None) r
adamc@618 158 -> unit = match r n1 with
adamc@618 159 | Some T => T
adamc@618 160 | None => unit
adamc@618 161 end.
adamc@618 162 intros;
adamc@618 163 match goal with
adamc@618 164 | [ H : disjoint _ _ |- _ ] => generalize (H n1)
adamc@618 165 end; rewrite name_eq_dec_refl;
adamc@618 166 destruct (r n1); intuition.
adamc@618 167 Qed.
adamc@618 168
adamc@618 169 Implicit Arguments cut_disjoint [v r].
adamc@618 170
adamc@618 171 Fixpoint eDen t (e : exp dvar tDen t) {struct e} : tDen t :=
adamc@618 172 match e in exp _ _ t return tDen t with
adamc@618 173 | Var _ x => x
adamc@618 174 | App _ _ e1 e2 => (eDen e1) (eDen e2)
adamc@618 175 | Abs _ _ e1 => fun x => eDen (e1 x)
adamc@618 176 | ECApp _ c _ _ e1 Hsub => match subs_correct Hsub in _ = T return T with
adamc@618 177 | refl_equal => (eDen e1) (cDen c)
adamc@618 178 end
adamc@618 179 | ECAbs _ _ e1 => fun X => eDen (e1 X)
adamc@618 180 | Cast _ _ Heq e1 => match deq_correct Heq in _ = T return T with
adamc@618 181 | refl_equal => eDen e1
adamc@618 182 end
adamc@618 183 | Empty => fun _ => tt
adamc@618 184 | Single c _ e1 => fun n => if name_eq_dec n (cDen c) as B
adamc@618 185 return (match (match (if B then _ else _) with Some _ => if B then _ else _ | None => _ end)
adamc@618 186 with Some _ => _ | None => unit end)
adamc@618 187 then eDen e1 else tt
adamc@618 188 | Proj c _ _ e1 =>
adamc@618 189 match name_eq_dec_refl (cDen c) in _ = B
adamc@618 190 return (match (match (if B then _ else _) with
adamc@618 191 | Some _ => if B then _ else _
adamc@618 192 | None => _ end)
adamc@618 193 return Set
adamc@618 194 with Some _ => _ | None => _ end) with
adamc@618 195 | refl_equal => (eDen e1) (cDen c)
adamc@618 196 end
adamc@618 197 | Cut c _ c' Hdisj e1 => fun n =>
adamc@618 198 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 199 with Some T => T | None => unit end
adamc@618 200 -> match (cDen c') n with
adamc@618 201 | None => unit
adamc@618 202 | Some T => T
adamc@618 203 end) with
adamc@618 204 | left Heq => fun _ =>
adamc@618 205 match sym_eq Heq in _ = n' return match cDen c' n' return Set with Some _ => _ | None => _ end with
adamc@618 206 | refl_equal =>
adamc@618 207 match cut_disjoint _ (disj_correct Hdisj) in _ = T return T with
adamc@618 208 | refl_equal => tt
adamc@618 209 end
adamc@618 210 end
adamc@618 211 | right _ => fun x => x
adamc@618 212 end ((eDen e1) n)
adamc@618 213
adamc@619 214 | Concat c1 c2 e1 e2 => fun n =>
adamc@619 215 match (cDen c1) n as D return match D with
adamc@619 216 | None => unit
adamc@619 217 | Some T => T
adamc@619 218 end
adamc@619 219 -> match (match D with
adamc@619 220 | None => (cDen c2) n
adamc@619 221 | v => v
adamc@619 222 end) with
adamc@619 223 | None => unit
adamc@619 224 | Some T => T
adamc@619 225 end with
adamc@619 226 | None => fun _ => (eDen e2) n
adamc@619 227 | _ => fun x => x
adamc@619 228 end ((eDen e1) n)
adamc@619 229
adamc@635 230 | Guarded _ _ _ _ e1 => fun pf => eDen (e1 pf)
adamc@635 231 | GuardedApp _ _ _ _ e1 Hdisj => (eDen e1) (disj_correct Hdisj)
adamc@618 232 end.