Commit f301a20b authored by Glen Mével's avatar Glen Mével
Browse files

prove admitted lemmas in program_logic/store.v

parent 82cab7c7
......@@ -620,3 +620,66 @@ Proof. move=>?????. by apply (anti_symm (⊑)). Qed.
Instance flip_partialorder {A : latticeT} :
@PartialOrder A () @PartialOrder A (flip ()).
Proof. move=>?. constructor; apply _. Qed.
(** Lemmas about big_sepL2 *)
From Require Import big_op.
From iris.proofmode Require Import tactics.
Section big_sepL2.
Lemma big_sepL2_split {PROP : bi} {A B : Type} (xs : list A) (ys : list B) (Φ Ψ : nat _ PROP) :
length xs = length ys
([ list] ix xs, Φ i x) ([ list] iy ys, Ψ i y)
([ list] ix;y xs;ys, Φ i x Ψ i y).
iIntros (?) "(HΦ & HΨ)". rewrite big_sepL2_sep. iSplitL "HΦ".
{ rewrite big_sepL2_alt. iSplit; first done.
rewrite -(big_sepL_fmap fst) fst_zip; last lia. done. }
{ rewrite big_sepL2_alt. iSplit; first done.
rewrite -(big_sepL_fmap snd) snd_zip; last lia. done. }
Local Lemma destruct_list_end {A : Type} (xs : list A) :
xs = [] xs' x, xs = xs' ++ [x].
induction xs as [|x0 xs' IH]; first auto. right. destruct IH as [->|(xs'' & x & ->)].
- by exists [], x0.
- by exists (x0 :: xs''), x.
Global Instance big_sepL2_into_pure {PROP : bi} {A B : Type} (xs : list A) (ys : list B)
(Φ φ : nat A B _) :
( i x y, xs !! i = Some x ys !! i = Some y IntoPure (Φ i x y) (φ i x y))
IntoPure (PROP:=PROP) ([ list] ix;y xs;ys, Φ i x y)
(length xs = length ys
i x y, xs !! i = Some x ys !! i = Some y φ i x y).
intros H. rewrite /IntoPure. iIntros "Hxys".
iAssert length xs = length ys%I as %Hlen. { by iApply big_sepL2_length. }
iSplit; first done.
iInduction xs as [|x xs'] "IH" using rev_ind forall (ys H Hlen); first by destruct ys.
destruct (destruct_list_end ys) as [->|(ys' & y & ->)].
{ exfalso. rewrite app_length /= in Hlen. lia. }
assert (length xs' = length ys') as Hlen'. { rewrite 2!app_length/= in Hlen. lia. }
iDestruct (big_sepL2_app_inv with "Hxys") as "[Hxys' Hxy]"; first done.
eassert _ as H'; last iDestruct ("IH" $! ys' H' Hlen' with "Hxys'") as %Hxys'.
{ intros. apply H; by apply lookup_app_l_Some. }
iClear "IH Hxys'". rewrite /= (right_id emp%I) Nat.add_0_r.
assert (IntoPure (Φ (length xs') x y) (φ (length xs') x y)) as H0.
{ apply H; rewrite lookup_app_r ?Hlen' ?Nat.sub_diag; done. }
iDestruct "Hxy" as %Hxy. iPureIntro. clear dependent PROP Hlen.
intros i x0 y0 EQxs EQys.
destruct (decide (i < length xs')%nat).
{ rewrite lookup_app_l in EQxs; last done.
rewrite lookup_app_l in EQys; last by rewrite -Hlen'.
auto. }
{ assert (i = length xs') as ->.
{ apply lookup_lt_Some in EQxs. rewrite app_length/= in EQxs. lia. }
rewrite lookup_app_r Hlen' ?Nat.sub_diag /= in EQxs; last done. injection EQxs as <-.
rewrite lookup_app_r Hlen' ?Nat.sub_diag /= in EQys; last done. injection EQys as <-.
done. }
End big_sepL2.
......@@ -408,8 +408,6 @@ Notation "ℓ *↦at vs" := (mapsto_at_view_block ℓ ((λ v, (v, ∅)) <$> vs)
Section blockwise_store.
Context `{!storeG Σ}.
(* TODO: Prove admitted lemmas! *)
Lemma mapsto_na_block_equiv vs q :
mapsto_na_block vs q ⊣⊢ mapsto_na_block' vs q.
......@@ -479,13 +477,24 @@ Section blockwise_store.
Lemma hist_na_block_agree hs1 hs2 q1 q2 :
hist_na_block hs1 q1 - hist_na_block hs2 q2 - hs1 = hs2.
rewrite hist_na_block_eq/hist_na_block_def.
iIntros "[Hlen1 Hh1] [Hlen2 Hh2]".
iDestruct (has_length_agree with "Hlen1 Hlen2") as %Hlen.
iDestruct (big_sepL2_split with "[$Hh1 $Hh2]") as "H12" ; first lia.
iDestruct (big_sepL2_mono with "H12") as "H12".
{ intros. by apply bi.wand_elim_l', hist_na_agree. }
iDestruct "H12" as %[??]. iPureIntro.
eapply list_eq_same_length; by eauto.
Lemma store_interp_hist_na_block σ hs q :
store_interp σ - hist_na_block hs q -
[ list] ih hs, ⌜σ !! .[i] = Some (store_elt_na h).
rewrite hist_na_block_eq/hist_na_block_def big_andL_forall.
iIntros "Hσ [_?]" (i h Hi). iApply (store_interp_hist_na with "Hσ").
by iApply (big_sepL_lookup (λ i h, hist_na _ _ _) _ _ _ Hi).
Global Instance mapsto_na_block_timeless vs q : Timeless ( *{q} vs).
Proof. apply _. Qed.
......@@ -549,14 +558,29 @@ Section blockwise_store.
Proof. split. done. apply _. Qed.
Lemma mapsto_at_view_block_agree vVs1 vVs2 q1 q2 :
*at{q1}() vVs1 - *at{q2}() vVs2 - vVs1 = vVs2.
*at{q1}() vVs1 - *at{q2}() vVs2 - fst <$> vVs1 = fst <$> vVs2.
rewrite mapsto_at_view_block_eq/mapsto_at_view_block_def.
iIntros "[Hlen1 H1] [Hlen2 H2]".
iDestruct (has_length_agree with "Hlen1 Hlen2") as %Hlen.
iDestruct (big_sepL2_split with "[$H1 $H2]") as "H12"; first lia.
iDestruct (big_sepL2_mono _ (λ _ vV1 vV2, fst vV1 = fst vV2%I) with "H12") as "H12".
{ intros i [??] [??] ??. by apply bi.wand_elim_l', mapsto_at_view_agree. }
iDestruct "H12" as %[??]. iPureIntro.
eapply list_eq_same_length; try by rewrite fmap_length.
intros i v1 v2 Hi H1 H2.
rewrite ->list_lookup_fmap, fmap_Some in H1; destruct H1 as (vV1 & H1 & ->).
rewrite ->list_lookup_fmap, fmap_Some in H2; destruct H2 as (vV2 & H2 & ->).
by eauto.
Lemma store_interp_mapsto_at_view_block σ vVs q :
store_interp σ - *at{q}() vVs -
[ list] ivV vVs, let '(v, V) := vV in
⌜∃ V, V V σ !! .[i] = Some (store_elt_at v V).
rewrite mapsto_at_view_block_eq/mapsto_at_view_block_def big_andL_forall.
iIntros "Hσ [_?]" (i [v V] Hi). iApply (store_interp_mapsto_at_view with "Hσ").
by iApply (big_sepL_lookup (λ i vV, let '(v, V) := vV in mapsto_at_view _ _ _ _) _ _ _ Hi).
End blockwise_store.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment