Fix more cleanup subtleties when multiple goals are spawned, fix bad order if...

Fix more cleanup subtleties when multiple goals are spawned, fix bad order if both spatial and intuitionistic context get used

diaframe/lib/laterable.v

@@ -120,7 +120,7 @@ Section laterable_hyp.
   Proof.
     rewrite /AtomIntoWand /IntoWand2 /= later_part_of_eq pers_part_of_eq.
     iStep 3 as (E) "HPL1 HPL2".
-    by iMod ("HPL2" with "HPL1") as "$".
+    by iMod ("HPL1" with "HPL2") as "$".
   Qed.
 
   Global Instance pers_part_pers (L P : PROP) : Persistent (pers_part_of L P).

diaframe/steps/ipm_hyp_renamer.v

@@ -8,10 +8,11 @@ Ltac2 rec read_ipm_hyp_names_from_env (env : constr) : string list :=
   | Esnoc ?env' (IAnon _) _ => (read_ipm_hyp_names_from_env env')
   end.
 
+(* We reverse the result since Env are snoc-lists *)
 Ltac2 read_ipm_hyp_names (delta : constr) : string list :=
   lazy_match! delta with
   | Envs ?gamma_i ?gamma_s _ =>
-    List.append (read_ipm_hyp_names_from_env gamma_i) (read_ipm_hyp_names_from_env gamma_s)
+    List.rev (List.append (read_ipm_hyp_names_from_env gamma_s) (read_ipm_hyp_names_from_env gamma_i))
   end.
 
 Ltac2 get_ipm_hyp_names (_ : unit) : string list :=
@@ -122,8 +123,8 @@ Ltac2 rename_ipm_hyps_after_base
       List.map (fun mi => match mi with Some i => i | _ => Control.throw Not_found end) (
         List.filter (fun i => match i with Some _ => true | _ => false end) (Array.to_list name_store)
       ) in
-                (* Need to reverse since Env are snoc-lists, which feels reversed to the user *)
-    let to_rename := List.rev (List.filter (fun i => Bool.neg (List.mem string_equal i remaining_names)) current_names) in
+
+    let to_rename := List.filter (fun i => Bool.neg (List.mem string_equal i remaining_names)) current_names in
 
     let new_names_len := List.length new_names in
     let to_rename_len := List.length to_rename in
@@ -229,4 +230,9 @@ Proof.
   Fail reintro_ipm_delete_handle (fun d => iIntros "H1 H2 H3"; d ("HP")) as "HP HQ HR HS".
 Abort.
 
+Lemma test_order_pers {PROP : bi} (P Q R S : PROP) : ⊢ P -∗ □ Q -∗ □ R -∗ S -∗ False.
+Proof.
+  reintro_ipm_after (iIntros "H1 #H2 #H3 H4") as "HQ HR HP HS".
+Abort.
+
 

diaframe/utils_ltac2.v

@@ -20,11 +20,23 @@ Ltac2 is_solved_goal (_ : unit) :=
   Control.enter (fun _ => cell.(contents) := true);
   Bool.neg (cell.(contents)).
 
