Commit 27eecdc3 authored by Hai Dang's avatar Hai Dang
Browse files

Minor cleanup

parent 4c3c9058
......@@ -1176,10 +1176,7 @@ Proof.
- intros u1 o1 oV1 u2 o2 uV2 oV2 In1 In2.
destruct (NI _ _ In1), (NI _ _ In2).
do 3 (rewrite lookup_app_1_ne; [|done]). by apply SCLIFO.
- (* TODO: lemma stk_cons_xo_eco_insert *)
intros ??? [?|[-> <-]]%lookup_app_1; [by eapply SCMO|].
rewrite elem_of_union elem_of_singleton. clear -SubM.
intros [->|?%SubM%lookup_lt_is_Some]; [done|subst E; lia]. }
- clear -SCMO SUB'. by apply graph_insert_xo_eco. }
iMod (ge_list_auth_update' _ _ _ LeT' with "oT") as "[oT' #LT']".
iMod (graph_master_update _ _ G' with "Gm") as "[[G1 G2] #Gs']"; [done..|].
......@@ -1389,10 +1386,8 @@ Proof.
- intros u1 o1 oV1 u2 o2 uV2 oV2 In1 In2.
destruct (NI _ _ In1), (NI _ _ In2).
do 3 (rewrite lookup_app_1_ne; [|done]). by apply (stk_cons_LIFO _ SC).
- (* TODO: lemma stk_cons_xo_eco_insert *)
intros ??? [?|[-> <-]]%lookup_app_1; [by eapply (stk_cons_mo_hb _ SC)|].
rewrite elem_of_union elem_of_singleton. clear -SubM.
intros [->|?%SubM%lookup_lt_is_Some]; [done|subst E; lia]. }
- clear -SC SUB'.
apply graph_insert_xo_eco; [by apply (stk_cons_mo_hb _ SC)|done]. }
iMod (ge_list_auth_update' _ _ _ LeT' with "oT") as "[oT' #LT']".
iMod (graph_master_update _ _ _ LeG' with "Gm") as "[[G1 G2] #Gs']"; [done..|].
......@@ -1837,11 +1832,8 @@ Proof.
rewrite lookup_app_1_ne in Equ2; [|done].
rewrite lookup_app_1_ne in Eqo2; [|done].
revert In1 In2 NEqu Eqo1 Equ2 Eqo2. by apply (stk_cons_LIFO _ SC).
- intros ??? [?|[-> <-]]%lookup_app_1; [by eapply (stk_cons_mo_hb _ SC)|].
assert (SubeV2 := egcons_logview_closed _ EGCs _ _ EqeVps).
rewrite 2!elem_of_union elem_of_singleton. clear -SubM SubeV2.
intros [?%SubM%lookup_lt_is_Some|[->|?%SubeV2%lookup_lt_is_Some]];
[subst E; lia|done|lia].
- clear -SubM' SC.
apply graph_insert_xo_eco; [apply (stk_cons_mo_hb _ SC)|done].
}
have SP' : StackProps G' Gb Gx' T' true.
......@@ -2139,10 +2131,8 @@ Proof.
- intros u1 o1 oV1 u2 o2 uV2 oV2 In1 In2.
destruct (NI _ _ In1), (NI _ _ In2).
do 3 (rewrite lookup_app_1_ne; [|done]). by apply (stk_cons_LIFO _ SC).
- (* TODO: lemma stk_cons_xo_eco_insert *)
intros ??? [?|[-> <-]]%lookup_app_1; [by eapply (stk_cons_mo_hb _ SC)|].
rewrite elem_of_union elem_of_singleton. clear -SubM.
intros [->|?%SubM%lookup_lt_is_Some]; [done|subst E; lia]. }
- clear -SC SUB'.
apply graph_insert_xo_eco; [apply (stk_cons_mo_hb _ SC)|done]. }
have SP' : StackProps G' Gb' Gx T' true.
{ constructor.
......@@ -2440,12 +2430,8 @@ Proof.
rewrite lookup_app_1_ne in Equ2; [|done].
rewrite lookup_app_1_ne in Eqo2; [|done].
revert In1 In2 NEqu Eqo1 Equ2 Eqo2. by apply (stk_cons_LIFO _ SC).
- (* TODO: lemma stk_cons_xo_eco_insert *)
intros ??? [?|[-> <-]]%lookup_app_1; [by eapply (stk_cons_mo_hb _ SC)|].
assert (SubeV2 := egcons_logview_closed _ EGCs _ _ EqeVps).
rewrite 2!elem_of_union elem_of_singleton. clear -SubM SubeV2.
intros [?%SubM%lookup_lt_is_Some|[->|?%SubeV2%lookup_lt_is_Some]];
[subst E; lia|done|lia]. }
- clear -SubM' SC.
apply graph_insert_xo_eco; [apply (stk_cons_mo_hb _ SC)|done]. }
(* TODO: dup with push case also *)
have SP' : StackProps G' Gb' Gx T' true.
......
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