Mercurial > urweb

annotate src/coq/Semantics.v @ 615:3c77133afd9a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Start of Featherweight Ur semantics
author Adam Chlipala <adamc@hcoop.net>
date Tue, 17 Feb 2009 14:49:28 -0500
parents
children d26d1f3acfd6
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@615 28 Require Import Arith List Omega TheoryList.
adamc@615 29
adamc@615 30 Require Import Syntax.
adamc@615 31
adamc@615 32 Set Implicit Arguments.
adamc@615 33
adamc@615 34
adamc@615 35 Section row'.
adamc@615 36 Variable A : Type.
adamc@615 37
adamc@615 38 Inductive row' : list name -> Type :=
adamc@615 39 | Nil : row' nil
adamc@615 40 | Cons : forall n ls, A -> AllS (lt n) ls -> row' ls -> row' (n :: ls).
adamc@615 41 End row'.
adamc@615 42
adamc@615 43 Implicit Arguments Nil [A].
adamc@615 44
adamc@615 45 Record row (A : Type) : Type := Row {
adamc@615 46 keys : list name;
adamc@615 47 data : row' A keys
adamc@615 48 }.
adamc@615 49
adamc@615 50 Inductive record' : forall ls, row' Set ls -> Set :=
adamc@615 51 | RNil : record' Nil
adamc@615 52 | RCons : forall n ls (T : Set) (pf : AllS (lt n) ls) r, T -> record' r -> record' (Cons T pf r).
adamc@615 53
adamc@615 54 Definition record (r : row Set) := record' (data r).
adamc@615 55
adamc@615 56 Fixpoint kDen (k : kind) : Type :=
adamc@615 57 match k with
adamc@615 58 | KType => Set
adamc@615 59 | KName => name
adamc@615 60 | KArrow k1 k2 => kDen k1 -> kDen k2
adamc@615 61 | KRecord k1 => row (kDen k1)
adamc@615 62 end.
adamc@615 63
adamc@615 64 Axiom cheat : forall T, T.
adamc@615 65
adamc@615 66 Fixpoint cinsert (n : name) (ls : list name) {struct ls} : list name :=
adamc@615 67 match ls with
adamc@615 68 | nil => n :: nil
adamc@615 69 | n' :: ls' =>
adamc@615 70 if eq_nat_dec n n'
adamc@615 71 then ls
adamc@615 72 else if le_lt_dec n n'
adamc@615 73 then n :: ls
adamc@615 74 else n' :: cinsert n ls'
adamc@615 75 end.
adamc@615 76
adamc@615 77 Hint Constructors AllS.
adamc@615 78 Hint Extern 1 (_ < _) => omega.
adamc@615 79
adamc@615 80 Lemma insert_front' : forall n n',
adamc@615 81 n <> n'
adamc@615 82 -> n <= n'
adamc@615 83 -> forall ls, AllS (lt n') ls
adamc@615 84 -> AllS (lt n) ls.
adamc@615 85 induction 3; auto.
adamc@615 86 Qed.
adamc@615 87
adamc@615 88 Lemma insert_front : forall n n',
adamc@615 89 n <> n'
adamc@615 90 -> n <= n'
adamc@615 91 -> forall ls, AllS (lt n') ls
adamc@615 92 -> AllS (lt n) (n' :: ls).
adamc@615 93 Hint Resolve insert_front'.
adamc@615 94 eauto.
adamc@615 95 Qed.
adamc@615 96
adamc@615 97 Lemma insert_continue : forall n n',
adamc@615 98 n <> n'
adamc@615 99 -> n' < n
adamc@615 100 -> forall ls, AllS (lt n') ls
adamc@615 101 -> AllS (lt n') (cinsert n ls).
adamc@615 102 induction 3; simpl; auto;
adamc@615 103 repeat (match goal with
adamc@615 104 | [ |- context[if ?E then _ else _] ] => destruct E
adamc@615 105 end; auto).
adamc@615 106 Qed.
adamc@615 107
adamc@615 108 Fixpoint insert T (n : name) (v : T) ls (r : row' T ls) {struct r} : row' T (cinsert n ls) :=
adamc@615 109 match r in row' _ ls return row' T (cinsert n ls) with
adamc@615 110 | Nil => Cons (n := n) v (allS_nil _) Nil
adamc@615 111 | Cons n' ls' v' pf r' =>
adamc@615 112 match eq_nat_dec n n' as END
adamc@615 113 return row' _ (if END then _ else _) with
adamc@615 114 | left _ => Cons (n := n') v' pf r'
adamc@615 115 | right pfNe =>
adamc@615 116 match le_lt_dec n n' as LLD
adamc@615 117 return row' _ (if LLD then _ else _) with
adamc@615 118 | left pfLe => Cons (n := n) v (insert_front pfNe pfLe pf) (Cons (n := n') v' pf r')
adamc@615 119 | right pfLt => Cons (n := n') v' (insert_continue pfNe pfLt pf) (insert n v r')
adamc@615 120 end
adamc@615 121 end
adamc@615 122 end.
adamc@615 123
adamc@615 124 Fixpoint cconcat (ls1 ls2 : list name) {struct ls1} : list name :=
adamc@615 125 match ls1 with
adamc@615 126 | nil => ls2
adamc@615 127 | n :: ls1' => cinsert n (cconcat ls1' ls2)
adamc@615 128 end.
adamc@615 129
adamc@615 130 Fixpoint concat T ls1 ls2 (r1 : row' T ls1) (r2 : row' T ls2) {struct r1} : row' T (cconcat ls1 ls2) :=
adamc@615 131 match r1 in row' _ ls1 return row' _ (cconcat ls1 _) with
adamc@615 132 | Nil => r2
adamc@615 133 | Cons n _ v _ r1' => insert n v (concat r1' r2)
adamc@615 134 end.
adamc@615 135
adamc@615 136 Fixpoint cfold T T' (f : name -> T -> T' -> T') (i : T') ls (r : row' T ls) {struct r} : T' :=
adamc@615 137 match r with
adamc@615 138 | Nil => i
adamc@615 139 | Cons n _ v _ r' => f n v (cfold f i r')
adamc@615 140 end.
adamc@615 141
adamc@615 142 Fixpoint cDen k (c : con kDen k) {struct c} : kDen k :=
adamc@615 143 match c in con _ k return kDen k with
adamc@615 144 | CVar _ x => x
adamc@615 145 | Arrow c1 c2 => cDen c1 -> cDen c2
adamc@615 146 | Poly _ c1 => forall x, cDen (c1 x)
adamc@615 147 | CAbs _ _ c1 => fun x => cDen (c1 x)
adamc@615 148 | CApp _ _ c1 c2 => (cDen c1) (cDen c2)
adamc@615 149 | Name n => n
adamc@615 150 | TRecord c1 => record (cDen c1)
adamc@615 151 | CEmpty _ => Row Nil
adamc@615 152 | CSingle _ c1 c2 => Row (Cons (n := cDen c1) (cDen c2) (allS_nil _) Nil)
adamc@615 153 | CConcat _ c1 c2 => Row (concat (data (cDen c1)) (data (cDen c2)))
adamc@615 154 | CFold k1 k2 => fun f i r => cfold f i (data r)
adamc@615 155 | CGuarded _ _ _ _ c => cDen c
adamc@615 156 end.