Mercurial > cpdt > repo

comparison src/Impure.v @ 190:094bd1e353dd

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Import predicative Impure example
author Adam Chlipala <adamc@hcoop.net>
date Tue, 18 Nov 2008 12:44:46 -0500
parents
children cf5ddf078858
comparison
equal deleted inserted replaced
189:0198181d1b64 190:094bd1e353dd
1 (* Copyright (c) 2008, Adam Chlipala
2 *
3 * This work is licensed under a
4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
5 * Unported License.
6 * The license text is available at:
7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
8 *)
9
10 (* begin hide *)
11 Require Import Arith List Omega.
12
13 Require Import Axioms Tactics.
14
15 Set Implicit Arguments.
16 (* end hide *)
17
18
19 (** %\chapter{Modeling Impure Languages}% *)
20
21 (** TODO: Prose for this chapter *)
22
23 Section var.
24 Variable var : Type.
25
26 Inductive term : Type :=
27 | Var : var -> term
28 | App : term -> term -> term
29 | Abs : (var -> term) -> term
30 | Unit : term.
31 End var.
32
33 Implicit Arguments Unit [var].
34
35 Notation "# v" := (Var v) (at level 70).
36 Notation "()" := Unit.
37
38 Infix "@" := App (left associativity, at level 72).
39 Notation "\ x , e" := (Abs (fun x => e)) (at level 73).
40 Notation "\ ? , e" := (Abs (fun _ => e)) (at level 73).
41
42
43 Module predicative.
44
45 Inductive val : Type :=
46 | Func : nat -> val
47 | VUnit.
48
49 Inductive computation : Type :=
50 | Return : val -> computation
51 | Bind : computation -> (val -> computation) -> computation
52 | CAbs : (val -> computation) -> computation
53 | CApp : val -> val -> computation.
54
55 Definition func := val -> computation.
56
57 Fixpoint get (n : nat) (ls : list func) {struct ls} : option func :=
58 match ls with
59 | nil => None
60 | x :: ls' =>
61 if eq_nat_dec n (length ls')
62 then Some x
63 else get n ls'
64 end.
65
66 Inductive eval : list func -> computation -> list func -> val -> Prop :=
67 | EvalReturn : forall ds d,
68 eval ds (Return d) ds d
69 | EvalBind : forall ds c1 c2 ds' d1 ds'' d2,
70 eval ds c1 ds' d1
71 -> eval ds' (c2 d1) ds'' d2
72 -> eval ds (Bind c1 c2) ds'' d2
73 | EvalCAbs : forall ds f,
74 eval ds (CAbs f) (f :: ds) (Func (length ds))
75 | EvalCApp : forall ds i d2 f ds' d3,
76 get i ds = Some f
77 -> eval ds (f d2) ds' d3
78 -> eval ds (CApp (Func i) d2) ds' d3.
79
80 Fixpoint termDenote (e : term val) : computation :=
81 match e with
82 | Var v => Return v
83 | App e1 e2 => Bind (termDenote e1) (fun f =>
84 Bind (termDenote e2) (fun x =>
85 CApp f x))
86 | Abs e' => CAbs (fun x => termDenote (e' x))
87
88 | Unit => Return VUnit
89 end.
90
91 Definition Term := forall var, term var.
92 Definition TermDenote (E : Term) := termDenote (E _).
93
94 Definition ident : Term := fun _ => \x, #x.
95 Eval compute in TermDenote ident.
96
97 Definition unite : Term := fun _ => ().
98 Eval compute in TermDenote unite.
99
100 Definition ident_self : Term := fun _ => ident _ @ ident _.
101 Eval compute in TermDenote ident_self.
102
103 Definition ident_unit : Term := fun _ => ident _ @ unite _.
104 Eval compute in TermDenote ident_unit.
105
106 Theorem eval_ident_unit : exists ds, eval nil (TermDenote ident_unit) ds VUnit.
107 compute.
108 repeat econstructor.
109 simpl.
110 rewrite (eta Return).
111 reflexivity.
112 Qed.
113
114 Hint Constructors eval.
115
116 Lemma app_nil_start : forall A (ls : list A),
117 ls = nil ++ ls.
118 reflexivity.
119 Qed.
120
121 Lemma app_cons : forall A (x : A) (ls : list A),
122 x :: ls = (x :: nil) ++ ls.
123 reflexivity.
124 Qed.
125
126 Theorem eval_monotone : forall ds c ds' d,
127 eval ds c ds' d
128 -> exists ds'', ds' = ds'' ++ ds.
129 Hint Resolve app_nil_start app_ass app_cons.
130
131 induction 1; firstorder; subst; eauto.
132 Qed.
133
134 Lemma length_app : forall A (ds2 ds1 : list A),
135 length (ds1 ++ ds2) = length ds1 + length ds2.
136 induction ds1; simpl; intuition.
137 Qed.
138
139 Lemma get_app : forall ds2 d ds1,
140 get (length ds2) (ds1 ++ d :: ds2) = Some d.
141 Hint Rewrite length_app : cpdt.
142
143 induction ds1; crush;
144 match goal with
145 | [ |- context[if ?E then _ else _] ] => destruct E
146 end; crush.
147 Qed.
148
149 Theorem invert_ident : forall (E : Term) ds ds' d,
150 eval ds (TermDenote (fun _ => ident _ @ E _)) ds' d
151 -> eval ((fun x => Return x) :: ds) (TermDenote E) ds' d.
152 inversion 1; subst.
153 clear H.
154 inversion H3; clear H3; subst.
155 inversion H6; clear H6; subst.
156 generalize (eval_monotone H2); crush.
157 inversion H5; clear H5; subst.
158 rewrite get_app in H3.
159 inversion H3; clear H3; subst.
160 inversion H7; clear H7; subst.
161 assumption.
162 Qed.
163
164 End predicative.