merge with main

theories/prelude/Reals_ext.v

@@ -19,6 +19,9 @@ Proof. intros ???. eapply Rgt_trans. Qed.
 #[global] Instance Rlt_Transitive: Transitive Rlt.
 Proof. intros ???. eapply Rlt_trans. Qed.
 
+#[global] Instance Req_decision (r1 r2 : R) : Decision (r1 = r2).
+Proof. destruct (Rle_dec r1 r2); destruct (Rle_dec r2 r1);
+ [left | right | right |]; lra. Qed.
 #[global] Instance Rgt_decision (r1 r2 : R) : Decision (Rgt r1 r2).
 Proof. apply Rgt_dec. Qed.
 #[global] Instance Rge_decision (r1 r2 : R) : Decision (Rge r1 r2).

theories/prob/countable_sum.v

@@ -378,8 +378,8 @@ Section filter.
 
   Implicit Types P Q : A → Prop.
 
-  Lemma is_seriesC_singleton (a : A) v :
-    is_seriesC (λ (n : A), if bool_decide (n = a) then v else 0) v.
+  Lemma is_seriesC_singleton_dependent (a : A) v :
+    is_seriesC (λ (n : A), if bool_decide (n = a) then v n else 0) (v a).
   Proof.
     rewrite /is_seriesC.
     eapply is_series_ext; [|apply (is_series_singleton (encode_nat a))].
@@ -391,10 +391,22 @@ Section filter.
       exfalso. apply Hneq. symmetry. by apply encode_inv_Some_nat.
   Qed.
 
+  Lemma is_seriesC_singleton (a : A) v :
+    is_seriesC (λ (n : A), if bool_decide (n = a) then v else 0) v.
+  Proof. apply is_seriesC_singleton_dependent. Qed.
+
+  Lemma ex_seriesC_singleton_dependent (a : A) v :
+    ex_seriesC (λ (n : A), if bool_decide (n = a) then v n else 0).
+  Proof. eexists. eapply is_seriesC_singleton_dependent. Qed.
+
   Lemma ex_seriesC_singleton (a : A) v :
     ex_seriesC (λ (n : A), if bool_decide (n = a) then v else 0).
   Proof. eexists. eapply is_seriesC_singleton. Qed.
 
+  Lemma SeriesC_singleton_dependent (a : A) v :
+    SeriesC (λ n, if bool_decide (n = a) then v n else 0) = v a.
+  Proof. apply is_series_unique, is_seriesC_singleton_dependent. Qed.
+
   Lemma SeriesC_singleton (a : A) v :
     SeriesC (λ n, if bool_decide (n = a) then v else 0) = v.
   Proof. apply is_series_unique, is_seriesC_singleton. Qed.

theories/tpref_logic/examples/galton_watson_tree.v

@@ -79,6 +79,7 @@ Section task_loop_spec.
       iIntros (f) "[Hq Hf]".
       wp_pures.
       iApply (rwp_couple_tape _ (λ m s, s = n + m)%nat); [|iFrame "Hspec Hα"].
+      (* Notice how the model step in the preceding line introduces a later in the goal. *)
       { iIntros (σ Hσ).
         rewrite /state_step /=.
         rewrite bool_decide_eq_true_2; [|by eapply elem_of_dom_2].
@@ -88,6 +89,7 @@ Section task_loop_spec.
         apply Rcoupl_dret; eauto. }
       rewrite {2}/task_spec /tc_opaque.
       iIntros "!>" (m ? ->) "Hspec Hα /=".
+      (* Notice how the above line strips a later from the goal and the Loeb induction hyptothesis. *)
       iSpecialize ("Hf" with "Hq Hα Hna").
       wp_apply (rwp_wand with "Hf").
       iIntros (v) "(Hna & Hq & Hα)".
@@ -108,6 +110,7 @@ Section task_loop_spec.
     wp_rec. wp_pures.
     iModIntro. iFrame.
     iIntros "!> %n %m Hq Hα Hna".
