Mercurial > urweb

annotate src/coq/Semantics.v @ 617:5b358e8f9f09

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
map-only syntax and semantics
author Adam Chlipala <adamc@hcoop.net>
date Sat, 21 Feb 2009 11:23:24 -0500
parents d26d1f3acfd6
children be88d2d169f6
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@616 28 Require Import Axioms.
adamc@615 29 Require Import Syntax.
adamc@615 30
adamc@615 31 Set Implicit Arguments.
adamc@615 32
adamc@615 33
adamc@617 34 Definition row (A : Type) : Type := name -> option A.
adamc@615 35
adamc@617 36 Definition record (r : row Set) := forall n, match r n with
adamc@617 37 | None => unit
adamc@617 38 | Some T => T
adamc@617 39 end.
adamc@615 40
adamc@615 41 Fixpoint kDen (k : kind) : Type :=
adamc@615 42 match k with
adamc@615 43 | KType => Set
adamc@615 44 | KName => name
adamc@615 45 | KArrow k1 k2 => kDen k1 -> kDen k2
adamc@615 46 | KRecord k1 => row (kDen k1)
adamc@615 47 end.
adamc@615 48
adamc@615 49 Fixpoint cDen k (c : con kDen k) {struct c} : kDen k :=
adamc@615 50 match c in con _ k return kDen k with
adamc@615 51 | CVar _ x => x
adamc@615 52 | Arrow c1 c2 => cDen c1 -> cDen c2
adamc@615 53 | Poly _ c1 => forall x, cDen (c1 x)
adamc@615 54 | CAbs _ _ c1 => fun x => cDen (c1 x)
adamc@615 55 | CApp _ _ c1 c2 => (cDen c1) (cDen c2)
adamc@615 56 | Name n => n
adamc@615 57 | TRecord c1 => record (cDen c1)
adamc@617 58 | CEmpty _ => fun _ => None
adamc@617 59 | CSingle _ c1 c2 => fun n => if name_eq_dec n (cDen c1) then Some (cDen c2) else None
adamc@617 60 | CConcat _ c1 c2 => fun n => match (cDen c1) n with
adamc@617 61 | None => (cDen c2) n
adamc@617 62 | v => v
adamc@617 63 end
adamc@617 64 | CMap k1 k2 => fun f r n => match r n with
adamc@617 65 | None => None
adamc@617 66 | Some T => Some (f T)
adamc@617 67 end
adamc@615 68 | CGuarded _ _ _ _ c => cDen c
adamc@615 69 end.
adamc@616 70
adamc@616 71 Theorem subs_correct : forall k1 (c1 : con kDen k1) k2 (c2 : _ -> con kDen k2) c2',
adamc@616 72 subs c1 c2 c2'
adamc@616 73 -> cDen (c2 (cDen c1)) = cDen c2'.
adamc@616 74 induction 1; simpl; intuition; try (apply ext_eq_forallS || apply ext_eq);
adamc@616 75 repeat match goal with
adamc@616 76 | [ H : _ |- _ ] => rewrite H
adamc@616 77 end; intuition.
adamc@616 78 Qed.
adamc@616 79
adamc@616 80 Definition disjoint T (r1 r2 : row T) :=
adamc@617 81 forall n, match r1 n, r2 n with
adamc@617 82 | Some _, Some _ => False
adamc@617 83 | _, _ => True
adamc@617 84 end.
adamc@616 85 Definition dvar k (c1 c2 : con kDen (KRecord k)) :=
adamc@616 86 disjoint (cDen c1) (cDen c2).
adamc@616 87
adamc@616 88 Scheme deq_mut := Minimality for deq Sort Prop
adamc@616 89 with disj_mut := Minimality for disj Sort Prop.
adamc@616 90
adamc@616 91 Theorem deq_correct : forall k (c1 c2 : con kDen k),
adamc@616 92 deq dvar c1 c2
adamc@616 93 -> cDen c1 = cDen c2.
adamc@617 94 Ltac t := repeat progress (simpl; intuition; subst).
adamc@617 95
adamc@617 96 Ltac 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@617 106 end.
adamc@617 107 Ltac use_disjoint := use_disjoint' ltac:(fun _ => idtac).
adamc@616 108
adamc@616 109 apply (deq_mut (dvar := 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@616 128 Qed.