From 0694eb9eca2bc3dd8274c0dd9f3fc1feaabaaccb Mon Sep 17 00:00:00 2001
From: Hei Li <hei411@gmail.com>
Date: Tue, 9 Jan 2024 15:56:27 +0100
Subject: [PATCH 01/21] starting to write total weakest pre

---
 theories/bi/weakestpre.v                | 76 +++++++++++++++++++++++++
 theories/ub_logic/ub_total_weakestpre.v | 16 ++++++
 2 files changed, 92 insertions(+)
 create mode 100644 theories/ub_logic/ub_total_weakestpre.v

diff --git a/theories/bi/weakestpre.v b/theories/bi/weakestpre.v
index ed78831c..4695efd1 100644
--- a/theories/bi/weakestpre.v
+++ b/theories/bi/weakestpre.v
@@ -19,6 +19,15 @@ Global Arguments wp {_ _ _ _ _} _ _ _%E _%I.
 Global Instance: Params (@wp) 9 := {}.
 Global Arguments wp_default : simpl never.
 
+Class Twp (PROP EXPR VAL A : Type) := {
+    twp : A → coPset → EXPR → (VAL → PROP) → PROP;
+    twp_default : A
+    }.
+Global Arguments twp {_ _ _ _ _} _ _ _%E _%I.
+Global Instance: Params (@twp) 9 := {}.
+Global Arguments twp_default : simpl never.
+
+
 (** Notations for partial weakest preconditions *)
 (** Notations without binder -- only parsing because they overlap with the
 notations with binder. *)
@@ -176,3 +185,70 @@ Notation "'⟨⟨⟨' P ⟩ ⟩ ⟩ e @ E ⟨⟨⟨ 'RET' pat ; Q ⟩ ⟩ ⟩" :
   (∀ Φ, P -∗ (Q -∗ Φ pat%V) -∗ WP e @ E {{ Φ }}) : stdpp_scope.
 Notation "'⟨⟨⟨' P ⟩ ⟩ ⟩ e ⟨⟨⟨ 'RET' pat ; Q ⟩ ⟩ ⟩" :=
   (∀ Φ, P -∗ (Q -∗ Φ pat%V) -∗ WP e {{ Φ }}) : stdpp_scope.
+
+
+
+(** Notations for total weakest preconditions *)
+(** Notations without binder -- only parsing because they overlap with the
+notations with binder. *)
+Notation "'WP' e @ s ; E [{ Φ } ]" := (twp s E e%E Φ)
+  (at level 20, e, Φ at level 200, only parsing) : bi_scope.
+Notation "'WP' e @ E [{ Φ } ]" := (twp wp_default E e%E Φ)
+  (at level 20, e, Φ at level 200, only parsing) : bi_scope.
+Notation "'WP' e [{ Φ } ]" := (twp wp_default ⊤ e%E Φ)
+  (at level 20, e, Φ at level 200, only parsing) : bi_scope.
+
+(** Notations with binder. *)
+Notation "'WP' e @ s ; E [{ v , Q } ]" := (twp s E e%E (λ v, Q))
+  (at level 20, e, Q at level 200,
+   format "'[hv' 'WP'  e  '/' @  '[' s ;  '/' E  ']' '/' [{  '[' v ,  '/' Q  ']' } ] ']'") : bi_scope.
+Notation "'WP' e @ E [{ v , Q } ]" := (twp twp_default E e%E (λ v, Q))
+  (at level 20, e, Q at level 200,
+   format "'[hv' 'WP'  e  '/' @  E  '/' [{  '[' v ,  '/' Q  ']' } ] ']'") : bi_scope.
+Notation "'WP' e [{ v , Q } ]" := (twp twp_default ⊤ e%E (λ v, Q))
+  (at level 20, e, Q at level 200,
+   format "'[hv' 'WP'  e  '/' [{  '[' v ,  '/' Q  ']' } ] ']'") : bi_scope.
+
+(* Texan triples *)
+Notation "'[[{' P } ] ] e @ s ; E [[{ x .. y , 'RET' pat ; Q } ] ]" :=
+  (□ ∀ Φ,
+      P -∗ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ s; E [{ Φ }])%I
+    (at level 20, x closed binder, y closed binder,
+     format "'[hv' [[{  '[' P  ']' } ] ]  '/  ' e  '/' @  '[' s ;  '/' E  ']' '/' [[{  '[hv' x  ..  y ,  RET  pat ;  '/' Q  ']' } ] ] ']'") : bi_scope.
+Notation "'[[{' P } ] ] e @ E [[{ x .. y , 'RET' pat ; Q } ] ]" :=
+  (□ ∀ Φ,
+      P -∗ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E [{ Φ }])%I
+    (at level 20, x closed binder, y closed binder,
+     format "'[hv' [[{  '[' P  ']' } ] ]  '/  ' e  '/' @  E  '/' [[{  '[hv' x  ..  y ,  RET  pat ;  '/' Q  ']' } ] ] ']'") : bi_scope.
+Notation "'[[{' P } ] ] e [[{ x .. y , 'RET' pat ; Q } ] ]" :=
+  (□ ∀ Φ,
+      P -∗ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e [{ Φ }])%I
+    (at level 20, x closed binder, y closed binder,
+       format "'[hv' [[{  '[' P  ']' } ] ]  '/  ' e  '/' [[{  '[hv' x  ..  y ,  RET  pat ;  '/' Q  ']' } ] ] ']'") : bi_scope.
+
+Notation "'[[{' P } ] ] e @ s ; E [[{ 'RET' pat ; Q } ] ]" :=
+  (□ ∀ Φ, P -∗ (Q -∗ Φ pat%V) -∗ WP e @ s; E [{ Φ }])%I
+    (at level 20,
+     format "'[hv' [[{  '[' P  ']' } ] ]  '/  ' e  '/' @  '[' s ;  '/' E  ']' '/' [[{  '[hv' RET  pat ;  '/' Q  ']' } ] ] ']'") : bi_scope.
+Notation "'[[{' P } ] ] e @ E [[{ 'RET' pat ; Q } ] ]" :=
+  (□ ∀ Φ, P -∗ (Q -∗ Φ pat%V) -∗ WP e @ E [{ Φ }])%I
+    (at level 20,
+     format "'[hv' [[{  '[' P  ']' } ] ]  '/  ' e  '/' @  E  '/' [[{  '[hv' RET  pat ;  '/' Q  ']' } ] ] ']'") : bi_scope.
+Notation "'[[{' P } ] ] e [[{ 'RET' pat ; Q } ] ]" :=
+  (□ ∀ Φ, P -∗ (Q -∗ Φ pat%V) -∗ WP e [{ Φ }])%I
+    (at level 20,
+     format "'[hv' [[{  '[' P  ']' } ] ]  '/  ' e  '/' [[{  '[hv' RET  pat ;  '/' Q  ']' } ] ] ']'") : bi_scope.
+
+(** Aliases for stdpp scope -- they inherit the levels and format from above. *)
+Notation "'[[{' P } ] ] e @ s ; E [[{ x .. y , 'RET' pat ; Q } ] ]" :=
+  (∀ Φ, P -∗ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ s; E [{ Φ }]) : stdpp_scope.
+Notation "'[[{' P } ] ] e @ E [[{ x .. y , 'RET' pat ; Q } ] ]" :=
+  (∀ Φ, P -∗ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E [{ Φ }]) : stdpp_scope.
+Notation "'[[{' P } ] ] e [[{ x .. y , 'RET' pat ; Q } ] ]" :=
+  (∀ Φ, P -∗ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e [{ Φ }]) : stdpp_scope.
+Notation "'[[{' P } ] ] e @ s ; E [[{ 'RET' pat ; Q } ] ]" :=
+  (∀ Φ, P -∗ (Q -∗ Φ pat%V) -∗ WP e @ s; E [{ Φ }]) : stdpp_scope.
+Notation "'[[{' P } ] ] e @ E [[{ 'RET' pat ; Q } ] ]" :=
+  (∀ Φ, P -∗ (Q -∗ Φ pat%V) -∗ WP e @ E [{ Φ }]) : stdpp_scope.
+Notation "'[[{' P } ] ] e [[{ 'RET' pat ; Q } ] ]" :=
+  (∀ Φ, P -∗ (Q -∗ Φ pat%V) -∗ WP e [{ Φ }]) : stdpp_scope. 
diff --git a/theories/ub_logic/ub_total_weakestpre.v b/theories/ub_logic/ub_total_weakestpre.v
new file mode 100644
index 00000000..c94b6ebd
--- /dev/null
+++ b/theories/ub_logic/ub_total_weakestpre.v
@@ -0,0 +1,16 @@
+From clutch.ub_logic Require Export ub_weakestpre.
+
+Import uPred.
+
+(** * The total weakest precondition *)
+Definition ub_twp_pre `{!irisGS Λ Σ}
+  (wp : coPset -d> expr Λ -d> (val Λ -d> iPropO Σ) -d> iPropO Σ) :
+    coPset -d> expr Λ -d> (val Λ -d> iPropO Σ) -d> iPropO Σ := λ E e1 Φ,
+  match to_val e1 with
+  | Some v => |={E}=> Φ v
+  | None => ∀ σ1 ε,
+      state_interp σ1 ∗ err_interp ε ={E,∅}=∗
+      exec_ub e1 σ1 (λ ε2 '(e2, σ2),
+        |={∅,E}=> state_interp σ2 ∗ err_interp ε2 ∗ wp E e2 Φ) ε
+end%I.
+

From 6b53586129c275d31b8ff295c6bc81e112b61b1b Mon Sep 17 00:00:00 2001
From: Hei Li <hei411@gmail.com>
Date: Wed, 10 Jan 2024 13:10:38 +0100
Subject: [PATCH 02/21] First file for twp completed

---
 theories/ub_logic/ub_total_weakestpre.v | 291 ++++++++++++++++++++++++
 1 file changed, 291 insertions(+)

diff --git a/theories/ub_logic/ub_total_weakestpre.v b/theories/ub_logic/ub_total_weakestpre.v
index c94b6ebd..6a877078 100644
--- a/theories/ub_logic/ub_total_weakestpre.v
+++ b/theories/ub_logic/ub_total_weakestpre.v
@@ -1,3 +1,4 @@
+From iris.proofmode Require Import base proofmode.
 From clutch.ub_logic Require Export ub_weakestpre.
 
 Import uPred.
@@ -14,3 +15,293 @@ Definition ub_twp_pre `{!irisGS Λ Σ}
         |={∅,E}=> state_interp σ2 ∗ err_interp ε2 ∗ wp E e2 Φ) ε
 end%I.
 
