completed

logsem · Dec 1, 2023 · c594f70 · c594f70
1 parent b96c7db
commit c594f70
Show file tree

Hide file tree

Showing 3 changed files with 271 additions and 79 deletions.
diff --git a/theories/prob/distribution.v b/theories/prob/distribution.v
@@ -890,6 +890,14 @@ Section subset_distribution_lemmas.
   Proof.
     rewrite /ssd /ssd_pmf /pmf /=.
     destruct (P a) => /=; lra.
+  Qed.
+
+  Lemma ssd_remove P μ : (∀ a, negb (P a) -> μ a = 0) -> ssd P μ = μ.
+  Proof.
+    move=> H0.
+    apply distr_ext. move=> a. destruct (P a) eqn:H'.
+    - by rewrite /ssd{1}/pmf/ssd_pmf H'. 
+    - rewrite /ssd{1}/pmf/ssd_pmf H'. rewrite H0; [done|by rewrite H']. 
   Qed. 
 
 End subset_distribution_lemmas.

diff --git a/theories/program_logic/exec.v b/theories/program_logic/exec.v
@@ -553,15 +553,126 @@ Section prim_exec_lim.
              apply IHn.
   Qed.
 
-  (** * strengthen lemma? *)
+
 
 
+  (** * strengthen lemma? *)
   Lemma ssd_fix_value_lim_exec_val_lim_exec_cfg e σ (v : val Λ):
     SeriesC (ssd (λ '(e', σ'), bool_decide (to_val e' = Some v)) (lim_exec_cfg (e, σ))) =
     SeriesC (ssd (λ e' : val Λ, bool_decide (e' = v)) (lim_exec_val (e, σ))).
   Proof.
