Fixed slower examples.

theories/examples/comparison/barrier.v

@@ -104,6 +104,8 @@ Section proof.
   Program Instance p1p2fupd_atom : AtomAndConnective true (P1 1 ={⊤∖↑N}=∗ P2 1).
   Program Instance p2p1fupd_atom : AtomAndConnective true (P2 1 ={⊤∖↑N}=∗ P1 1).
 
+  Ltac connective_as_atom_shortcut ::= biabd_step_atom_shortcut.
+
   Instance newbarrier_spec (threads : positive) :
     SPEC {{ P1 1 ∗ □ (P1 1 ={⊤∖↑N}=∗ P2 1) ∗ □ (P2 1 ={⊤∖↑N}=∗ P1 1) }} 
       make_barrier #()
@@ -113,7 +115,7 @@ Section proof.
     iLeft; iLeft.
     erewrite (right_id ∅); last iSolveTC.
     iStepsS.
- Qed.
+  Qed.
 
   Program Instance peek_spec threads γp1 γp2 γt γb (v : val) :
     SPEC {{ is_barrier threads γp1 γp2 γt γb v }}
@@ -127,7 +129,7 @@ Section proof.
   Proof.
     iStepsS. iLöb as "IH".
     wp_lam. iStepsS; try iSmash. (* iSmash deals with failing CAS's *)
-    - destruct (decide (x1 + 1 = Z.pos threads)%Z) as [Heq|Hneq]; iSmash.
+    - destruct (decide (x0 + 1 = Z.pos threads)%Z) as [Heq|Hneq]; iSmash.
     - destruct (decide (threads = xH)) as [Heq|Hneq]; iSmash.
   Qed.
 
@@ -138,7 +140,7 @@ Section proof.
   Proof.
     iStepsS. iLöb as "IH".
     wp_lam. iStepsS; try iSmash.
-    - destruct (decide (z = x3)) as [-> | Hneq]; iSmash.
+    - destruct (decide (z = x2)) as [-> | Hneq]; iSmash.
     - iRevert "H4"; iSmash.
   Qed. 
   (* we need reverts in some places to detect extra inequalities: at some places we have 3 tickets and mergablepersist does not get all currently *)
@@ -155,8 +157,8 @@ Section proof.
   Proof.
     iStepsS. iLöb as "IH".
     wp_lam. iStepsS; try iSmash. (* iSmash deals with failing CAS's *)
-    - destruct (decide (x1 - 1 = Z.neg threads)%Z) as [Heq|Hneq]; iSmash.
-    - destruct (decide (x1 - 1 = Z.neg threads)%Z) as [Heq|Hneq]; iSmash.
+    - destruct (decide (x0 - 1 = Z.neg threads)%Z) as [Heq|Hneq]; iSmash.
+    - destruct (decide (x0 - 1 = Z.neg threads)%Z) as [Heq|Hneq]; iSmash.
   Qed.
 
   Instance sync_down_exit_spec threads γp1 γp2 γb γt (z : Z) (v : val) :
@@ -166,7 +168,7 @@ Section proof.
   Proof.
     iStepsS. iLöb as "IH".
     wp_lam. iStepsS; try iSmash.
-    - destruct (decide (Z.opp z = x3)) as [<- | Hneq]; iSmash.
+    - destruct (decide (Z.opp z = x2)) as [<- | Hneq]; iSmash.
     - iRevert "H4"; iSmash.
   Qed.
 
@@ -190,12 +192,12 @@ Section barrier_specs2. (* this is currently necessary since otherwise TC search
     SPEC HP1 HP2, {{ is_barrier P1 P2 (Fractional0 := HP1) (Fractional1 := HP2) threads γp1 γp2 γt γb v ∗ token P1 γp1 }}
       sync_up threads v
     {{ RET #(); token P2 γp2 }}.
-  Proof. do 5 iStepS. assert (H1 := sync_up_spec P1 P2). iStepsS. Qed.
+  Proof. do 3 iStepS. assert (H1 := sync_up_spec P1 P2). iStepsS. Qed.
 
   Global Instance sync_down_spec_frac_reuse threads γp1 γp2 γt γb (v : val) :
     SPEC HP1 HP2, {{ is_barrier P1 P2 (Fractional0 := HP1) (Fractional1 := HP2) threads γp1 γp2 γt γb v ∗ token P2 γp2 }}
       sync_down threads v
     {{ RET #(); token P1 γp1 }}.
-  Proof. do 5 iStepS. assert (H1 := sync_down_spec P1 P2). iStepsS. Qed.
+  Proof. do 3 iStepS. assert (H1 := sync_down_spec P1 P2). iStepsS. Qed.
 End barrier_specs2.
 

theories/examples/comparison/barrier_client.v

@@ -105,17 +105,13 @@ Section proof.
       increment #l
     {{ RET #(); P1 γc q }}.
 
-  Global Instance has_right_id {A : ucmra} (a : A) :
-    HasRightId a.
-  Proof. exists ε. rewrite right_id //. Qed.
-
   Instance check_rising_spec γc (l : loc) :
     SPEC q, {{ P1 γc q ∗ inv N (counter_inv γc l) }}
       check_rising #l
     {{ RET #(); P1 γc q }}.
   Proof.
     iStepsS.
-    assert (x8 = x8 `max` x1) as Hx8 by lia. rewrite {2}Hx8.
+    assert (x5 = x5 `max` x0) as Hx8 by lia. rewrite {2}Hx8.
     iLeft. iStepS. rewrite -Hx8. iSmash.
   Qed.
 
@@ -130,12 +126,10 @@ Section proof.
     {{ RET #(); P2 γc q }}.
   Proof.
     iStepsS.
-    assert (x9 = x9 `max` x1) as Hx9 by lia. rewrite {3}Hx9.
+    assert (x6 = x6 `max` x0) as Hx9 by lia. rewrite {3}Hx9.
     iRight. iStepS. rewrite -Hx9. iSmash.
   Qed.
 
-  Opaque P1 P2.
-
   Program Instance client_thread_spec threads γp1 γp2 γt γb (v : val) γc (l : loc) :
     SPEC {{ is_counter_barrier threads γp1 γp2 γt γb v γc ∗ token (P1 γc) γp1 ∗ inv N (counter_inv γc l) }}
       client_thread threads #l v
@@ -156,28 +150,24 @@ Section proof.
     iStepsS.
   Qed.
 
-  Transparent P1 P2. 
-  (* currently needed because of bug in repeated applications of into_texist; notypeclasses refine works, simple eapply does not.
-     problem occurs for biabd_exist lemma, and for TeleSummarize typeclass *)
-
   Global Instance client_spec threads :
     SPEC {{ True }}
       client threads #()
     {{ RET #(); True }}.
   Proof.
     iStepsS.
-    iAssert (|={⊤}=> ∃ γc, inv N (counter_inv γc x0) ∗ P1 γc 1)%I with "[H2]" as ">[%γc [#HI [%n1 [%n2 HPn]]]]".
+    iAssert (|={⊤}=> ∃ γc, inv N (counter_inv γc x) ∗ P1 γc 1)%I with "[H1]" as ">[%γc [#HI [%n1 [%n2 HPn]]]]".
     { iSmash. }
     assert (H' := newbarrier_spec (P1 γc) (P2 γc) threads).
     iStepS.
     iStepS.
     unseal_diaframe => /=.
     iSplitR; [ | iSplitR; iIntros "!>"; [ | iStepsS]].
-    - iIntros "!> !>". iStepS. 
+    - iStepS. iStepS. 
       iInv N as "HN". iRevert "HN".
       iStepsS; case: H0 => /= H1 /to_agree_equiv H2; simplify_eq.
       iRight. iStepsS.
-    - iIntros "!> !>". iStepS. 
+    - iStepS. iStepS.
       iInv N as "HN". iRevert "HN".
       iStepsS; case: H0 => /= H1 /to_agree_equiv H2; simplify_eq.
       iSmash.

theories/examples/comparison/peterson.v

@@ -109,7 +109,7 @@ Section spec.
     {{ RET #(); waitl ↦{#1/2} #true ∗ own γR (◯ (Some $ Cinl $ Excl ())) ∗ R }}.
   Proof.
     iStepsS. iLöb as "IH".
-    wp_lam. do 6 iStepS.
+    wp_lam. do 4 iStepS.
     iExpr (! _)%E has post ({{ (b : bool), RET #b; waitl ↦{#1 / 2} #true ∗ 
         (⌜b = true⌝ ∗ own γl (◯ Some (Cinr (Excl ()))) ∨ ⌜b = false⌝ ∗ own γR (◯ Some (Cinl (Excl ()))) ∗ R) }})%I with ["H2"; "H3"]; 
       last iStepsS.
@@ -122,7 +122,7 @@ Section spec.
        acquire_l p
     {{ RET #(); left_acquired γl γr γR p ∗ R }}.
   Proof.
-    do 37 iStepS.
+    do 25 iStepS.
     iExpr (_ <- _)%E has post ({{ RET #(); x3 ↦{#1/2} # true ∗ own γl (◯ (Some (Cinl (Excl ())))) }})%I with ["H2"; "H3"];
     iSmash.
   Qed.
@@ -141,7 +141,7 @@ Section spec.
     {{ RET #(); waitr ↦{#1/2} #true ∗ own γR (◯ (Some $ Cinr $ Excl ())) ∗ R }} | 50.
   Proof.
     iStepsS. iLöb as "IH".
-    wp_lam. do 6 iStepS.
+    wp_lam. do 4 iStepS.
     iExpr (! _)%E has post ({{ (b : bool), RET #b; waitr ↦{#1 / 2} #true ∗ 
         (⌜b = true⌝ ∗ own γr (◯ Some (Cinr (Excl ()))) ∨ ⌜b = false⌝ ∗ own γR (◯ Some (Cinr (Excl ()))) ∗ R) }})%I with ["H2"; "H3"];
       last iStepsS.
@@ -154,7 +154,7 @@ Section spec.
        acquire_r p
     {{ RET #(); right_acquired γl γr γR p ∗ R }}.
   Proof.
-    do 37 iStepS.
+    do 25 iStepS.
     iExpr (_ <- _)%E has post ({{ RET #(); x4 ↦{#1/2} # true ∗ own γr (◯ Some (Cinl $ Excl ())) }})%I with ["H2"; "H3"];
     iSmash.
   Qed.

theories/lib/greatest_laterable_fixpoint.v

@@ -151,6 +151,7 @@ Section glp_lemmas.
 
   (* This should be able to be improved, to require less proof steps: just put only the non-Laterable things in the argument P.
     However, my initial attempts failed. This is because the order matters in which things are put into the goal,
+        < order matters because we don't make progress on (∀ a, H) ⊢ (∀ a, H) ∗ R >
     and the current approach keeps the order currently found in the environment, which seems to be okay. 
     Maybe we need a MakeSep which determines heuristically which goals should be put on the RHS? *)
   Global Instance intuitionistically_introducable Δ F P :