+Ltac2 count_goals (_ : unit) :=
+  let cnt : int ref := { contents := 0} in
+  Control.enter (fun _ =>
+    (* TODO: is this run concurrently? *)
+    cnt.(contents) := Int.add (cnt.(contents)) 1
+  );
+  cnt.(contents).
+
+Ltac2 focus_last (continuation : unit -> 'a) : 'a :=
+  let n := count_goals () in
+  Control.focus n n continuation.
+
 Ltac2 find_fresh_idents_between (u : unit) : (unit -> ident list) * (unit -> unit) :=
   (** If this function is called, it returns two closure. If the first
      closure is called on a single goal, it will return all the idents that have
-     been newly introduced into the Coq context. If no goals remain,
-     you are required to call the second closure for clean up *)
+     been newly introduced into the Coq context. Once you are done,
+     you are required to call the second closure to clean up *)
 
   (** Unfortunately, doing that is a bit more complicated than looking 
     at the difference between two calls to [Control.hyps ()]. That approach
@@ -65,7 +77,8 @@ Ltac2 find_fresh_idents_between (u : unit) : (unit -> ident list) * (unit -> uni
      The client should manually check if all goals get solved and call the below cleanup
      closure to get rid of the uninstantiated evar. *)
   let cleanup := (fun _ => 
-    Control.new_goal raw_evar; exact I
+    Control.new_goal raw_evar; 
+    focus_last (fun _ => exact I)
   ) in
 
   (* and return the closure: *)
@@ -94,9 +107,9 @@ Ltac2 find_fresh_idents_between (u : unit) : (unit -> ident list) * (unit -> uni
       These are the idents which have been 'kept' since this closure was generated. *)
     let kept_idents := List.filter (fun i => List.mem Ident.equal i old_idents) new_idents_only in
 
-    (* We now have all information we need, so get rid of the evar *)
-    unify $refreshed_evar I;
+    (* We now have all the information we need. We clear (but do not unify!) the evar from this goal. *)
     Std.clear [checkme];
+    (* We do not unify so that other goals can still read the required information from the evar. *)
 
     (* We return precisely the idents which are not in [kept_idents] *)
     List.filter (fun i => Bool.neg (List.mem Ident.equal i kept_idents)) (get_idents ())
@@ -176,9 +189,10 @@ Ltac2 reintroduce_with_pats (b : ReintroductionWarningBehavior)
     | Silent => run_intros ()
     | Verbose =>
       (* To obtain and print the actual names, we reuse [find_fresh_idents_between] *)
-      let (f, _) := find_fresh_idents_between () in
+      let (f, cleanup) := find_fresh_idents_between () in
       run_intros ();
       let new_idents := f () in
+      cleanup ();
       List.iter (fun i =>
         printf "Please supply a name for  %I : %t" i (Constr.type (Control.hyp i))
       ) new_idents
@@ -190,14 +204,14 @@ Ltac2 rename_after_closure (b : ReintroductionWarningBehavior)
   (closure : unit -> unit) :=
   let (f, cleanup) := find_fresh_idents_between () in
   closure ();
-  if is_solved_goal () then cleanup() else
   Control.enter (fun _ =>
     (* need to use Control.enter to force application of below to single goals. 
         If no goals remain, this is essentially unit. *)
     let new_idents := f () in
     let raw_pat_list := Option.get (Ltac1.to_list raw_intro_pats) in
     reintroduce_with_pats Verbose new_idents raw_pat_list
-  ).
+  );
+  cleanup ().
 
 Module test_reintro.
   Local Tactic Notation "reintro_after" tactic(the_tac) "as" ne_simple_intropattern_list(xs) :=
@@ -215,6 +229,11 @@ Module test_reintro.
     reintro_after (do 2 intro; subst; intro x; intro) as a b Hb. Undo 1.
     reintro_after (do 2 intro; subst; intro x; intro; exact I) as a b Hb.
   Qed.
+
+  Lemma test2 : (forall (b : bool), b = b) /\ (forall (n : nat), n = n).
+  Proof.
+    reintro_after (split; intro) as x. (* TODO: what if we want to give these different names? *)
+  Abort.
 End test_reintro.
 
 

diaframe_heap_lang/base_hints.v

@@ -24,8 +24,8 @@ Section instances.
     Proof.
       rewrite /MergableConsume => p Pin Pout [-> ->].
       rewrite bi.intuitionistically_if_elim.
-      iStep.
-      iDestruct (mapsto_combine with "H1 H2") as "[H ->]".
+      iStep as "Hl1 Hl2".
+      iDestruct (mapsto_combine with "Hl1 Hl2") as "[_ ->]".
       iSteps.
     Qed.
 
@@ -37,8 +37,8 @@ Section instances.
     Proof.
       rewrite /MergableConsume => p Pin Pout [-> [+ ->]].
       rewrite bi.intuitionistically_if_elim => Hq.
-      iStep.
-      iDestruct (mapsto_combine with "H1 H2") as "[H ->]".
+      iStep as "Hl1 Hl2".
+      iDestruct (mapsto_combine with "Hl1 Hl2") as "[H ->]".
       rewrite dfrac_op_own Hq.
       iDestruct (mapsto_valid with "H") as %Hl.
       rewrite dfrac_valid_own in Hl.
@@ -50,8 +50,8 @@ Section instances.
     Proof.
       rewrite /MergableConsume => p Pin Pout [-> ->].
       rewrite bi.intuitionistically_if_elim.
-      iStep.
-      iDestruct (mapsto_combine with "H1 H2") as "[H ->]".
+      iStep as "Hl1 Hl2".
+      iDestruct (mapsto_combine with "Hl1 Hl2") as "[H ->]".
       iDestruct (mapsto_valid with "H") as %?%dfrac_valid_own_l.
       iSteps.
     Qed.
@@ -70,8 +70,8 @@ Section instances.
     Proof.
       rewrite /MergableConsume => p Pin Pout [-> ->].
       rewrite bi.intuitionistically_if_elim.
-      iStep.
-      iDestruct (mapsto_combine with "H1 H2") as "[H ->]".
+      iStep as "Hl1 Hl2".
+      iDestruct (mapsto_combine with "Hl1 Hl2") as "[H ->]".
       iSteps.
     Qed.
 
