adamc@190: (* Copyright (c) 2008, Adam Chlipala adamc@190: * adamc@190: * This work is licensed under a adamc@190: * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 adamc@190: * Unported License. adamc@190: * The license text is available at: adamc@190: * http://creativecommons.org/licenses/by-nc-nd/3.0/ adamc@190: *) adamc@190: adamc@190: (* begin hide *) adamc@190: Require Import Arith List Omega. adamc@190: adamc@190: Require Import Axioms Tactics. adamc@190: adamc@190: Set Implicit Arguments. adamc@190: (* end hide *) adamc@190: adamc@190: adamc@190: (** %\chapter{Modeling Impure Languages}% *) adamc@190: adamc@190: (** TODO: Prose for this chapter *) adamc@190: adamc@190: Section var. adamc@190: Variable var : Type. adamc@190: adamc@190: Inductive term : Type := adamc@190: | Var : var -> term adamc@190: | App : term -> term -> term adamc@190: | Abs : (var -> term) -> term adamc@190: | Unit : term. adamc@190: End var. adamc@190: adamc@190: Implicit Arguments Unit [var]. adamc@190: adamc@190: Notation "# v" := (Var v) (at level 70). adamc@190: Notation "()" := Unit. adamc@190: adamc@190: Infix "@" := App (left associativity, at level 72). adamc@190: Notation "\ x , e" := (Abs (fun x => e)) (at level 73). adamc@190: Notation "\ ? , e" := (Abs (fun _ => e)) (at level 73). adamc@190: adamc@191: Definition Term := forall var, term var. adamc@191: adamc@191: Definition ident : Term := fun _ => \x, #x. adamc@191: Definition unite : Term := fun _ => (). adamc@191: Definition ident_self : Term := fun _ => ident _ @ ident _. adamc@191: Definition ident_unit : Term := fun _ => ident _ @ unite _. adamc@191: adamc@191: adamc@191: Module impredicative. adamc@191: Inductive dynamic : Set := adamc@191: | Dyn : forall (dynTy : Type), dynTy -> dynamic. adamc@191: adamc@191: Inductive computation (T : Type) : Set := adamc@191: | Return : T -> computation T adamc@191: | Bind : forall (T' : Type), adamc@191: computation T' -> (T' -> computation T) -> computation T adamc@191: | Unpack : dynamic -> computation T. adamc@191: adamc@191: Inductive eval : forall T, computation T -> T -> Prop := adamc@191: | EvalReturn : forall T (v : T), adamc@191: eval (Return v) v adamc@191: | EvalUnpack : forall T (v : T), adamc@191: eval (Unpack T (Dyn v)) v adamc@191: | EvalBind : forall T1 T2 (c1 : computation T1) (c2 : T1 -> computation T2) v1 v2, adamc@191: eval c1 v1 adamc@191: -> eval (c2 v1) v2 adamc@191: -> eval (Bind c1 c2) v2. adamc@191: adamc@192: (* begin thide *) adamc@191: Fixpoint termDenote (e : term dynamic) : computation dynamic := adamc@191: match e with adamc@191: | Var v => Return v adamc@191: | App e1 e2 => Bind (termDenote e1) (fun f => adamc@191: Bind (termDenote e2) (fun x => adamc@191: Bind (Unpack (dynamic -> computation dynamic) f) (fun f' => adamc@191: f' x))) adamc@191: | Abs e' => Return (Dyn (fun x => termDenote (e' x))) adamc@191: adamc@191: | Unit => Return (Dyn tt) adamc@191: end. adamc@192: (* end thide *) adamc@191: adamc@191: Definition TermDenote (E : Term) := termDenote (E _). adamc@191: adamc@191: Eval compute in TermDenote ident. adamc@191: Eval compute in TermDenote unite. adamc@191: Eval compute in TermDenote ident_self. adamc@191: Eval compute in TermDenote ident_unit. adamc@191: adamc@191: Theorem eval_ident_unit : eval (TermDenote ident_unit) (Dyn tt). adamc@192: (* begin thide *) adamc@191: compute. adamc@191: repeat econstructor. adamc@191: simpl. adamc@191: constructor. adamc@191: Qed. adamc@192: (* end thide *) adamc@191: adamc@191: Theorem invert_ident : forall (E : Term) d, adamc@191: eval (TermDenote (fun _ => ident _ @ E _)) d adamc@191: -> eval (TermDenote E) d. adamc@192: (* begin thide *) adamc@191: inversion 1. adamc@191: adamc@191: crush. adamc@191: adamc@191: Focus 3. adamc@191: crush. adamc@191: unfold TermDenote in H0. adamc@191: simpl in H0. adamc@191: (** [injection H0.] *) adamc@191: Abort. adamc@192: (* end thide *) adamc@191: adamc@191: End impredicative. adamc@191: adamc@190: adamc@190: Module predicative. adamc@190: adamc@190: Inductive val : Type := adamc@190: | Func : nat -> val adamc@190: | VUnit. adamc@190: adamc@190: Inductive computation : Type := adamc@190: | Return : val -> computation adamc@190: | Bind : computation -> (val -> computation) -> computation adamc@190: | CAbs : (val -> computation) -> computation adamc@190: | CApp : val -> val -> computation. adamc@190: adamc@190: Definition func := val -> computation. adamc@190: adamc@190: Fixpoint get (n : nat) (ls : list func) {struct ls} : option func := adamc@190: match ls with adamc@190: | nil => None adamc@190: | x :: ls' => adamc@190: if eq_nat_dec n (length ls') adamc@190: then Some x adamc@190: else get n ls' adamc@190: end. adamc@190: adamc@190: Inductive eval : list func -> computation -> list func -> val -> Prop := adamc@190: | EvalReturn : forall ds d, adamc@190: eval ds (Return d) ds d adamc@190: | EvalBind : forall ds c1 c2 ds' d1 ds'' d2, adamc@190: eval ds c1 ds' d1 adamc@190: -> eval ds' (c2 d1) ds'' d2 adamc@190: -> eval ds (Bind c1 c2) ds'' d2 adamc@190: | EvalCAbs : forall ds f, adamc@190: eval ds (CAbs f) (f :: ds) (Func (length ds)) adamc@190: | EvalCApp : forall ds i d2 f ds' d3, adamc@190: get i ds = Some f adamc@190: -> eval ds (f d2) ds' d3 adamc@190: -> eval ds (CApp (Func i) d2) ds' d3. adamc@190: adamc@192: (* begin thide *) adamc@190: Fixpoint termDenote (e : term val) : computation := adamc@190: match e with adamc@190: | Var v => Return v adamc@190: | App e1 e2 => Bind (termDenote e1) (fun f => adamc@190: Bind (termDenote e2) (fun x => adamc@190: CApp f x)) adamc@190: | Abs e' => CAbs (fun x => termDenote (e' x)) adamc@190: adamc@190: | Unit => Return VUnit adamc@190: end. adamc@192: (* end thide *) adamc@190: adamc@190: Definition TermDenote (E : Term) := termDenote (E _). adamc@190: adamc@190: Eval compute in TermDenote ident. adamc@190: Eval compute in TermDenote unite. adamc@190: Eval compute in TermDenote ident_self. adamc@190: Eval compute in TermDenote ident_unit. adamc@190: adamc@190: Theorem eval_ident_unit : exists ds, eval nil (TermDenote ident_unit) ds VUnit. adamc@192: (* begin thide *) adamc@190: compute. adamc@190: repeat econstructor. adamc@190: simpl. adamc@190: rewrite (eta Return). adamc@190: reflexivity. adamc@190: Qed. adamc@190: adamc@190: Hint Constructors eval. adamc@190: adamc@190: Lemma app_nil_start : forall A (ls : list A), adamc@190: ls = nil ++ ls. adamc@190: reflexivity. adamc@190: Qed. adamc@190: adamc@190: Lemma app_cons : forall A (x : A) (ls : list A), adamc@190: x :: ls = (x :: nil) ++ ls. adamc@190: reflexivity. adamc@190: Qed. adamc@190: adamc@190: Theorem eval_monotone : forall ds c ds' d, adamc@190: eval ds c ds' d adamc@190: -> exists ds'', ds' = ds'' ++ ds. adamc@190: Hint Resolve app_nil_start app_ass app_cons. adamc@190: adamc@190: induction 1; firstorder; subst; eauto. adamc@190: Qed. adamc@190: adamc@190: Lemma length_app : forall A (ds2 ds1 : list A), adamc@190: length (ds1 ++ ds2) = length ds1 + length ds2. adamc@190: induction ds1; simpl; intuition. adamc@190: Qed. adamc@190: adamc@190: Lemma get_app : forall ds2 d ds1, adamc@190: get (length ds2) (ds1 ++ d :: ds2) = Some d. adamc@190: Hint Rewrite length_app : cpdt. adamc@190: adamc@190: induction ds1; crush; adamc@190: match goal with adamc@190: | [ |- context[if ?E then _ else _] ] => destruct E adamc@190: end; crush. adamc@190: Qed. adamc@192: (* end thide *) adamc@190: adamc@190: Theorem invert_ident : forall (E : Term) ds ds' d, adamc@190: eval ds (TermDenote (fun _ => ident _ @ E _)) ds' d adamc@190: -> eval ((fun x => Return x) :: ds) (TermDenote E) ds' d. adamc@192: (* begin thide *) adamc@190: inversion 1; subst. adamc@190: clear H. adamc@190: inversion H3; clear H3; subst. adamc@190: inversion H6; clear H6; subst. adamc@190: generalize (eval_monotone H2); crush. adamc@190: inversion H5; clear H5; subst. adamc@190: rewrite get_app in H3. adamc@190: inversion H3; clear H3; subst. adamc@190: inversion H7; clear H7; subst. adamc@190: assumption. adamc@190: Qed. adamc@192: (* end thide *) adamc@190: adamc@190: End predicative.