Library cps


Require Import semantics.

Coevaluation for terms in CPS form





Inductive isatom: term -> Prop :=

  | isatom_var: forall x,

      isatom (Var x)

  | isatom_const: forall c,

      isatom (Const c)

  | isatom_fun: forall x b,

      isbody b ->

      isatom (Fun x b)



with isbody: term -> Prop :=

  | isbody_atom: forall a,

      isatom a ->

      isbody a

  | isbody_app: forall b a,

      isbody b -> isatom a ->

      isbody (App b a).




Scheme isatom_ind2 := Minimality for isatom Sort Prop

  with isbody_ind2 := Minimality for isbody Sort Prop.




Lemma isbody_subst:

  forall x a b, isatom a -> isbody b -> isbody (subst x a b).

Proof.

  assert (forall b, isbody b -> forall x a, isatom a -> isbody (subst x a b)).

  apply (isbody_ind2

    (fun a' => forall x a, isatom a -> isatom (subst x a a'))

    (fun b => forall x a, isatom a -> isbody (subst x a b))); intros; simpl.

  case (var_eq x0 x); intro. auto. constructor.

  constructor.

  case (var_eq x0 x); intro; constructor. auto.

  apply H0. auto. apply isbody_atom. auto.

  apply isbody_app; auto.

  auto.

Qed.




Lemma eval_body_atom:

  forall b v, eval b v -> isbody b -> isatom v.

Proof.

  induction 1; intros.

  constructor.

  inversion H. auto.

  inversion H2; subst. inversion H3.

  apply IHeval3. apply isbody_subst.

  apply IHeval2. apply isbody_atom. auto.

  generalize (IHeval1 H5); intro. inversion H3; auto.

Qed.




Lemma eval_body_fun:

  forall b x c, eval b (Fun x c) -> isbody b -> isbody c.

Proof.

  intros. generalize (eval_body_atom _ _ H H0); intro. inversion H1; auto.

Qed.




Fixpoint isfree (x: var) (a: term) {struct a} : Prop :=

  match a with

  | Var y => y = x

  | Const c => False

  | Fun y b => isfree x b /\ y <> x

  | App b c => isfree x b \/ isfree x c

  end.




Definition closed (a: term) : Prop := forall x, ~isfree x a.




Lemma isfree_subst:

  forall x a, closed a ->

  forall b y, isfree y (subst x a b) -> isfree y b /\ y <> x.

Proof.

  induction b; simpl; intros.

  destruct (var_eq x v). elim (H _ H0).

  simpl in H0. split; congruence.

  tauto.

  destruct (var_eq x v). intuition congruence. firstorder.

  firstorder.

Qed.




Lemma closed_subst:

  forall x a b, closed (Fun x a) -> closed b -> closed (subst x b a).

Proof.

  intros; red; intro y; red; intro.

  elim (isfree_subst _ _ H0 _ _ H1); intros.

  elim (H y). simpl. split; auto.

Qed.




Lemma closed_App_inv:

  forall a b, closed (App a b) -> closed a /\ closed b.

Proof.

  unfold closed; firstorder.

Qed.




Lemma closed_eval:

  forall a v, eval a v -> closed a -> closed v.

Proof.

  induction 1; intros.

  auto.

  auto.

  elim (closed_App_inv _ _ H2); intros.

  apply IHeval3. apply closed_subst. auto. auto.

Qed.




Lemma not_evalinf_atom:

  forall a, evalinf a -> isatom a -> False.

Proof.

  intros. inversion H0; subst; inversion H.

Qed.




Lemma eval_atom:

  forall a, isatom a -> closed a -> eval a a.

Proof.

  induction 1; intros.

  elim (H x). simpl. auto.

  constructor.

  constructor.

Qed.




Lemma eval_atom_inv:

  forall a v, eval a v -> isatom a -> v = a.

Proof.

  intros. inversion H0; subst; inversion H; auto.

Qed.




Remark subst_omega:

  forall b, subst vx b omega = omega.

Proof.

  intros. reflexivity.

Qed.




Definition Omega := Fun vx omega.




Lemma evalinf_coeval_cps:

  forall b, evalinf b -> isbody b -> closed b -> coeval b Omega.

Proof.

  cofix COINDHYP; intros.

  inversion H0; subst; clear H0. elim (not_evalinf_atom _ H H2).

  assert (closed b0).

    red; intros. generalize (H1 x). simpl. tauto.

  assert (closed a).

    red; intros. generalize (H1 x). simpl. tauto.

  inversion H; subst.

  apply coeval_app with vx omega a. apply COINDHYP; assumption.

  apply eval_coeval. apply eval_atom; auto.

  rewrite subst_omega. apply coeval_omega.

  elim (not_evalinf_atom _ H8 H3).

  apply coeval_app with x c vb.

  apply eval_coeval; assumption.

  apply eval_coeval; assumption.

  apply COINDHYP. assumption.

  apply isbody_subst.

  generalize (eval_atom_inv _ _ H8 H3); intro. subst vb. assumption.

  eapply eval_body_fun; eauto.

  eapply closed_subst; eauto; eapply closed_eval; eauto.

Qed.




Lemma coeval_cps_characterization:

  forall b, isbody b -> closed b ->

  ((exists v, coeval b v) <-> evalinf b \/ (exists v, eval b v)).

Proof.

  intros. split.

  intros [v COEVAL].

  elim (coeval_eval_or_evalinf _ _ COEVAL); intro; firstorder.

  intros [EVALINF | [v EVAL]].

  exists Omega; apply evalinf_coeval_cps; auto.

  exists v; apply eval_coeval; auto.

Qed.