refactor tpref adequacy

theories/prelude/iris_ext.v

@@ -1,8 +1,31 @@
 From iris.bi Require Export bi fixpoint.
 From iris.proofmode Require Import base proofmode.
-From iris.base_logic.lib Require Export fancy_updates.
+From iris.base_logic.lib Require Export fancy_updates wsat.
 Import uPred.
 
+Section fupd.
+  Local Existing Instances invGpreS_wsat invGpreS_lc.
+
+  (* TODO: remove when Iris is updated (this is on upstream main now) *)
+  Lemma fupd_soundness_no_lc_unfold `{!invGpreS Σ} m E :
+    ⊢ |==> ∃ `(Hws: invGS_gen HasNoLc Σ) (ω : coPset → iProp Σ),
+        £ m ∗ ω E ∗ □ (∀ E1 E2 P, (|={E1, E2}=> P) -∗ ω E1 ==∗ ◇ (ω E2 ∗ P)).
+  Proof.
+    iMod wsat_alloc as (Hw) "[Hw HE]".
+    (* We don't actually want any credits, but we need the [lcGS]. *)
+    iMod (later_credits.le_upd.lc_alloc m) as (Hc) "[_ Hlc]".
+    set (Hi := InvG HasNoLc _ Hw Hc).
+   iExists Hi, (λ E, wsat ∗ ownE E)%I.
+    rewrite (union_difference_L E ⊤); [|set_solver].
+    rewrite ownE_op; [|set_solver].
+    iDestruct "HE" as "[HE _]". iFrame.
+    iIntros "!>!>" (E1 E2 P) "HP HwE".
+    rewrite fancy_updates.uPred_fupd_unseal
+      /fancy_updates.uPred_fupd_def -assoc /=.
+    by iApply ("HP" with "HwE").
+  Qed.
+End fupd.
+
 (* TODO: upstream? *)
 Section fupd_plainly_derived.
   Context {PROP : bi}.

theories/prob/couplings.v

@@ -794,6 +794,12 @@ Section refRcoupl.
         by apply (Rdiv_le_1 (SeriesC μ1)).
   Qed.
 
+  Lemma refRcoupl_dret_trivial (μ : distr A) (b : B) :
+    refRcoupl μ (dret b) (λ _ _, True).
+  Proof.
+    apply refRcoupl_trivial. rewrite dret_mass. eapply pmf_SeriesC.
+  Qed.
+
 End refRcoupl.
 
 Notation "μ1 '≾' μ2 ':' R" :=

theories/prob/markov.v

@@ -478,6 +478,13 @@ Section markov.
     rewrite pexec_O. by apply dret_1_1.
   Qed.
 
+  Lemma lim_exec_not_final a :
+    ¬ is_final a →
+    lim_exec a = step a ≫= lim_exec.
+  Proof.
+    intros Hn. rewrite lim_exec_step step_or_final_no_final //.
+  Qed.  
+
   Lemma lim_exec_leq a b (r : R) :
     (∀ n, exec n a b <= r) →
     lim_exec a b <= r.

theories/prob_lang/metatheory.v

@@ -1129,3 +1129,13 @@ Proof.
   pose proof (elem_fresh_ne _ _ _ H).
   by rewrite lookup_insert_ne.
 Qed.
+
+(* TODO: reducible should be a general property of Markov chains, so all the
+     theory in [language.v] about stuck, irreducible etc. should be generalized *)
+Lemma reducible_not_final (e : expr) (σ : state) :
+  reducible e σ → ¬ is_final (e, σ).
+Proof.
+  rewrite /reducible /=.
+  intros [v Hv] ?%is_final_dzero.
+  simpl in H. rewrite H in Hv. inv_distr.
+Qed.