Library densem

Require Import Classical.
Require Import semantics.
Require Omega.
Require Import Arith.
Require Import Max.
Hint Resolve le_refl le_trans le_max_l le_max_r.

Connections with a simple form of denotational semantics.

Inductive result : Set :=
  | Bottom: result   | Error: result   | Result: term -> result.
Definition step (rec: term -> result) (a: term) : result :=
  match a with
  | Var v => Error
  | Const n => Result (Const n)
  | Fun v b => Result (Fun v b)
  | App b c =>
      match rec b with
      | Bottom => Bottom
      | Error => Error
      | Result vb =>
          match rec c with
          | Bottom => Bottom
          | Error => Error
          | Result vc =>
              match vb with
              | Fun x d => rec (subst x vc d)
              | _ => Error

Fixpoint compute (n: nat) : term -> result :=
  match n with
  | O => (fun a => Bottom)
  | S n1 => step (compute n1)

Definition evaluates (a: term) (r: result) : Prop :=
  exists n, forall m, n <= m -> compute m a = r.

Lemma evaluates_unique:
  forall a r1 r2, evaluates a r1 -> evaluates a r2 -> r1 = r2.
  intros a r1 r2 [n1 C1] [n2 C2].
  rewrite <- (C1 (max n1 n2)).
  rewrite <- (C2 (max n1 n2)).
  auto. auto.

Inductive result_le: result -> result -> Prop :=
  | result_le_refl:
      forall r, result_le r r
  | result_le_bot:
      forall r, result_le Bottom r.

Lemma step_increasing:
  forall (rec1 rec2: term -> result),
  (forall a, result_le (rec1 a) (rec2 a)) ->
  (forall a, result_le (step rec1 a) (step rec2 a)).
  intros. destruct a; simpl; try constructor.
  generalize (H a1); intro; inversion H0; try constructor.
  destruct (rec1 a1); try constructor.
  generalize (H a2); intro; inversion H2; try constructor.
  destruct (rec1 a2); try constructor.
  destruct t; auto || constructor.

Lemma compute_increasing:
  forall n1 n2 a, n1 <= n2 -> result_le (compute n1 a) (compute n2 a).
  induction n1; simpl; intros.
  destruct n2. elimtype False; omega.
  simpl. apply step_increasing.
  intros. apply IHn1. omega.

Lemma evaluates_total:
  forall a, exists r, evaluates a r.
  intro. elim (classic (forall n, compute n a = Bottom)); intros.
  exists Bottom; exists 0; intros; auto.
  assert (exists n, compute n a <> Bottom).
    change (exists n, ~((fun m => compute m a = Bottom) n)).
    apply not_all_ex_not. assumption.
  destruct H0 as [n EQ].
  exists (compute n a); exists n; intros.
  generalize (compute_increasing _ _ a H0); intro.
  inversion H1. auto. congruence.

Lemma evaluates_limsup:
  forall a r n, evaluates a r -> result_le (compute n a) r.
  intros a r n [m COMP].
  assert (n <= m \/ m <= n). omega. elim H; intros.
  rewrite <- (COMP m). apply compute_increasing. auto. omega.
  rewrite <- (COMP n). constructor. auto.

Lemma evaluates_compute_either:
  forall a r n, evaluates a r -> compute n a = Bottom \/ compute n a = r.
  intros. generalize (evaluates_limsup _ _ n H); intro.
  inversion H0; auto.

Lemma compute_converges:
  forall n a v, compute n a = Result v -> evaluates a (Result v).
  intros. exists n. intros.
  generalize (compute_increasing n m a H0); rewrite H; intro.
  inversion H1; auto.

Lemma compute_gets_stuck:
  forall n a, compute n a = Error -> evaluates a Error.
  intros. exists n. intros.
  generalize (compute_increasing n m a H0); rewrite H; intro.
  inversion H1; auto.

Ltac caseEq name :=
  generalize (refl_equal name); pattern name at -1 in |- *; case name.

Lemma compute_diverges:
  forall a, evaluates a Bottom -> forall n, compute n a = Bottom.
  intros. elim (evaluates_compute_either a Bottom n H); congruence.

Lemma converges_eval:
  forall a v, evaluates a (Result v) -> eval a v.
  assert (forall n a v, compute n a = Result v -> eval a v).
    induction n; intros until v; destruct a; simpl; try congruence.
    intro. inversion H. constructor.
    intro. inversion H. constructor.
    caseEq (compute n a1); try congruence.
    intros v1 COMP1.
    caseEq (compute n a2); try congruence.
    intros v2 COMP2.
    destruct v1; try congruence. intro COMP3.
    econstructor; eauto.
  intros a v [n COMP]. apply H with n. apply COMP. omega.

Lemma eval_converges:
  forall a v, eval a v -> evaluates a (Result v).
  induction 1.
  apply compute_converges with 1. reflexivity.
  apply compute_converges with 1. reflexivity.
  destruct IHeval1 as [n1 A1].
  destruct IHeval2 as [n2 A2].
  destruct IHeval3 as [n3 A3].
  apply compute_converges with (S (max n1 (max n2 n3))). simpl.
  rewrite A1; eauto. rewrite A2; eauto.

Lemma diverges_evalinf:
  forall a, evaluates a Bottom -> evalinf a.
  cofix COINDHYP; intros. generalize (compute_diverges a H); intro.
  destruct a; try (generalize (H0 1); simpl; congruence).
  destruct (evaluates_total a1) as [r1 EVAL1].
  elim EVAL1; intros n1 COMP1.
  destruct r1.
  apply evalinf_app_l. auto.
  generalize (H0 (S n1)); simpl. rewrite COMP1. congruence. auto.
  destruct (evaluates_total a2) as [r2 EVAL2].
  elim EVAL2; intros n2 COMP2.
  destruct r2.
  apply evalinf_app_r with t. apply converges_eval; auto. auto.
  generalize (H0 (S (max n1 n2))); simpl.
  rewrite COMP1. rewrite COMP2. congruence. eauto. eauto.
  assert (exists x, exists b, t = Fun x b).
    generalize (H0 (S (max n1 n2))); simpl.
    rewrite COMP1; eauto. rewrite COMP2; eauto.
    destruct t; intros; try congruence.
    exists v; exists t; auto.
  destruct H1 as [x [b EQ]]. subst t.
  apply evalinf_app_f with x b t0.
  apply converges_eval; auto.
  apply converges_eval; auto.
  apply COINDHYP. exists (max n1 n2); intros.
  generalize (H0 (S m)). simpl.
  rewrite COMP1; eauto. rewrite COMP2; eauto.

Lemma evalinf_diverges:
  forall a, evalinf a -> evaluates a Bottom.
  assert (forall n a, evalinf a -> compute n a = Bottom).
  induction n; intros.
  inversion H; simpl.
  rewrite IHn; auto.
  elim (evaluates_compute_either _ _ n (eval_converges _ _ H0));
  intro EQ1; rewrite EQ1.
  auto. rewrite (IHn b); auto.
  elim (evaluates_compute_either _ _ n (eval_converges _ _ H0));
  intro EQ1; rewrite EQ1.
  elim (evaluates_compute_either _ _ n (eval_converges _ _ H1));
  intro EQ2; rewrite EQ2.
  apply IHn. auto.

  intros. exists 0; auto.