Mercurial > cpdt > repo

comparison src/Hoas.v @ 158:fabfaa93c9ea

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Hoas, up to type soundness
author Adam Chlipala <adamc@hcoop.net>
date Mon, 03 Nov 2008 09:43:32 -0500
parents
children 8b2b652ab0ee
comparison
equal deleted inserted replaced
157:2022e3f2aa26 158:fabfaa93c9ea
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 Eqdep String List.
12
13 Require Import Tactics.
14
15 Set Implicit Arguments.
16 (* end hide *)
17
18
19 (** %\chapter{Higher-Order Abstract Syntax}% *)
20
21 (** TODO: Prose for this chapter *)
22
23
24 (** * Parametric Higher-Order Abstract Syntax *)
25
26 Inductive type : Type :=
27 | Bool : type
28 | Arrow : type -> type -> type.
29
30 Infix "-->" := Arrow (right associativity, at level 60).
31
32 Section exp.
33 Variable var : type -> Type.
34
35 Inductive exp : type -> Type :=
36 | Const' : bool -> exp Bool
37 | Var : forall t, var t -> exp t
38 | App' : forall dom ran, exp (dom --> ran) -> exp dom -> exp ran
39 | Abs' : forall dom ran, (var dom -> exp ran) -> exp (dom --> ran).
40 End exp.
41
42 Implicit Arguments Const' [var].
43 Implicit Arguments Var [var t].
44 Implicit Arguments Abs' [var dom ran].
45
46 Definition Exp t := forall var, exp var t.
47 Definition Exp1 t1 t2 := forall var, var t1 -> exp var t2.
48
49 Definition Const (b : bool) : Exp Bool :=
50 fun _ => Const' b.
51 Definition App dom ran (F : Exp (dom --> ran)) (X : Exp dom) : Exp ran :=
52 fun _ => App' (F _) (X _).
53 Definition Abs dom ran (B : Exp1 dom ran) : Exp (dom --> ran) :=
54 fun _ => Abs' (B _).
55
56 Section flatten.
57 Variable var : type -> Type.
58
59 Fixpoint flatten t (e : exp (exp var) t) {struct e} : exp var t :=
60 match e in exp _ t return exp _ t with
61 | Const' b => Const' b
62 | Var _ e' => e'
63 | App' _ _ e1 e2 => App' (flatten e1) (flatten e2)
64 | Abs' _ _ e' => Abs' (fun x => flatten (e' (Var x)))
65 end.
66 End flatten.
67
68 Definition Subst t1 t2 (E1 : Exp t1) (E2 : Exp1 t1 t2) : Exp t2 := fun _ =>
69 flatten (E2 _ (E1 _)).
70
71
72 (** * A Type Soundness Proof *)
73
74 Reserved Notation "E1 ==> E2" (no associativity, at level 90).
75
76 Inductive Val : forall t, Exp t -> Prop :=
77 | VConst : forall b, Val (Const b)
78 | VAbs : forall dom ran (B : Exp1 dom ran), Val (Abs B).
79
80 Hint Constructors Val.
81
82 Inductive Step : forall t, Exp t -> Exp t -> Prop :=
83 | Beta : forall dom ran (B : Exp1 dom ran) (X : Exp dom),
84 App (Abs B) X ==> Subst X B
85 | Cong1 : forall dom ran (F : Exp (dom --> ran)) (X : Exp dom) F',
86 F ==> F'
87 -> App F X ==> App F' X
88 | Cong2 : forall dom ran (F : Exp (dom --> ran)) (X : Exp dom) X',
89 Val F
90 -> X ==> X'
91 -> App F X ==> App F X'
92
93 where "E1 ==> E2" := (Step E1 E2).
94
95 Hint Constructors Step.
96
97 Inductive Closed : forall t, Exp t -> Prop :=
98 | CConst : forall b,
99 Closed (Const b)
100 | CApp : forall dom ran (E1 : Exp (dom --> ran)) E2,
101 Closed E1
102 -> Closed E2
103 -> Closed (App E1 E2)
104 | CAbs : forall dom ran (E1 : Exp1 dom ran),
105 Closed (Abs E1).
106
107 Axiom closed : forall t (E : Exp t), Closed E.
108
109 Ltac my_crush :=
110 crush;
111 repeat (match goal with
112 | [ H : _ |- _ ] => generalize (inj_pairT2 _ _ _ _ _ H); clear H
113 end; crush).
114
115 Lemma progress' : forall t (E : Exp t),
116 Closed E
117 -> Val E \/ exists E', E ==> E'.
118 induction 1; crush;
119 try match goal with
120 | [ H : @Val (_ --> _) _ |- _ ] => inversion H; my_crush
121 end; eauto.
122 Qed.
123
124 Theorem progress : forall t (E : Exp t),
125 Val E \/ exists E', E ==> E'.
126 intros; apply progress'; apply closed.
127 Qed.
128