Skip to content

Commit

Permalink
Merge pull request #8 from hei411/rand-adv
Browse files Browse the repository at this point in the history 
Solving all admits of the rand adv lemma in ub_rules
  • Loading branch information
@hei411
hei411 authored Jan 25, 2024
2 parents 94af3db + 6c55db7 commit f96f49d
Show file tree
Hide file tree
Showing 2 changed files with 107 additions and 9 deletions.
42 changes: 41 additions & 1 deletion theories/prob/countable_sum.v
View file
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
From Coq Require Import Reals Psatz.
From Coquelicot Require Import Series Hierarchy Lim_seq Rbar Lub.
From stdpp Require Import option.
From stdpp Require Export countable finite.
From stdpp Require Export countable finite gmap.
From clutch.prelude Require Import base Reals_ext Coquelicot_ext Series_ext stdpp_ext classical.
Set Default Proof Using "Type*".
Import Hierarchy.
Expand Down Expand Up @@ -472,6 +472,46 @@ Section filter.
+ intro a'; rewrite (bool_decide_ext (a = a') (a' = a)); done.
Qed.

Lemma ex_seriesC_list (l : list A) (f : A -> R):
ex_seriesC (λ (a : A), if bool_decide(a ∈ l) then f a else 0).
Proof.
induction l.
{ eapply ex_seriesC_ext; last apply ex_seriesC_0.
intros; done.
}
destruct (decide(a ∈ l)).
{ eapply ex_seriesC_ext; last done.
intros.
simpl.
erewrite bool_decide_ext; first done.
set_solver.
}
eapply ex_seriesC_ext; last apply ex_seriesC_plus.
2:{ apply IHl. }
2:{ eapply (ex_seriesC_singleton _ (f a)). }
intros x.
simpl.
repeat case_bool_decide; try set_solver.
all: try (by subst).
all: try lra.
- subst. apply Rplus_0_l.
- subst. set_solver.
Qed.

Lemma ex_seriesC_finite_from_option (l : list A) (f : B -> R) (g : A -> option B):
(∀ a : A, is_Some (g a) <-> a ∈ l) ->
ex_seriesC (λ (a : A), from_option f 0%R (g a)).
Proof.
intros Hl.
eapply ex_seriesC_ext; last apply (ex_seriesC_list l).
intros a.
simpl.
case_bool_decide as H1; first done.
destruct (g a) eqn:K.
{ exfalso. apply H1. apply Hl. done. }
done.
Qed.

Lemma is_seriesC_filter_pos f v P `{∀ x, Decision (P x)} :
(∀ n, 0 <= f n) →
is_seriesC f v →
Expand Down
74 changes: 66 additions & 8 deletions theories/ub_logic/ub_rules.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -428,13 +428,15 @@ Proof.
set (foo := (λ (ρ : expr * state),
ε3 +
match ρ with
| (Val (LitV (LitInt n)), σ1) =>
if bool_decide (0 ≤ n)%Z
| (Val (LitV (LitInt n)), σ) =>
if bool_decide(σ = σ1)
then if bool_decide (0 ≤ n)%Z
then match (lt_dec (Z.to_nat n) (S (Z.to_nat z))) with
| left H => ε2 (@Fin.of_nat_lt (Z.to_nat n) (S (Z.to_nat z)) H)
| _ => nnreal_zero
end
else nnreal_zero
else nnreal_zero
else nnreal_zero
| _ => nnreal_zero
end)%NNR).
iExists
Expand All @@ -450,7 +452,7 @@ Proof.
{ transitivity (ε2 0%fin); auto.
apply cond_nonneg.
}
do 5 (case_match; auto).
do 6 (case_match; auto).
apply Hε2.
}
iSplit.
Expand Down Expand Up @@ -487,7 +489,11 @@ Proof.
do 14 (case_match; simplify_eq).
f_equal.
*** do 3 f_equal.
admit.
assert (fin_to_nat (nat_to_fin l0) = fin_to_nat (nat_to_fin l)) as He.
{ by rewrite Hc1. }
rewrite !fin_to_nat_to_fin in He.
apply Z2Nat.inj;
[by eapply bool_decide_eq_true_1|by eapply bool_decide_eq_true_1|done].
*** apply bool_decide_eq_true_1 in H2.
apply bool_decide_eq_true_1 in H.
simplify_eq. done.
Expand Down Expand Up @@ -529,13 +535,64 @@ Proof.
[rewrite SeriesC_0; auto; by rewrite Rmult_0_r|].
intro; rewrite dret_0; auto.
intro; simplify_eq.
** admit.
** eapply ex_seriesC_finite_from_option.
instantiate (1 := (λ n:nat, ( Val #(LitInt n), σ1)) <$> (seq 0%nat (S (Z.to_nat z)))).
intros [e s].
split.
--- case_bool_decide; last first.
{ intros H0. inversion H0. done. }
case_match; try (intros H1; by inversion H1).
case_match; try (intros H2; by inversion H2).
case_match; try (intros H3; by inversion H3).
case_bool_decide; try (intros H4; by inversion H4).
case_match; try (intros H5; by inversion H5).
intros. subst. eapply elem_of_list_fmap_1_alt; last first.
{ repeat f_equal. instantiate (1 := Z.to_nat n). lia. }
rewrite elem_of_seq. lia.
--- intros H. apply elem_of_list_fmap_2 in H.
destruct H as [n[H1 H2]].
inversion H1.
replace (bool_decide (_=_)) with true.
2: { case_bool_decide; done. }
replace (bool_decide _) with true.
2: { case_bool_decide; lia. }
case_match; first done.
rewrite elem_of_seq in H2. lia.
+ rewrite SeriesC_scal_r.
rewrite <- Rmult_1_l.
apply Rmult_le_compat; auto; try lra.
apply cond_nonneg.
- by apply ex_seriesC_scal_r.
- admit.
- eapply ex_seriesC_ext; last eapply ex_seriesC_list.
intros [e s].
instantiate (2 := (λ n:nat, ( Val #(LitInt n), σ1)) <$> (seq 0%nat (S (Z.to_nat z)))).
case_bool_decide; last first.
+ repeat (case_match; try (simpl; lra)).
exfalso. apply H. subst.
eapply elem_of_list_fmap_1_alt; last first.
{ apply bool_decide_eq_true_1 in H3, H4. repeat f_equal.
- instantiate (1 := Z.to_nat n). lia.
- done.
}
rewrite elem_of_seq. lia.
+ instantiate (1 :=
(λ '(e, s), (prim_step (rand #z) σ1 (e, s) *
match e with
| Val #(LitInt n) =>
if bool_decide (s = σ1)
then
if bool_decide (0 ≤ n)%Z
then
match lt_dec (Z.to_nat n) (S (Z.to_nat z)) with
| left H0 => ε2 (nat_to_fin H0)
| right _ => nnreal_zero
end
else nnreal_zero
else nnreal_zero
| _ => nnreal_zero
end)%R)).
simpl. repeat f_equal.
repeat (case_match; try (simpl; lra)).
}
iSplit.
{
Expand All @@ -547,6 +604,7 @@ Proof.
iIntros ((e2 & σ2)) "%H".
destruct H as (n & Hn1); simplify_eq.
rewrite /foo /=.
rewrite bool_decide_eq_true_2; last done.
rewrite bool_decide_eq_true_2; last first.
{
by zify.
Expand All @@ -569,7 +627,7 @@ Proof.
rewrite fin_to_nat_to_fin.
rewrite Nat2Z.id.
reflexivity.
Admitted.
Qed.



Expand Down

0 comments on commit f96f49d

Please sign in to comment.