-  Admitted.
-
+    rewrite {2}/ssd {2}/pmf/ssd_pmf.
+    pose (id := λ a: val Λ, a).
+    assert ( SeriesC (λ a : val Λ, if bool_decide (a = v) then lim_exec_val (e, σ) a else 0) =
+      (SeriesC (λ a : val Λ, if bool_decide (id a = v) then lim_exec_val (e, σ) v else 0))). 
+    { f_equal. apply functional_extensionality_dep.
+      intros. rewrite /id. case_bool_decide; by subst. }
+    rewrite H.
+    rewrite SeriesC_singleton_inj; [|eauto]. clear H id.
+
+    replace (SeriesC _) with
+            (SeriesC (λ σ', lim_exec_cfg (e, σ) (of_val v, σ'))); last first.
+    { erewrite <-(dmap_mass _ (λ s, s.2)). f_equal.
+      apply functional_extensionality_dep.
+      intros.
+      rewrite /dmap.
+      rewrite {2}/pmf/=/dbind_pmf.
+      replace (SeriesC _) with (SeriesC (λ s, if bool_decide (s = (of_val v, x)) then lim_exec_cfg (e, σ) (of_val v, x) else 0)).
+      2: { f_equal. apply functional_extensionality_dep. intros [].
+           case_bool_decide; rewrite /ssd {2}/pmf/=/ssd_pmf; first case_bool_decide.
+           - inversion H. rewrite dret_1_1; [|done]. by rewrite Rmult_1_r.
+           - inversion H. subst. rewrite to_of_val in H0. done.
+           - rewrite /pmf. case_bool_decide.
+             + apply of_to_val in H0. rewrite H0 in H.
+               replace (dret_pmf _ _) with 0; [lra|].
+               assert (s ≠ x); [intro; by subst|].
+               rewrite /dret_pmf. case_bool_decide; [done|lra].
+             + lra. 
+      }
+      rewrite SeriesC_singleton_inj; eauto.
+    }
+    assert ( (λ σ', lim_exec_cfg (e, σ) (of_val v, σ')) = (λ σ', Sup_seq (λ n, exec_cfg n (e, σ) (of_val v, σ')))).
+    { apply functional_extensionality_dep. by intros. }
+    rewrite H.
+    assert (SeriesC (λ σ', Sup_seq (λ n : nat, exec_cfg n (e, σ) (of_val v, σ'))) = Sup_seq (λ n, SeriesC (λ σ', exec_cfg n (e, σ) (of_val v, σ')))).
+    { eapply MCT_seriesC.
+      - by intros.
+      - intros. apply exec_cfg_mon.
+      - intros.
+        by exists 1.
+      - intros. apply SeriesC_correct. apply ex_distr_lmarg.
+      - rewrite (Rbar_le_sandwich 0 1).
+        + eapply is_sup_seq_ext; last first.
+          { eapply Sup_seq_correct. }
+          intros; done.
+        + eapply (Sup_seq_minor_le _ _ 0%nat). apply SeriesC_ge_0' => ?. done.
+        + apply upper_bound_ge_sup => n.
+          assert ((SeriesC (λ σ', exec_cfg n (e, σ) (of_val v, σ'))) = lmarg (exec_cfg n (e, σ)) (of_val v)).
+          { rewrite lmarg_pmf. done. }
+          rewrite H0.
+          apply pmf_le_1.
+    }
+    rewrite H0. clear H0 H. rewrite lim_exec_val_rw.
+    repeat f_equal. apply functional_extensionality_dep.
+    intros n. revert e σ.
+    induction n; intros.
+    - simpl. destruct (to_val e) eqn:H.
+      + apply of_to_val in H.
+        rewrite /dret/pmf/dret_pmf.
+        case_bool_decide.
+        -- assert ((λ σ', dret (e, σ) (of_val v, σ')) = (dret σ)).
+           { apply functional_extensionality_dep. intros.
+             unfold dret, pmf, dret_pmf.
+             repeat case_bool_decide; try done.
+             + inversion H1. done.
+             + subst. done. 
+           }
+           rewrite H1. f_equal. apply dret_mass.
+        -- assert ( (λ σ', if bool_decide ((of_val v, σ') = (e, σ)) then 1 else 0) = dzero).
+           { apply functional_extensionality_dep. intros. case_bool_decide.
+             - inversion H1. subst. apply of_to_val_flip in H3. rewrite to_of_val in H3.
+               inversion H3. done.
+             - done. 
+           }
+         rewrite H1. f_equal. apply dzero_mass. 
+      + replace (dzero _) with 0; [|done].
+        f_equal. eapply SeriesC_0. intros. done.
+    - destruct (to_val e) eqn:H.
+      + erewrite SeriesC_ext; last first.
+        { intros. simpl. rewrite H. done. }
+        simpl. rewrite H.
+        rewrite /dret/pmf/dret_pmf.
+        case_bool_decide.
+        -- subst.
+           assert ((λ n0 : state Λ, if bool_decide ((of_val v0, n0) = (e, σ)) then 1 else 0) = dret σ).
+           { apply functional_extensionality_dep. intros.
+             unfold dret, pmf, dret_pmf.
+             repeat case_bool_decide; try done.
+             + inversion H0. done.
+             + subst. apply of_to_val in H. by subst. 
+           }
+           rewrite H0. f_equal. apply dret_mass.
+        -- assert ((λ n0 : state Λ, if bool_decide ((of_val v, n0) = (e, σ)) then 1 else 0) = dzero).
+           { apply functional_extensionality_dep. intros. case_bool_decide.
+             - inversion H1. subst. rewrite to_of_val in H.
+               inversion H. done.
+             - done. 
+           }
+         rewrite H1. f_equal. apply dzero_mass. 
+      + simpl. rewrite H.
+        rewrite /dbind/pmf/=/dbind_pmf.
+        assert (SeriesC (λ σ', SeriesC (λ a : cfg Λ, prim_step e σ a * exec_cfg n a (of_val v, σ'))) =
+               SeriesC (λ a: cfg Λ, SeriesC (λ σ', prim_step e σ a * exec_cfg n a (of_val v, σ')))).
+        { rewrite distr_double_swap_lmarg. f_equal. }
+        rewrite H0. clear H0.
+        assert (SeriesC (λ a : cfg Λ, SeriesC (λ σ', prim_step e σ a * exec_cfg n a (of_val v, σ'))) =
+                SeriesC (λ a : cfg Λ, prim_step e σ a * SeriesC (λ σ', exec_cfg n a (of_val v, σ')))).
+        { f_equal. apply functional_extensionality_dep. intros. rewrite SeriesC_scal_l. done. }
+        rewrite H0. clear H0.
+        repeat f_equal. apply functional_extensionality_dep.
+        intros []. f_equal. apply Rbar_finite_eq. apply IHn.
+  Qed. 
+
 
   Lemma lim_exec_val_exec_det n ρ (v : val Λ) σ :
     exec n ρ (of_val v, σ) = 1 →