+    (* Notice how the above line strips later from the goal and the Loeb IH since task_spec has a later in front *)
     wp_pures.
     wp_apply ("Hc" with "Hα"); iIntros "Hα".
     wp_pures.

theories/ub_logic/adequacy.v

@@ -69,7 +69,7 @@ Section adequacy.
     }
     clear.
     iIntros "!#" ([ε'' [e1 σ1]]). rewrite /Φ/F/exec_ub_pre.
-    iIntros "[ (%R & %ε1 & %ε2 & % & %Hlift & H)| [ (%R & %ε1 & %ε2 & (%r & %Hr) & % & %Hlift & H)| H]] %Hv".
+    iIntros "[ (%R & %ε1 & %ε2 & %Hred & % & %Hlift & H)| [ (%R & %ε1 & %ε2 & %Hred & (%r & %Hr) & % & %Hlift & H)| [H|H]]] %Hv".
     - iApply step_fupdN_mono.
       { apply pure_mono.
         eapply UB_mon_grading; eauto. }
@@ -111,6 +111,31 @@ Section adequacy.
       rewrite big_orL_cons.
       iDestruct "H" as "[H | Ht]"; [done|].
       by iApply "IH".
+   - rewrite exec_Sn_not_final; [|eauto].
+      iDestruct (big_orL_mono _ (λ _ _,
+                     |={∅}▷=>^(S n)
+                       ⌜ub_lift (prim_step e1 σ1 ≫= exec n) φ ε''⌝)%I
+                  with "H") as "H".
+      { iIntros (i α Hα%elem_of_list_lookup_2) "(% & %ε1 & %ε2 & %Hε'' & %Hleq & %Hlift & H)".
+        replace (prim_step e1 σ1) with (step (e1, σ1)) => //.
+        rewrite -exec_Sn_not_final; [|eauto].
+        iApply (step_fupdN_mono _ _ _
+                  (⌜∀ σ2 , R2 σ2 → ub_lift (exec (S n) (e1, σ2)) φ (ε2 (e1, σ2))⌝)%I).
+        - iIntros (?). iPureIntro.
+          rewrite /= /get_active in Hα.
+          apply elem_of_elements, elem_of_dom in Hα as [bs Hα].
+          erewrite (Rcoupl_eq_elim _ _ (prim_coupl_step_prim _ _ _ _ _ Hα)); eauto.
+          apply (UB_mon_grading _ _
+                   (ε1 + (SeriesC (λ ρ : language.state prob_lang, language.state_step σ1 α ρ * ε2 (e1, ρ))))) => //.
+          eapply ub_lift_dbind_adv; eauto; [by destruct ε1|].
+          destruct Hε'' as [r Hr]; exists r.
+          intros a.
+          split; [by destruct (ε2 _) | by apply Hr].
+        - iIntros (??). by iMod ("H" with "[//] [//]"). }
+      iInduction (language.get_active σ1) as [| α] "IH"; [done|].
+      rewrite big_orL_cons.
+      iDestruct "H" as "[H | Ht]"; [done|].
+      by iApply "IH".
   Qed.
 
   Theorem wp_refRcoupl_step_fupdN (e : expr) (σ : state) (ε : nonnegreal) n φ  :
@@ -144,7 +169,7 @@ Section adequacy.
         apply (UB_mon_grading _ _ 0); [apply cond_nonneg | ].
         apply ub_lift_dret; auto.
       + rewrite ub_wp_unfold /ub_wp_pre /= Heq.
-        iMod ("Hwp" with "[$]") as "(%Hexec_ub & Hlift)".
+        iMod ("Hwp" with "[$]") as "Hlift".
         iModIntro.
         iPoseProof
           (exec_ub_mono _ (λ ε' '(e2, σ2), |={∅}▷=>^(S n)