Commit 84abe0cd authored by Ralf Jung's avatar Ralf Jung

shrink proof of timestamp_sub

parent 3b5b94cf
......@@ -216,13 +216,6 @@ Section atomic_snapshot.
iMod (own_op with "Ht") as "[Ht● Ht◯]". iModIntro. iFrame.
Lemma fmap_undo {A B} (f : A -> B) (m : gmap Z A) k v :
f <$> m !! k = Some v ->
exists v', m !! k = Some v' /\ v = f v'.
intros Hl. destruct (m !! k); inversion Hl. subst. eauto.
Lemma timestamp_sub γ (T1 T2 : gmap Z val):
own γ ( gmap_to_UR T1) own γ ( gmap_to_UR T2) -
......@@ -230,16 +223,13 @@ Section atomic_snapshot.
iIntros "[Hγ⚫ Hγ◯]".
iDestruct (own_valid_2 with "Hγ⚫ Hγ◯") as
%[H Hv]%auth_valid_discrete_2. iPureIntro. intros t x Ht.
pose proof (iffLR (lookup_included (gmap_to_UR T2) (gmap_to_UR T1)) H t).
repeat rewrite lookup_fmap in H0.
rewrite Ht in H0. simpl in H0.
pose proof (mk_is_Some (Some (to_agree x)) _ eq_refl) as Hsome.
pose proof (is_Some_included _ _ H0 Hsome); clear Hsome.
destruct H1 as [c Heqx]. rewrite Heqx in H0.
apply (iffLR (Some_included_total _ _)) in H0.
destruct (fmap_undo to_agree _ _ _ Heqx) as [c' [Heq1 Heq2]]. subst.
apply to_agree_included in H0. apply leibniz_equiv in H0. subst. done.
%[H Hv]%auth_valid_discrete_2. iPureIntro. intros t x HT2.
pose proof (iffLR (lookup_included (gmap_to_UR T2) (gmap_to_UR T1)) H t) as Ht.
rewrite !lookup_fmap HT2 /= in Ht.
destruct (is_Some_included _ _ Ht) as [? [t2 [Ht2 ->]]%fmap_Some_1]; first by eauto.
revert Ht.
rewrite Ht2 Some_included_total to_agree_included. fold_leibniz.
by intros ->.
Lemma writeY_spec e (y2: val) γ p :
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