Mercurial > urweb

annotate src/coq/Semantics.v @ 616:d26d1f3acfd6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Semantics for ordered rows only
author Adam Chlipala <adamc@hcoop.net>
date Wed, 18 Feb 2009 09:32:17 -0500
parents 3c77133afd9a
children 5b358e8f9f09
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 Arith List TheoryList.
adamc@615 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@616 36 Definition row (T : Type) := list (name * T).
adamc@615 37
adamc@616 38 Fixpoint record (r : row Set) : Set :=
adamc@616 39 match r with
adamc@616 40 | nil => unit
adamc@616 41 | (_, T) :: r' => T * record r'
adamc@616 42 end%type.
adamc@615 43
adamc@615 44 Fixpoint kDen (k : kind) : Type :=
adamc@615 45 match k with
adamc@615 46 | KType => Set
adamc@615 47 | KName => name
adamc@615 48 | KArrow k1 k2 => kDen k1 -> kDen k2
adamc@615 49 | KRecord k1 => row (kDen k1)
adamc@615 50 end.
adamc@615 51
adamc@616 52 Fixpoint cfold T T' (f : name -> T -> T' -> T') (i : T') (r : row T) {struct r} : T' :=
adamc@615 53 match r with
adamc@616 54 | nil => i
adamc@616 55 | (n, v) :: r' => f n v (cfold f i r')
adamc@615 56 end.
adamc@615 57
adamc@615 58 Fixpoint cDen k (c : con kDen k) {struct c} : kDen k :=
adamc@615 59 match c in con _ k return kDen k with
adamc@615 60 | CVar _ x => x
adamc@615 61 | Arrow c1 c2 => cDen c1 -> cDen c2
adamc@615 62 | Poly _ c1 => forall x, cDen (c1 x)
adamc@615 63 | CAbs _ _ c1 => fun x => cDen (c1 x)
adamc@615 64 | CApp _ _ c1 c2 => (cDen c1) (cDen c2)
adamc@615 65 | Name n => n
adamc@615 66 | TRecord c1 => record (cDen c1)
adamc@616 67 | CEmpty _ => nil
adamc@616 68 | CSingle _ c1 c2 => (cDen c1, cDen c2) :: nil
adamc@616 69 | CConcat _ c1 c2 => cDen c1 ++ cDen c2
adamc@616 70 | CFold k1 k2 => @cfold _ _
adamc@615 71 | CGuarded _ _ _ _ c => cDen c
adamc@615 72 end.
adamc@616 73
adamc@616 74 Theorem subs_correct : forall k1 (c1 : con kDen k1) k2 (c2 : _ -> con kDen k2) c2',
adamc@616 75 subs c1 c2 c2'
adamc@616 76 -> cDen (c2 (cDen c1)) = cDen c2'.
adamc@616 77 induction 1; simpl; intuition; try (apply ext_eq_forallS || apply ext_eq);
adamc@616 78 repeat match goal with
adamc@616 79 | [ H : _ |- _ ] => rewrite H
adamc@616 80 end; intuition.
adamc@616 81 Qed.
adamc@616 82
adamc@616 83 Definition disjoint T (r1 r2 : row T) :=
adamc@616 84 AllS (fun p1 => AllS (fun p2 => fst p1 <> fst p2) r2) r1.
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 Lemma AllS_app : forall T P (ls2 : list T),
adamc@616 89 AllS P ls2
adamc@616 90 -> forall ls1, AllS P ls1
adamc@616 91 -> AllS P (ls1 ++ ls2).
adamc@616 92 induction 2; simpl; intuition.
adamc@616 93 Qed.
adamc@616 94
adamc@616 95 Lemma AllS_weaken : forall T (P P' : T -> Prop),
adamc@616 96 (forall x, P x -> P' x)
adamc@616 97 -> forall ls,
adamc@616 98 AllS P ls
adamc@616 99 -> AllS P' ls.
adamc@616 100 induction 2; simpl; intuition.
adamc@616 101 Qed.
adamc@616 102
adamc@616 103 Theorem disjoint_symm : forall T (r1 r2 : row T),
adamc@616 104 disjoint r1 r2
adamc@616 105 -> disjoint r2 r1.
adamc@616 106 Hint Constructors AllS.
adamc@616 107 Hint Resolve AllS_weaken.
adamc@616 108
adamc@616 109 unfold disjoint; induction r2; simpl; intuition.
adamc@616 110 constructor.
adamc@616 111 eapply AllS_weaken; eauto.
adamc@616 112 intuition.
adamc@616 113 inversion H0; auto.
adamc@616 114
adamc@616 115 apply IHr2.
adamc@616 116 eapply AllS_weaken; eauto.
adamc@616 117 intuition.
adamc@616 118 inversion H0; auto.
adamc@616 119 Qed.
adamc@616 120
adamc@616 121 Lemma map_id : forall k (r : row k),
adamc@616 122 cfold (fun x x0 (x1 : row _) => (x, x0) :: x1) nil r = r.
adamc@616 123 induction r; simpl; intuition;
adamc@616 124 match goal with
adamc@616 125 | [ H : _ |- _ ] => rewrite H
adamc@616 126 end; intuition.
adamc@616 127 Qed.
adamc@616 128
adamc@616 129 Lemma map_dist : forall T1 T2 (f : T1 -> T2) (r2 r1 : row T1),
adamc@616 130 cfold (fun x x0 (x1 : row _) => (x, f x0) :: x1) nil (r1 ++ r2)
adamc@616 131 = cfold (fun x x0 (x1 : row _) => (x, f x0) :: x1) nil r1
adamc@616 132 ++ cfold (fun x x0 (x1 : row _) => (x, f x0) :: x1) nil r2.
adamc@616 133 induction r1; simpl; intuition;
adamc@616 134 match goal with
adamc@616 135 | [ H : _ |- _ ] => rewrite H
adamc@616 136 end; intuition.
adamc@616 137 Qed.
adamc@616 138
adamc@616 139 Lemma fold_fuse : forall T1 T2 T3 (f : name -> T1 -> T2 -> T2) (i : T2) (f' : T3 -> T1) (c : row T3),
adamc@616 140 cfold f i (cfold (fun x x0 (x1 : row _) => (x, f' x0) :: x1) nil c)
adamc@616 141 = cfold (fun x x0 => f x (f' x0)) i c.
adamc@616 142 induction c; simpl; intuition;
adamc@616 143 match goal with
adamc@616 144 | [ H : _ |- _ ] => rewrite <- H
adamc@616 145 end; intuition.
adamc@616 146 Qed.
adamc@616 147
adamc@616 148 Scheme deq_mut := Minimality for deq Sort Prop
adamc@616 149 with disj_mut := Minimality for disj Sort Prop.
adamc@616 150
adamc@616 151 Theorem deq_correct : forall k (c1 c2 : con kDen k),
adamc@616 152 deq dvar c1 c2
adamc@616 153 -> cDen c1 = cDen c2.
adamc@616 154 Hint Resolve map_id map_dist fold_fuse AllS_app disjoint_symm.
adamc@616 155 Hint Extern 1 (_ = _) => unfold row; symmetry; apply app_ass.
adamc@616 156
adamc@616 157 apply (deq_mut (dvar := dvar)
adamc@616 158 (fun k (c1 c2 : con kDen k) =>
adamc@616 159 cDen c1 = cDen c2)
adamc@616 160 (fun k (c1 c2 : con kDen (KRecord k)) =>
adamc@616 161 disjoint (cDen c1) (cDen c2)));
adamc@616 162 simpl; intuition;
adamc@616 163 repeat (match goal with
adamc@616 164 | [ H : _ |- _ ] => rewrite H
adamc@616 165 | [ H : subs _ _ _ |- _ ] => rewrite <- (subs_correct H)
adamc@616 166 end; simpl; intuition); try congruence; unfold disjoint in *; intuition;
adamc@616 167 fold kDen in *; repeat match goal with
adamc@616 168 | [ H : AllS _ (_ :: _) |- _ ] => inversion H; clear H; subst; simpl in *
adamc@616 169 end; auto.
adamc@616 170 Qed.