Skip to content

GitLab

Commit 001500e2 authored by Hai Dang's avatar Hai Dang
Browse files

Remove some unused properties of elim stack proof

parent fda69eb6
Hide whitespace changes
Inline Side-by-side
theories/examples/stack/proof_elim_graph.v
View file @ 001500e2
......@@ -152,8 +152,6 @@ Record StackProps
stk_dom_length :
(* the list T maps G to Gb and Ex *)
length T = length G.(Es) ;
stk_no_dup : (* TODO: no use yet *)
NoDup T ;
stk_event_id_map_inj :
(* T is injective *)
∀ ee1 ee2 e, T !! ee1 = Some e → T !! ee2 = Some e → ee1 = ee2 ;
......@@ -163,10 +161,6 @@ Record StackProps
stk_event_id_map_dom_r :
(* Right elements in T simulate the successful exchange events *)
∀ e, inr e ∈ T ↔ is_successful_xchg_event Gx.(Es) e ;
stk_event_id_mo_mono :
(* simulation of mo *) (* TODO: not used yet *)
∀ e1 e2 ee1 ee2, T !! e1 = Some ee1 → T !! e2 = Some ee2 →
sum_relation (≤)%nat (≤)%nat ee1 ee2 → (e1 ≤ e2)%nat ;
stk_base_stack_map :
(* connecting base stack and elim stack *)
stk_props_stk_map G Gb T ;
......@@ -233,7 +227,6 @@ Definition ElimStackLocalEvents T (M Mb : logView) : Prop :=
Lemma StackProps_empty : StackProps ∅ ∅ ∅ [] true.
Proof.
constructor; try done.
- constructor.
- intros. rewrite elem_of_nil /=. lia.
- intros. rewrite elem_of_nil /= /is_successful_xchg_event /is_xchg_event lookup_nil.
naive_solver.
......@@ -987,8 +980,7 @@ Proof.
{ (* exchange fails *)
iDestruct "F" as %(-> & Eqsox' & ? & ? & ? & ->).
simpl in *. iPureIntro. split; [|done].
constructor;
[apply SP..|done|apply SP|apply SP|done|apply SP| |apply SP|apply SP].
constructor; [apply SP..|done|apply SP|done|apply SP| |apply SP|apply SP].
intros ???? Eq1 Eq2. rewrite Eqsox' (stk_so_sim SP _ _ _ _ Eq1 Eq2).
apply sum_relation_iff; [done|]. rewrite EqGx'. intros x1 x2 -> ->.
(* TODO hard to find lemmas *)
......@@ -1002,7 +994,7 @@ Proof.
iDestruct "F" as %(Lt & -> & EqGx & Eqsox' & Eqcox' & ? & ? & EGx' & ECx').
simpl. iPureIntro. split; [|done].
(* StackProps false ==> StackProps true *)
constructor; [apply SP..|done|apply SP|apply SP|done| | |apply SP|apply SP].
constructor; [apply SP..|done|apply SP|done| | |apply SP|apply SP].
+ clear -SP EqGx' ECx' Eqcox' Lt Posv EqGx.
(* xchgs_in_pairs G T *)
destruct (stk_xchg_push_pop SP) as (Ex & xe & EqEx & Eqxe).
......@@ -1034,7 +1026,7 @@ Proof.
iDestruct "F" as %(Lt & -> & Eqsox' & Eqcox').
simpl. iPureIntro. split; [|done].
(* StackProps true ==> StackProps false *)
constructor; [apply SP..|done|apply SP|apply SP|done| | |apply SP|apply SP].
constructor; [apply SP..|done|apply SP|done| | |apply SP|apply SP].
+ exists Gx.(Es). eexists. split; [exact EqGx'|].
rewrite /= bool_decide_false; [apply SP|done].
+ rewrite Eqsox' EqGx'. clear -SP NPU NPO.
......@@ -1086,9 +1078,6 @@ Proof.
assert (SP': StackProps G' Gb Gx' T' false).
{ constructor.
- by rewrite /= !app_length /= (stk_dom_length SP).
- apply NoDup_app. split; [apply (stk_no_dup SP)|].
split; [|apply NoDup_singleton]. clear -FRT.
intros ? InT ->%elem_of_list_singleton. by apply FRT.
- intros ?? ee [Eq1|[-> <-]]%lookup_app_1 [Eq2|[-> Eqee]]%lookup_app_1; [..|done].
+ apply (stk_event_id_map_inj SP _ _ _ Eq1 Eq2).
+ clear -Eqee FRT Eq1. exfalso. apply FRT.
......@@ -1101,13 +1090,6 @@ Proof.
rewrite elem_of_app (stk_event_id_map_dom_r SP) elem_of_list_singleton
EqGx' /is_successful_xchg_event -is_xchg_event_append.
clear -ISX. naive_solver.
- intros ?? ee1 ee2 [Eq1|[-> <-]]%lookup_app_1 [Eq2|[-> <-]]%lookup_app_1;
[..|done].
+ apply (stk_event_id_mo_mono SP _ _ _ _ Eq1 Eq2).
+ intros _. clear -Eq1. apply lookup_lt_Some in Eq1. lia.
+ inversion 1 as [|? ee2' Lee2]. subst ee2. exfalso.
clear -SP Eq2 Lee2. subst psx.
apply (StackProps_is_Some_r_1_1 SP), lookup_lt_is_Some in Eq2. lia.
- intros ???? EqG [EqT|[_ Eqr]]%lookup_app_1 Eqee; [|clear -Eqr; done].
eapply (stk_base_stack_map SP); [|exact EqT|exact Eqee].
rewrite lookup_app_l in EqG; [done|].
......@@ -1283,8 +1265,6 @@ Proof.
have SP' : StackProps G' Gb' Gx T' true.
{ constructor.
- by rewrite 2!app_length (stk_dom_length SP) /=.
- apply NoDup_app. split; [apply SP|]. split; [|apply NoDup_singleton].
clear -FRT. intros ?? ->%elem_of_list_singleton. by apply FRT.
- intros ?? ee [Eq1|[-> <-]]%lookup_app_1 [Eq2|[-> Eqee]]%lookup_app_1; [..|done].
+ apply (stk_event_id_map_inj SP _ _ _ Eq1 Eq2).
+ clear -Eqee FRT Eq1. exfalso. apply FRT.
......@@ -1297,13 +1277,6 @@ Proof.
+ intros [?| ->]%(Nat.lt_succ_r e)%Nat.le_lteq; [left;lia|by right].
- intros e. rewrite elem_of_app elem_of_list_singleton.
rewrite -(stk_event_id_map_dom_r SP). clear. naive_solver.
- intros ?? ee1 ee2 [Eq1|[-> <-]]%lookup_app_1 [Eq2|[-> <-]]%lookup_app_1;
[..|done].
+ apply (stk_event_id_mo_mono SP _ _ _ _ Eq1 Eq2).
+ intros _. clear -Eq1. apply lookup_lt_Some in Eq1. lia.
+ inversion 1 as [? ee2' Lee2|]. subst ee2. exfalso.
clear -SP Eq2 Lee2.
apply (StackProps_is_Some_l_1 SP), lookup_lt_is_Some in Eq2. lia.
- intros ?? eV' ? EqG [EqT|[-> Eql]]%lookup_app_1 Eqee.
+ eapply (stk_base_stack_map SP); [|exact EqT|].
* rewrite lookup_app_l in EqG; [done|].
......@@ -1627,8 +1600,7 @@ Proof.
iDestruct "F" as %(-> & EqSo' & ? & ? & ? & ->).
simpl. iPureIntro. split; [|done].
(* StackProps G Gb Gx' T true *)
constructor;
[apply SP..|done|apply SP|apply SP|done|apply SP| |apply SP|apply SP].
constructor; [apply SP..|done|apply SP|done|apply SP| |apply SP|apply SP].
rewrite EqSo' EqGx'. clear -SP NPO NPU.
intros ???? Eq1 Eq2. rewrite (stk_so_sim SP _ _ _ _ Eq1 Eq2).
apply sum_relation_iff; [done|]. intros x1 x2 -> ->.
......@@ -1643,7 +1615,7 @@ Proof.
- iDestruct "F" as %(Lt & -> & EqGx & Eqsox' & Eqcox' & ? & ? & ? & ECx').
simpl. iPureIntro. split; [|done].
(* StackProps false ==> StackProps true *)
constructor; [apply SP..|done|apply SP|apply SP|done| | |apply SP|apply SP].
constructor; [apply SP..|done|apply SP|done| | |apply SP|apply SP].
+ destruct (stk_xchg_push_pop SP) as (Ex' & xe & EqEx' & ISP).
have Eqpsx : psx = (length Gx.(Es) - 1)%nat.
{ destruct (xchg_cons_matches _ ECx' psx ppx) as [EqS _].
......@@ -1670,8 +1642,7 @@ Proof.
- iDestruct "F" as %(? & -> & EqSo' & ?).
simpl. iPureIntro. split; [|done].
(* StackProps true ==> StackProps false *)
constructor;
[apply SP..|done|apply SP|apply SP|done| | |apply SP|apply SP].
constructor; [apply SP..|done|apply SP|done| | |apply SP|apply SP].
+ exists Gx.(Es). eexists. split; [exact EqGx'|]. rewrite /=. apply SP.
+ rewrite EqSo' EqGx'. clear -SP NPU NPO.
intros ???? Eq1 Eq2. rewrite (stk_so_sim SP _ _ _ _ Eq1 Eq2).
......@@ -1839,9 +1810,6 @@ Proof.
have SP' : StackProps G' Gb Gx' T' true.
{ constructor.
- by rewrite /= !app_length /= (stk_dom_length SP).
- apply NoDup_app. split; [apply (stk_no_dup SP)|].
split; [|apply NoDup_singleton]. clear -FRT.
intros ? InT ->%elem_of_list_singleton. by apply FRT.
- intros ?? ee [Eq1|[-> <-]]%lookup_app_1 [Eq2|[-> Eqee]]%lookup_app_1; [..|done].
+ apply (stk_event_id_map_inj SP _ _ _ Eq1 Eq2).
+ clear -Eqee FRT Eq1. exfalso. apply FRT.
......@@ -1854,13 +1822,6 @@ Proof.
rewrite elem_of_app (stk_event_id_map_dom_r SP) elem_of_list_singleton EqGx'.
rewrite /is_successful_xchg_event -is_xchg_event_append.
clear -ISX. naive_solver.
- intros ?? ee1 ee2 [Eq1|[-> <-]]%lookup_app_1 [Eq2|[-> <-]]%lookup_app_1;
[..|done].
+ apply (stk_event_id_mo_mono SP _ _ _ _ Eq1 Eq2).
+ intros _. clear -Eq1. apply lookup_lt_Some in Eq1. lia.
+ inversion 1 as [|? ee2' Lee2]. subst ee2. exfalso.
clear -SP Eq2 Lee2. subst ppx.
apply (StackProps_is_Some_r_1_1 SP), lookup_lt_is_Some in Eq2. lia.
- intros ???? EqG [EqT|[_ Eqr]]%lookup_app_1 Eqee; [|clear -Eqr; done].
eapply (stk_base_stack_map SP); [|exact EqT|exact Eqee].
rewrite lookup_app_l in EqG; [done|].
......@@ -2137,8 +2098,6 @@ Proof.
have SP' : StackProps G' Gb' Gx T' true.
{ constructor.
- by rewrite 2!app_length /= (stk_dom_length SP).
- apply NoDup_app. split; [apply SP|]. split; [|apply NoDup_singleton].
clear -FRT. intros ?? ->%elem_of_list_singleton. by apply FRT.
- intros ?? ee [Eq1|[-> <-]]%lookup_app_1 [Eq2|[-> Eqee]]%lookup_app_1; [..|done].
+ apply (stk_event_id_map_inj SP _ _ _ Eq1 Eq2).
+ clear -Eqee FRT Eq1. subst ee. by apply elem_of_list_lookup_2, FRT in Eq1.
......@@ -2150,12 +2109,6 @@ Proof.
+ intros [?| ->]%(Nat.lt_succ_r e)%Nat.le_lteq; [left;lia|by right].
- intros e. rewrite elem_of_app elem_of_list_singleton.
rewrite -(stk_event_id_map_dom_r SP). clear. naive_solver.
- intros ?? ee1 ee2 [Eq1|[-> <-]]%lookup_app_1 [Eq2|[-> <-]]%lookup_app_1;
[..|done].
+ apply (stk_event_id_mo_mono SP _ _ _ _ Eq1 Eq2).
+ intros _. clear -Eq1. apply lookup_lt_Some in Eq1. lia.
+ inversion 1 as [? ee2' Lee2|]. subst ee2. exfalso. clear -SP Eq2 Lee2.
apply (StackProps_is_Some_l_1 SP), lookup_lt_is_Some in Eq2. lia.
- intros ?? eV' eVb EqG [EqT|[-> <-%inl_inj]]%lookup_app_1 Eqee.
+ eapply (stk_base_stack_map SP); [|exact EqT|].
* rewrite lookup_app_l in EqG; [done|].
......@@ -2437,8 +2390,6 @@ Proof.
have SP' : StackProps G' Gb' Gx T' true.
{ constructor.
- by rewrite 2!app_length /= (stk_dom_length SP).
- apply NoDup_app. split; [apply SP|]. split; [|apply NoDup_singleton].
clear -FRT. intros ?? ->%elem_of_list_singleton. by apply FRT.
- intros ?? ee [Eq1|[-> <-]]%lookup_app_1 [Eq2|[-> Eqee]]%lookup_app_1; [..|done].
+ apply (stk_event_id_map_inj SP _ _ _ Eq1 Eq2).
+ clear -Eqee FRT Eq1. exfalso. apply FRT.
......@@ -2451,13 +2402,6 @@ Proof.
+ intros [?| ->]%(Nat.lt_succ_r e)%Nat.le_lteq; [left;lia|by right].
- intros e. rewrite elem_of_app elem_of_list_singleton.
rewrite -(stk_event_id_map_dom_r SP). clear. naive_solver.
- intros ?? ee1 ee2 [Eq1|[-> <-]]%lookup_app_1 [Eq2|[-> <-]]%lookup_app_1;
[..|done].
+ apply (stk_event_id_mo_mono SP _ _ _ _ Eq1 Eq2).
+ intros _. clear -Eq1. apply lookup_lt_Some in Eq1. lia.
+ inversion 1 as [? ee2' Lee2|]. subst ee2. exfalso.
clear -SP Eq2 Lee2.
apply (StackProps_is_Some_l_1 SP), lookup_lt_is_Some in Eq2. lia.
- intros ?? eV' eVb EqG [EqT|[-> <-%inl_inj]]%lookup_app_1 Eqee.
+ eapply (stk_base_stack_map SP); [|exact EqT|].
* rewrite lookup_app_l in EqG; [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