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.