Twp

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. 

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 twp_default E e%E Φ)
+  (at level 20, e, Φ at level 200, only parsing) : bi_scope.
+Notation "'WP' e [{ Φ } ]" := (twp twp_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. 

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)) →

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) : *)

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.
 

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.