Skip to content

GitLab

Commit c6c7f702 authored by Hai Dang's avatar Hai Dang
Browse files

More proof reuse

parent a25e7a98
Hide whitespace changes
Inline Side-by-side
theories/examples/stack/proof_elim_graph.v
View file @ c6c7f702
......@@ -162,6 +162,11 @@ Definition stk_props_so_sim (G Gb : graph sevent) (Gx : graph xchg_event) T : Pr
is_pop_xchg_event Gx.(Es) ex2)
e1 e2.
Definition stk_props_stk_logview (E Eb : event_list sevent) T : Prop :=
∀ ee1 ee2 e1 e2, T !! ee1 = Some (inl e1) → T !! ee2 = Some (inl e2) →
∀ eV22 eV2, E !! ee2 = Some eV22 → Eb !! e2 = Some eV2 →
ee1 ∈ eV22.(ge_lview) → e1 ∈ eV2.(ge_lview).
Record StackProps
{G Gb : graph sevent} {Gx : graph xchg_event} {T : list (event_id + event_id)}
{cons : bool} := mkStackProps {
......@@ -195,17 +200,13 @@ Record StackProps
xchgs_in_pairs G T ;
stk_so_sim : (* simulation of so *) stk_props_so_sim G Gb Gx T ;
stk_xchg_consec :
(* we know that exchange event pairs are adjacent *)
(* exchange event pairs are adjacent *)
∀ ee1 ee2 e1 e2,
T !! ee1 = Some (inr e1) → T !! ee2 = Some (inr e2) →
(ee1, ee2) ∈ G.(so) → ee2 = S ee1 ;
stk_base_stack_logview :
(* eco between elim stack events implies eco between base-stack events *)
∀ ee1 ee2 e1 e2,
T !! ee1 = Some (inl e1) → T !! ee2 = Some (inl e2) →
∀ eV22 eV2,
G.(Es) !! ee2 = Some eV22 → Gb.(Es) !! e2 = Some eV2 →
ee1 ∈ eV22.(ge_lview) → e1 ∈ eV2.(ge_lview) ;
stk_props_stk_logview G.(Es) Gb.(Es) T ;
}.
Arguments StackProps : clear implicits.
......@@ -342,6 +343,45 @@ Proof.
intros T' DR e'. rewrite elem_of_app elem_of_list_singleton DR. naive_solver.
Qed.
Lemma StackProps_stk_logview_insert_r E Eb T e eV :
let E' := E ++ [eV] in let T' := T ++ [inr e] in
length T = length E →
stk_props_stk_logview E Eb T → stk_props_stk_logview E' Eb T'.
Proof.
intros E' T' EqL SL ee1 ee2 e1 e2 [Eqee1|[_ ?]]%lookup_app_1; [|done].
intros [Eqee2|[_ ?]]%lookup_app_1; [|done].
intros eV22 eV2 [EqeV2|[-> <-]]%lookup_app_1.
- apply (SL _ _ _ _ Eqee1 Eqee2 _ _ EqeV2).
- exfalso. clear -EqL Eqee2. apply lookup_lt_Some in Eqee2. lia.
Qed.
Lemma StackProps_stk_logview_insert E Eb T eV eVb :
let E' := E ++ [eV] in let Eb' := Eb ++ [eVb] in
let e' := length E in let eb' := length Eb in let T' := T ++ [inl eb'] in
length T = length E →
(∀ e eV, E !! e = Some eV → set_in_bound eV.(ge_lview) E) →
stk_props_dom_l Eb T →
(∀ ee1 e1, T !! ee1 = Some (inl e1) → ee1 ∈ eV.(ge_lview) → e1 ∈ eVb.(ge_lview)) →
(e' ∈ eV.(ge_lview) → eb' ∈ eVb.(ge_lview)) →
stk_props_stk_logview E Eb T → stk_props_stk_logview E' Eb' T'.
Proof.
intros E' Eb' e' eb' T' EqL EGC DL HEEb HEEb' SL.
intros ee1 ee2 e1 e2 Eqee1 Eqee2 eV22 eV2 EqeV22 EqeV2 IneV22.
apply lookup_app_1 in EqeV22 as [EqeV22|[-> <-]]; last first.
{ rewrite -EqL lookup_app_1_eq in Eqee2. apply Some_inj, inl_inj in Eqee2 as <-.
rewrite lookup_app_1_eq in EqeV2. apply Some_inj in EqeV2 as <-.
apply lookup_app_1 in Eqee1 as [Eqee1|[-> <-%inl_inj]].
- apply (HEEb _ _ Eqee1 IneV22).
- apply HEEb'. by rewrite /e' -EqL. }
rewrite lookup_app_1_ne in Eqee2; last first.
{ clear -EqeV22 EqL. intros ->. apply lookup_lt_Some in EqeV22. lia. }
rewrite lookup_app_1_ne in Eqee1; last first.
{ apply (EGC _ _ EqeV22), lookup_lt_is_Some in IneV22. intros ->. lia. }
rewrite lookup_app_1_ne in EqeV2; last first.
{ apply elem_of_list_lookup_2, DL in Eqee2. clear -Eqee2. intros ->. lia. }
by apply (SL _ _ _ _ Eqee1 Eqee2 _ _ EqeV22 EqeV2).
Qed.
(** Simulating unmatched push of base stack *)
Lemma StackProps_unmatched_push {G Gb Gx T u ub} :
StackProps G Gb Gx T true →
......@@ -1185,12 +1225,8 @@ Proof.
rewrite lookup_app_1_ne in Eqe2; [|done].
apply (stk_xchg_consec SP _ _ _ _ Eqe1 Eqe2 InG).
- (* logview of base stack *)
intros ee1 ee2 e1 e2 [Eqee1|[_ ?]]%lookup_app_1; [|done].
intros [Eqee2|[_ ?]]%lookup_app_1; [|done].
intros eV22 eV2 [EqeV2|[-> <-]]%lookup_app_1.
+ apply (stk_base_stack_logview SP _ _ _ _ Eqee1 Eqee2 _ _ EqeV2).
+ exfalso. clear -SP Eqee2.
by apply (StackProps_is_Some_1 SP), lookup_length_not_is_Some in Eqee2. }
apply StackProps_stk_logview_insert_r;
[apply (stk_dom_length SP)|apply (stk_base_stack_logview SP)]. }
assert (SC' : StackConsistent G').
{ destruct SC as [SCNZ SCMA SCFN SCME SCNE SCSO SCLIFO SCMO].
......@@ -1351,30 +1387,18 @@ Proof.
rewrite lookup_app_1_ne in Eqe2; [|done].
apply (stk_xchg_consec SP _ _ _ _ Eqe1 Eqe2 InG).
- (* logview of base stack *)
intros ee1 ee2 e1 e2 Eqee1 Eqee2 eV22 eV2 EqeV22 EqeV2 IneV22.
apply lookup_app_1 in EqeV22 as [EqeV22|[-> <-]]; last first.
{ rewrite EqTps' in Eqee2. apply Some_inj, inl_inj in Eqee2 as <-.
rewrite EqGbps in EqeV2. apply Some_inj in EqeV2 as <-.
move : IneV22. rewrite /= elem_of_union elem_of_singleton.
intros [->|InM].
- rewrite EqTps' in Eqee1. apply Some_inj, inl_inj in Eqee1 as <-. done.
- rewrite lookup_app_1_ne in Eqee1; last first.
{ apply SubM, (StackProps_is_Some _ SP) in InM. clear -InM.
intros ->. by apply lookup_length_not_is_Some in InM. }
apply EL0 in InM as (ee' & Eqee' & In').
rewrite (prefix_lookup _ _ _ _ Eqee' LeT0) in Eqee1.
apply Some_inj in Eqee1 as ->. by apply SubMb0, In'. }
rewrite lookup_app_1_ne in Eqee2; last first.
{ clear -EqeV22 SP. apply (StackProps_is_Some_2 SP) in EqeV22.
intros ->. by apply lookup_length_not_is_Some in EqeV22. }
rewrite lookup_app_1_ne in Eqee1; last first.
{ apply (egcons_logview_closed _ EGCs _ _ EqeV22),
(StackProps_is_Some _ SP) in IneV22. clear -IneV22.
intros ->. by apply lookup_length_not_is_Some in IneV22. }
rewrite EqGb' lookup_app_1_ne in EqeV2; last first.
{ apply (StackProps_is_Some_l_1 SP) in Eqee2. clear -Eqee2.
intros ->. by apply lookup_length_not_is_Some in Eqee2. }
by apply (stk_base_stack_logview SP _ _ _ _ Eqee1 Eqee2 _ _ EqeV22 EqeV2). }
rewrite EqGb'.
apply StackProps_stk_logview_insert;
[apply (stk_dom_length SP)|apply (egcons_logview_closed _ EGCs)
|apply (stk_event_id_map_dom_l SP)|..|done
|apply (stk_base_stack_logview SP)].
clear -SP EL0 SubMb0 LeT0. simpl. intros ee1 e1 Eqee1.
rewrite /= elem_of_union elem_of_singleton. intros [->|InM].
+ exfalso. apply lookup_lt_Some in Eqee1.
rewrite /psIde (stk_dom_length SP) in Eqee1. lia.
+ apply EL0 in InM as (ee' & Eqee' & In').
rewrite (prefix_lookup _ _ _ _ Eqee' LeT0) in Eqee1.
apply Some_inj in Eqee1 as ->. by apply SubMb0, In'. }
assert (SC' : StackConsistent G').
{ destruct SC as [SCNZ SCMA SCFN SCME SCNE SCSO SCLIFO SCMO].
......@@ -1861,18 +1885,8 @@ Proof.
rewrite lookup_app_1_ne in Eqe2; [|done].
apply (stk_xchg_consec SP _ _ _ _ Eqe1 Eqe2 InG).
- (* logview of base stack *)
intros ee1 ee2 e1 e2 Eqee1 Eqee2 eV22 eV2 EqeV22 EqeV2 IneV22.
apply lookup_app_1 in EqeV22 as [EqeV22|[-> <-]]; last first.
{ rewrite EqTpp in Eqee2. clear -Eqee2. by apply Some_inj in Eqee2. }
rewrite lookup_app_1_ne in Eqee2; last first.
{ clear -EqeV22 SP. apply (StackProps_is_Some_2 SP) in EqeV22.
intros ->. by apply lookup_length_not_is_Some in EqeV22. }
rewrite lookup_app_1_ne in Eqee1; last first.
{ apply (egcons_logview_closed _ EGCs _ _ EqeV22),
(StackProps_is_Some _ SP) in IneV22. clear -IneV22.
intros ->. by apply lookup_length_not_is_Some in IneV22. }
by apply (stk_base_stack_logview SP _ _ _ _ Eqee1 Eqee2 _ _ EqeV22 EqeV2).
}
apply StackProps_stk_logview_insert_r;
[apply (stk_dom_length SP)|apply (stk_base_stack_logview SP)]. }
(* update the graph *)
iMod (graph_master_update _ _ _ LeG' with "Gm") as "[[G1 G2] #Gs']"; [done..|].
......@@ -2076,32 +2090,19 @@ Proof.
rewrite lookup_app_1_ne in Eqe2; [|done].
apply (stk_xchg_consec SP _ _ _ _ Eqe1 Eqe2 InG).
- (* logview of base stack *)
intros ee1 ee2 e1 e2 Eqee1 Eqee2 eV22 eV2 EqeV22 EqeV2 IneV22.
apply lookup_app_1 in EqeV22 as [EqeV22|[-> <-]]; last first.
{ rewrite EqTpp in Eqee2. apply Some_inj, inl_inj in Eqee2 as <-.
rewrite Eqpp in EqeV2. apply Some_inj in EqeV2 as <-.
move : IneV22. rewrite /= elem_of_union elem_of_singleton.
intros [->|InM].
- rewrite EqTpp in Eqee1. apply Some_inj, inl_inj in Eqee1 as <-.
rewrite EqMb' -/ppId. set_solver-.
- rewrite lookup_app_1_ne in Eqee1; last first.
{ apply SubM, (StackProps_is_Some _ SP) in InM. clear -InM.
intros ->. by apply lookup_length_not_is_Some in InM. }
apply EL0 in InM as (ee' & Eqee' & In').
rewrite (prefix_lookup _ _ _ _ Eqee' LeT0) in Eqee1.
apply Some_inj in Eqee1 as ->. by apply SubMb0, In'. }
rewrite lookup_app_1_ne in Eqee2; last first.
{ clear -EqeV22 SP. apply (StackProps_is_Some_2 SP) in EqeV22.
intros ->. by apply lookup_length_not_is_Some in EqeV22. }
rewrite lookup_app_1_ne in Eqee1; last first.
{ apply (egcons_logview_closed _ EGCs _ _ EqeV22),
(StackProps_is_Some _ SP) in IneV22. clear -IneV22.
intros ->. by apply lookup_length_not_is_Some in IneV22. }
rewrite EqGb' lookup_app_1_ne in EqeV2; last first.
{ apply (StackProps_is_Some_l_1 SP) in Eqee2. clear -Eqee2.
intros ->. by apply lookup_length_not_is_Some in Eqee2. }
by apply (stk_base_stack_logview SP _ _ _ _ Eqee1 Eqee2 _ _ EqeV22 EqeV2).
}
rewrite EqGb'.
apply StackProps_stk_logview_insert;
[apply (stk_dom_length SP)|apply (egcons_logview_closed _ EGCs)
|apply (stk_event_id_map_dom_l SP)|..| |
|apply (stk_base_stack_logview SP)]; last first.
{ intros _. simpl. rewrite EqMb'. set_solver-. }
clear -SP EL0 SubMb0 LeT0. simpl. intros ee1 e1 Eqee1.
rewrite /= elem_of_union elem_of_singleton. intros [->|InM].
+ exfalso. apply lookup_lt_Some in Eqee1.
rewrite /ppIde (stk_dom_length SP) in Eqee1. lia.
+ apply EL0 in InM as (ee' & Eqee' & In').
rewrite (prefix_lookup _ _ _ _ Eqee' LeT0) in Eqee1.
apply Some_inj in Eqee1 as ->. by apply SubMb0, In'. }
iMod (graph_master_update _ _ _ LeG' with "Gm") as "[[G1 G2] #Gs']"; [done..|].
......@@ -2324,37 +2325,20 @@ Proof.
rewrite lookup_app_1_ne in Eqe2; [|done].
apply (stk_xchg_consec SP _ _ _ _ Eqe1 Eqe2 InG).
- (* logview of base stack *)
intros ee1 ee2 e1 e2 Eqee1 Eqee2 eV22 eV2 EqeV22 EqeV2 IneV22.
apply lookup_app_1 in EqeV22 as [EqeV22|[-> <-]]; last first.
{ rewrite EqTpp in Eqee2. apply Some_inj, inl_inj in Eqee2 as <-.
rewrite Eqpp in EqeV2. apply Some_inj in EqeV2 as <-.
move : IneV22. rewrite /= 2!elem_of_union elem_of_singleton.
intros [InM|[->|InM]].
- rewrite lookup_app_1_ne in Eqee1; last first.
{ apply SubM, (StackProps_is_Some _ SP) in InM. clear -InM.
intros ->. by apply lookup_length_not_is_Some in InM. }
apply EL0 in InM as (ee' & Eqee' & In').
rewrite (prefix_lookup _ _ _ _ Eqee' LeT0) in Eqee1.
apply Some_inj in Eqee1 as ->. by apply SubMb0, In'.
- rewrite EqTpp in Eqee1. apply Some_inj, inl_inj in Eqee1 as <-.
exact InppMb.
- rewrite lookup_app_1_ne in Eqee1; last first.
{ apply (egcons_logview_closed _ EGCs _ _ EqeVps),
(StackProps_is_Some _ SP) in InM. clear -InM.
intros ->. by apply lookup_length_not_is_Some in InM. }
apply SubeV,
(stk_base_stack_logview SP _ _ _ _ Eqee1 EqTps _ _ EqeVps Eqps InM). }
rewrite lookup_app_1_ne in Eqee2; last first.
{ clear -EqeV22 SP. apply (StackProps_is_Some_2 SP) in EqeV22.
intros ->. by apply lookup_length_not_is_Some in EqeV22. }
rewrite lookup_app_1_ne in Eqee1; last first.
{ apply (egcons_logview_closed _ EGCs _ _ EqeV22),
(StackProps_is_Some _ SP) in IneV22. clear -IneV22.
intros ->. by apply lookup_length_not_is_Some in IneV22. }
rewrite EqGb' lookup_app_1_ne in EqeV2; last first.
{ apply (StackProps_is_Some_l_1 SP) in Eqee2. clear -Eqee2.
intros ->. by apply lookup_length_not_is_Some in Eqee2. }
by apply (stk_base_stack_logview SP _ _ _ _ Eqee1 Eqee2 _ _ EqeV22 EqeV2).
rewrite EqGb'.
apply StackProps_stk_logview_insert;
[apply (stk_dom_length SP)|apply (egcons_logview_closed _ EGCs)
|apply (stk_event_id_map_dom_l SP)|..|done
|apply (stk_base_stack_logview SP)].
clear -SP EL0 SubMb0 LeT0 SubeV Eqps EqeVps EqTps. intros ee1 e1 Eqee1.
rewrite /= 2!elem_of_union elem_of_singleton. intros [InM|[->|InM]].
+ apply EL0 in InM as (ee' & Eqee' & In').
rewrite (prefix_lookup _ _ _ _ Eqee' LeT0) in Eqee1.
apply Some_inj in Eqee1 as ->. by apply SubMb0, In'.
+ exfalso. apply lookup_lt_Some in Eqee1.
rewrite /ppIde (stk_dom_length SP) in Eqee1. lia.
+ apply SubeV,
(stk_base_stack_logview SP _ _ _ _ Eqee1 EqTps _ _ EqeVps Eqps InM).
}
iMod (graph_master_update _ _ _ LeG' with "Gm") as "[[G1 G2] #Gs']"; [done..|].
......
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