Mercurial > cpdt > repo

annotate 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
rev   line source
adamc@158 1 (* Copyright (c) 2008, Adam Chlipala
adamc@158 2 *
adamc@158 3 * This work is licensed under a
adamc@158 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
adamc@158 5 * Unported License.
adamc@158 6 * The license text is available at:
adamc@158 7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
adamc@158 8 *)
adamc@158 9
adamc@158 10 (* begin hide *)
adamc@158 11 Require Import Arith Eqdep String List.
adamc@158 12
adamc@158 13 Require Import Tactics.
adamc@158 14
adamc@158 15 Set Implicit Arguments.
adamc@158 16 (* end hide *)
adamc@158 17
adamc@158 18
adamc@158 19 (** %\chapter{Higher-Order Abstract Syntax}% *)
adamc@158 20
adamc@158 21 (** TODO: Prose for this chapter *)
adamc@158 22
adamc@158 23
adamc@158 24 (** * Parametric Higher-Order Abstract Syntax *)
adamc@158 25
adamc@158 26 Inductive type : Type :=
adamc@158 27 | Bool : type
adamc@158 28 | Arrow : type -> type -> type.
adamc@158 29
adamc@158 30 Infix "-->" := Arrow (right associativity, at level 60).
adamc@158 31
adamc@158 32 Section exp.
adamc@158 33 Variable var : type -> Type.
adamc@158 34
adamc@158 35 Inductive exp : type -> Type :=
adamc@158 36 | Const' : bool -> exp Bool
adamc@158 37 | Var : forall t, var t -> exp t
adamc@158 38 | App' : forall dom ran, exp (dom --> ran) -> exp dom -> exp ran
adamc@158 39 | Abs' : forall dom ran, (var dom -> exp ran) -> exp (dom --> ran).
adamc@158 40 End exp.
adamc@158 41
adamc@158 42 Implicit Arguments Const' [var].
adamc@158 43 Implicit Arguments Var [var t].
adamc@158 44 Implicit Arguments Abs' [var dom ran].
adamc@158 45
adamc@158 46 Definition Exp t := forall var, exp var t.
adamc@158 47 Definition Exp1 t1 t2 := forall var, var t1 -> exp var t2.
adamc@158 48
adamc@158 49 Definition Const (b : bool) : Exp Bool :=
adamc@158 50 fun _ => Const' b.
adamc@158 51 Definition App dom ran (F : Exp (dom --> ran)) (X : Exp dom) : Exp ran :=
adamc@158 52 fun _ => App' (F _) (X _).
adamc@158 53 Definition Abs dom ran (B : Exp1 dom ran) : Exp (dom --> ran) :=
adamc@158 54 fun _ => Abs' (B _).
adamc@158 55
adamc@158 56 Section flatten.
adamc@158 57 Variable var : type -> Type.
adamc@158 58
adamc@158 59 Fixpoint flatten t (e : exp (exp var) t) {struct e} : exp var t :=
adamc@158 60 match e in exp _ t return exp _ t with
adamc@158 61 | Const' b => Const' b
adamc@158 62 | Var _ e' => e'
adamc@158 63 | App' _ _ e1 e2 => App' (flatten e1) (flatten e2)
adamc@158 64 | Abs' _ _ e' => Abs' (fun x => flatten (e' (Var x)))
adamc@158 65 end.
adamc@158 66 End flatten.
adamc@158 67
adamc@158 68 Definition Subst t1 t2 (E1 : Exp t1) (E2 : Exp1 t1 t2) : Exp t2 := fun _ =>
adamc@158 69 flatten (E2 _ (E1 _)).
adamc@158 70
adamc@158 71
adamc@158 72 (** * A Type Soundness Proof *)
adamc@158 73
adamc@158 74 Reserved Notation "E1 ==> E2" (no associativity, at level 90).
adamc@158 75
adamc@158 76 Inductive Val : forall t, Exp t -> Prop :=
adamc@158 77 | VConst : forall b, Val (Const b)
adamc@158 78 | VAbs : forall dom ran (B : Exp1 dom ran), Val (Abs B).
adamc@158 79
adamc@158 80 Hint Constructors Val.
adamc@158 81
adamc@158 82 Inductive Step : forall t, Exp t -> Exp t -> Prop :=
adamc@158 83 | Beta : forall dom ran (B : Exp1 dom ran) (X : Exp dom),
adamc@158 84 App (Abs B) X ==> Subst X B
adamc@158 85 | Cong1 : forall dom ran (F : Exp (dom --> ran)) (X : Exp dom) F',
adamc@158 86 F ==> F'
adamc@158 87 -> App F X ==> App F' X
adamc@158 88 | Cong2 : forall dom ran (F : Exp (dom --> ran)) (X : Exp dom) X',
adamc@158 89 Val F
adamc@158 90 -> X ==> X'
adamc@158 91 -> App F X ==> App F X'
adamc@158 92
adamc@158 93 where "E1 ==> E2" := (Step E1 E2).
adamc@158 94
adamc@158 95 Hint Constructors Step.
adamc@158 96
adamc@158 97 Inductive Closed : forall t, Exp t -> Prop :=
adamc@158 98 | CConst : forall b,
adamc@158 99 Closed (Const b)
adamc@158 100 | CApp : forall dom ran (E1 : Exp (dom --> ran)) E2,
adamc@158 101 Closed E1
adamc@158 102 -> Closed E2
adamc@158 103 -> Closed (App E1 E2)
adamc@158 104 | CAbs : forall dom ran (E1 : Exp1 dom ran),
adamc@158 105 Closed (Abs E1).
adamc@158 106
adamc@158 107 Axiom closed : forall t (E : Exp t), Closed E.
adamc@158 108
adamc@158 109 Ltac my_crush :=
adamc@158 110 crush;
adamc@158 111 repeat (match goal with
adamc@158 112 | [ H : _ |- _ ] => generalize (inj_pairT2 _ _ _ _ _ H); clear H
adamc@158 113 end; crush).
adamc@158 114
adamc@158 115 Lemma progress' : forall t (E : Exp t),
adamc@158 116 Closed E
adamc@158 117 -> Val E \/ exists E', E ==> E'.
adamc@158 118 induction 1; crush;
adamc@158 119 try match goal with
adamc@158 120 | [ H : @Val (_ --> _) _ |- _ ] => inversion H; my_crush
adamc@158 121 end; eauto.
adamc@158 122 Qed.
adamc@158 123
adamc@158 124 Theorem progress : forall t (E : Exp t),
adamc@158 125 Val E \/ exists E', E ==> E'.
adamc@158 126 intros; apply progress'; apply closed.
adamc@158 127 Qed.
adamc@158 128