Merge branch 'robbert/fill' into 'master'

More consistent names for `fill` lemmas of `LanguageCtx`.

See merge request iris/iris!389

CHANGELOG.md

@@ -67,6 +67,13 @@ Coq development, but not every API-breaking change is listed.  Changes marked
   PROP-level binary relations.
 * Add new introduction pattern `-# pat` that moves a hypothesis from the
   intuitionistic context to the spatial context.
+* Made lemma names for `fill` more consistent
+  - Use the `_inv` suffix for the the backwards directions:
+   `reducible_fill` → `reducible_fill_inv`,
+   `reducible_no_obs_fill` → `reducible_no_obs_fill_inv`,
+   `not_stuck_fill` → `not_stuck_fill_inv`.
+  - Use the non-`_inv` names (that freed up) for the forwards directions:
+   `reducible_fill`, `reducible_no_obs_fill`, `irreducible_fill_inv`.
 
 **Changes in heap_lang:**
 

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_fill (fill K))]
+                    apply IH; [done| by eapply (not_stuck_fill_inv (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_fill (fill [ResolveMCtx _ _])); simpl].
+                 by eapply (not_stuck_fill_inv (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_fill (fill [ResolveRCtx _ _])); simpl].
+                 by eapply (not_stuck_fill_inv (fill [ResolveRCtx _ _])); simpl].
 Qed.
 
 Lemma erased_prim_step_prim_step e1 σ1 κ e2 σ2 efs:

theories/program_logic/language.v

@@ -153,12 +153,18 @@ Section language.
   Proof. unfold Atomic. destruct a; eauto using val_irreducible. Qed.
 
   Lemma reducible_fill `{!@LanguageCtx Λ K} e σ :
+    reducible e σ → reducible (K e) σ.
+  Proof. unfold reducible in *. naive_solver eauto using fill_step. Qed.
+  Lemma reducible_fill_inv `{!@LanguageCtx Λ K} e σ :
     to_val e = None → reducible (K e) σ → reducible e σ.
   Proof.
     intros ? (e'&σ'&k&efs&Hstep); unfold reducible.
     apply fill_step_inv in Hstep as (e2' & _ & Hstep); eauto.
   Qed.
   Lemma reducible_no_obs_fill `{!@LanguageCtx Λ K} e σ :
+    reducible_no_obs e σ → reducible_no_obs (K e) σ.
+  Proof. unfold reducible_no_obs in *. naive_solver eauto using fill_step. Qed.
+  Lemma reducible_no_obs_fill_inv `{!@LanguageCtx Λ K} e σ :
     to_val e = None → reducible_no_obs (K e) σ → reducible_no_obs e σ.
   Proof.
     intros ? (e'&σ'&efs&Hstep); unfold reducible_no_obs.
@@ -166,19 +172,22 @@ Section language.
   Qed.
   Lemma irreducible_fill `{!@LanguageCtx Λ K} e σ :
     to_val e = None → irreducible e σ → irreducible (K e) σ.
+  Proof. rewrite -!not_reducible. naive_solver eauto using reducible_fill_inv. Qed.
+  Lemma irreducible_fill_inv `{!@LanguageCtx Λ K} e σ :
+    irreducible (K e) σ → irreducible e σ.
   Proof. rewrite -!not_reducible. naive_solver eauto using reducible_fill. Qed.
 
-  Lemma not_stuck_fill K `{!@LanguageCtx Λ K} e σ :
+  Lemma not_stuck_fill_inv 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.
+    - destruct (decide (to_val e = None)); auto using reducible_fill_inv.
   Qed.
 
   Lemma stuck_fill `{!@LanguageCtx Λ K} e σ :
     stuck e σ → stuck (K e) σ.
-  Proof. rewrite -!not_not_stuck. eauto using not_stuck_fill. Qed.
+  Proof. rewrite -!not_not_stuck. eauto using not_stuck_fill_inv. 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).

theories/program_logic/total_weakestpre.v

@@ -186,7 +186,7 @@ Proof.
     iApply (twp_pre_mono with "[] IH"). by iIntros "!>" (E e Φ') "[_ ?]". }
   rewrite /twp_pre fill_not_val //.
   iIntros (σ1 κs n) "Hσ". iMod ("IH" with "[$]") as "[% IH]". iModIntro; iSplit.
-  { destruct s; eauto using reducible_no_obs_fill. }
+  { destruct s; eauto using reducible_no_obs_fill_inv. }
   iIntros (κ e2 σ2 efs Hstep).
   iMod ("IH" $! κ (K e2) σ2 efs with "[]") as (?) "(Hσ & IH & IHefs)"; eauto using fill_step.
   iModIntro. iFrame "Hσ". iSplit; first done. iSplitR "IHefs".
@@ -199,7 +199,7 @@ Proof.
   iIntros "H". iLöb as "IH" forall (E e Φ).
   rewrite wp_unfold twp_unfold /wp_pre /twp_pre. destruct (to_val e) as [v|]=>//.
   iIntros (σ1 κ κs n) "Hσ". iMod ("H" with "Hσ") as "[% H]". iIntros "!>". iSplitR.
-  { destruct s; last done. eauto using reducible_no_obs_reducible. }
+  { destruct s; eauto using reducible_no_obs_reducible. }
   iIntros (e2 σ2 efs) "Hstep". iMod ("H" with "Hstep") as (->) "(Hσ & H & Hfork)".
   iApply step_fupd_intro; [set_solver+|]. iNext.
   iFrame "Hσ". iSplitL "H". by iApply "IH".

theories/program_logic/weakestpre.v

@@ -160,8 +160,7 @@ Proof.
   { apply of_to_val in He as <-. by iApply fupd_wp. }
   rewrite wp_unfold /wp_pre fill_not_val //.
   iIntros (σ1 κ κs n) "Hσ". iMod ("H" with "[$]") as "[% H]". iModIntro; iSplit.
-  { iPureIntro. destruct s; last done.
-    unfold reducible in *. naive_solver eauto using fill_step. }
+  { destruct s; eauto using reducible_fill. }
   iIntros (e2 σ2 efs Hstep).
   destruct (fill_step_inv e σ1 κ e2 σ2 efs) as (e2'&->&?); auto.
   iMod ("H" $! e2' σ2 efs with "[//]") as "H". iIntros "!>!>".
@@ -177,7 +176,7 @@ Proof.
   { apply of_to_val in He as <-. by rewrite !wp_unfold /wp_pre. }
   rewrite fill_not_val //.
   iIntros (σ1 κ κs n) "Hσ". iMod ("H" with "[$]") as "[% H]". iModIntro; iSplit.
-  { destruct s; eauto using reducible_fill. }
+  { destruct s; eauto using reducible_fill_inv. }
   iIntros (e2 σ2 efs Hstep).
   iMod ("H" $! (K e2) σ2 efs with "[]") as "H"; [by eauto using fill_step|].
   iIntros "!>!>". iMod "H" as "(Hσ & H & Hefs)".