Progress with flip presample spec

theories/coneris/lib/flip_spec.v

@@ -313,66 +313,77 @@ Next Obligation.
     + by rewrite Z_to_bool_eq_0.
 Qed.
 Next Obligation.
+  simpl.
+  iIntros (????????????? Hsubset Hpos Hineq) "#Hinv #Hvs HP Hfrag".
+  iApply wp_update_state_step_coupl.
+  iIntros (σ ε) "((Hheap&Htapes)&Hε)".
+  iMod (inv_acc with "Hinv") as "[>(% & % & H1 & H2 & H3 & H4 ) Hclose]"; [done|].
+  iDestruct (hocap_tapes_agree with "[$][$]") as "%K".
+  rewrite lookup_fmap_Some in K. destruct K as (?&M&?).
+  simplify_eq.
+  unshelve epose proof fmap_inj _ _ _ _ M as ->.
+  { intros [][]?; by simplify_eq. }
+  erewrite <-(insert_delete m) at 1; last done.
+  rewrite fmap_insert.
+  rewrite big_sepM_insert; last first.
+  { rewrite fmap_delete. apply lookup_delete. }
+  simpl.
+  iDestruct "H3" as "[Htape H3]".
+  iDestruct (tapeN_lookup with "[$][$]") as "(%&%&%Heq)".
+  iDestruct (ec_supply_bound with "[$][$]") as "%".
+  iMod (ec_supply_decrease with "[$][$]") as (ε1' ε_rem -> Hε1') "Hε_supply". subst.
+  iApply fupd_mask_intro; [set_solver|]; iIntros "Hclose'".
+  iApply (state_step_coupl_iterM_state_adv_comp_con_prob_lang num α); first done.
+  unshelve iExists (λ x, mknonnegreal (if length x =? num then ε2 ε1' (nat_to_bool <$> (fin_to_nat <$> x)) else 1) _).
+  { case_match; last (simpl;lra). apply Hpos; first apply cond_nonneg.
+    rewrite !fmap_length.
+    by apply Nat.eqb_eq.
+  }
+  iSplit.
+  { iPureIntro.
+    simpl.
+    unshelve epose proof (Hineq ε1' _) as H'; first apply cond_nonneg.
+    admit. 
+    (* rewrite SeriesC_finite_foldr/=. *)
+    (* rewrite nat_to_bool_eq_0 nat_to_bool_neq_0; last lia. *)
+    (* simpl in *. lra. *)
+  }
+  iIntros (sample) "<-".
+  destruct (Rlt_decision (nonneg ε_rem + (ε2 ε1' (nat_to_bool <$> (fin_to_nat <$> sample))))%R 1%R) as [Hdec|Hdec]; last first.
+  { apply Rnot_lt_ge, Rge_le in Hdec.
+    iApply state_step_coupl_ret_err_ge_1.
+    simpl. simpl in *. rewrite Nat.eqb_refl. lra.
+  }
+  iApply state_step_coupl_ret.
+  unshelve iMod (ec_supply_increase _ (mknonnegreal (ε2 ε1' (nat_to_bool <$> (fin_to_nat <$> sample))) _) with "Hε_supply") as "[Hε_supply Hε]".
+  { apply Hpos; first apply cond_nonneg. by rewrite !fmap_length. }
+  { simpl. done. }
+  simpl.
+  iMod (tapeN_update_append' _ _ _ _ sample with "[$][Htape]") as "[Htapes Htape]".
+  { by erewrite Heq. }
+  iMod (hocap_tapes_presample' _ _ _ _ _ (fin_to_nat <$> sample) with "[$][$]") as "[H4 Hfrag]".
+  iMod "Hclose'" as "_".
+  iMod ("Hvs" with "[$]") as "[%|[H2 HT]]".
+  { iExFalso. iApply (ec_contradict with "[$]"). exact. }
+  assert (∀ (x: list (fin (2))), bool_to_nat <$> (nat_to_bool <$> (fin_to_nat <$> x)) = fin_to_nat <$> x) as Hrewrite.
+  { intros l.
+  rewrite -list_fmap_compose.
+  rewrite <-list_fmap_id.
+  apply list_fmap_ext.
+  intros ?? K. simpl. rewrite nat_to_bool_to_nat; first done.
+  apply list_lookup_fmap_inv in K as (x'&->&?).
+  pose proof fin_to_nat_lt x'. lia. }
+  iMod ("Hclose" with "[$Hε $H2 Htape H3 H4]") as "_".
+  { iNext.
+    iExists (<[α:=(ns ++ (nat_to_bool<$>(fin_to_nat <$> sample)))]>m).
+    rewrite fmap_insert.
+    rewrite big_sepM_insert_delete Heq/=.
+    rewrite fmap_delete. iFrame.
+    rewrite fmap_app/=.
+    rewrite !Hrewrite. iFrame.
+  }
+  iApply fupd_mask_intro_subseteq; first set_solver.
+  iFrame. rewrite fmap_app/=Hrewrite. iFrame.
+  erewrite (nnreal_ext _ _); first done.
+  simpl. by rewrite Nat.eqb_refl.
 Admitted.
-(*   simpl. *)
-(*   iIntros (???????????? Hsubset Hpos Hineq) "#Hinv #Hvs HP Hfrag". *)
-(*   iApply wp_update_state_step_coupl. *)
-(*   iIntros (σ ε) "((Hheap&Htapes)&Hε)". *)
-(*   iMod (inv_acc with "Hinv") as "[>(% & % & H1 & H2 & H3 & H4 ) Hclose]"; [done|]. *)
-(*   iDestruct (hocap_tapes_agree with "[$][$]") as "%K". *)
-(*   rewrite lookup_fmap_Some in K. destruct K as (?&M&?). *)
-(*   simplify_eq. *)
-(*   unshelve epose proof fmap_inj _ _ _ _ M as ->. *)
-(*   { intros [][]?; by simplify_eq. } *)
-(*   erewrite <-(insert_delete m) at 1; last done. *)
-(*   rewrite fmap_insert. *)
-(*   rewrite big_sepM_insert; last first. *)
-(*   { rewrite fmap_delete. apply lookup_delete. } *)
-(*   simpl. *)
-(*   iDestruct "H3" as "[Htape H3]". *)
-(*   iDestruct (tapeN_lookup with "[$][$]") as "(%&%&%Heq)". *)
-(*   iDestruct (ec_supply_bound with "[$][$]") as "%". *)
-(*   iMod (ec_supply_decrease with "[$][$]") as (ε1' ε_rem -> Hε1') "Hε_supply". subst. *)
-(*   iApply fupd_mask_intro; [set_solver|]; iIntros "Hclose'". *)
-(*   iApply state_step_coupl_state_adv_comp_con_prob_lang; first done. *)
-(*   unshelve iExists (λ x, mknonnegreal (ε2 ε1' (nat_to_bool (fin_to_nat x))) _). *)
-(*   { apply Hpos. apply cond_nonneg. } *)
-(*   iSplit. *)
-(*   { iPureIntro. *)
-(*     simpl. *)
-(*     unshelve epose proof (Hineq ε1' _) as H'; first apply cond_nonneg. *)
-(*     rewrite SeriesC_finite_foldr/=. *)
-(*     rewrite nat_to_bool_eq_0 nat_to_bool_neq_0; last lia. *)
-(*     simpl in *. lra. *)
-(*   } *)
-(*   iIntros (sample). *)
-(*   destruct (Rlt_decision (nonneg ε_rem + (ε2 ε1' (nat_to_bool (fin_to_nat sample))))%R 1%R) as [Hdec|Hdec]; last first. *)
-(*   { apply Rnot_lt_ge, Rge_le in Hdec. *)
-(*     iApply state_step_coupl_ret_err_ge_1. *)
-(*     simpl. simpl in *. lra. *)
-(*   } *)
-(*   iApply state_step_coupl_ret. *)
-(*   unshelve iMod (ec_supply_increase _ (mknonnegreal (ε2 ε1' (nat_to_bool (fin_to_nat sample))) _) with "Hε_supply") as "[Hε_supply Hε]". *)
-(*   { apply Hpos. apply cond_nonneg. } *)
-(*   { simpl. done. } *)
-(*   simpl. *)
-(*   iMod (tapeN_update_append _ _ _ _ sample with "[$][Htape]") as "[Htapes Htape]". *)
-(*   { by erewrite Heq. } *)
-(*   iMod (hocap_tapes_presample _ _ _ _ _ (fin_to_nat sample) with "[$][$]") as "[H4 Hfrag]". *)
-(*   iMod "Hclose'" as "_". *)
-(*   iMod ("Hvs" with "[$]") as "[%|[H2 HT]]". *)
-(*   { iExFalso. iApply (ec_contradict with "[$]"). exact. } *)
-(*   iMod ("Hclose" with "[$Hε $H2 Htape H3 H4]") as "_". *)
-(*   { iNext. *)
-(*     iExists (<[α:=(ns ++ [nat_to_bool sample])]>m). *)
-(*     rewrite fmap_insert. *)
-(*     rewrite big_sepM_insert_delete Heq/=. *)
-(*     rewrite fmap_delete. iFrame. *)
-(*     rewrite fmap_app/= nat_to_bool_to_nat; first iFrame. *)
-(*     pose proof fin_to_nat_lt sample. lia. *)
-(*   } *)
-(*   iApply fupd_mask_intro_subseteq; first set_solver. *)
-(*   iFrame. *)
-(*   rewrite fmap_app/= nat_to_bool_to_nat; first done. *)
-(*   pose proof fin_to_nat_lt sample. lia. *)
-(* Qed. *)

theories/coneris/lib/hocap.v

@@ -111,6 +111,13 @@ Section tapes_lemmas.
     iApply (ghost_map_update with "[$][$]"). 
   Qed.
 
+  Lemma hocap_tapes_presample' γ m k N ns ns':
+    (● m @ γ) -∗ (k ◯↪N (N; ns) @ γ) ==∗ (● (<[k:=(N,ns++ns')]>m) @ γ) ∗ (k ◯↪N (N; ns++ns') @ γ).
+  Proof.
+    iIntros "H1 H2".
+    iApply (ghost_map_update with "[$][$]"). 
+  Qed.
+
   Lemma hocap_tapes_pop γ m k N ns n:
     (● m @ γ) -∗ (k ◯↪N (N; n::ns) @ γ) ==∗ (● (<[k:=(N,ns)]>m) @ γ) ∗ (k ◯↪N (N; ns) @ γ).
   Proof.

theories/coneris/primitive_laws.v

@@ -127,6 +127,15 @@ Section tape_interface.
     iFrame.
     by rewrite fmap_app.
   Qed. 
+
+  Lemma tapeN_update_append' α N m (ns ns':list (fin (S N))):
+    tapes_auth 1 m -∗ α ↪N (N; fin_to_nat <$> ns) ==∗ tapes_auth 1 (<[α:=(N; ns ++ ns')]> m) ∗ α ↪N (N; (fin_to_nat <$> ns) ++ (fin_to_nat <$> ns')).
+  Proof.
+    iIntros "? (%&%&?)".
+    iMod (ghost_map_update with "[$][$]") as "[??]".
+    iFrame.
+    by rewrite fmap_app.
+  Qed. 
 
   (*
   Lemma spec_tapeN_to_empty l M :