# 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               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)).   rewrite <- (C2 (max n1 n2)).   auto.   auto. 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. elimtype False; omega.   simpl. apply step_increasing.   intros. apply IHn1. omega. Qed. Lemma evaluates_total:   forall a, exists r, evaluates a r. Proof.   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. 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). omega. elim H; intros.   rewrite <- (COMP m). apply compute_increasing. auto. omega.   rewrite <- (COMP n). constructor. auto. 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. 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. 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.     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. 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; eauto. rewrite A2; eauto. 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. 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. 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.   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.   auto.   elim (evaluates_compute_either _ _ n (eval_converges _ _ H1));   intro EQ2; rewrite EQ2.   auto.   apply IHn. auto.   intros. exists 0; auto. Qed. ```