Some thoughts on improving speed of log.atom verifications.

theories/examples/wip/logatom/atomic_clhlock.v

@@ -209,8 +209,9 @@ Section spec.
   Next Obligation. verify_tac. Qed.
   Next Obligation. verify_tac. Qed.
   Next Obligation. verify_tac. Qed.
-  Next Obligation. intros; iSmash. Qed. (* verify_tac fails since it does induction, then gets conflicted on a ▷ ⌜_⌝ which is not used because of the later *)
+  Next Obligation. smash_verify_tac. Qed.
   Next Obligation. intros; iSmash. Qed.
+    (* fails because we don't DropModal ▷ on WPs *)
 End spec.
 
 

theories/lib/greatest_laterable_fixpoint.v

@@ -149,6 +149,10 @@ Section glp_lemmas.
 
   (* finally, when the environment is empty, mark the 'modality' as introducable *)
 
+  (* 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,
+    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 :
     TCEq (env_spatial Δ) Enil → IntroducableInAs (PROP := PROP) (greatest_laterable_fixpoint_wrt F) P Δ (IntroduceHyp P (F P))  | 30.
   Proof.