Rename lemma `not_stuck_under_ectx` → `not_stuck_fill`, to be consistent with `stuck_fill`.

Also refactor the proofs to make better reuse of existing lemmas.

theories/heap_lang/proph_erasure.v

@@ -470,7 +470,7 @@ Proof.
             lazymatch K with
             | [] => fail
             | _ => apply (prim_step_matched_by_erased_steps_ectx K);
-                    apply IH; [done| by eapply (not_stuck_under_ectx (fill K))]
+                    apply IH; [done| by eapply (not_stuck_fill (fill K))]
             end
         in
         reshape_expr e tac
@@ -587,11 +587,11 @@ Proof.
         end.
       apply (prim_step_matched_by_erased_steps_ectx [ResolveMCtx _ _]).
       apply IH; [rewrite !app_length /=; lia|done|
-                 by eapply (not_stuck_under_ectx (fill [ResolveMCtx _ _])); simpl].
+                 by eapply (not_stuck_fill (fill [ResolveMCtx _ _])); simpl].
   - (** e1 is of the form ([Resolve] e1_ e1_2 e13) and e1_3 takes a prim_step. *)
     apply (prim_step_matched_by_erased_steps_ectx [ResolveRCtx _ _]).
     apply IH; [rewrite !app_length /=; lia|done|
-                 by eapply (not_stuck_under_ectx (fill [ResolveRCtx _ _])); simpl].
+                 by eapply (not_stuck_fill (fill [ResolveRCtx _ _])); simpl].
 Qed.
 
 Lemma erased_prim_step_prim_step e1 σ1 κ e2 σ2 efs:

theories/program_logic/language.v

@@ -168,9 +168,17 @@ Section language.
     to_val e = None → irreducible e σ → irreducible (K e) σ.
   Proof. rewrite -!not_reducible. naive_solver eauto using reducible_fill. Qed.
 
+  Lemma not_stuck_fill K `{!@LanguageCtx Λ K} e σ :
+    not_stuck (K e) σ → not_stuck e σ.
+  Proof.
+    rewrite /not_stuck -!not_eq_None_Some. intros [?|?].
+    - auto using fill_not_val.
+    - destruct (decide (to_val e = None)); auto using reducible_fill.
+  Qed.
+
   Lemma stuck_fill `{!@LanguageCtx Λ K} e σ :
     stuck e σ → stuck (K e) σ.
-  Proof. intros [??]. split. by apply fill_not_val. by apply irreducible_fill. Qed.
+  Proof. rewrite -!not_not_stuck. eauto using not_stuck_fill. Qed.
 
   Lemma step_Permutation (t1 t1' t2 : list (expr Λ)) κ σ1 σ2 :
     t1 ≡ₚ t1' → step (t1,σ1) κ (t2,σ2) → ∃ t2', t2 ≡ₚ t2' ∧ step (t1',σ1) κ (t2',σ2).
@@ -235,16 +243,6 @@ Section language.
     rtc pure_step e1 e2 → rtc pure_step (K e1) (K e2).
   Proof. eauto using rtc_congruence, pure_step_ctx. Qed.
 
-  Lemma not_stuck_under_ectx K `{!@LanguageCtx Λ K} e σ :
-    not_stuck (K e) σ → not_stuck e σ.
-  Proof.
-    rewrite /not_stuck /reducible /=.
-    intros [[? HK]|(?&?&?&?&Hstp)]; simpl in *.
-    - left. apply not_eq_None_Some; intros ?%fill_not_val; simplify_eq.
-    - destruct (to_val e) eqn:?; first by left; eauto.
-      apply fill_step_inv in Hstp; naive_solver.
-  Qed.
-
   (* We do not make this an instance because it is awfully general. *)
   Lemma pure_exec_ctx K `{!@LanguageCtx Λ K} φ n e1 e2 :
     PureExec φ n e1 e2 →