Finish ub_lift_lim proof

theories/prob/union_bounds.v

@@ -4,6 +4,7 @@ From Coquelicot Require Import Rcomplements.
 From stdpp Require Export countable.
 From clutch.prelude Require Export base Coquelicot_ext Reals_ext stdpp_ext.
 From clutch.prob Require Export countable_sum distribution.
+From Coquelicot Require Import Rcomplements Rbar Lim_seq.
 
 Open Scope R.
 
@@ -393,7 +394,98 @@ 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.
+  intros Hε' H'.
+  assert (forall seq,(∃ b, ∀ n, 0 <= - seq n <= b) -> (∀ n, ub_lift μ f (ε'-seq n))->ub_lift μ f (ε'-Sup_seq seq)) as H_limit.
+  { clear H'.
+    rewrite /ub_lift.
+    intros.
+    rewrite Rcomplements.Rle_minus_r.
+    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 (H3 n P H4). rewrite rbar_le_rle. lra.
+    + destruct H2 as [b H2].
+      apply (is_finite_bounded (-b) 0).
+      -- eapply (Sup_seq_minor_le _ _ 0). destruct (H2 0%nat). apply Ropp_le_contravar in H6.
+         rewrite Ropp_involutive in H6. apply H6.
+      -- apply upper_bound_ge_sup. intros n. destruct (H2 n). apply Ropp_le_contravar in H5.
+         rewrite Ropp_involutive in H5. rewrite Ropp_0 in H5. done.
+  }
+  replace ε' with (ε'- Sup_seq (λ x,(λ n,-1%R/(S n)) x)).
+  - 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<=S n); try lra.
+            rewrite S_INR.
+            pose proof (pos_INR n).
+            lra.
+         ++ rewrite S_INR.
+            pose proof (pos_INR n).
+            lra. 
+    }
+    intros. apply H'.
+    assert (1/(S n) > 0); try lra.
+    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 / 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 H2|].
+                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 H2.
+            --- 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 H5.
+                  exfalso. rewrite -H5 in H3. lra.
+                }
+                2: { rewrite Z.compare_gt_iff in H5. exfalso.
+                     assert (IZR (up r) >= 0) by lra.
+                     apply IZR_lt in H5. lra. 
+                }
+                lra.
+Qed.
 
 End ub_theory.
 

theories/ub_logic/adequacy.v

@@ -224,3 +224,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.