Small fixes in unimportant files.

theories/examples/comparison/manual/bag_stack_manual.v

@@ -54,10 +54,10 @@ Section spec.
       new_stack #() 
     {{ (s : val), RET s; is_stack P s }}.
   Proof. iStepS.
-    iIntros "_ HΦ".
     wp_lam.
     wp_alloc l as "Hl".
-    iApply "HΦ".
+    iExists #l.
+    iSplitR => //.
     iExists l.
     iSplitR => //.
     iApply inv_alloc. 
@@ -70,8 +70,8 @@ Section spec.
     SPEC {{ is_stack P s ∗ l ↦ v ∗ (l +ₗ 1) ↦ w ∗ P v }}
       push_this s #l
     {{ RET #(); True }}.
-  Proof. iStepS.
-    iIntros "(_ & (%s' & -> & #Hpl) & Hl & Hl' & Hw) HΦ".
+  Proof. iStartProof2 => /=.
+    iIntros "(_ & (%s' & -> & #Hpl) & Hl & Hl' & Hw)".
     iLöb as "IH" forall (w).
     wp_lam. wp_pures.
     wp_bind (! _)%E.
@@ -99,38 +99,37 @@ Section spec.
         { iApply bupd_fupd.
           rewrite -(bi.later_intro (_ ↦□ _)).
           iApply mapsto_persist => //. }
-        eauto with iFrame.
+        by iFrame.
       * iIntros "!>".
-        wp_pures. by iApply "HΦ".
+        wp_pures. eauto.
     - wp_cmpxchg_fail. 
       iSplitL "HP Hs".
       { iExists _. iFrame => //. iExists _. by iFrame. }
       iIntros "!>".
-      wp_pures. iApply ("IH" with "Hl Hl' Hw"). eauto.
+      wp_pures. iApply ("IH" with "Hl Hl' Hw").
   Qed.
 
   Global Instance push_spec P (s v : val) :
     SPEC {{ is_stack P s ∗ P v }} 
       push s v 
     {{ RET #(); True }}.
-  Proof. iStepS.
-    iIntros "(_ & (%s' & -> & #Hpl) & HPv) HΦ".
+  Proof. iStartProof2 => /=.
+    iIntros "(_ & (%s' & -> & #Hpl) & HPv)".
     wp_lam.
     wp_alloc l as "Hl" => //. simpl.
     wp_pures.
     iStepS.
     iStepS.
     iIntros "!> !> _ !>".
-    wp_pures.
-    by iApply "HΦ".
+    wp_pures. eauto.
   Qed.
 
   Global Instance pop_spec P (s : val) :
     SPEC {{ is_stack P s }} 
       pop s 
     {{ (ov : val), RET ov; ⌜ov = NONEV⌝ ∨ ∃ w, ⌜ov = SOMEV w⌝ ∗ P w }}.
-  Proof. iStepS.
-    iIntros "(_ & (%s' & -> & #Hpl)) HΦ".
+  Proof. iStartProof2 => /=.
+    iIntros "(_ & (%s' & -> & #Hpl))".
     iLöb as "IH".
     wp_lam.
     wp_bind (! _)%E.
@@ -141,8 +140,7 @@ Section spec.
       iSplitL "Hs".
       { iExists _. iFrame => //. by iExists []. }
       iIntros "!>".
-      wp_pures. iApply "HΦ".
-      eauto.
+      wp_pures. eauto.
     - simpl. iDestruct "HP" as "(%l & -> & #Hl & HP & (%lv & #Hlv & HR))".
       iSplitL "Hs HP HR".
       { iExists _. iFrame "Hs" => //. iExists (x' :: xs'). iSplitL => //=. 
@@ -150,16 +148,13 @@ Section spec.
         iExists _. by iFrame "# ∗".
       }
       iIntros "!>".
-      wp_pures.
-      wp_load.
-      wp_pures.
+      wp_load. wp_pures.
       wp_bind (CmpXchg _ _ _).
       iInv N as "(%vs2 & >Hs & (%xs & HP & >%))".
       destruct (decide (vs2 = InjRV #l)) as [->|Hneq].
       * wp_cmpxchg_suc. clear xs'.
         destruct xs as [|x'' xs'].
         { simpl. iDestruct "HP" as %?. by contradict H1. }
-        simpl.
         iDestruct "HP" as "(%l' & % & #Hl2 & HP & (%lv' & #Hlv2 & HR))". 
         simplify_eq.
         iDestruct (mapsto_agree with "Hl Hl2") as "->". iClear "Hl2".
@@ -176,7 +171,7 @@ Section spec.
             iExists _. by iFrame "# ∗". }
         iIntros "!>".
         wp_load.
-        wp_pures. iApply "HΦ". iRight. iExists _. by iFrame.
+        wp_pures. iExists _. iSplitR => //. iRight. eauto with iFrame.
       * wp_cmpxchg_fail.
         iSplitL "HP Hs".
         { iExists _. iFrame => //. iExists _. by iFrame. }

theories/examples/wip/grammar_problems.v

@@ -18,9 +18,9 @@ Section problems.
   Proof.
     iStepDebug.
     solveStep with empty_hyp_first.
-    eapply search_abd.abd_from_unfold_hyp.
-    search_abd.find_abd_step.
-    search_abd.find_abd_step.
+    find_abd_initial_step.
+    simple eapply abdhyp_from_unfold_goal.
+    abd_step_goal_exist ltac:(idtac).
     eapply search_abd.abd_unfoldgoal_from_base.
     eapply weakestpre.abduct_from_execution. iSolveTC. split.
     match goal with
@@ -73,7 +73,15 @@ Section problems.
           vs
         https://prover.dioxygen.io/?goal=RmF0aGVyOigpLT4oKSwgTW90aGVyOigpLT4oKSwgQ2hpbGQ6OigpJigpLCBEZXNjZW5kYW50OjooKSYoKTsgKGV4aXN0cyB5OigpLiBleGlzdHMgYTooKS4gQ2hpbGQoYSwgRmF0aGVyKHkpKSksIChmb3JhbGwgYTooKS5mb3JhbGwgYjooKS4gQ2hpbGQoYSwgYikgLT4gRGVzY2VuZGFudChNb3RoZXIoYSksIGIpKSB8LSBleGlzdHMgeDooKS4gZXhpc3RzIHk6KCkuIERlc2NlbmRhbnQoeCwgRmF0aGVyKHkpKQ%3D%3D
       (yes these URLs are very slightly different)
-  *)
+  *)  
+  Section side_cond_problems.
+    Context `{!Inhabited A} {P Q R : A → iProp Σ}.
+    Axiom example : ∀ (a : A), BiAbd (TTl := [tele]) (TTr := [tele]) false (P a) (Q a) id (R a) emp%I.
+    Local Existing Instance example.
+
+    Lemma test :( (∀ a, P a) ∗ |==> ∃ a, R a)%I ⊢@{iPropI Σ} |==> ∃ a, Q a ∗ emp.
+    Proof. iStepsS. Qed.
+  End side_cond_problems.
 
   Context `{!Fractional (PROP := iPropI Σ) P}.
   Context `{!inG Σ $ authUR $ optionUR $ exclR $ leibnizO Qp}.