Update other examples with mergableenv and rewrite stuff.

theories/examples/comparison/barrier.v

@@ -165,8 +165,7 @@ Section proof.
   Proof.
     iStepsS. iLöb as "IH".
     wp_lam. iStepsS; try iSmash.
-    - destruct (decide (Z.opp z = x2)) as [<- | Hneq]; iSmash.
-    - iRevert "H4"; iSmash.
+    destruct (decide (Z.opp z = x2)) as [<- | Hneq]; iSmash.
   Qed.
 
   Global Program Instance sync_down_spec threads γp1 γp2 γt γb (v : val) :

theories/examples/external/actris/par_map.v

@@ -30,14 +30,17 @@ Section contribution_biabd.
     iMod (@update_client with "H1 H2") as "[$ $]"; eauto.
   Qed.
 
-  Global Instance server_agree γ n (x y : A) P:
+  Global Instance server_agree γ n (x y : A) P j :
     MergablePersist (server γ n x) (λ p Pin Pout,
       TCAnd (TCEq Pin (client γ y)) $
       TCAnd (IsIncludedMerge y x P) $
-            (TCEq Pout (∃ i, ⌜n = S i⌝ ∧ P ∧ ⌜(S i = 1 → x ≡ y)⌝)%I)).
+      TCIf (TCEq n (S j)) (TCEq Pout P) $ 
+      (* need to take into account that rewrites from mergable persist might revert the key hypothesis! *)
+           TCAnd (TCEq j 0%nat) 
+          (TCEq Pout (P ∧ ∃ i, ⌜n = S i⌝ ∧ ⌜(n = 1 → x ≡ y)⌝)%I)).
   Proof.
     rewrite /MergablePersist => p Pin Pout.
-    case => [-> [HP ->]] /=.
+    case => [-> [HP HPout]] /=.
     rewrite bi.intuitionistically_if_elim.
     iIntros "[Hs Hc]".
     iDestruct (@server_agree with "Hs Hc") as %[? ?]; destruct n as [|n] =>//=.
@@ -48,8 +51,10 @@ Section contribution_biabd.
     destruct n as [|n].
     - iDestruct (@server_1_agree with "Hs Hc") as %?.
       iIntros "!>".
+      case: HPout => [_ -> | [_ ->] ];
       iStepsS.
     - iIntros "!>". 
+      case: HPout => [_ -> | [_ ->] ];
       iStepsS.
   Qed.
 
@@ -128,8 +133,9 @@ Section actris_test.
     {{ RET #(); True }}.
   Proof.
     iStepsS. iLöb as "IH".
-    wp_lam. iStepsS.
-    { destruct x1; eauto. right. fold_leibniz. by apply H1. }
+    wp_lam.
+    iStepsS.
+    { destruct x1; eauto. right. fold_leibniz. by apply H2. }
     destruct x; iStepsS; multiset_solver.
   Qed.
 

theories/examples/external/reloc/stack_refinement.v

@@ -160,15 +160,13 @@ Section proof.
     iStepsS.
     iLöb as "IH". rel_rec_l.
     iStepsS.
-    destruct x4 as [|h1 ls1]; iRevert "H3 H6"; iStepS.
+    destruct x4 as [|h1 ls1]; iRevert "H3 H7"; iStepS.
     - iStepS. 
       iStepR; iStepsS. iRestore.
       iStepsS.
-    - iStepS. iReIntro "H3".
-      iRestore. 
+    - iStepS.
+      iRestore.
       iStepsS.
-      * iRevert "H10 H4"; iStepsS.
-      * iRevert "H10 H4"; iStepsS.
   Qed.
 
   Definition stackInt A : lrel Σ := LRel (λ v1 v2,