Module densem


From Coq Require Import Classical Lia Arith.
Require Import semantics.

Connections with a simple form of denotational semantics.

Inductive result : Type :=
  | 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
              end
          end
      end
  end.

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

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.
Proof.
  intros a r1 r2 [n1 C1] [n2 C2].
  rewrite <- (C1 (max n1 n2)) by lia.
  rewrite <- (C2 (max n1 n2)) by lia.
  auto.
Qed.

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)).
Proof.
  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.
Qed.

Lemma compute_increasing:
  forall n1 n2 a, n1 <= n2 -> result_le (compute n1 a) (compute n2 a).
Proof.
  induction n1; simpl; intros.
  constructor.
  destruct n2. lia.
  simpl. apply step_increasing.
  intros. apply IHn1. lia.
Qed.

Lemma evaluates_total:
  forall a, exists r, evaluates a r.
Proof.
  intro. elim (classic (forall n, compute n a = Bottom)); intros.
- exists Bottom, 0; intros; auto.
- apply not_all_ex_not in H. destruct H as [n EQ].
  exists (compute n a), n; intros.
  generalize (compute_increasing _ _ a H); intro.
  inversion H0. auto. congruence.
Qed.

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

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

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

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

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

Lemma converges_eval:
  forall a v, evaluates a (Result v) -> eval a v.
Proof.
  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.
  - inversion H. constructor.
  - destruct (compute n a1) eqn:COMP1; try congruence.
    destruct (compute n a2) eqn:COMP2; try congruence.
    destruct t; try congruence.
    econstructor; eauto.
  }
  intros a v [n COMP]. apply H with n. apply COMP. lia.
Qed.

Lemma eval_converges:
  forall a v, eval a v -> evaluates a (Result v).
Proof.
  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 by lia. rewrite A2 by lia. apply A3; lia.
Qed.

Lemma diverges_evalinf:
  forall a, evaluates a Bottom -> evalinf a.
Proof.
  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 by lia. rewrite COMP2 by lia. congruence.
+ assert (exists x, exists b, t = Fun x b).
  { generalize (H0 (S (max n1 n2))); simpl.
    rewrite COMP1 by lia. rewrite COMP2 by lia.
    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 by lia. rewrite COMP2 by lia. auto.
Qed.

Lemma evalinf_diverges:
  forall a, evalinf a -> evaluates a Bottom.
Proof.
  assert (forall n a, evalinf a -> compute n a = Bottom).
  { induction n; intros.
  - reflexivity.
  - inversion H; simpl.
  + (* function part diverges *)
    rewrite IHn; auto.
  + (* argument part diverges *)
    elim (evaluates_compute_either _ _ n (eval_converges _ _ H0));
    intro EQ1; rewrite EQ1.
    auto. rewrite (IHn b); auto.
  + (* body diverges *)
    elim (evaluates_compute_either _ _ n (eval_converges _ _ H0));
    intro EQ1; rewrite EQ1.
    auto.
    elim (evaluates_compute_either _ _ n (eval_converges _ _ H1));
    intro EQ2; rewrite EQ2.
    auto.
    apply IHn. auto.
  }
  intros. exists 0; auto.
Qed.
Generated by coq2html