Mercurial > cpdt > repo

annotate src/Impure.v @ 197:f6293ba66559

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
map_id
author Adam Chlipala <adamc@hcoop.net>
date Fri, 28 Nov 2008 14:10:23 -0500
parents 32ce9b28d7e7
children cbf2f74a5130
rev   line source
adamc@190 1 (* Copyright (c) 2008, Adam Chlipala
adamc@190 2 *
adamc@190 3 * This work is licensed under a
adamc@190 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
adamc@190 5 * Unported License.
adamc@190 6 * The license text is available at:
adamc@190 7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
adamc@190 8 *)
adamc@190 9
adamc@190 10 (* begin hide *)
adamc@190 11 Require Import Arith List Omega.
adamc@190 12
adamc@190 13 Require Import Axioms Tactics.
adamc@190 14
adamc@190 15 Set Implicit Arguments.
adamc@190 16 (* end hide *)
adamc@190 17
adamc@190 18
adamc@190 19 (** %\chapter{Modeling Impure Languages}% *)
adamc@190 20
adamc@190 21 (** TODO: Prose for this chapter *)
adamc@190 22
adamc@190 23 Section var.
adamc@190 24 Variable var : Type.
adamc@190 25
adamc@190 26 Inductive term : Type :=
adamc@190 27 | Var : var -> term
adamc@190 28 | App : term -> term -> term
adamc@190 29 | Abs : (var -> term) -> term
adamc@190 30 | Unit : term.
adamc@190 31 End var.
adamc@190 32
adamc@190 33 Implicit Arguments Unit [var].
adamc@190 34
adamc@190 35 Notation "# v" := (Var v) (at level 70).
adamc@190 36 Notation "()" := Unit.
adamc@190 37
adamc@190 38 Infix "@" := App (left associativity, at level 72).
adamc@190 39 Notation "\ x , e" := (Abs (fun x => e)) (at level 73).
adamc@190 40 Notation "\ ? , e" := (Abs (fun _ => e)) (at level 73).
adamc@190 41
adamc@191 42 Definition Term := forall var, term var.
adamc@191 43
adamc@191 44 Definition ident : Term := fun _ => \x, #x.
adamc@191 45 Definition unite : Term := fun _ => ().
adamc@191 46 Definition ident_self : Term := fun _ => ident _ @ ident _.
adamc@191 47 Definition ident_unit : Term := fun _ => ident _ @ unite _.
adamc@191 48
adamc@191 49
adamc@191 50 Module impredicative.
adamc@191 51 Inductive dynamic : Set :=
adamc@191 52 | Dyn : forall (dynTy : Type), dynTy -> dynamic.
adamc@191 53
adamc@191 54 Inductive computation (T : Type) : Set :=
adamc@191 55 | Return : T -> computation T
adamc@191 56 | Bind : forall (T' : Type),
adamc@191 57 computation T' -> (T' -> computation T) -> computation T
adamc@191 58 | Unpack : dynamic -> computation T.
adamc@191 59
adamc@191 60 Inductive eval : forall T, computation T -> T -> Prop :=
adamc@191 61 | EvalReturn : forall T (v : T),
adamc@191 62 eval (Return v) v
adamc@191 63 | EvalUnpack : forall T (v : T),
adamc@191 64 eval (Unpack T (Dyn v)) v
adamc@191 65 | EvalBind : forall T1 T2 (c1 : computation T1) (c2 : T1 -> computation T2) v1 v2,
adamc@191 66 eval c1 v1
adamc@191 67 -> eval (c2 v1) v2
adamc@191 68 -> eval (Bind c1 c2) v2.
adamc@191 69
adamc@192 70 (* begin thide *)
adamc@191 71 Fixpoint termDenote (e : term dynamic) : computation dynamic :=
adamc@191 72 match e with
adamc@191 73 | Var v => Return v
adamc@191 74 | App e1 e2 => Bind (termDenote e1) (fun f =>
adamc@191 75 Bind (termDenote e2) (fun x =>
adamc@191 76 Bind (Unpack (dynamic -> computation dynamic) f) (fun f' =>
adamc@191 77 f' x)))
adamc@191 78 | Abs e' => Return (Dyn (fun x => termDenote (e' x)))
adamc@191 79
adamc@191 80 | Unit => Return (Dyn tt)
adamc@191 81 end.
adamc@192 82 (* end thide *)
adamc@191 83
adamc@191 84 Definition TermDenote (E : Term) := termDenote (E _).
adamc@191 85
adamc@191 86 Eval compute in TermDenote ident.
adamc@191 87 Eval compute in TermDenote unite.
adamc@191 88 Eval compute in TermDenote ident_self.
adamc@191 89 Eval compute in TermDenote ident_unit.
adamc@191 90
adamc@191 91 Theorem eval_ident_unit : eval (TermDenote ident_unit) (Dyn tt).
adamc@192 92 (* begin thide *)
adamc@191 93 compute.
adamc@191 94 repeat econstructor.
adamc@191 95 simpl.
adamc@191 96 constructor.
adamc@191 97 Qed.
adamc@192 98 (* end thide *)
adamc@191 99
adamc@191 100 Theorem invert_ident : forall (E : Term) d,
adamc@191 101 eval (TermDenote (fun _ => ident _ @ E _)) d
adamc@191 102 -> eval (TermDenote E) d.
adamc@192 103 (* begin thide *)
adamc@191 104 inversion 1.
adamc@191 105
adamc@191 106 crush.
adamc@191 107
adamc@191 108 Focus 3.
adamc@191 109 crush.
adamc@191 110 unfold TermDenote in H0.
adamc@191 111 simpl in H0.
adamc@191 112 (** [injection H0.] *)
adamc@191 113 Abort.
adamc@192 114 (* end thide *)
adamc@191 115
adamc@191 116 End impredicative.
adamc@191 117
adamc@190 118
adamc@190 119 Module predicative.
adamc@190 120
adamc@190 121 Inductive val : Type :=
adamc@190 122 | Func : nat -> val
adamc@190 123 | VUnit.
adamc@190 124
adamc@190 125 Inductive computation : Type :=
adamc@190 126 | Return : val -> computation
adamc@190 127 | Bind : computation -> (val -> computation) -> computation
adamc@190 128 | CAbs : (val -> computation) -> computation
adamc@190 129 | CApp : val -> val -> computation.
adamc@190 130
adamc@190 131 Definition func := val -> computation.
adamc@190 132
adamc@190 133 Fixpoint get (n : nat) (ls : list func) {struct ls} : option func :=
adamc@190 134 match ls with
adamc@190 135 | nil => None
adamc@190 136 | x :: ls' =>
adamc@190 137 if eq_nat_dec n (length ls')
adamc@190 138 then Some x
adamc@190 139 else get n ls'
adamc@190 140 end.
adamc@190 141
adamc@190 142 Inductive eval : list func -> computation -> list func -> val -> Prop :=
adamc@190 143 | EvalReturn : forall ds d,
adamc@190 144 eval ds (Return d) ds d
adamc@190 145 | EvalBind : forall ds c1 c2 ds' d1 ds'' d2,
adamc@190 146 eval ds c1 ds' d1
adamc@190 147 -> eval ds' (c2 d1) ds'' d2
adamc@190 148 -> eval ds (Bind c1 c2) ds'' d2
adamc@190 149 | EvalCAbs : forall ds f,
adamc@190 150 eval ds (CAbs f) (f :: ds) (Func (length ds))
adamc@190 151 | EvalCApp : forall ds i d2 f ds' d3,
adamc@190 152 get i ds = Some f
adamc@190 153 -> eval ds (f d2) ds' d3
adamc@190 154 -> eval ds (CApp (Func i) d2) ds' d3.
adamc@190 155
adamc@192 156 (* begin thide *)
adamc@190 157 Fixpoint termDenote (e : term val) : computation :=
adamc@190 158 match e with
adamc@190 159 | Var v => Return v
adamc@190 160 | App e1 e2 => Bind (termDenote e1) (fun f =>
adamc@190 161 Bind (termDenote e2) (fun x =>
adamc@190 162 CApp f x))
adamc@190 163 | Abs e' => CAbs (fun x => termDenote (e' x))
adamc@190 164
adamc@190 165 | Unit => Return VUnit
adamc@190 166 end.
adamc@192 167 (* end thide *)
adamc@190 168
adamc@190 169 Definition TermDenote (E : Term) := termDenote (E _).
adamc@190 170
adamc@190 171 Eval compute in TermDenote ident.
adamc@190 172 Eval compute in TermDenote unite.
adamc@190 173 Eval compute in TermDenote ident_self.
adamc@190 174 Eval compute in TermDenote ident_unit.
adamc@190 175
adamc@190 176 Theorem eval_ident_unit : exists ds, eval nil (TermDenote ident_unit) ds VUnit.
adamc@192 177 (* begin thide *)
adamc@190 178 compute.
adamc@190 179 repeat econstructor.
adamc@190 180 simpl.
adamc@190 181 rewrite (eta Return).
adamc@190 182 reflexivity.
adamc@190 183 Qed.
adamc@190 184
adamc@190 185 Hint Constructors eval.
adamc@190 186
adamc@190 187 Lemma app_nil_start : forall A (ls : list A),
adamc@190 188 ls = nil ++ ls.
adamc@190 189 reflexivity.
adamc@190 190 Qed.
adamc@190 191
adamc@190 192 Lemma app_cons : forall A (x : A) (ls : list A),
adamc@190 193 x :: ls = (x :: nil) ++ ls.
adamc@190 194 reflexivity.
adamc@190 195 Qed.
adamc@190 196
adamc@190 197 Theorem eval_monotone : forall ds c ds' d,
adamc@190 198 eval ds c ds' d
adamc@190 199 -> exists ds'', ds' = ds'' ++ ds.
adamc@190 200 Hint Resolve app_nil_start app_ass app_cons.
adamc@190 201
adamc@190 202 induction 1; firstorder; subst; eauto.
adamc@190 203 Qed.
adamc@190 204
adamc@190 205 Lemma length_app : forall A (ds2 ds1 : list A),
adamc@190 206 length (ds1 ++ ds2) = length ds1 + length ds2.
adamc@190 207 induction ds1; simpl; intuition.
adamc@190 208 Qed.
adamc@190 209
adamc@190 210 Lemma get_app : forall ds2 d ds1,
adamc@190 211 get (length ds2) (ds1 ++ d :: ds2) = Some d.
adamc@190 212 Hint Rewrite length_app : cpdt.
adamc@190 213
adamc@190 214 induction ds1; crush;
adamc@190 215 match goal with
adamc@190 216 | [ |- context[if ?E then _ else _] ] => destruct E
adamc@190 217 end; crush.
adamc@190 218 Qed.
adamc@192 219 (* end thide *)
adamc@190 220
adamc@190 221 Theorem invert_ident : forall (E : Term) ds ds' d,
adamc@190 222 eval ds (TermDenote (fun _ => ident _ @ E _)) ds' d
adamc@190 223 -> eval ((fun x => Return x) :: ds) (TermDenote E) ds' d.
adamc@192 224 (* begin thide *)
adamc@190 225 inversion 1; subst.
adamc@190 226 clear H.
adamc@190 227 inversion H3; clear H3; subst.
adamc@190 228 inversion H6; clear H6; subst.
adamc@190 229 generalize (eval_monotone H2); crush.
adamc@190 230 inversion H5; clear H5; subst.
adamc@190 231 rewrite get_app in H3.
adamc@190 232 inversion H3; clear H3; subst.
adamc@190 233 inversion H7; clear H7; subst.
adamc@190 234 assumption.
adamc@190 235 Qed.
adamc@192 236 (* end thide *)
adamc@190 237
adamc@190 238 End predicative.