+Local Lemma ub_twp_pre_mono `{!irisGS Λ Σ}
+  (wp1 wp2 : coPset -d> expr Λ -d> (val Λ -d> iPropO Σ) -d> iPropO Σ) :
+  ⊢ (□ ∀ E e Φ, wp1 E e Φ -∗ wp2 E e Φ) →
+    ∀ E e Φ, ub_twp_pre wp1 E e Φ -∗ ub_twp_pre wp2 E e Φ.
+Proof.
+  iIntros "#H".
+  iIntros (E e Φ) "Hwp". rewrite /ub_twp_pre.
+  case_match; first done.
+  iIntros (σ ε) "He". iMod ("Hwp" with "He") as "Hwp".
+  iModIntro. iApply (exec_ub_mono_pred with "[][$Hwp]").
+  iIntros (ε' [e' s]) "He".
+  iApply (fupd_wand_l with "[H He]").
+  iFrame. iIntros "[?[??]]". iFrame.
+  by iApply "H".
+Qed.
+
+Local Definition ub_twp_pre' `{!irisGS Λ Σ} :
+  (prodO (prodO (leibnizO coPset) (exprO Λ)) (val Λ -d> iPropO Σ) → iPropO Σ) →
+  prodO (prodO (leibnizO coPset) (exprO Λ)) (val Λ -d> iPropO Σ) → iPropO Σ :=
+  uncurry3 ∘ ub_twp_pre ∘ curry3.
+
+Local Instance ub_twp_pre_mono' `{!irisGS Λ Σ} :
+  BiMonoPred (ub_twp_pre').
+Proof.
+  constructor.
+  - iIntros (wp1 wp2 ??) "#H"; iIntros ([[E e1] Φ]); iRevert (E e1 Φ).
+    iApply ub_twp_pre_mono. iIntros "!>" (E e Φ). iApply ("H" $! (E,e,Φ)).
+  - intros wp Hwp n [[E1 e1] Φ1] [[E2 e2] Φ2]
+      [[?%leibniz_equiv ?%leibniz_equiv] ?]; simplify_eq/=.
+    rewrite /curry3 /ub_twp_pre. do 7 (f_equiv).
+    rewrite /exec_ub /exec_ub'.
+    f_equiv.
+    intros Φ e. unfold exec_ub_pre.
+    do 21 f_equiv.
+    { by apply pair_ne. }
+    do 2 f_equiv.
+    by apply pair_ne.
+Qed.
+
+Local Definition ub_twp_def `{!irisGS Λ Σ} : Twp (iProp Σ) (expr Λ) (val Λ) () :=
+  {| twp := λ (_ : ()) E e Φ, (bi_least_fixpoint ub_twp_pre') (E, e, Φ); twp_default := () |}.
+Local Definition ub_twp_aux : seal (@ub_twp_def). Proof. by eexists. Qed.
+Definition ub_twp' := ub_twp_aux.(unseal).
+Global Arguments ub_twp' {Λ Σ _}.
+Global Existing Instance ub_twp'.
+Local Lemma ub_twp_unseal `{!irisGS Λ Σ} : twp = (@ub_twp_def Λ Σ _).(twp).
+Proof. rewrite -ub_twp_aux.(seal_eq) //. Qed.
+
+Section ub_twp.
+  Context `{!irisGS Λ Σ}.
+  Implicit Types P : iProp Σ.
+  Implicit Types Φ : val Λ → iProp Σ.
+  Implicit Types v : val Λ.
+  Implicit Types e : expr Λ.
+  Implicit Types σ : state Λ.
+  Implicit Types ρ : cfg Λ.
+  Implicit Types ε : R.
+
+  (* Total Wekaest pre *)
+  Lemma ub_twp_unfold s E e Φ : WP e @ s; E [{ Φ }] ⊣⊢ ub_twp_pre (twp (PROP:=iProp Σ) s) E e Φ.
+  Proof. rewrite ub_twp_unseal /ub_twp_def. simpl. rewrite least_fixpoint_unfold. done. Qed.
+
+  Lemma ub_twp_ind s Ψ :
+  (∀ n E e, Proper (pointwise_relation _ (dist n) ==> dist n) (Ψ E e)) →
+  □ (∀ e E Φ, ub_twp_pre (λ E e Φ, Ψ E e Φ ∧ WP e @ s; E [{ Φ }]) E e Φ -∗ Ψ E e Φ) -∗
+  ∀ e E Φ, WP e @ s; E [{ Φ }] -∗ Ψ E e Φ.
+  Proof.
+    iIntros (HΨ). iIntros "#IH" (e E Φ) "H". rewrite ub_twp_unseal.
+    set (Ψ' := uncurry3 Ψ :
+           prodO (prodO (leibnizO coPset) (exprO Λ)) (val Λ -d> iPropO Σ) → iPropO Σ).
+    assert (NonExpansive Ψ').
+    { intros n [[E1 e1] Φ1] [[E2 e2] Φ2]
+        [[?%leibniz_equiv ?%leibniz_equiv] ?]; simplify_eq/=. by apply HΨ. }
+    iApply (least_fixpoint_ind _ Ψ' with "[] H").
+    iIntros "!>" ([[??] ?]) "H". by iApply "IH".
+  Qed.
+
+  Global Instance ub_twp_ne s E e n :
+    Proper (pointwise_relation _ (dist n) ==> dist n) (twp (PROP:=iProp Σ) s E e).
+  Proof.
+    intros Φ1 Φ2 HΦ. rewrite !ub_twp_unseal. by apply (least_fixpoint_ne _), pair_ne, HΦ.
+  Qed.
+  Global Instance ub_twp_proper s E e :
+    Proper (pointwise_relation _ (≡) ==> (≡)) (twp (PROP:=iProp Σ) s E e).
+  Proof.
+    by intros Φ Φ' ?; apply equiv_dist=>n; apply ub_twp_ne=>v; apply equiv_dist.
+  Qed.
+
+  Lemma ub_twp_value_fupd' s E Φ v : WP of_val v @ s; E [{ Φ }] ⊣⊢ |={E}=> Φ v.
+  Proof. rewrite ub_twp_unfold /ub_twp_pre to_of_val. auto. Qed.
+
+  Lemma ub_twp_strong_mono s1 s2 E1 E2 e Φ Ψ :
+    E1 ⊆ E2 →
+    WP e @ s1; E1 [{ Φ }] -∗ (∀ v, Φ v ={E2}=∗ Ψ v) -∗ WP e @ s2; E2 [{ Ψ }].
+  Proof.
+    iIntros (HE) "H HΦ". iRevert (E2 Ψ HE) "HΦ"; iRevert (e E1 Φ) "H".
+    iApply ub_twp_ind; first solve_proper.
+    iIntros "!>" (e E1 Φ) "IH"; iIntros (E2 Ψ HE) "HΦ".
+    rewrite !ub_twp_unfold /ub_twp_pre. destruct (to_val e) as [v|] eqn:?.
+    { iApply ("HΦ" with "[> -]"). by iApply (fupd_mask_mono E1 _). }    
+    iIntros (σ1 ε1) "[Hs He]".
+    iMod (fupd_mask_subseteq E1) as "Hclose"; first done.
+    iMod ("IH" with "[$Hs $He]") as "IH".
+    iModIntro.
+    iApply (exec_ub_mono_pred with "[Hclose HΦ] IH").
+    iIntros (ε [e' s]) "H".
+    iMod "H". iMod "Hclose". iModIntro.
+    iDestruct "H" as "[Hs[He Hk]]".
+    iFrame. by iApply "Hk".
+  Qed.
+
+  
+  Lemma fupd_ub_twp s E e Φ : (|={E}=> WP e @ s; E [{ Φ }]) ⊢ WP e @ s; E [{ Φ }].
+  Proof.
+    rewrite ub_twp_unfold /ub_twp_pre. iIntros "H". destruct (to_val e) as [v|] eqn:?.
+    { by iMod "H". }
+    iIntros (s' ε) "[Hs He]".
+    iMod "H". iApply "H". iFrame.
+  Qed.
+  Lemma ub_twp_fupd s E e Φ : WP e @ s; E [{ v, |={E}=> Φ v }] ⊢ WP e @ s; E [{ Φ }].
+  Proof. iIntros "H". iApply (ub_twp_strong_mono with "H"); auto. Qed.
+
+  Lemma ub_twp_atomic s E1 E2 e Φ `{!Atomic StronglyAtomic e} :
+    (|={E1,E2}=> WP e @ s; E2 [{ v, |={E2,E1}=> Φ v }]) ⊢ WP e @ s; E1 [{ Φ }].
+  Proof.
+    iIntros "H". rewrite !ub_twp_unfold /ub_twp_pre /=.
+    destruct (to_val e) as [v|] eqn:He.
+    { by iDestruct "H" as ">>> $". }
+    iIntros (σ1 ε) "[Hs He]". iMod "H". iMod ("H" $! σ1 ε with "[$Hs $He]") as "H".
+  iModIntro. iApply (exec_ub_strong_mono with "[][]H"); [done|].
+  iIntros (e2 σ2 ε2) "([%σ' %Hstep]&H)".
+  iMod "H" as "(Hσ&Hε&Hwp)".
+  rewrite !ub_twp_unfold /ub_twp_pre.
+  destruct (to_val e2) as [?|] eqn:He2.
+    + iFrame. do 2 (iMod "Hwp"). by do 2 iModIntro.
+    + iMod ("Hwp" $! _ _ with "[Hσ Hε]") as "Hwp"; [iFrame|].
+      specialize (atomic _ _ _ Hstep) as Hatomic. (* key step *)
+      destruct Hatomic.
+      congruence. (* how do we do this "by hand"? Not obvious to me *)
+  Qed.
+
+  Lemma ub_twp_bind K `{!LanguageCtx K} s E e Φ :
+    WP e @ s; E [{ v, WP K (of_val v) @ s; E [{ Φ }] }] ⊢ WP K e @ s; E [{ Φ }].
+  Proof.
+    revert Φ. cut (∀ Φ', WP e @ s; E [{ Φ' }] -∗ ∀ Φ,
+                     (∀ v, Φ' v -∗ WP K (of_val v) @ s; E [{ Φ }]) -∗ WP K e @ s; E [{ Φ }]).
+    { iIntros (help Φ) "H". iApply (help with "H"); auto. }
+    iIntros (Φ') "H". iRevert (e E Φ') "H". iApply ub_twp_ind; first solve_proper.
+    iIntros "!>" (e E1 Φ') "IH". iIntros (Φ) "HΦ".
+    rewrite /ub_twp_pre. destruct (to_val e) as [v|] eqn:He.
+    { apply of_to_val in He as <-. iApply fupd_ub_twp. by iApply "HΦ". }
+    rewrite ub_twp_unfold /ub_twp_pre fill_not_val //.
+    iIntros (σ1 ε1) "[Hσ Hε]". iMod ("IH" with "[$]") as "IH".
+    iModIntro.
+    iApply exec_ub_bind; [done|].
+    iApply (exec_ub_mono with "[][HΦ][$]"); first done.
+    iIntros (ε [e' σ]) "H".
+    iMod "H". iModIntro. iDestruct "H" as "[?[?K]]".
+    iFrame. by iApply "K".
+  Qed.
+  
+  (* Lemma ub_twp_bind_inv K `{!LanguageCtx K} s E e Φ : *)
+  (*   WP K e @ s; E [{ Φ }] -∗ WP e @ s; E [{ v, WP K (of_val v) @ s; E [{ Φ }] }]. *)
+  (* Proof. *)
+  (*   iIntros "H". remember (K e) as e' eqn:He'. *)
+  (*   iRevert (e He'). iRevert (e' E Φ) "H". iApply ub_twp_ind; first solve_proper. *)
+  (*   iIntros "!>" (e' E1 Φ) "IH". iIntros (e ->). *)
+  (*   rewrite !ub_twp_unfold {2}/ub_twp_pre. destruct (to_val e) as [v|] eqn:He. *)
+  (*   { iModIntro. apply of_to_val in He as <-. rewrite !ub_twp_unfold. *)
+  (*     iApply (ub_twp_pre_mono with "[] IH"). by iIntros "!>" (E e Φ') "[_ ?]". } *)
+  (*   rewrite /ub_twp_pre fill_not_val //. *)
+  (*   iIntros (σ ε) "[Hσ Hε]". *)
+  (*   iMod ("IH" with "[$Hσ $Hε]") as "H". *)
+  (*   iModIntro. *)
+  (*   iApply (exec_ub_mono with "[][][H]"). *)
+  (*   { done. } *)
+  (* Admitted. *)
+
+  Lemma ub_twp_ub_wp s E e Φ : WP e @ s; E [{ Φ }] -∗ WP e @ s; E {{ Φ }}.
+  Proof.
+    iIntros "H". iLöb as "IH" forall (E e Φ).
+    rewrite ub_wp_unfold ub_twp_unfold /ub_wp_pre /ub_twp_pre. destruct (to_val e) as [v|]=>//=.
+    iIntros (σ1 ε) "[Hσ Hε]". iMod ("H" with "[$Hσ $Hε]") as "H".
+    iIntros "!>".
+    iApply exec_ub_mono_pred; last iFrame.
+    iIntros (ε' [e' s']).
+    iIntros "H". iNext. iMod "H" as "[?[?H]]".
+    iModIntro. iFrame. iApply "IH". done.
+  Qed.
+
+  (** * Derived rules *)
+  Lemma ub_twp_mono s E e Φ Ψ :
+    (∀ v, Φ v ⊢ Ψ v) → WP e @ s; E [{ Φ }] ⊢ WP e @ s; E [{ Ψ }].
+  Proof.
+    iIntros (HΦ) "H"; iApply (ub_twp_strong_mono with "H"); auto.
+    iIntros (v) "?". by iApply HΦ.
+  Qed.
+  Lemma ub_twp_mask_mono s E1 E2 e Φ :
+    E1 ⊆ E2 → WP e @ s; E1 [{ Φ }] -∗ WP e @ s; E2 [{ Φ }].
+  Proof. iIntros (?) "H"; iApply (ub_twp_strong_mono with "H"); auto. Qed.
+  Global Instance ub_twp_mono' s E e :
+    Proper (pointwise_relation _ (⊢) ==> (⊢)) (twp (PROP:=iProp Σ) s E e).
+  Proof. by intros Φ Φ' ?; apply ub_twp_mono. Qed.
+
+  Lemma ub_twp_value_fupd s E Φ e v : IntoVal e v → WP e @ s; E [{ Φ }] ⊣⊢ |={E}=> Φ v.
+  Proof. intros <-. by apply ub_twp_value_fupd'. Qed.
+  Lemma ub_twp_value' s E Φ v : Φ v ⊢ WP (of_val v) @ s; E [{ Φ }].
+  Proof. rewrite ub_twp_value_fupd'. auto. Qed.
+  Lemma ub_twp_value s E Φ e v : IntoVal e v → Φ v ⊢ WP e @ s; E [{ Φ }].
+  Proof. intros <-. apply ub_twp_value'. Qed.
+
+  Lemma ub_twp_frame_l s E e Φ R : R ∗ WP e @ s; E [{ Φ }] ⊢ WP e @ s; E [{ v, R ∗ Φ v }].
+  Proof. iIntros "[? H]". iApply (ub_twp_strong_mono with "H"); auto with iFrame. Qed.
+  Lemma ub_twp_frame_r s E e Φ R : WP e @ s; E [{ Φ }] ∗ R ⊢ WP e @ s; E [{ v, Φ v ∗ R }].
+  Proof. iIntros "[H ?]". iApply (ub_twp_strong_mono with "H"); auto with iFrame. Qed.
+
+  Lemma ub_twp_wand s E e Φ Ψ :
+    WP e @ s; E [{ Φ }] -∗ (∀ v, Φ v -∗ Ψ v) -∗ WP e @ s; E [{ Ψ }].
+  Proof.
+    iIntros "H HΦ". iApply (ub_twp_strong_mono with "H"); auto.
+    iIntros (?) "?". by iApply "HΦ".
+  Qed.
+  Lemma ub_twp_wand_l s E e Φ Ψ :
+    (∀ v, Φ v -∗ Ψ v) ∗ WP e @ s; E [{ Φ }] -∗ WP e @ s; E [{ Ψ }].
+  Proof. iIntros "[H Hwp]". iApply (ub_twp_wand with "Hwp H"). Qed.
+  Lemma ub_twp_wand_r s E e Φ Ψ :
+    WP e @ s; E [{ Φ }] ∗ (∀ v, Φ v -∗ Ψ v) -∗ WP e @ s; E [{ Ψ }].
+  Proof. iIntros "[Hwp H]". iApply (ub_twp_wand with "Hwp H"). Qed.
+  Lemma ub_twp_frame_wand s E e Φ R :
+    R -∗ WP e @ s; E [{ v, R -∗ Φ v }] -∗ WP e @ s; E [{ Φ }].
+  Proof.
+    iIntros "HR HWP". iApply (ub_twp_wand with "HWP").
+    iIntros (v) "HΦ". by iApply "HΦ".
+  Qed.
+
+  Lemma ub_twp_wp_step s E e P Φ :
+    TCEq (to_val e) None →
+    ▷ P -∗
+    WP e @ s; E [{ v, P ={E}=∗ Φ v }] -∗ WP e @ s; E {{ Φ }}.
+  Proof.
+    iIntros (?) "HP Hwp".
+    iApply (ub_wp_step_fupd _ _ E _ P with "[HP]"); [auto..|]. by iApply ub_twp_ub_wp.
+  Qed.
+  
+End ub_twp.
+
+
+(** Proofmode class instances *)
+Section proofmode_classes.
+  Context `{!irisGS Λ Σ}.
+  Implicit Types P Q : iProp Σ.
+  Implicit Types Φ : val Λ → iProp Σ.
+  Implicit Types v : val Λ.
+  Implicit Types e : expr Λ.
+
+  Global Instance frame_ub_twp p s E e R Φ Ψ :
+    (∀ v, Frame p R (Φ v) (Ψ v)) →
+    Frame p R (WP e @ s; E [{ Φ }]) (WP e @ s; E [{ Ψ }]) | 2.
+  Proof. rewrite /Frame=> HR. rewrite ub_twp_frame_l. apply ub_twp_mono, HR. Qed.
+
+  Global Instance is_except_0_ub_twp s E e Φ : IsExcept0 (WP e @ s; E [{ Φ }]).
+  Proof. by rewrite /IsExcept0 -{2}fupd_ub_twp -except_0_fupd -fupd_intro. Qed.
+
+  Global Instance elim_modal_bupd_ub_twp p s E e P Φ :
+    ElimModal True p false (|==> P) P (WP e @ s; E [{ Φ }]) (WP e @ s; E [{ Φ }]).
+  Proof.
+    by rewrite /ElimModal intuitionistically_if_elim
+      (bupd_fupd E) fupd_frame_r wand_elim_r fupd_ub_twp.
+  Qed.
+
+  Global Instance elim_modal_fupd_ub_twp p s E e P Φ :
+    ElimModal True p false (|={E}=> P) P (WP e @ s; E [{ Φ }]) (WP e @ s; E [{ Φ }]).
+  Proof.
+    by rewrite /ElimModal intuitionistically_if_elim
+      fupd_frame_r wand_elim_r fupd_ub_twp.
+  Qed.
+
+  Global Instance elim_modal_fupd_ub_twp_atomic p s E1 E2 e P Φ :
+    ElimModal (Atomic StronglyAtomic e) p false
+      (|={E1,E2}=> P) P
+      (WP e @ s; E1 [{ Φ }]) (WP e @ s; E2 [{ v, |={E2,E1}=> Φ v }])%I | 100.
+  Proof.
+    intros ?. by rewrite intuitionistically_if_elim
+                fupd_frame_r wand_elim_r ub_twp_atomic.
+  Qed.
+
+  Global Instance add_modal_fupd_ub_twp s E e P Φ :
+    AddModal (|={E}=> P) P (WP e @ s; E [{ Φ }]).
+  Proof. by rewrite /AddModal fupd_frame_r wand_elim_r fupd_ub_twp. Qed.
+End proofmode_classes.

From 68e9aa4b579e4ae677ebe775c752608bb0809f7e Mon Sep 17 00:00:00 2001
From: Hei Li <hei411@gmail.com>
Date: Wed, 10 Jan 2024 15:11:51 +0100
Subject: [PATCH 03/21] start working on adequacy

---
 theories/bi/weakestpre.v           |  4 +--
 theories/ub_logic/total_adequacy.v | 51 ++++++++++++++++++++++++++++++
 2 files changed, 53 insertions(+), 2 deletions(-)
 create mode 100644 theories/ub_logic/total_adequacy.v

diff --git a/theories/bi/weakestpre.v b/theories/bi/weakestpre.v
index 4695efd1..6d4955df 100644
--- a/theories/bi/weakestpre.v
+++ b/theories/bi/weakestpre.v
@@ -193,9 +193,9 @@ Notation "'⟨⟨⟨' P ⟩ ⟩ ⟩ e ⟨⟨⟨ 'RET' pat ; Q ⟩ ⟩ ⟩" :=
 notations with binder. *)
 Notation "'WP' e @ s ; E [{ Φ } ]" := (twp s E e%E Φ)
   (at level 20, e, Φ at level 200, only parsing) : bi_scope.
-Notation "'WP' e @ E [{ Φ } ]" := (twp wp_default E e%E Φ)
+Notation "'WP' e @ E [{ Φ } ]" := (twp twp_default E e%E Φ)
   (at level 20, e, Φ at level 200, only parsing) : bi_scope.
-Notation "'WP' e [{ Φ } ]" := (twp wp_default ⊤ e%E Φ)
+Notation "'WP' e [{ Φ } ]" := (twp twp_default ⊤ e%E Φ)
   (at level 20, e, Φ at level 200, only parsing) : bi_scope.
 
 (** Notations with binder. *)
diff --git a/theories/ub_logic/total_adequacy.v b/theories/ub_logic/total_adequacy.v
new file mode 100644
index 00000000..271f92dc
--- /dev/null
+++ b/theories/ub_logic/total_adequacy.v
@@ -0,0 +1,51 @@
+From iris.proofmode Require Import base proofmode.
+From clutch.common Require Export language.
+From clutch.ub_logic Require Import ub_total_weakestpre adequacy primitive_laws.
+From clutch.prob Require Import distribution.
+
+Import uPred.
+
+Section adequacy.
+  Context `{!ub_clutchGS Σ}.
+
+  Theorem twp_step_fupd (e : expr) (σ : state) (ε : nonnegreal) φ  :
+    state_interp σ ∗ err_interp (ε) ∗ WP e [{ v, ⌜φ v⌝ }] ⊢
+    |={⊤,∅}=> ⌜(1 - ε <= SeriesC (lim_exec (e, σ)))%R⌝.
+  Proof.
+    iIntros "(Hstate & Herr & Htwp)".
+  Admitted.
+  
+End adequacy.
+
+
+Theorem twp_mass_lim_exec Σ `{ub_clutchGpreS Σ} (e : expr) (σ : state) (ε : nonnegreal) φ :
+  (∀ `{ub_clutchGS Σ}, ⊢ € ε -∗ WP e [{ v, ⌜φ v⌝ }]) →
+  (1 - ε <= SeriesC (lim_exec (e, σ)))%R.
+Proof.
+  intros Hwp.
+  eapply (step_fupdN_soundness_no_lc _ _ 0) => Hinv.
+  iIntros "_".
+  iMod (ghost_map_alloc σ.(heap)) as "[%γH [Hh _]]".
+  iMod (ghost_map_alloc σ.(tapes)) as "[%γT [Ht _]]".
+  iMod ec_alloc as (?) "[? ?]".
+  set (HclutchGS := HeapG Σ _ _ _ γH γT _).
+  epose proof (twp_step_fupd e σ ε φ).
+  iApply fupd_wand_r. iSplitL.
+  - iApply H1. iFrame. by iApply Hwp.
+  -  iIntros "%". iApply step_fupdN_intro; first done. by iModIntro.
+     Unshelve. constructor.
+Qed. 
+
+Theorem twp_union_bound_lim Σ `{ub_clutchGpreS Σ} (e : expr) (σ : state) (ε : nonnegreal) φ :
+  (∀ `{ub_clutchGS Σ}, ⊢ € ε -∗ WP e [{ v, ⌜φ v⌝ }]) →
+  ub_lift (lim_exec (e, σ)) φ ε.
+Proof.
+  intros.
+  eapply wp_union_bound_lim; first done.
+  intros H1.
+  iIntros "Hε".
+  iApply ub_twp_ub_wp.
+  iAssert (WP e [{ v, ⌜φ v⌝ }])%I with "[Hε]" as "H".
+  2:{ destruct twp_default. destruct wp_default. iExact "H". }
+  by iApply H0.
+Qed. 

From 605f0c06d5c1fcda06b78f59ed1a783b933bc414 Mon Sep 17 00:00:00 2001
From: Hei Li <hei411@gmail.com>
Date: Wed, 10 Jan 2024 16:20:30 +0100
Subject: [PATCH 04/21] some progress

---
 theories/ub_logic/total_adequacy.v | 23 +++++++++++++++++++----
 1 file changed, 19 insertions(+), 4 deletions(-)

diff --git a/theories/ub_logic/total_adequacy.v b/theories/ub_logic/total_adequacy.v
index 271f92dc..b2434303 100644
--- a/theories/ub_logic/total_adequacy.v
+++ b/theories/ub_logic/total_adequacy.v
@@ -1,7 +1,8 @@
 From iris.proofmode Require Import base proofmode.
+From Coquelicot Require Export Lim_seq Rbar.
 From clutch.common Require Export language.
 From clutch.ub_logic Require Import ub_total_weakestpre adequacy primitive_laws.
-From clutch.prob Require Import distribution.
+From clutch.prob Require Import distribution union_bounds.
 
 Import uPred.
 
@@ -13,6 +14,21 @@ Section adequacy.
     |={⊤,∅}=> ⌜(1 - ε <= SeriesC (lim_exec (e, σ)))%R⌝.
   Proof.
     iIntros "(Hstate & Herr & Htwp)".
+    iRevert (σ ε) "Hstate Herr".
+    pose proof (ub_twp_ind ()  (λ _ e _, ∀ (a : state) (a0 : nonnegreal),
+                                  state_interp a -∗ err_interp a0 ={⊤,∅}=∗ ⌜1 - a0 <= SeriesC (lim_exec (e, a))⌝)%I) as H.
+    simpl in H.
+    iApply H.
+    2: { destruct twp_default. done. }
+    clear H e.
+    iModIntro.
+    iIntros (e E Φ) "H".
+    iIntros (σ ε) "[Hheap Htapes] Hec".
+    rewrite /ub_twp_pre.
+    case_match.
+    - iApply fupd_mask_intro; first done. iIntros "_".
+      admit.
+    - iSpecialize ("H" $! σ ε). 
   Admitted.
   
 End adequacy.
@@ -23,7 +39,7 @@ Theorem twp_mass_lim_exec Σ `{ub_clutchGpreS Σ} (e : expr) (σ : state) (ε :
   (1 - ε <= SeriesC (lim_exec (e, σ)))%R.
 Proof.
   intros Hwp.
-  eapply (step_fupdN_soundness_no_lc _ _ 0) => Hinv.
+  eapply (step_fupdN_soundness_no_lc _ 0 0) => Hinv.
   iIntros "_".
   iMod (ghost_map_alloc σ.(heap)) as "[%γH [Hh _]]".
   iMod (ghost_map_alloc σ.(tapes)) as "[%γT [Ht _]]".
@@ -32,8 +48,7 @@ Proof.
   epose proof (twp_step_fupd e σ ε φ).
   iApply fupd_wand_r. iSplitL.
   - iApply H1. iFrame. by iApply Hwp.
-  -  iIntros "%". iApply step_fupdN_intro; first done. by iModIntro.
-     Unshelve. constructor.
+  -  iIntros "%". iApply step_fupdN_intro; first done. done. 
 Qed. 
 
 Theorem twp_union_bound_lim Σ `{ub_clutchGpreS Σ} (e : expr) (σ : state) (ε : nonnegreal) φ :

From 71e3be48c38895e890e42115ce2fb61a4272e70b Mon Sep 17 00:00:00 2001
From: Hei Li <hei411@gmail.com>
Date: Wed, 10 Jan 2024 17:04:31 +0100
Subject: [PATCH 05/21] state lemma of another induction hypothesis for twp, it
 is admitted for now

---
 theories/ub_logic/total_adequacy.v      | 15 ++++++++-------
 theories/ub_logic/ub_total_weakestpre.v |  7 +++++++
 2 files changed, 15 insertions(+), 7 deletions(-)

diff --git a/theories/ub_logic/total_adequacy.v b/theories/ub_logic/total_adequacy.v
index b2434303..7eac31ae 100644
--- a/theories/ub_logic/total_adequacy.v
+++ b/theories/ub_logic/total_adequacy.v
@@ -15,20 +15,21 @@ Section adequacy.
   Proof.
     iIntros "(Hstate & Herr & Htwp)".
     iRevert (σ ε) "Hstate Herr".
-    pose proof (ub_twp_ind ()  (λ _ e _, ∀ (a : state) (a0 : nonnegreal),
-                                  state_interp a -∗ err_interp a0 ={⊤,∅}=∗ ⌜1 - a0 <= SeriesC (lim_exec (e, a))⌝)%I) as H.
-    simpl in H.
-    iApply H.
+    pose proof (ub_twp_ind' ⊤ ()  (λ _ e _, ∀ (a : state) (a0 : nonnegreal),
+                                  state_interp a -∗ err_interp a0 ={⊤,∅}=∗ ⌜1 - a0 <= SeriesC (lim_exec (e, a))⌝)%I) as H. iApply H.
     2: { destruct twp_default. done. }
     clear H e.
     iModIntro.
-    iIntros (e E Φ) "H".
-    iIntros (σ ε) "[Hheap Htapes] Hec".
+    iIntros (e Φ) "H".
+    iIntros (σ ε) "Hs Hec".
     rewrite /ub_twp_pre.
     case_match.
     - iApply fupd_mask_intro; first done. iIntros "_".
       admit.
-    - iSpecialize ("H" $! σ ε). 
+    - iSpecialize ("H" $! σ ε with "[$]").
+      iMod "H".
+      rewrite exec_ub_unfold.
+      iDestruct "H" as "[H|[H|[H|H]]]".
   Admitted.
   
 End adequacy.
diff --git a/theories/ub_logic/ub_total_weakestpre.v b/theories/ub_logic/ub_total_weakestpre.v
index 6a877078..79feda5a 100644
--- a/theories/ub_logic/ub_total_weakestpre.v
+++ b/theories/ub_logic/ub_total_weakestpre.v
@@ -103,6 +103,13 @@ Section ub_twp.
     by intros Φ Φ' ?; apply equiv_dist=>n; apply ub_twp_ne=>v; apply equiv_dist.
   Qed.
 
+  Lemma ub_twp_ind' E s Ψ :
+  (∀ n e, Proper (pointwise_relation _ (dist n) ==> dist n) (Ψ E e)) →
+  □ (∀ e Φ, ub_twp_pre (λ E e Φ, Ψ E e Φ ∧ WP e @ s; E [{ Φ }]) E e Φ -∗ Ψ E e Φ) -∗
+  ∀ e Φ, WP e @ s; E [{ Φ }] -∗ Ψ E e Φ.
+  Proof.
+    Admitted.
+  
   Lemma ub_twp_value_fupd' s E Φ v : WP of_val v @ s; E [{ Φ }] ⊣⊢ |={E}=> Φ v.
   Proof. rewrite ub_twp_unfold /ub_twp_pre to_of_val. auto. Qed.
 

From d2b2b8057cae63b923cd7a6dd3e42064150ac22c Mon Sep 17 00:00:00 2001
From: Hei Li <hei411@gmail.com>
Date: Wed, 10 Jan 2024 19:49:49 +0100
Subject: [PATCH 06/21] Added real_le_limit lemma

---
 theories/prelude/Series_ext.v | 91 +++++++++++++++++++++++++++++++++++
 1 file changed, 91 insertions(+)

diff --git a/theories/prelude/Series_ext.v b/theories/prelude/Series_ext.v
index 211fcde7..9844a1d7 100644
--- a/theories/prelude/Series_ext.v
+++ b/theories/prelude/Series_ext.v
@@ -733,6 +733,97 @@ Proof.
       * apply series_pos_partial_le; auto.
 Qed.
 
+Lemma real_le_limit (x y:R) :
+  (∀ ε, ε > 0 -> x - ε <= y) -> x<=y.
+Proof.
+  intros H.
+  assert (forall seq,(∃ b, ∀ n, 0 <= - seq n <= b) -> (∀ n, (x+seq n) <= y)-> x+ Sup_seq (seq) <= y) as H_limit.
+  { intros ? H0 H1.
+    rewrite Rplus_comm.
+    rewrite -Rcomplements.Rle_minus_r.
+    rewrite <- rbar_le_rle.
+    rewrite rbar_finite_real_eq.
+    + apply upper_bound_ge_sup.
+      intros.
+      pose proof (H1 n). rewrite rbar_le_rle. lra.
+    + destruct H0 as [b H0].
+      apply (is_finite_bounded (-b) 0).
+      -- eapply (Sup_seq_minor_le _ _ 0). destruct (H0 0%nat). apply Ropp_le_contravar in H3.
+         rewrite Ropp_involutive in H3. apply H3.
+      -- apply upper_bound_ge_sup. intros n. destruct (H0 n). apply Ropp_le_contravar in H2.
+         rewrite Ropp_involutive in H2. rewrite Ropp_0 in H2. done.
+  }
+  replace x with (x + Sup_seq (λ m,(λ n,-1%R/INR (S n)) m)).
+  - apply H_limit.
+    { exists 1.
+      intros; split.
+      -- rewrite Ropp_div. rewrite Ropp_involutive.
+         apply Rcomplements.Rdiv_le_0_compat; try lra.
+         rewrite S_INR. pose proof (pos_INR n).
+         lra.
+      -- rewrite Ropp_div. rewrite Ropp_involutive.
+         rewrite Rcomplements.Rle_div_l; [|apply Rlt_gt].
+         ++ assert (1<=INR(S n)); try lra.
+            rewrite S_INR.
+            pose proof (pos_INR n).
+            lra.
+         ++ rewrite S_INR.
+            pose proof (pos_INR n).
+            lra. 
+    }
+    intros. rewrite Ropp_div.  apply H.
+    apply Rlt_gt.
+    apply Rdiv_lt_0_compat; first lra.
+    rewrite S_INR. pose proof (pos_INR n); lra.
+  - assert (Sup_seq (λ x : nat, - (1)%R / INR (S x))=0) as Hswap; last first.
+    + rewrite Hswap. erewrite<- eq_rbar_finite; [|done]. lra.
+    + apply is_sup_seq_unique. rewrite /is_sup_seq.
+      intros err.
+      split.
+      -- intros n.
+         eapply (Rbar_le_lt_trans _ (Rbar.Finite 0)); last first.
+         ++ rewrite Rplus_0_l. apply (cond_pos err).  
+         ++ apply Rge_le. rewrite Ropp_div. apply Ropp_0_le_ge_contravar.
+            apply Rcomplements.Rdiv_le_0_compat; try lra.
+            rewrite S_INR. pose proof (pos_INR n); lra.
+      -- pose (r := 1/err -1).
+         assert (exists n, r<INR n) as [n Hr]; last first.
+         ++ eexists n.
+            erewrite Ropp_div. replace (_-_) with (- (pos err)) by lra.
+            apply Ropp_lt_contravar.
+            rewrite Rcomplements.Rlt_div_l.
+            2:{ rewrite S_INR. pose proof pos_INR. apply Rlt_gt.
+                eapply Rle_lt_trans; [eapply H0|].
+                apply Rlt_n_Sn.
+            }
+            rewrite S_INR.
+            rewrite Rmult_comm.
+            rewrite <-Rcomplements.Rlt_div_l.
+            2:{ pose proof (cond_pos err); lra. }
+            rewrite <- Rcomplements.Rlt_minus_l.
+            rewrite -/r. done.
+         ++ pose proof (Rgt_or_ge 0 r).
+            destruct H0.
+            --- exists 0%nat. eapply Rlt_le_trans; last apply pos_INR.
+                lra.
+            --- exists (Z.to_nat (up r)).
+                pose proof (archimed r) as [? ?].
+                rewrite INR_IZR_INZ.
+                rewrite ZifyInst.of_nat_to_nat_eq.
+                rewrite /Z.max.
+                case_match.
+                { rewrite Z.compare_eq_iff in H3.
+                  exfalso. rewrite -H3 in H1. lra.
+                }
+                2: { rewrite Z.compare_gt_iff in H3. exfalso.
+                     assert (IZR (up r) >= 0) by lra.
+                     apply IZR_lt in H3. lra. 
+                }
+                lra.
+Qed.
+
+        
+
 (** Monotone convergence theorem  *)
 Lemma mon_sup_succ (h : nat → R) :
   (∀ n, h n <= h (S n)) →

From 230143e14e09ace261d071b37559ab3a46aa330e Mon Sep 17 00:00:00 2001
From: Hei Li <hei411@gmail.com>
Date: Wed, 10 Jan 2024 20:52:08 +0100
Subject: [PATCH 07/21] Added limit rules

---
 theories/ub_logic/total_adequacy.v | 30 +++++++++++++++++++++++++++++-
 1 file changed, 29 insertions(+), 1 deletion(-)

diff --git a/theories/ub_logic/total_adequacy.v b/theories/ub_logic/total_adequacy.v
index 7eac31ae..05e69d59 100644
--- a/theories/ub_logic/total_adequacy.v
+++ b/theories/ub_logic/total_adequacy.v
@@ -64,4 +64,32 @@ Proof.
   iAssert (WP e [{ v, ⌜φ v⌝ }])%I with "[Hε]" as "H".
   2:{ destruct twp_default. destruct wp_default. iExact "H". }
   by iApply H0.
-Qed. 
+Qed.
+
+(** limit rules *)
+Theorem twp_mass_lim_exec_limit Σ `{ub_clutchGpreS Σ} (e : expr) (σ : state) (ε : nonnegreal) φ :
+  (∀ `{ub_clutchGS Σ}, (∀ ε' : nonnegreal, ε' > ε -> ⊢ € ε' -∗ WP e [{ v, ⌜φ v⌝ }])) →
+  (1 - ε <= SeriesC (lim_exec (e, σ)))%R.
+Proof.
+  intros H'.
+  apply real_le_limit.
+  intros ε0 H1.
+  replace (1-_-_) with (1- (ε+ε0)) by lra.
+  assert (0<=ε+ ε0) as Hε0.
+  { trans ε; try lra. by destruct ε. }
+  pose (mknonnegreal (ε+ε0) Hε0) as NNRε0.
+  assert (ε+ε0 = (NNRbar_to_real (NNRbar.Finite (NNRε0)))) as Heq.
+  { by simpl. }
+  rewrite Heq.
+  eapply twp_mass_lim_exec; first done.
+  intros. iIntros "He".
+  iApply H'; try iFrame.
+  simpl. destruct ε; simpl in H1; simpl; lra.
+Qed.
+
+Theorem twp_union_bound_lim_limit Σ `{ub_clutchGpreS Σ} (e : expr) (σ : state) (ε : nonnegreal) φ :
+  (∀ `{ub_clutchGS Σ}, (∀ ε':nonnegreal, ε'>ε -> ⊢ € ε' -∗ WP e [{ v, ⌜φ v⌝ }])) →
+  ub_lift (lim_exec (e, σ)) φ ε.
+Proof.
+  (* This lemma can be proven with the continuity of ub_lift lemma in the pull request *)
+Admitted.

From a1c39e5bbf3d7c7a5d35af64a3a35ae1cde93754 Mon Sep 17 00:00:00 2001
From: Hei Li <hei411@gmail.com>
Date: Thu, 11 Jan 2024 15:01:01 +0100
Subject: [PATCH 08/21] added strong fixpoint rule

---
 theories/ub_logic/total_adequacy.v | 36 ++++++++++++++++++++++++++++--
 theories/ub_logic/ub_weakestpre.v  | 16 +++++++++++++
 2 files changed, 50 insertions(+), 2 deletions(-)

diff --git a/theories/ub_logic/total_adequacy.v b/theories/ub_logic/total_adequacy.v
index 05e69d59..9021e940 100644
--- a/theories/ub_logic/total_adequacy.v
+++ b/theories/ub_logic/total_adequacy.v
@@ -28,8 +28,40 @@ Section adequacy.
       admit.
     - iSpecialize ("H" $! σ ε with "[$]").
       iMod "H".
-      rewrite exec_ub_unfold.
-      iDestruct "H" as "[H|[H|[H|H]]]".
+      rewrite /exec_ub /exec_ub'.
+      iPoseProof (least_fixpoint_ind with "[][$H]") as "IH".
+      { apply exec_coupl_pre_mono. }
+      (* iDestruct "H" as "[H|[H|[H|H]]]". *)
+      (* + iDestruct "H" as "(%R & %ε1 & %ε2 & %Hred & %Hineq & %Hub & H)". *)
+      (*   rewrite lim_exec_step step_or_final_no_final. *)
+      (*   2: { rewrite /is_final. rewrite -eq_None_not_Some. simpl. by eapply reducible_not_val. } *)
+      (*   rewrite dbind_mass.  *)
+      (*   admit.  *)
+      (* + iDestruct "H" as "(%R & %ε1 & %ε2 & %Hred & %Hbound & %Hineq & %Hub & H)". *)
+      (*   rewrite lim_exec_step step_or_final_no_final. *)
+      (*   2: { rewrite /is_final. rewrite -eq_None_not_Some. simpl. by eapply reducible_not_val. } *)
+      (*   rewrite dbind_mass. *)
+      (*   admit.  *)
+      (* + iInduction (language.get_active σ) as [| l] "IH". *)
+      (*   { rewrite big_orL_nil //. } *)
+      (*   rewrite !big_orL_cons. *)
+      (*   iDestruct "H" as "[H|H]". *)
+      (*   2:{ by iApply "IH". } *)
+      (*   iDestruct "H" as "(%R & %ε1 & %ε2 & %Hineq & %Hub & H)". *)
+      (*   rewrite lim_exec_step step_or_final_no_final. *)
+      (*   2: { rewrite /is_final. rewrite -eq_None_not_Some. simpl. done. } *)
+      (*   rewrite dbind_mass. *)
+      (*   admit.  *)
+      (* + iInduction (language.get_active σ) as [| l] "IH". *)
+      (*   { rewrite big_orL_nil //. } *)
+      (*   rewrite !big_orL_cons. *)
+      (*   iDestruct "H" as "[H|H]". *)
+      (*   2:{ by iApply "IH". } *)
+      (*   iDestruct "H" as "(%R & %ε1 & %ε2  & %Hbound & %Hineq & %Hub & H)". *)
+      (*   rewrite lim_exec_step step_or_final_no_final. *)
+      (*   2: { rewrite /is_final. rewrite -eq_None_not_Some. simpl. done. } *)
+      (*   rewrite dbind_mass. *)
+      (*   admit. *) 
   Admitted.
   
 End adequacy.
diff --git a/theories/ub_logic/ub_weakestpre.v b/theories/ub_logic/ub_weakestpre.v
index 5156656f..9d6fbf23 100644
--- a/theories/ub_logic/ub_weakestpre.v
+++ b/theories/ub_logic/ub_weakestpre.v
@@ -591,6 +591,22 @@ Section exec_ub.
     iSplit; [done|done].
   Qed.
 
+  Lemma exec_ub_strong_ind (Ψ : nonnegreal → expr Λ → state Λ →  iProp Σ) (Z : nonnegreal → cfg Λ → iProp Σ) :
+    (∀ n e σ ε, Proper (dist n) (Ψ ε e σ)) →
+    ⊢ (□ (∀ e σ ε, exec_ub_pre Z (λ '(ε, (e, σ)), Ψ ε e σ ∧ exec_ub e σ Z ε)%I (ε, (e, σ)) -∗ Ψ ε e σ) →
+       ∀ e σ ε, exec_ub e σ Z ε -∗ Ψ ε e σ)%I.
+  Proof.
+    iIntros (HΨ). iIntros "#IH" (e σ ε) "H".
+    set (Ψ' := (λ '(ε, (e, σ)), Ψ ε e σ):
+           (prodO NNRO (prodO (exprO Λ) (stateO Λ))) → iProp Σ).
+    assert (NonExpansive Ψ').
+    { intros n [?[e1 σ1]] [?[e2 σ2]]
+        [?%leibniz_equiv[?%leibniz_equiv ?%leibniz_equiv]].
+      simplify_eq/=. f_equiv. }
+    rewrite /exec_ub/exec_ub'.
+    iApply (least_fixpoint_ind _ Ψ' with "[] H").
+    iModIntro. iIntros ([?[??]]) "H". by iApply "IH".
+  Qed. 
 
 
 (*

From 45e2230ad7c8f0351e0f8ee95d8b251fe5034dec Mon Sep 17 00:00:00 2001
From: Hei Li <hei411@gmail.com>
Date: Thu, 11 Jan 2024 15:32:58 +0100
Subject: [PATCH 09/21] Complete stronger induction lemma

---
 theories/ub_logic/total_adequacy.v | 62 ++++++++++++++----------------
 1 file changed, 28 insertions(+), 34 deletions(-)

diff --git a/theories/ub_logic/total_adequacy.v b/theories/ub_logic/total_adequacy.v
index 9021e940..4672ae89 100644
--- a/theories/ub_logic/total_adequacy.v
+++ b/theories/ub_logic/total_adequacy.v
@@ -28,40 +28,34 @@ Section adequacy.
       admit.
     - iSpecialize ("H" $! σ ε with "[$]").
       iMod "H".
-      rewrite /exec_ub /exec_ub'.
-      iPoseProof (least_fixpoint_ind with "[][$H]") as "IH".
-      { apply exec_coupl_pre_mono. }
-      (* iDestruct "H" as "[H|[H|[H|H]]]". *)
-      (* + iDestruct "H" as "(%R & %ε1 & %ε2 & %Hred & %Hineq & %Hub & H)". *)
-      (*   rewrite lim_exec_step step_or_final_no_final. *)
-      (*   2: { rewrite /is_final. rewrite -eq_None_not_Some. simpl. by eapply reducible_not_val. } *)
-      (*   rewrite dbind_mass.  *)
-      (*   admit.  *)
-      (* + iDestruct "H" as "(%R & %ε1 & %ε2 & %Hred & %Hbound & %Hineq & %Hub & H)". *)
-      (*   rewrite lim_exec_step step_or_final_no_final. *)
-      (*   2: { rewrite /is_final. rewrite -eq_None_not_Some. simpl. by eapply reducible_not_val. } *)
-      (*   rewrite dbind_mass. *)
-      (*   admit.  *)
-      (* + iInduction (language.get_active σ) as [| l] "IH". *)
-      (*   { rewrite big_orL_nil //. } *)
-      (*   rewrite !big_orL_cons. *)
-      (*   iDestruct "H" as "[H|H]". *)
-      (*   2:{ by iApply "IH". } *)
-      (*   iDestruct "H" as "(%R & %ε1 & %ε2 & %Hineq & %Hub & H)". *)
-      (*   rewrite lim_exec_step step_or_final_no_final. *)
-      (*   2: { rewrite /is_final. rewrite -eq_None_not_Some. simpl. done. } *)
-      (*   rewrite dbind_mass. *)
-      (*   admit.  *)
-      (* + iInduction (language.get_active σ) as [| l] "IH". *)
-      (*   { rewrite big_orL_nil //. } *)
-      (*   rewrite !big_orL_cons. *)
-      (*   iDestruct "H" as "[H|H]". *)
-      (*   2:{ by iApply "IH". } *)
-      (*   iDestruct "H" as "(%R & %ε1 & %ε2  & %Hbound & %Hineq & %Hub & H)". *)
-      (*   rewrite lim_exec_step step_or_final_no_final. *)
-      (*   2: { rewrite /is_final. rewrite -eq_None_not_Some. simpl. done. } *)
-      (*   rewrite dbind_mass. *)
-      (*   admit. *) 
+      iRevert (H).
+      iApply (exec_ub_strong_ind (λ ε e σ, ⌜language.to_val e = None⌝ ={∅}=∗ ⌜1 - ε <= SeriesC (lim_exec (e, σ))⌝)%I with "[][$H]").
+      iModIntro. clear e σ ε. simpl. iIntros (e σ ε) "H %Hval".
+      iDestruct "H" as "[H|[H|[H|H]]]".
+      + iDestruct "H" as "(%R & %ε1 & %ε2 & %Hred & %Hineq & %Hub & H)".
+        rewrite lim_exec_step step_or_final_no_final.
+        2: { rewrite /is_final. rewrite -eq_None_not_Some. simpl. by eapply reducible_not_val. }
+        rewrite dbind_mass.
+        admit.
+      + iDestruct "H" as "(%R & %ε1 & %ε2 & %Hred & %Hbound & %Hineq & %Hub & H)".
+        rewrite lim_exec_step step_or_final_no_final.
+        2: { rewrite /is_final. rewrite -eq_None_not_Some. simpl. by eapply reducible_not_val. }
+        rewrite dbind_mass.
+        admit.
+      + iInduction (get_active σ) as [| l] "IH".
+        { rewrite big_orL_nil //. }
+        rewrite !big_orL_cons.
+        iDestruct "H" as "[H|H]".
+        2:{ by iApply "IH". }
+        iDestruct "H" as "(%R & %ε1 & %ε2 & %Hineq & %Hub & H)".
+        admit.
+      + iInduction (get_active σ) as [| l] "IH".
+        { rewrite big_orL_nil //. }
+        rewrite !big_orL_cons.
+        iDestruct "H" as "[H|H]".
+        2:{ by iApply "IH". }
+        iDestruct "H" as "(%R & %ε1 & %ε2  & %Hbound & %Hineq & %Hub & H)".
+        admit. 
   Admitted.
   
 End adequacy.

From 7886b538fcf1f5fae767e6fecf55d1f82b4d2787 Mon Sep 17 00:00:00 2001
From: Hei Li <hei411@gmail.com>
Date: Thu, 11 Jan 2024 15:33:25 +0100
Subject: [PATCH 10/21] small add

---
 theories/ub_logic/total_adequacy.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/ub_logic/total_adequacy.v b/theories/ub_logic/total_adequacy.v
index 4672ae89..1f1c8381 100644
--- a/theories/ub_logic/total_adequacy.v
+++ b/theories/ub_logic/total_adequacy.v
@@ -30,7 +30,7 @@ Section adequacy.
       iMod "H".
       iRevert (H).
       iApply (exec_ub_strong_ind (λ ε e σ, ⌜language.to_val e = None⌝ ={∅}=∗ ⌜1 - ε <= SeriesC (lim_exec (e, σ))⌝)%I with "[][$H]").
-      iModIntro. clear e σ ε. simpl. iIntros (e σ ε) "H %Hval".
+      iModIntro. clear e σ ε. iIntros (e σ ε) "H %Hval".
       iDestruct "H" as "[H|[H|[H|H]]]".
       + iDestruct "H" as "(%R & %ε1 & %ε2 & %Hred & %Hineq & %Hub & H)".
         rewrite lim_exec_step step_or_final_no_final.

From fc6050468ac329207cc30e5308cb5b20ce38d076 Mon Sep 17 00:00:00 2001
From: Hei Li <hei411@gmail.com>
Date: Thu, 11 Jan 2024 15:34:05 +0100
Subject: [PATCH 11/21] Small fix

---
 theories/ub_logic/total_adequacy.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/ub_logic/total_adequacy.v b/theories/ub_logic/total_adequacy.v
index 1f1c8381..9f99b785 100644
--- a/theories/ub_logic/total_adequacy.v
+++ b/theories/ub_logic/total_adequacy.v
@@ -42,14 +42,14 @@ Section adequacy.
         2: { rewrite /is_final. rewrite -eq_None_not_Some. simpl. by eapply reducible_not_val. }
         rewrite dbind_mass.
         admit.
-      + iInduction (get_active σ) as [| l] "IH".
+      + iInduction (language.get_active σ) as [| l] "IH".
         { rewrite big_orL_nil //. }
         rewrite !big_orL_cons.
         iDestruct "H" as "[H|H]".
         2:{ by iApply "IH". }
         iDestruct "H" as "(%R & %ε1 & %ε2 & %Hineq & %Hub & H)".
         admit.
-      + iInduction (get_active σ) as [| l] "IH".
+      + iInduction (language.get_active σ) as [| l] "IH".
         { rewrite big_orL_nil //. }
         rewrite !big_orL_cons.
         iDestruct "H" as "[H|H]".

From efdcc0efc03d3c7217e077e0822a062199467551 Mon Sep 17 00:00:00 2001
From: Hei Li <hei411@gmail.com>
Date: Thu, 11 Jan 2024 17:19:56 +0100
Subject: [PATCH 12/21] make more progress on another induction lemma

---
 theories/ub_logic/total_adequacy.v      |  2 +-
 theories/ub_logic/ub_total_weakestpre.v | 23 ++++++++++++++++++++---
 2 files changed, 21 insertions(+), 4 deletions(-)

diff --git a/theories/ub_logic/total_adequacy.v b/theories/ub_logic/total_adequacy.v
index 9f99b785..ea0f48d7 100644
--- a/theories/ub_logic/total_adequacy.v
+++ b/theories/ub_logic/total_adequacy.v
@@ -15,7 +15,7 @@ Section adequacy.
   Proof.
     iIntros "(Hstate & Herr & Htwp)".
     iRevert (σ ε) "Hstate Herr".
-    pose proof (ub_twp_ind' ⊤ ()  (λ _ e _, ∀ (a : state) (a0 : nonnegreal),
+    pose proof (ub_twp_ind' ⊤ ()  (λ e _, ∀ (a : state) (a0 : nonnegreal),
                                   state_interp a -∗ err_interp a0 ={⊤,∅}=∗ ⌜1 - a0 <= SeriesC (lim_exec (e, a))⌝)%I) as H. iApply H.
     2: { destruct twp_default. done. }
     clear H e.
diff --git a/theories/ub_logic/ub_total_weakestpre.v b/theories/ub_logic/ub_total_weakestpre.v
index 79feda5a..3f1f0328 100644
--- a/theories/ub_logic/ub_total_weakestpre.v
+++ b/theories/ub_logic/ub_total_weakestpre.v
@@ -104,10 +104,27 @@ Section ub_twp.
   Qed.
 
   Lemma ub_twp_ind' E s Ψ :
-  (∀ n e, Proper (pointwise_relation _ (dist n) ==> dist n) (Ψ E e)) →
-  □ (∀ e Φ, ub_twp_pre (λ E e Φ, Ψ E e Φ ∧ WP e @ s; E [{ Φ }]) E e Φ -∗ Ψ E e Φ) -∗
-  ∀ e Φ, WP e @ s; E [{ Φ }] -∗ Ψ E e Φ.
+  (∀ n e, Proper (pointwise_relation _ (dist n) ==> dist n) (Ψ e)) →
+  □ (∀ e Φ, ub_twp_pre (λ E e Φ, Ψ e Φ ∧ WP e @ s; E [{ Φ }]) E e Φ -∗ Ψ e Φ) -∗
+  ∀ e Φ, WP e @ s; E [{ Φ }] -∗ Ψ e Φ.
   Proof.
+    iIntros (Hp) "#IH". iIntros (e Φ) "Hwp".
+    iRevert "IH".
+    iApply (ub_twp_ind _ (λ E e Φ, _) with "[][$]").
+    - admit.
+    - iModIntro.
+      clear. iIntros (e E Φ) "H #IH".
+      iApply "IH".
+      rewrite {2 4}/ub_twp_pre. case_match; first done.
+      iIntros (σ ε) "[Hs He]".
+      iMod ("H" with "[$]") as "H".
+      iModIntro.
+      iApply (exec_ub_mono_pred with "[]H").
+      iIntros ([] []) "H".
+      iMod "H". iModIntro. iDestruct "H" as "(?&?&H)".
+      iFrame. iSplit.
+      { by iApply "H". }
+      by iDestruct "H" as "[_?]".
     Admitted.
   
   Lemma ub_twp_value_fupd' s E Φ v : WP of_val v @ s; E [{ Φ }] ⊣⊢ |={E}=> Φ v.

From 5d04db1e74ce20220f76c95ccc75bbbf47f903ba Mon Sep 17 00:00:00 2001
From: Hei Li <hei411@gmail.com>
Date: Thu, 11 Jan 2024 18:04:54 +0100
Subject: [PATCH 13/21] Solved ind'

---
 theories/ub_logic/ub_total_weakestpre.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/ub_logic/ub_total_weakestpre.v b/theories/ub_logic/ub_total_weakestpre.v
index 3f1f0328..d271263c 100644
--- a/theories/ub_logic/ub_total_weakestpre.v
+++ b/theories/ub_logic/ub_total_weakestpre.v
@@ -111,7 +111,7 @@ Section ub_twp.
     iIntros (Hp) "#IH". iIntros (e Φ) "Hwp".
     iRevert "IH".
     iApply (ub_twp_ind _ (λ E e Φ, _) with "[][$]").
-    - admit.
+    - intros. intros ???. repeat f_equiv.
     - iModIntro.
       clear. iIntros (e E Φ) "H #IH".
       iApply "IH".
@@ -125,7 +125,7 @@ Section ub_twp.
       iFrame. iSplit.
       { by iApply "H". }
       by iDestruct "H" as "[_?]".
-    Admitted.
+  Qed.
   
   Lemma ub_twp_value_fupd' s E Φ v : WP of_val v @ s; E [{ Φ }] ⊣⊢ |={E}=> Φ v.
   Proof. rewrite ub_twp_unfold /ub_twp_pre to_of_val. auto. Qed.

From be101591cbc11e245382d1cc0cd64eb4aa77dae7 Mon Sep 17 00:00:00 2001
From: Hei Li <hei411@gmail.com>
Date: Fri, 12 Jan 2024 11:27:10 +0100
Subject: [PATCH 14/21] simplify some hypothesis

---
 theories/ub_logic/total_adequacy.v | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)

diff --git a/theories/ub_logic/total_adequacy.v b/theories/ub_logic/total_adequacy.v
index ea0f48d7..d3bea656 100644
--- a/theories/ub_logic/total_adequacy.v
+++ b/theories/ub_logic/total_adequacy.v
@@ -36,11 +36,29 @@ Section adequacy.
         rewrite lim_exec_step step_or_final_no_final.
         2: { rewrite /is_final. rewrite -eq_None_not_Some. simpl. by eapply reducible_not_val. }
         rewrite dbind_mass.
+        iAssert (∀ ρ2 : language.expr prob_lang * language.state prob_lang,
+          ⌜R ρ2⌝ ={∅}=∗
+          let
+          '(e2, σ2) := ρ2 in
+          |={∅}=> ⌜1 - ε2 <= SeriesC (lim_exec (e2, σ2))⌝)%I with "[H]" as "H".
+        { iIntros (ρ2) "%Hρ2". iMod ("H" $! ρ2 Hρ2) as "H".
+          destruct ρ2. iMod "H" as "(?&?&H)".
+          iMod ("H" with "[$][$]"). iModIntro. iModIntro. done.
+        } 
         admit.
       + iDestruct "H" as "(%R & %ε1 & %ε2 & %Hred & %Hbound & %Hineq & %Hub & H)".
         rewrite lim_exec_step step_or_final_no_final.
         2: { rewrite /is_final. rewrite -eq_None_not_Some. simpl. by eapply reducible_not_val. }
         rewrite dbind_mass.
+        iAssert (∀ ρ2 : language.expr prob_lang * language.state prob_lang,
+          ⌜R ρ2⌝ ={∅}=∗
+          let
+          '(e2, σ2) := ρ2 in
+          |={∅}=> ⌜1 - (ε2 ρ2) <= SeriesC (lim_exec (e2, σ2))⌝)%I with "[H]" as "H".
+        { iIntros (ρ2) "%Hρ2". iMod ("H" $! ρ2 Hρ2) as "H".
+          destruct ρ2. iMod "H" as "(?&?&H)".
+          iMod ("H" with "[$][$]"). iModIntro. iModIntro. done.
+        }
         admit.
       + iInduction (language.get_active σ) as [| l] "IH".
         { rewrite big_orL_nil //. }
@@ -48,6 +66,9 @@ Section adequacy.
         iDestruct "H" as "[H|H]".
         2:{ by iApply "IH". }
         iDestruct "H" as "(%R & %ε1 & %ε2 & %Hineq & %Hub & H)".
+        iAssert (∀ σ2 : language.state prob_lang,
+                   ⌜R σ2⌝ ={∅}=∗ ⌜1 - ε2 <= SeriesC (lim_exec (e, σ2))⌝)%I with "[H]" as "H".
+        { iIntros. iMod ("H" $! σ2 (H)) as "H". iDestruct "H" as "[H _]". iApply "H". done. }
         admit.
       + iInduction (language.get_active σ) as [| l] "IH".
         { rewrite big_orL_nil //. }
@@ -55,6 +76,9 @@ Section adequacy.
         iDestruct "H" as "[H|H]".
         2:{ by iApply "IH". }
         iDestruct "H" as "(%R & %ε1 & %ε2  & %Hbound & %Hineq & %Hub & H)".
+        iAssert (∀ σ2 : language.state prob_lang,
+                   ⌜R σ2⌝ ={∅}=∗ ⌜1 - (ε2 (e, σ2)) <= SeriesC (lim_exec (e, σ2))⌝)%I with "[H]" as "H".
+        { iIntros. iMod ("H" $! σ2 (H)) as "H". iDestruct "H" as "[H _]". iApply "H". done. }
         admit. 
   Admitted.
   

From ac691422b8fc14c4f17987de04d4139adf59f45a Mon Sep 17 00:00:00 2001
From: Hei Li <hei411@gmail.com>
Date: Fri, 12 Jan 2024 12:55:48 +0100
Subject: [PATCH 15/21] translate adequacy to just pure lemmas

---
 theories/ub_logic/total_adequacy.v | 26 +++++++++++++++++++++-----
 1 file changed, 21 insertions(+), 5 deletions(-)

diff --git a/theories/ub_logic/total_adequacy.v b/theories/ub_logic/total_adequacy.v
index d3bea656..9cbf4be0 100644
--- a/theories/ub_logic/total_adequacy.v
+++ b/theories/ub_logic/total_adequacy.v
@@ -44,8 +44,12 @@ Section adequacy.
         { iIntros (ρ2) "%Hρ2". iMod ("H" $! ρ2 Hρ2) as "H".
           destruct ρ2. iMod "H" as "(?&?&H)".
           iMod ("H" with "[$][$]"). iModIntro. iModIntro. done.
-        } 
-        admit.
+        }
+        iApply (fupd_mono _ _ (⌜∀ e, R e -> 1 - ε2 <= SeriesC (lim_exec e)⌝)%I).
+        { iIntros (H). iPureIntro. admit. }
+        iIntros (a HR). iMod ("H" $! a (HR)) as "H".
+        destruct a.
+        iApply "H".
       + iDestruct "H" as "(%R & %ε1 & %ε2 & %Hred & %Hbound & %Hineq & %Hub & H)".
         rewrite lim_exec_step step_or_final_no_final.
         2: { rewrite /is_final. rewrite -eq_None_not_Some. simpl. by eapply reducible_not_val. }
@@ -59,7 +63,11 @@ Section adequacy.
           destruct ρ2. iMod "H" as "(?&?&H)".
           iMod ("H" with "[$][$]"). iModIntro. iModIntro. done.
         }
-        admit.
+        iApply (fupd_mono _ _ (⌜∀ e, R e -> 1 - (ε2 e) <= SeriesC (lim_exec e)⌝)%I).
+        { iIntros (H). iPureIntro. admit. }
+        iIntros (a HR). iMod ("H" $! a (HR)) as "H".
+        destruct a.
+        iApply "H".
       + iInduction (language.get_active σ) as [| l] "IH".
         { rewrite big_orL_nil //. }
         rewrite !big_orL_cons.
@@ -69,7 +77,11 @@ Section adequacy.
         iAssert (∀ σ2 : language.state prob_lang,
                    ⌜R σ2⌝ ={∅}=∗ ⌜1 - ε2 <= SeriesC (lim_exec (e, σ2))⌝)%I with "[H]" as "H".
         { iIntros. iMod ("H" $! σ2 (H)) as "H". iDestruct "H" as "[H _]". iApply "H". done. }
-        admit.
+        iApply (fupd_mono _ _ (⌜∀ s, R s -> 1 - ε2 <= SeriesC (lim_exec (e, s))⌝)%I).
+        { iIntros (H). iPureIntro. admit. }
+        iIntros (a HR). iMod ("H" $! a (HR)) as "H".
+        destruct a.
+        iApply "H".
       + iInduction (language.get_active σ) as [| l] "IH".
         { rewrite big_orL_nil //. }
         rewrite !big_orL_cons.
@@ -79,7 +91,11 @@ Section adequacy.
         iAssert (∀ σ2 : language.state prob_lang,
                    ⌜R σ2⌝ ={∅}=∗ ⌜1 - (ε2 (e, σ2)) <= SeriesC (lim_exec (e, σ2))⌝)%I with "[H]" as "H".
         { iIntros. iMod ("H" $! σ2 (H)) as "H". iDestruct "H" as "[H _]". iApply "H". done. }
-        admit. 
+        iApply (fupd_mono _ _ (⌜∀ s, R s -> 1 - ε2 (e, s) <= SeriesC (lim_exec (e, s))⌝)%I).
+        { iIntros (H). iPureIntro. admit. }
+        iIntros (a HR). iMod ("H" $! a (HR)) as "H".
+        destruct a.
+        iApply "H".
   Admitted.
   
 End adequacy.

From 3bced867519d2e6db925b295c2a39d1b887f7841 Mon Sep 17 00:00:00 2001
From: Hei Li <hei411@gmail.com>
Date: Fri, 12 Jan 2024 12:56:31 +0100
Subject: [PATCH 16/21] small change

---
 theories/ub_logic/total_adequacy.v | 1 +
 1 file changed, 1 insertion(+)

diff --git a/theories/ub_logic/total_adequacy.v b/theories/ub_logic/total_adequacy.v
index 9cbf4be0..f7a6afb1 100644
--- a/theories/ub_logic/total_adequacy.v
+++ b/theories/ub_logic/total_adequacy.v
@@ -25,6 +25,7 @@ Section adequacy.
     rewrite /ub_twp_pre.
     case_match.
     - iApply fupd_mask_intro; first done. iIntros "_".
+      iPureIntro.
       admit.
     - iSpecialize ("H" $! σ ε with "[$]").
       iMod "H".

From ac3d35d7f19076439299e2ef698c1d093a7d860c Mon Sep 17 00:00:00 2001
From: Hei Li <hei411@gmail.com>
Date: Fri, 12 Jan 2024 15:59:38 +0100
Subject: [PATCH 17/21] Completed val case

---
 theories/ub_logic/total_adequacy.v | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/theories/ub_logic/total_adequacy.v b/theories/ub_logic/total_adequacy.v
index f7a6afb1..ae4fe9d3 100644
--- a/theories/ub_logic/total_adequacy.v
+++ b/theories/ub_logic/total_adequacy.v
@@ -26,7 +26,11 @@ Section adequacy.
     case_match.
     - iApply fupd_mask_intro; first done. iIntros "_".
       iPureIntro.
-      admit.
+      etrans.
+      2:{ eapply SeriesC_ge_elem; last done. intros. apply pmf_pos. }
+      erewrite (lim_exec_term 0).
+      { simpl. rewrite H. rewrite dret_1_1; last done. destruct ε. simpl. lra. }
+      simpl. rewrite H. by rewrite dret_mass.
     - iSpecialize ("H" $! σ ε with "[$]").
       iMod "H".
       iRevert (H).

From 89af689b35843b94fd7d8e60eb1df6148fc8e389 Mon Sep 17 00:00:00 2001
From: Hei Li <hei411@gmail.com>
Date: Mon, 22 Jan 2024 12:54:23 +0100
Subject: [PATCH 18/21] Now remaining two ugly lemmas

---
 theories/ub_logic/total_adequacy.v | 76 +++++++++++++++++++++++++-----
 1 file changed, 65 insertions(+), 11 deletions(-)

diff --git a/theories/ub_logic/total_adequacy.v b/theories/ub_logic/total_adequacy.v
index ae4fe9d3..0abe46c8 100644
--- a/theories/ub_logic/total_adequacy.v
+++ b/theories/ub_logic/total_adequacy.v
@@ -6,6 +6,24 @@ From clutch.prob Require Import distribution union_bounds.
 
 Import uPred.
 
+Lemma twp_step_fupd_ineq_prim_step (e : language.expr prob_lang) σ (ε ε1:nonnegreal) (ε2: language.cfg prob_lang -> nonnegreal) R:
+  (∃ r, ∀ ρ : language.cfg prob_lang, ε2 ρ <= r) ->
+  ε1 + SeriesC
+         (λ ρ, prim_step e σ ρ * ε2 ρ) <= ε -> ub_lift (prim_step e σ) R ε1 ->
+  (∀ e, R e → 1 - ε2 e <= SeriesC (lim_exec e)) ->
+  1 - ε <= SeriesC (λ a, step (e, σ) a * SeriesC (lim_exec a)).
+Proof.
+Admitted.
+
+Lemma twp_step_fupd_ineq_state_step (e : language.expr prob_lang) σ l (ε ε1:nonnegreal) (ε2: _ -> nonnegreal) R:
+  (∃ r, ∀ ρ : language.cfg prob_lang, ε2 ρ <= r) ->
+  ε1 + SeriesC
+         (λ ρ, language.state_step σ l ρ * ε2 (e, ρ)) <= ε -> ub_lift (language.state_step σ l) R ε1 ->
+  (∀ s, R s → 1 - ε2 (e, s) <= SeriesC (lim_exec (e, s))) ->
+  1 - ε <= SeriesC (λ a, state_step σ l a * SeriesC (lim_exec (e, a))).
+Proof.
+Admitted.
+
 Section adequacy.
   Context `{!ub_clutchGS Σ}.
 
@@ -51,7 +69,17 @@ Section adequacy.
           iMod ("H" with "[$][$]"). iModIntro. iModIntro. done.
         }
         iApply (fupd_mono _ _ (⌜∀ e, R e -> 1 - ε2 <= SeriesC (lim_exec e)⌝)%I).
-        { iIntros (H). iPureIntro. admit. }
+        { iIntros (H). iPureIntro.
+          eapply (twp_step_fupd_ineq_prim_step _ _ _ _ (λ _, ε2)); try done.
+          - exists ε. intros. trans (ε1 + ε2); last lra. destruct ε1, ε2. simpl. lra.
+          - rewrite SeriesC_scal_r. etrans; last exact Hineq.
+            pose proof (pmf_SeriesC (prim_step e σ)).
+            cut (SeriesC (prim_step e σ) * ε2 <= ε2).
+            + intros; lra.
+            + rewrite <-Rmult_1_l. apply Rmult_le_compat_r.
+              * apply cond_nonneg.
+              * exact.
+        }
         iIntros (a HR). iMod ("H" $! a (HR)) as "H".
         destruct a.
         iApply "H".
@@ -69,42 +97,68 @@ Section adequacy.
           iMod ("H" with "[$][$]"). iModIntro. iModIntro. done.
         }
         iApply (fupd_mono _ _ (⌜∀ e, R e -> 1 - (ε2 e) <= SeriesC (lim_exec e)⌝)%I).
-        { iIntros (H). iPureIntro. admit. }
+        { iIntros (H). iPureIntro. by eapply twp_step_fupd_ineq_prim_step. }
         iIntros (a HR). iMod ("H" $! a (HR)) as "H".
         destruct a.
         iApply "H".
-      + iInduction (language.get_active σ) as [| l] "IH".
+      + remember (language.get_active σ) as l.
+        assert (l ⊆ language.get_active σ) as Hsubseteq by set_solver.
+        clear Heql.
+        iInduction (l) as [| l] "IH".
         { rewrite big_orL_nil //. }
         rewrite !big_orL_cons.
         iDestruct "H" as "[H|H]".
-        2:{ by iApply "IH". }
+        2:{ iApply "IH"; try done. iPureIntro. set_solver. }
         iDestruct "H" as "(%R & %ε1 & %ε2 & %Hineq & %Hub & H)".
         iAssert (∀ σ2 : language.state prob_lang,
                    ⌜R σ2⌝ ={∅}=∗ ⌜1 - ε2 <= SeriesC (lim_exec (e, σ2))⌝)%I with "[H]" as "H".
         { iIntros. iMod ("H" $! σ2 (H)) as "H". iDestruct "H" as "[H _]". iApply "H". done. }
         iApply (fupd_mono _ _ (⌜∀ s, R s -> 1 - ε2 <= SeriesC (lim_exec (e, s))⌝)%I).
-        { iIntros (H). iPureIntro. admit. }
+        { iIntros (H). iPureIntro. rewrite (erasure.lim_exec_eq_erasure [l]); last set_solver.
+          simpl. erewrite SeriesC_ext; last by (intros; rewrite dret_id_right).
+          rewrite dbind_mass.
+          erewrite SeriesC_ext.
+          - eapply (twp_step_fupd_ineq_state_step _ _ _ _ _ (λ _, ε2)); try done.
+            + exists ε. intros. trans (ε1 + ε2); last lra. destruct ε1, ε2. simpl. lra.
+            + rewrite SeriesC_scal_r. etrans; last exact Hineq.
+              pose proof (pmf_SeriesC (language.state_step σ l)).
+              cut (SeriesC (language.state_step σ l) * ε2 <= ε2).
+              -- intros; lra.
+              -- rewrite <-Rmult_1_l. apply Rmult_le_compat_r.
+                 ++ apply cond_nonneg.
+                 ++ exact.
+          - intros. by simpl. 
+        }
         iIntros (a HR). iMod ("H" $! a (HR)) as "H".
         destruct a.
         iApply "H".
-      + iInduction (language.get_active σ) as [| l] "IH".
+      + remember (language.get_active σ) as l.
+        assert (l ⊆ language.get_active σ) as Hsubseteq by set_solver.
+        clear Heql.
+        iInduction l as [| l] "IH".
         { rewrite big_orL_nil //. }
         rewrite !big_orL_cons.
         iDestruct "H" as "[H|H]".
-        2:{ by iApply "IH". }
+        2:{ iApply "IH"; try done. iPureIntro. set_solver. }
         iDestruct "H" as "(%R & %ε1 & %ε2  & %Hbound & %Hineq & %Hub & H)".
         iAssert (∀ σ2 : language.state prob_lang,
                    ⌜R σ2⌝ ={∅}=∗ ⌜1 - (ε2 (e, σ2)) <= SeriesC (lim_exec (e, σ2))⌝)%I with "[H]" as "H".
         { iIntros. iMod ("H" $! σ2 (H)) as "H". iDestruct "H" as "[H _]". iApply "H". done. }
         iApply (fupd_mono _ _ (⌜∀ s, R s -> 1 - ε2 (e, s) <= SeriesC (lim_exec (e, s))⌝)%I).
-        { iIntros (H). iPureIntro. admit. }
+        { iIntros (H). iPureIntro. rewrite (erasure.lim_exec_eq_erasure [l]); last set_solver.
+          simpl. erewrite SeriesC_ext; last by (intros; rewrite dret_id_right).
+          rewrite dbind_mass.
+          erewrite SeriesC_ext.
+          - by eapply twp_step_fupd_ineq_state_step.
+          - intros; simpl. done.
+        }    
         iIntros (a HR). iMod ("H" $! a (HR)) as "H".
         destruct a.
         iApply "H".
-  Admitted.
+  Qed.
   
 End adequacy.
-
+  
 
 Theorem twp_mass_lim_exec Σ `{ub_clutchGpreS Σ} (e : expr) (σ : state) (ε : nonnegreal) φ :
   (∀ `{ub_clutchGS Σ}, ⊢ € ε -∗ WP e [{ v, ⌜φ v⌝ }]) →
@@ -120,7 +174,7 @@ Proof.
   epose proof (twp_step_fupd e σ ε φ).
   iApply fupd_wand_r. iSplitL.
   - iApply H1. iFrame. by iApply Hwp.
-  -  iIntros "%". iApply step_fupdN_intro; first done. done. 
+  - iIntros "%". iApply step_fupdN_intro; first done. done. 
 Qed. 
 
 Theorem twp_union_bound_lim Σ `{ub_clutchGpreS Σ} (e : expr) (σ : state) (ε : nonnegreal) φ :

From 1931b323e6f9c487880e2cf99d94d0b2ca667ae1 Mon Sep 17 00:00:00 2001
From: Hei Li <hei411@gmail.com>
Date: Mon, 22 Jan 2024 16:20:52 +0100
Subject: [PATCH 19/21] COMPLETED

---
 theories/ub_logic/total_adequacy.v | 232 ++++++++++++++++++++++++++++-
 1 file changed, 229 insertions(+), 3 deletions(-)

diff --git a/theories/ub_logic/total_adequacy.v b/theories/ub_logic/total_adequacy.v
index 0abe46c8..b1674f56 100644
--- a/theories/ub_logic/total_adequacy.v
+++ b/theories/ub_logic/total_adequacy.v
@@ -7,22 +7,246 @@ From clutch.prob Require Import distribution union_bounds.
 Import uPred.
 
 Lemma twp_step_fupd_ineq_prim_step (e : language.expr prob_lang) σ (ε ε1:nonnegreal) (ε2: language.cfg prob_lang -> nonnegreal) R:
+  reducible e σ -> 
   (∃ r, ∀ ρ : language.cfg prob_lang, ε2 ρ <= r) ->
   ε1 + SeriesC
          (λ ρ, prim_step e σ ρ * ε2 ρ) <= ε -> ub_lift (prim_step e σ) R ε1 ->
   (∀ e, R e → 1 - ε2 e <= SeriesC (lim_exec e)) ->
   1 - ε <= SeriesC (λ a, step (e, σ) a * SeriesC (lim_exec a)).
 Proof.
-Admitted.
+  intros Hred Hbound Hsum Hub H.
+  simpl.
+  assert (1 - (ε1 + SeriesC (λ ρ, prim_step e σ ρ * ε2 ρ)) <=
+            SeriesC (λ a, prim_step e σ a * SeriesC (lim_exec a))) as Hint; last first.
+  { etrans; last exact. apply Rminus_le. lra. }
+  rewrite Rcomplements.Rle_minus_l Rplus_comm Rplus_assoc.
+  rewrite <-SeriesC_plus; last first.
+  { eapply ex_seriesC_le; last first.
+    - instantiate (1 := prim_step e σ).
+      apply pmf_ex_seriesC.
+    -  intros. split.
+       + by apply Rmult_le_pos.
+       + rewrite <-Rmult_1_r. by apply Rmult_le_compat_l.
+  }
+  { destruct Hbound as [r ?]. eapply ex_seriesC_le; last first.
+    - instantiate (1 := λ ρ, prim_step e σ ρ * r).
+      apply ex_seriesC_scal_r.
+      apply pmf_ex_seriesC.
+    -  intros. split.
+       + apply Rmult_le_pos; first done. apply cond_nonneg. 
+       + by apply Rmult_le_compat_l.
+  }
+  erewrite SeriesC_ext; last first.
+  { intros n. by rewrite <-Rmult_plus_distr_l. }
+  simpl in Hub, H, R. simpl.
+  assert (forall ρ, Decision (R ρ)) as Hdec.
+  { intros. apply make_decision. }
+  rewrite (SeriesC_ext _
+             (λ ρ, (if bool_decide(R ρ) then prim_step e σ ρ * (ε2 ρ + SeriesC (lim_exec ρ)) else 0)+
+                     if bool_decide (~R ρ) then prim_step e σ ρ * (ε2 ρ + SeriesC (lim_exec ρ)) else 0
+          )); last first.
+  { intros. repeat case_bool_decide; try done.
+    - by rewrite Rplus_0_r.
+    - by rewrite Rplus_0_l.
+  }
+  rewrite SeriesC_plus; last first.
+  { eapply ex_seriesC_filter_pos.
+    - intros. apply Rmult_le_pos; first done.
+      apply Rplus_le_le_0_compat; [apply cond_nonneg|apply pmf_SeriesC_ge_0].
+    - destruct Hbound as [r?].
+      eapply ex_seriesC_ext; last first.
+      + eapply pmf_ex_seriesC_mult_fn. shelve.
+      + intros. simpl. f_equal.
+        Unshelve. exists (r+1).
+        intros; split.
+        * apply Rplus_le_le_0_compat; [apply cond_nonneg|apply pmf_SeriesC_ge_0].
+        * by apply Rplus_le_compat.
+  }
+  { eapply ex_seriesC_filter_pos.
+    - intros. apply Rmult_le_pos; first done.
+      apply Rplus_le_le_0_compat; [apply cond_nonneg|apply pmf_SeriesC_ge_0].
+    - destruct Hbound as [r?].
+      eapply ex_seriesC_ext; last first.
+      + eapply pmf_ex_seriesC_mult_fn. shelve.
+      + intros. simpl. f_equal.
+        Unshelve. exists (r+1).
+        intros; split.
+        * apply Rplus_le_le_0_compat; [apply cond_nonneg|apply pmf_SeriesC_ge_0].
+        * by apply Rplus_le_compat.
+  }
+  trans (ε1 +
+  (SeriesC
+     (λ x : expr * state,
+        if bool_decide (R x) then prim_step e σ x else 0) +
+   SeriesC
+     (λ x : expr * state,
+        if bool_decide (¬ R x) then prim_step e σ x * (ε2 x + SeriesC (lim_exec x)) else 0))).
+  2:{ apply Rplus_le_compat_l. apply Rplus_le_compat_r.
+      apply SeriesC_le.
+      - intros. case_bool_decide; last done.
+        split; [apply pmf_pos|].
+        rewrite -{1}(Rmult_1_r (prim_step _ _ _)). apply Rmult_le_compat_l; [apply pmf_pos|].
+        pose proof (H n H0).
+        rewrite Rplus_comm. by rewrite <-Rcomplements.Rle_minus_l.
+      - apply ex_seriesC_filter_pos.
+        + intros. apply Rmult_le_pos; [apply pmf_pos|].
+          apply Rplus_le_le_0_compat; [apply cond_nonneg|apply pmf_SeriesC_ge_0].
+        + apply pmf_ex_seriesC_mult_fn. destruct Hbound as [r?]. exists (r+1).
+          intros; split.
+          * apply Rplus_le_le_0_compat; [apply cond_nonneg|apply pmf_SeriesC_ge_0].
+          * by apply Rplus_le_compat.
+  }
+  trans (ε1 +
+           (SeriesC (λ x : expr * state, if bool_decide (R x) then prim_step e σ x else 0))); last first.
+  { rewrite -Rplus_assoc. rewrite -{1}(Rplus_0_r (_+_)).
+    apply Rplus_le_compat_l. apply SeriesC_ge_0'.
+    intros. case_bool_decide; try lra.
+    apply Rmult_le_pos; [apply pmf_pos|].
+    apply Rplus_le_le_0_compat; [apply cond_nonneg|apply pmf_SeriesC_ge_0].
+  }
+  rewrite /ub_lift in Hub.
+  assert (prob (prim_step e σ) (∽(λ ρ, bool_decide(R ρ)))%P <= ε1).
+  { apply Hub. intros. by apply bool_decide_eq_true_2. }
+  etrans.
+  2: { apply Rplus_le_compat_r. exact. }
+  rewrite /prob. simpl.
+  rewrite <-SeriesC_plus; last first.
+  - apply ex_seriesC_filter_pos; [apply pmf_pos|apply pmf_ex_seriesC].
+  - eapply ex_seriesC_ext.
+    + intros. by rewrite <- bool_decide_not.
+    + apply ex_seriesC_filter_pos; [apply pmf_pos|apply pmf_ex_seriesC].
+  - rewrite (SeriesC_ext _ (λ ρ, prim_step e σ ρ)); last first.
+    { intros. case_bool_decide; simpl.
+      - apply Rplus_0_l.
+      - apply Rplus_0_r.
+    }
+    simpl. apply Req_le_sym.
+    epose proof (@prim_step_mass prob_lang) as K. simpl in K.
+    apply K. apply Hred.
+Qed.
 
 Lemma twp_step_fupd_ineq_state_step (e : language.expr prob_lang) σ l (ε ε1:nonnegreal) (ε2: _ -> nonnegreal) R:
+  l ∈ language.get_active σ -> 
   (∃ r, ∀ ρ : language.cfg prob_lang, ε2 ρ <= r) ->
   ε1 + SeriesC
          (λ ρ, language.state_step σ l ρ * ε2 (e, ρ)) <= ε -> ub_lift (language.state_step σ l) R ε1 ->
   (∀ s, R s → 1 - ε2 (e, s) <= SeriesC (lim_exec (e, s))) ->
   1 - ε <= SeriesC (λ a, state_step σ l a * SeriesC (lim_exec (e, a))).
 Proof.
-Admitted.
+intros Hred Hbound Hsum Hub H.
+  simpl.
+  assert (1 - (ε1 + SeriesC (λ ρ, state_step σ l ρ * ε2 (e, ρ))) <=
+            SeriesC (λ a, state_step σ l a * SeriesC (lim_exec (e, a)))) as Hint; last first.
+  { etrans; last exact. rewrite -Ropp_minus_distr -(Ropp_minus_distr (_+_)).
+    apply Ropp_le_cancel. rewrite !Ropp_involutive Rcomplements.Rle_minus_l.
+    rewrite Rplus_assoc Rplus_opp_l Rplus_0_r. done.
+  }
+  rewrite Rcomplements.Rle_minus_l Rplus_comm Rplus_assoc.
+  rewrite <-SeriesC_plus; last first.
+  { eapply ex_seriesC_le; last first.
+    - instantiate (1 := state_step σ l).
+      apply pmf_ex_seriesC.
+    -  intros. split.
+       + by apply Rmult_le_pos.
+       + rewrite <-Rmult_1_r. by apply Rmult_le_compat_l.
+  }
+  { destruct Hbound as [r ?]. eapply ex_seriesC_le; last first.
+    - instantiate (1 := λ ρ, state_step σ l ρ * r).
+      apply ex_seriesC_scal_r.
+      apply pmf_ex_seriesC.
+    -  intros. split.
+       + apply Rmult_le_pos; first done. apply cond_nonneg. 
+       + by apply Rmult_le_compat_l.
+  }
+  erewrite SeriesC_ext; last first.
+  { intros n. by rewrite <-Rmult_plus_distr_l. }
+  simpl in Hub, H, R. simpl.
+  assert (forall ρ, Decision (R ρ)) as Hdec.
+  { intros. apply make_decision. }
+  rewrite (SeriesC_ext _
+             (λ ρ, (if bool_decide(R ρ) then state_step σ l ρ * (ε2 (e, ρ) + SeriesC (lim_exec (e, ρ))) else 0)+
+                     if bool_decide (~R ρ) then state_step σ l ρ * (ε2 (e, ρ) + SeriesC (lim_exec (e, ρ))) else 0
+          )); last first.
+  { intros. repeat case_bool_decide; try done.
+    - by rewrite Rplus_0_r.
+    - by rewrite Rplus_0_l.
+  }
+  rewrite SeriesC_plus; last first.
+  { eapply ex_seriesC_filter_pos.
+    - intros. apply Rmult_le_pos; first done.
+      apply Rplus_le_le_0_compat; [apply cond_nonneg|apply pmf_SeriesC_ge_0].
+    - destruct Hbound as [r?].
+      eapply ex_seriesC_ext; last first.
+      + eapply pmf_ex_seriesC_mult_fn. shelve.
+      + intros. simpl. f_equal.
+        Unshelve. exists (r+1).
+        intros; split.
+        * apply Rplus_le_le_0_compat; [apply cond_nonneg|apply pmf_SeriesC_ge_0].
+        * by apply Rplus_le_compat.
+  }
+  { eapply ex_seriesC_filter_pos.
+    - intros. apply Rmult_le_pos; first done.
+      apply Rplus_le_le_0_compat; [apply cond_nonneg|apply pmf_SeriesC_ge_0].
+    - destruct Hbound as [r?].
+      eapply ex_seriesC_ext; last first.
+      + eapply pmf_ex_seriesC_mult_fn. shelve.
+      + intros. simpl. f_equal.
+        Unshelve. exists (r+1).
+        intros; split.
+        * apply Rplus_le_le_0_compat; [apply cond_nonneg|apply pmf_SeriesC_ge_0].
+        * by apply Rplus_le_compat.
+  }
+  trans (ε1 +
+  (SeriesC
+     (λ x,
+        if bool_decide (R x) then state_step σ l x else 0) +
+   SeriesC
+     (λ x,
+        if bool_decide (¬ R x) then state_step σ l x * (ε2 (e, x) + SeriesC (lim_exec (e, x))) else 0))).
+  2:{ apply Rplus_le_compat_l. apply Rplus_le_compat_r.
+      apply SeriesC_le.
+      - intros. case_bool_decide; last done.
+        split; [apply pmf_pos|].
+        rewrite -{1}(Rmult_1_r (state_step _ _ _)). apply Rmult_le_compat_l; [apply pmf_pos|].
+        pose proof (H n H0).
+        rewrite Rplus_comm. by rewrite <-Rcomplements.Rle_minus_l.
+      - apply ex_seriesC_filter_pos.
+        + intros. apply Rmult_le_pos; [apply pmf_pos|].
+          apply Rplus_le_le_0_compat; [apply cond_nonneg|apply pmf_SeriesC_ge_0].
+        + apply pmf_ex_seriesC_mult_fn. destruct Hbound as [r?]. exists (r+1).
+          intros; split.
+          * apply Rplus_le_le_0_compat; [apply cond_nonneg|apply pmf_SeriesC_ge_0].
+          * by apply Rplus_le_compat.
+  }
+  trans (ε1 +
+           (SeriesC (λ x, if bool_decide (R x) then state_step σ l x else 0))); last first.
+  { rewrite -Rplus_assoc. rewrite -{1}(Rplus_0_r (_+_)).
+    apply Rplus_le_compat_l. apply SeriesC_ge_0'.
+    intros. case_bool_decide; try lra.
+    apply Rmult_le_pos; [apply pmf_pos|].
+    apply Rplus_le_le_0_compat; [apply cond_nonneg|apply pmf_SeriesC_ge_0].
+  }
+  rewrite /ub_lift in Hub.
+  assert (prob (state_step σ l) (∽(λ ρ, bool_decide(R ρ)))%P <= ε1).
+  { apply Hub. intros. by apply bool_decide_eq_true_2. }
+  etrans.
+  2: { apply Rplus_le_compat_r. exact. }
+  rewrite /prob. simpl.
+  rewrite <-SeriesC_plus; last first.
+  - apply ex_seriesC_filter_pos; [apply pmf_pos|apply pmf_ex_seriesC].
+  - eapply ex_seriesC_ext.
+    + intros. by rewrite <- bool_decide_not.
+    + apply ex_seriesC_filter_pos; [apply pmf_pos|apply pmf_ex_seriesC].
+  - rewrite (SeriesC_ext _ (λ ρ, state_step σ l ρ)); last first.
+    { intros. case_bool_decide; simpl.
+      - apply Rplus_0_l.
+      - apply Rplus_0_r.
+    }
+    simpl. apply Req_le_sym.
+    epose proof (@state_step_mass) as K. simpl in K.
+    apply K. simpl in Hred. rewrite /get_active in Hred.
+    set_solver. 
+Qed.
 
 Section adequacy.
   Context `{!ub_clutchGS Σ}.
@@ -119,6 +343,7 @@ Section adequacy.
           rewrite dbind_mass.
           erewrite SeriesC_ext.
           - eapply (twp_step_fupd_ineq_state_step _ _ _ _ _ (λ _, ε2)); try done.
+            + set_solver.
             + exists ε. intros. trans (ε1 + ε2); last lra. destruct ε1, ε2. simpl. lra.
             + rewrite SeriesC_scal_r. etrans; last exact Hineq.
               pose proof (pmf_SeriesC (language.state_step σ l)).
@@ -149,7 +374,8 @@ Section adequacy.
           simpl. erewrite SeriesC_ext; last by (intros; rewrite dret_id_right).
           rewrite dbind_mass.
           erewrite SeriesC_ext.
-          - by eapply twp_step_fupd_ineq_state_step.
+          - eapply twp_step_fupd_ineq_state_step; try done.
+            set_solver. 
           - intros; simpl. done.
         }    
         iIntros (a HR). iMod ("H" $! a (HR)) as "H".

From 88ba1b31b915a63e979d5ecfcb921cc40659dab5 Mon Sep 17 00:00:00 2001
From: Hei Li <hei411@gmail.com>
Date: Tue, 23 Jan 2024 11:11:46 +0100
Subject: [PATCH 20/21] ported continuity laws and prove the ones for ub_logic
 wp and app coupl wp

---
 theories/prob/couplings_app.v | 12 ++++++++++++
 theories/prob/union_bounds.v  | 12 +++++++++++-
 2 files changed, 23 insertions(+), 1 deletion(-)

diff --git a/theories/prob/couplings_app.v b/theories/prob/couplings_app.v
index b7ca0e2c..c51134cb 100644
--- a/theories/prob/couplings_app.v
+++ b/theories/prob/couplings_app.v
@@ -953,6 +953,18 @@ Qed.
     intros ; by eapply ARcoupl_refRcoupl, Rcoupl_refRcoupl.
   Qed.
 
+  Lemma ARcoupl_limit `{Countable A, Countable B} μ1 μ2 ε (ψ : A -> B -> Prop):
+    (forall ε', ε' > ε -> ARcoupl μ1 μ2 ψ ε') -> ARcoupl μ1 μ2 ψ ε.
+  Proof.
+    rewrite /ARcoupl.
+    intros Hlimit. intros.
+    apply real_le_limit.
+    intros. rewrite Rle_minus_l.
+    rewrite Rplus_assoc.
+    apply Hlimit; try done.
+    lra.
+  Qed.
+
 (* Lemma Rcoupl_fair_conv_comb `{Countable A, Countable B} *)
 (*   f `{Inj bool bool (=) (=) f, Surj bool bool (=) f} *)
 (*   (S : A → B → Prop) (μ1 μ2 : distr A) (μ1' μ2' : distr B) : *)
diff --git a/theories/prob/union_bounds.v b/theories/prob/union_bounds.v
index fe2df764..71a1fbc2 100644
--- a/theories/prob/union_bounds.v
+++ b/theories/prob/union_bounds.v
@@ -393,7 +393,17 @@ Proof.
   by apply HP, Hequiv.
 Qed.
 
-
+Lemma ub_lift_epsilon_limit `{Eq: EqDecision A} (μ : distr A) f ε':
+  ε'>=0 -> (forall ε, ε>ε' -> ub_lift μ f ε) -> ub_lift μ f ε'.
+Proof.
+  rewrite /ub_lift.
+  intros Hε' H'.
+  intros. apply real_le_limit.
+  intros ε Hε.
+  rewrite Rle_minus_l.
+  apply H'; first lra.
+  done.
+Qed.
 
 End ub_theory.
 

From c048e6dac0d404a126abcd40302042a3cd5782a0 Mon Sep 17 00:00:00 2001
From: Hei Li <hei411@gmail.com>
Date: Tue, 23 Jan 2024 11:28:45 +0100
Subject: [PATCH 21/21] Implement limit adequacy theorem for ub twp

---
 theories/app_rel_logic/adequacy.v  | 19 +++++++++++++++++++
 theories/ub_logic/adequacy.v       | 20 ++++++++++++++++++++
 theories/ub_logic/total_adequacy.v |  9 +++++++--
 3 files changed, 46 insertions(+), 2 deletions(-)

diff --git a/theories/app_rel_logic/adequacy.v b/theories/app_rel_logic/adequacy.v
index 40759a6d..74253aa4 100644
--- a/theories/app_rel_logic/adequacy.v
+++ b/theories/app_rel_logic/adequacy.v
@@ -337,3 +337,22 @@ Proof.
     apply upper_bound_ge_sup.
     intro; simpl. auto.
 Qed.
+
+Theorem wp_ARcoupl_epsilon_lim Σ `{app_clutchGpreS Σ} (e e' : expr) (σ σ' : state) (ε : nonnegreal) φ :
+  (∀ `{app_clutchGS Σ} (ε' : nonnegreal), ε<ε' -> ⊢ spec_ctx -∗ ⤇ e' -∗ € ε' -∗ WP e {{ v, ∃ v', ⤇ Val v' ∗ ⌜φ v v'⌝ }} ) →
+  ARcoupl (lim_exec (e, σ)) (lim_exec (e', σ')) φ ε.
+Proof.
+  intros H'.
+  apply ARcoupl_limit.
+  intros ε' Hineq.
+  assert (0<=ε') as Hε'.
+  { trans ε; try lra. by destruct ε. }
+  pose (mknonnegreal ε' Hε') as NNRε'.
+  assert (ε' = (NNRbar_to_real (NNRbar.Finite NNRε'))) as Heq.
+  { by simpl. }
+  rewrite Heq.
+  eapply wp_aRcoupl_lim; first done.
+  intros. iIntros "Hctx".
+  iApply (H' with "[$Hctx]").
+  lra.
+Qed. 
diff --git a/theories/ub_logic/adequacy.v b/theories/ub_logic/adequacy.v
index b7bf2bb1..f38a2c3c 100644
--- a/theories/ub_logic/adequacy.v
+++ b/theories/ub_logic/adequacy.v
@@ -249,3 +249,23 @@ Proof.
   intro n.
   apply (wp_union_bound Σ); auto.
 Qed.
+
+Theorem wp_union_bound_epsilon_lim Σ `{ub_clutchGpreS Σ} (e : expr) (σ : state) (ε : nonnegreal) φ :
+  (∀ `{ub_clutchGS Σ} (ε':nonnegreal), ε<ε' -> ⊢ € ε' -∗ WP e {{ v, ⌜φ v⌝ }}) →
+  ub_lift (lim_exec (e, σ)) φ ε.
+Proof.
+  intros H'.
+  apply ub_lift_epsilon_limit.
+  { destruct ε. simpl. lra. }
+  intros ε0 H1.
+  assert (0<=ε0) as Hε0.
+  { trans ε; try lra. by destruct ε. }
+  pose (mknonnegreal ε0 Hε0) as NNRε0.
+  assert (ε0 = (NNRbar_to_real (NNRbar.Finite (NNRε0)))) as Heq.
+  { by simpl. }
+  rewrite Heq.
+  eapply wp_union_bound_lim; first done.
+  intros. iIntros "He".
+  iApply H'; try iFrame.
+  simpl. destruct ε; simpl in H1; simpl; lra.
+Qed.
diff --git a/theories/ub_logic/total_adequacy.v b/theories/ub_logic/total_adequacy.v
index b1674f56..f8ccf43e 100644
--- a/theories/ub_logic/total_adequacy.v
+++ b/theories/ub_logic/total_adequacy.v
@@ -442,5 +442,10 @@ Theorem twp_union_bound_lim_limit Σ `{ub_clutchGpreS Σ} (e : expr) (σ : state
   (∀ `{ub_clutchGS Σ}, (∀ ε':nonnegreal, ε'>ε -> ⊢ € ε' -∗ WP e [{ v, ⌜φ v⌝ }])) →
   ub_lift (lim_exec (e, σ)) φ ε.
 Proof.
-  (* This lemma can be proven with the continuity of ub_lift lemma in the pull request *)
-Admitted.
+  intros. eapply wp_union_bound_epsilon_lim; first done.
+  intros. iStartProof. iIntros "Herr". iApply ub_twp_ub_wp.
+  iAssert (WP e [{ v, ⌜φ v⌝ }])%I with "[Herr]" as "K".
+  2:{ destruct twp_default. destruct wp_default. done. }
+  iApply (H0 with "[$]").
+  apply Rlt_gt. done.
+Qed.