@@ -112,8 +112,8 @@ Section instances.
       HINT l ↦{#q1} v1 ✱ [- ; ⌜v1 = v2⌝] ⊫ [id]; l ↦{#q2}v2 ✱ [⌜v1 = v2⌝ ∗ match mq with | Some q => l ↦{#q} v1 | _ => True end] | 54.
     Proof.
       rewrite /= /FracSub => <-.
-      destruct mq; iSteps.
-      iDestruct "H1" as "[H1 H1']".
+      destruct mq; iSteps as "Hl".
+      iDestruct "Hl" as "[Hl Hl']".
       iSteps.
     Qed.
 
@@ -172,9 +172,9 @@ Section instances.
            (l ↦∗{q} take (Z.to_nat i) vs) ∗ ⌜vs !! Z.to_nat i = Some v⌝ ∗ (l' ↦∗{q} drop (S $ Z.to_nat i) vs)] | 20.
     Proof.
       rewrite /SolveSepSideCondition /= => Hi ->.
-      iStep.
-      rewrite -{1}(take_drop_middle _ _ _ H).
-      rewrite array_app array_cons; iRevert "H1"; iStep.
+      iStep as (Hvs) "Hl".
+      rewrite -{1}(take_drop_middle _ _ _ Hvs).
+      rewrite array_app array_cons; iRevert "Hl"; iStep as "Hl Hli Hli'".
       rewrite take_length_le; last lia.
       rewrite Z2Nat.id; last lia.
       iSteps.
@@ -189,8 +189,8 @@ Section instances.
            l ↦∗{q} vs2 ✱ [emp] | 51.
     Proof.
       rewrite /SolveSepSideCondition => Hl -> /=.
-      iStep.
-      rewrite -{2}(take_drop (length vs1) vs2) H array_app.
+      iStep as (Hvs) "Hl Hvs".
+      rewrite -{2}(take_drop (length vs1) vs2) Hvs array_app.
       iSteps.
     Qed.
 
@@ -205,7 +205,7 @@ Section instances.
     Global Instance fork_abduct e (Φ : val → iPropI Σ) s E :
       HINT1 ε₁ ✱ [▷ Φ #() ∗ ▷ WP e @ s; ⊤ {{ _, True }}] ⊫ [id]; wp s E (Fork e) Φ.
     Proof. (* eliding the type of Φ will give fork_abduct weird unsimplified (and ununifiable!) TeleO -t> T types *)
-      iSteps. iApply (wp_fork with "H2"). iSteps.
+      iSteps as "HΦ HWP". iApply (wp_fork with "HWP"). iSteps.
     Qed.
   End abds.
 

diaframe_heap_lang/specs.v

@@ -50,8 +50,8 @@ Section heap_lang_instances.
   Global Instance load_step_wp l E1 E2 s :
     SPEC ⟨E1, E2⟩ v q, {{ ▷ l ↦{q} v }} ! #l @ s {{ RET v; l ↦{q} v }}.
   Proof.
-    iSteps.
-    iApply (wp_load with "H1").
+    iSteps as (v q) "Hl".
+    iApply (wp_load with "Hl").
     iSteps.
   Qed.
 
@@ -78,16 +78,16 @@ Section heap_lang_instances.
   Global Instance store_step_wp l v' E1 E2 s :
     SPEC ⟨E1, E2⟩ v, {{ ▷ l ↦ v }} #l <- v' @ s {{ RET #(); l ↦ v' }}.
   Proof.
-    iSteps.
-    iApply (wp_store with "H1").
+    iSteps as (v) "Hl".
+    iApply (wp_store with "Hl").
     iSteps.
   Qed.
 
   Global Instance free_step_wp l E1 E2 s :
     SPEC ⟨E1, E2⟩ v, {{ ▷ l ↦ v }} Free #l @ s {{ RET #(); True }}.
   Proof.
-    iSteps.
-    iApply (wp_free with "H1").
+    iSteps as (v) "Hl".
+    iApply (wp_free with "Hl").
     iSteps.
   Qed.
 
@@ -112,19 +112,19 @@ Section heap_lang_instances.
           ⊫ [id]; WP e_in @ s ; E1 {{ Φ }} | 45.
   Proof.
     case => -> [HK [He1 [He3 He2]]] HLU HM1 HM2 Hev'.
-    iStep. iApply wp_bind. iMod "H2" as (pvs) "[Hp Hwp]".
+    iStep as "Hpre HL". iApply wp_bind. iMod "HL" as (pvs) "[Hp Hwp]".
     { apply resolve_atomic. destruct s; try tc_solve. }
     iApply (wp_resolve with "Hp"). apply He2. simpl.
     iDestruct "Hwp" as (ttl) "[Hl HΦ]".
     rewrite /ReductionStep' /ReductionTemplateStep in HLU.
-    iPoseProof (HLU with "H1") as "HWP". simpl.
+    iPoseProof (HLU with "Hpre") as "HWP". simpl.
     iApply "HWP". iApply HM1 => /=.
     iExists ttl. iFrame. iIntros "!>" (tt2) "HU". iApply HM2 => /=.
     revert Hev'. rewrite /TCTForall /IntoVal => /(dep_eval_tele ttl) /(dep_eval_tele tt2) => Hev'.
     rewrite -Hev'.
     iApply wp_value. iIntros (pvs').
-    iStep.
-    iStep. iSpecialize ("H8" $! pvs' tt2). rewrite -Hev'. iApply "H8".
+    iStep 2 as "Hpost Hproph".
+    iSpecialize ("Hpost" $! pvs' tt2). rewrite -Hev'. iApply "Hpost".
     iSteps.
   Qed.
 
@@ -136,9 +136,10 @@ Section heap_lang_instances.
           ⊫ [id]; WP e_in @ s ; E1 {{ Φ }} | 45.
   Proof.
     case => -> HK.
-    iStep. iApply wp_bind. iMod "H1". iReIntro "H1".
-    iApply (wp_resolve with "H2"). done.
-    wp_pures. do 3 iStep. iMod ("H3" with "[H4]"); iSteps.
+    iStep as "H". iApply wp_bind. iMod "H". iDecompose "H" as (ps) "Hproph Hpost".
+    iApply (wp_resolve with "Hproph"). done.
+    wp_pures. iStep 3 as (ps') "Hpost Hproph". 
+    iMod ("Hpost" with "[Hproph]"); iSteps.
   Qed.
 
   Opaque vals_compare_safe.
@@ -152,13 +153,13 @@ Section heap_lang_instances.
           ⌜b = true⌝ ∗ ⌜v = v1⌝ ∗ l ↦{q} v2   ∨
           ⌜b = false⌝ ∗ ⌜v ≠ v1⌝ ∗ l ↦{q} v }}.
   Proof.
-    iSteps.
-    - destruct (decide (x = v1)) as [->|Hneq].
-      * iApply (wp_cmpxchg_suc with "H1") => //.
+    iStep 3 as (v q Hv1 Hv2) "Hl".
+    - destruct (decide (v = v1)) as [->|Hneq].
+      * iApply (wp_cmpxchg_suc with "Hl") => //.
         iSteps.
-      * iApply (wp_cmpxchg_fail with "H1") => //.
+      * iApply (wp_cmpxchg_fail with "Hl") => //.
         iSteps.
-    - iApply (wp_cmpxchg_fail with "H1") => //.
+    - iApply (wp_cmpxchg_fail with "Hl") => //.
       iSteps.
   Qed.
 
@@ -167,16 +168,16 @@ Section heap_lang_instances.
       Xchg #l v @ s 
     {{ RET v'; l ↦ v }}.
   Proof.
-    iSteps.
-    iApply (wp_xchg with "H1").
+    iSteps as "Hl".
+    iApply (wp_xchg with "Hl").
     iSteps.
   Qed.
 
   Global Instance faa_step_wp l i E1 E2 s :
     SPEC ⟨E1, E2⟩ (z : Z), {{ ▷ l ↦ #z }} FAA #l #i @ s {{ RET #z; l ↦ #(z + i) }}.
   Proof.
-    iSteps.
-    iApply (wp_faa with "H1").
+    iSteps as (z) "Hl".
+    iApply (wp_faa with "Hl").
     iSteps.
   Qed.
 
@@ -232,15 +233,15 @@ Section extra_lock_step_instances.
   Global Instance acquire_step_wp lk γ R :
     SPEC {{ is_lock L γ lk R }} acquire L lk {{ RET #(); locked L γ ∗ R }}.
   Proof.
-    iSteps.
+    iSteps as "HL".
     iApply acquire_spec; iSteps.
   Qed.
 
   Global Instance release_step_wp lk γ R :
     SPEC {{ is_lock L γ lk R ∗ locked L γ ∗ R }} release L lk {{ RET #(); True }}.
   Proof.
-    iSteps.
-    iApply (release_spec with "[H2 H3]"); iSteps.
+    iSteps as "HL Hlocked HR".
+    iApply (release_spec with "[Hlocked HR]"); iSteps.
   Qed.
 
 End extra_lock_step_instances.