Clean up

theories/simulation/behavior.v

@@ -31,8 +31,8 @@ Section beh.
       some form of "well-formedness", so we do not define it in general and
       instead expect each language to define a suitable one. *)
 
-  (** * A more classical definition of 'behavioral refinement', equivalent to
-      the above. *)
+  (** * An ITree definition of 'behavioral refinement', which implies the refinement
+    above. *)
 
   (** First we define the possible "behaviors" of a program, and which behaviors
       we consider observably refining others (lifting O to behaviors). *)
@@ -60,7 +60,6 @@ Section beh.
   (* Divergence predicate for ITrees :
     We can characterize a predicate that states that there exists some branch
     of computation that will diverge. *)
-  (* TODO : Move to "Utils" or the like ? *)
   Inductive has_divergenceF {E X} (P : itree E X -> Prop) : itree' E X -> Prop :=
     | hDivTau : forall (t : itree E X), P t -> has_divergenceF P (TauF t)
     | hDivVis : forall {A} (k : A -> itree E X) (e: E A),
@@ -186,7 +185,7 @@ Section beh.
     induction H; inv Heqi.
   Qed.
 
-  (** * [Classical] prove of equivalence of the two notions of behavior. *)
+  (** * [Classical] prove refinement of the two notions of behavior. *)
   Lemma has_beh_ub p T σ :
     has_beh p T σ ub ↔ pool_reach_stuck p T σ.
   Proof.
@@ -283,44 +282,11 @@ Section beh.
     forall p T σ, Proper (eutt eq ==> iff) (has_beh p T σ).
   Proof.
     repeat intro.
-    split; intro HB; induction HB; try solve [econstructor; eauto].
-    - eapply HasBehStuck; auto. rewrite <- H; auto.
-    - eapply HasBehDiv; auto. rewrite <- H; auto.
-    - eapply HasBehRet; auto. rewrite <- H; auto.
-    - eapply HasBehStuck; auto. rewrite H; auto.
-    - eapply HasBehDiv; auto. rewrite H; auto.
-    - eapply HasBehRet; auto. rewrite H; auto.
+    split; intro HB; induction HB;
+      solve [econstructor; auto; try rewrite <- H; eauto |
+             econstructor; auto; try rewrite H; eauto ].
   Qed.
 
-  (* Lemma prog_ref_to_alt p_t p_s : *)
-  (*   prog_ref p_t p_s → prog_ref_alt p_t p_s. *)
-  (* Proof. *)
-  (*   intros HB σ_t σ_s b_t HI Ht. *)
-  (*   destruct (classic (reach_stuck p_s (of_call main u) σ_s)) as [HUB | HnoUB]. *)
-  (*   { exists ub. split; last by constructor. *)
-  (*     apply has_beh_ub. done. } *)
-  (*   specialize (HB _ _ HI HnoUB). destruct HB as (Hdiv & Hret & Hsafe). *)
-  (*   remember ([of_call main u]). *)
-  (*   remember b_t. remember p_t. *)
-  (*   assert (Ht' := Ht). *)
-  (*   induction Ht. *)
-  (*   - (* Stuck *) exfalso. subst. *)
-  (*     rewrite H0 in Ht'. apply has_beh_ub in Ht'. apply Hsafe. done. *)
-  (*   - (* Div *) *)
-  (*     exists t. split; [ | apply ObsBehEutt]. *)
-  (*     { subst. apply has_beh_div, Hdiv; auto. } *)
-  (*     subst. *)
-  (*     apply has_beh_div in Ht'; auto. *)
-  (*     admit. *)
-  (*   - (* Ret *) subst. rewrite H in Ht'. *)
-  (*     apply has_beh_ret in Ht' as (T_t' & σ_t' & J_t & Hsteps_t). *)
-  (*     destruct (Hret _ _ _ _ Hsteps_t) as (v_s' & T_s' & σ_s' & J_s & Hsteps_s & HO). *)
-  (*     exists (Ret v_s'). split; [| apply ObsBehEutt]. *)
-  (*     + apply has_beh_ret. eauto. *)
-  (*     + rewrite H. apply eqit_Ret; auto. *)
-  (*   - (* Step *) *)
-  (* Admitted. *)
-
   (* More itree utility lemmas *)
   Lemma eutt_inv_Ret_r {E A} (t : itree E A) r (RR : A -> A -> Prop) :
     eutt RR t (Ret r) -> exists r', t ≈ Ret r'.
@@ -376,7 +342,6 @@ Section beh.
         eapply eutt_inv_Ret_l in H. destruct H.
         rewrite H in Hbeh_s.
         rewrite H in Hrel.
-
         apply has_beh_ret in Hbeh_s.
         destruct Hbeh_s as (T' & σ' & I' & Hbeh_s).
         eexists x, _, _, _. split; eauto.
@@ -412,10 +377,4 @@ Section beh.
         rewrite H0 in Hbeh_s. done.
   Qed.
 
-  Lemma prog_ref_equiv p_t p_s :
-    prog_ref p_t p_s ↔ prog_ref_alt p_t p_s.
-  Proof.
-    split; eauto using prog_ref_to_alt, prog_ref_from_alt.
-  Qed.
-
 End beh.