Commit 4a86f45a authored by Joseph Tassarotti's avatar Joseph Tassarotti
Browse files

Helper lemmas for stepshifts for refine monoid.

parent e5e724bc
......@@ -90,6 +90,7 @@ program_logic/sts.v
program_logic/namespaces.v
program_logic/refine_raw.v
program_logic/refine_raw_adequacy.v
program_logic/refine.v
heap_lang/lang.v
heap_lang/tactics.v
heap_lang/wp_tactics.v
......
......@@ -542,6 +542,12 @@ Proof.
unseal; split=> n' x y ?? /=. by rewrite (dist_le _ _ _ _ Ha); last lia.
Qed.
Global Instance ownM_proper: Proper (() ==> (⊣⊢)) (@uPred_ownM M) := ne_proper _.
Global Instance ownMl_ne n : Proper (dist n ==> dist n) (@uPred_ownMl M).
Proof.
intros a b Ha.
unseal; split=> n' x y ?? /=. by rewrite (dist_le _ _ _ _ Ha); last lia.
Qed.
Global Instance ownMl_proper: Proper (() ==> (⊣⊢)) (@uPred_ownMl M) := ne_proper _.
Global Instance valid_ne {A : cmraT} n :
Proper (dist n ==> dist n) (@uPred_valid M A).
Proof.
......@@ -1720,11 +1726,41 @@ Proof. unseal; split=> n x ??; by exists x; rewrite left_id. Qed.
Lemma ownM_empty' : Emp uPred_ownM .
Proof. unseal; split=> n x ??; by split; auto; exists x; rewrite left_id. Qed.
(* Own Linear *)
Lemma ownMl_op (a1 a2 : M) :
uPred_ownMl (a1 a2) ⊣⊢ (uPred_ownMl a1 uPred_ownMl a2).
Proof.
unseal; split=> n x y ??; split.
- intros ?. exists x, (core x), a1, a2;
split_and!; simpl; auto.
by rewrite cmra_core_r.
- intros (y1&y2&q1&q2&Hx&Hy&Hy1&Hy2).
simpl in *. by rewrite Hy Hy1 Hy2.
Qed.
Lemma relevant_ownMl_core (a : M) : ( uPred_ownMl (core a)) ⊣⊢ uPred_ownMl (core a).
Proof.
split=> n x y; split.
- unseal. intros (Hx&?); simpl. simpl in Hx. rewrite Hx. auto.
- unseal=>//=. intros Heq. rewrite -?Heq -(cmra_core_idemp a) Heq.
by rewrite persistent.
Qed.
Lemma relevant_ownMl (a : M) : Persistent a ( uPred_ownMl a) ⊣⊢ uPred_ownMl a.
Proof. intros. by rewrite -(persistent a) relevant_ownMl_core. Qed.
Lemma ownMl_something : True a, uPred_ownMl a.
Proof. unseal; split=> n x y ???. by exists y; simpl. Qed.
Lemma ownMl_empty : Emp ⊣⊢ uPred_ownMl .
Proof. unseal; split=> n x y ??. simpl. split; auto. Qed.
(* Valid *)
Lemma ownM_valid (a : M) : uPred_ownM a a.
Proof.
unseal; split=> n x y Hv ? [a' ?]; cofe_subst; eauto using cmra_validN_op_l.
Qed.
Lemma ownMl_valid (a : M) : uPred_ownMl a (uPred_ownMl a ⧆✓ a).
Proof.
unseal; split=> n x y Hv //= ? Heq.
exists x, (core x), y, . rewrite ?cmra_core_r ?right_id. split_and!; auto; by cofe_subst.
Qed.
Lemma valid_intro {A : cmraT} (a : A) : a True a.
Proof. unseal=> ?; split=> n x y ? ? _ /=; by apply cmra_valid_validN. Qed.
Lemma valid_elim {A : cmraT} (a : A) : ¬ {0} a a False.
......@@ -2010,6 +2046,8 @@ Proof.
*)
Global Instance ownM_relevant : Persistent a RelevantP ((@uPred_ownM M a)).
Proof. intros; rewrite /RelevantP. rewrite relevant_affine unlimited_ownM //=. Qed.
Global Instance ownMl_relevant : Persistent a RelevantP (@uPred_ownMl M a).
Proof. intros; rewrite /RelevantP. rewrite relevant_ownMl //=. Qed.
Global Instance default_relevant {A} P (Ψ : A uPred M) (mx : option A) :
RelevantP P ( x, RelevantP (Ψ x)) RelevantP (default P mx Ψ).
Proof. destruct mx; apply _. Qed.
......
......@@ -3,7 +3,6 @@ From iris.algebra Require Export iprod.
From iris.program_logic Require Export pviewshifts pstepshifts global_functor.
From iris.program_logic Require Import ownership.
Import uPred.
Definition own `{inG Λ Σ (gmapR gname A)} (γ : gname) (a : A) : iPropG Λ Σ :=
ownG (to_globalF γ a).
Definition ownl `{inG Λ Σ (gmapR gname A)} (γ : gname) (a : A) : iPropG Λ Σ :=
......@@ -267,3 +266,32 @@ Qed.
End globale_step.
End globale.
Section globalle.
Context `{i : inG Λ Σ A}.
Implicit Types a : A.
(** * Properties of own *)
Global Instance ownle_ne n : Proper (dist n ==> dist n) (ownle).
Proof. intros x y Heq. rewrite /ownle. solve_proper. Qed.
Global Instance ownle_proper : Proper (() ==> (⊣⊢)) (ownle) := ne_proper _.
Lemma ownle_op a1 a2 : ownle (a1 a2) ⊣⊢ (ownle a1 ownle a2).
Proof. by rewrite /ownle -ownGl_op to_globalFe_op. Qed.
Lemma ownle_valid a : ownle a ⊣⊢ (ownle a ⧆✓ a).
Proof.
apply (anti_symm ()); last apply (sep_elim_l).
rewrite /ownle {1}ownGl_valid_r /to_globalFe.
rewrite iprod_validI (forall_elim inG_id) iprod_lookup_singleton.
apply sep_mono; auto.
trans (⧆✓ cmra_transport inG_prf a : iPropG Λ Σ)%I; last destruct inG_prf; auto.
Qed.
Lemma ownle_valid_r a : ownle a (ownle a ⧆✓ a).
Proof. rewrite {1}ownle_valid //=. Qed.
Lemma ownle_valid_l a : ownle a (⧆✓ a ownle a).
Proof. by rewrite comm -ownle_valid_r. Qed.
Global Instance ownle_core_persistent a : Persistent a RelevantP (ownle a).
Proof. rewrite /ownle; apply _. Qed.
End globalle.
\ No newline at end of file
......@@ -65,6 +65,19 @@ Proof. rewrite /ownG; apply _. Qed.
Global Instance ownG_relevant m : Persistent m RelevantP (ownG m).
Proof. rewrite /ownG; apply _. Qed.
(* linear ghost state *)
Global Instance ownGl_ne n : Proper (dist n ==> dist n) (@ownGl Λ Σ).
Proof. solve_proper. Qed.
Global Instance ownGl_proper : Proper (() ==> (⊣⊢)) (@ownGl Λ Σ) := ne_proper _.
Lemma ownGl_op m1 m2 : ownGl (m1 m2) ⊣⊢ (ownGl m1 ownGl m2).
Proof. by rewrite /ownGl -uPred.ownMl_op Res_op !left_id. Qed.
Lemma ownGl_valid_r m : ownGl m (ownGl m ⧆✓ m).
Proof. rewrite /ownGl {1}uPred.ownMl_valid res_validI /= ?uPred.affine_and; auto with I. Qed.
Lemma ownGl_empty : Emp (ownGl : iProp Λ Σ).
Proof. by rewrite /ownGl uPred.ownMl_empty. Qed.
Global Instance ownGl_relevant m : Persistent m RelevantP (ownGl m).
Proof. rewrite /ownGl; apply _. Qed.
(* inversion lemmas *)
Lemma ownI_spec n r r' i P :
{n} r
......
......@@ -2131,6 +2131,433 @@ Qed.
* intros Hval. inversion Heq. destruct y.
simpl in *. auto.
Qed.
Definition prim_step_nofork : (relation (expr Λ * state Λ)) :=
λ c c', prim_step (fst c) (snd c) (fst c') (snd c') None.
Lemma idx_step_diff j c c' i (e: expr Λ):
idx_step i c c'
nth_error (fst c) j = Some e
i j
nth_error (fst c') j = Some e.
Proof.
rewrite idx_step_equiv. intros Hidx. revert j e. induction Hidx; intros.
- destruct j; [ omega | auto ].
simpl in *. rewrite nth_error_app1; auto.
apply nth_error_Some; congruence.
- destruct j; simpl in *; [ congruence | eapply IHHidx; auto ].
Qed.
Lemma nostep_fixed_extension cfgs1 e ts1 ts2 σ csext ixs1 ixs_ext n:
valid_cfg_idx_seq (cfgs1 ++ [(ts1 ++ e :: ts2, σ)] ++ csext) (ixs1 ++ ixs_ext)
length ixs1 = length cfgs1
length ts1 = n
n ixs_ext
ts1' ts2' σ', length ts1' = n
last (cfgs1 ++ [(ts1 ++ e :: ts2, σ)] ++ csext) =
Some (ts1' ++ e :: ts2', σ').
Proof.
induction csext as [|c'] using rev_ind.
- simpl. rewrite last_snoc; eauto.
- intros (is1a&is1b&?&?&?&Histeps)%valid_cfg_extract'' Hlen.
apply app_inj_1 in H as (->&->); auto.
clear -Histeps.
revert ts1 ts2 σ Histeps.
induction is1b.
* intros. inversion Histeps.
subst. rewrite ?app_assoc last_snoc. eauto.
* intros. inversion Histeps.
subst.
SearchAbout nth_error.
assert (nth_error (fst y) (length ts1) = Some e) as (ts1'&ts2'&Heq&Hlen)%nth_error_split.
{
eapply (idx_step_diff (length ts1)); eauto.
{ rewrite /fst. rewrite nth_error_app2; auto.
replace (length ts1 - length ts1) with 0 by (omega); eauto. }
{ set_solver. }
}
destruct y as (yts&yσ).
subst. edestruct (IHis1b ts1' ts2') as (ts1''&ts2''&σ''&Hlen''&Hlast); eauto.
{ rewrite -Heq. eauto. }
{ set_solver. }
exists ts1'', ts2'', σ''.
split; auto.
rewrite ?assoc ?last_snoc in Hlast *.
auto.
* rewrite Hlen. auto.
Qed.
Lemma valid_seq_join' cs1 c is1 cs2 is2:
valid_cfg_idx_seq (cs1) is1
valid_cfg_idx_seq ([c] ++ cs2) is2
last cs1 = Some c
valid_cfg_idx_seq (cs1 ++ cs2) (is1 ++ is2).
Proof.
destruct cs1 as [| c' cs1] using rev_ind.
- simpl. congruence.
- rewrite last_snoc. intros Hval1 Hval2. inversion 1. subst.
rewrite -assoc. apply valid_seq_join; eauto.
Qed.
Lemma prim_step_nofork_valid_cfg K' ts1 ts2 e sσ e' sσ':
1 K'
nsteps (prim_step_nofork) K' (e, sσ) (e', sσ')
cs ixs,
valid_cfg_idx_seq ([(ts1 ++ e :: ts2, sσ)] ++ cs ++ [(ts1 ++ e' :: ts2, sσ')]) ixs
length ixs = K' i, i ixs i = length ts1.
Proof.
intros Hle Hnsteps.
remember (e, sσ) as c eqn:Heqc.
remember (e', sσ') as c' eqn:Heqc'.
revert e sσ e' sσ' Heqc Heqc' Hle ts1 ts2. induction Hnsteps as [|???? Hprim Hnsteps IH].
- intros; omega.
- intros e sσ e' sσ' -> -> Hle ts1 ts2.
destruct y as (e'', sσ'').
destruct n.
* exists [], [length ts1].
split_and!; auto; last set_solver+.
simpl. econstructor; last econstructor.
rewrite /prim_step_nofork in Hprim.
simpl in *.
inversion Hnsteps. subst.
econstructor; simpl; eauto.
rewrite ?app_nil_r //=.
* edestruct IH as (cs'&ixs'&Hval&Hlen&Hin); eauto.
{ omega. }
exists ((ts1 ++ e'' :: ts2, sσ'') :: cs').
exists (length ts1 :: ixs').
split_and!; simpl; auto.
** econstructor; simpl in *; last eauto.
econstructor; eauto. rewrite ?app_nil_r. auto.
** intros i. clear -Hin. set_solver.
Qed.
Lemma count_occ_le_length {A: Type} (a: A) l eq_dec:
count_occ eq_dec l a length l.
Proof.
induction l; auto.
simpl. destruct eq_dec; omega.
Qed.
Lemma snap_master_stepshift_nofork i e e' ts ts' sσ sσ' sσ'' cs cs' ixs ixs' K':
nth_error ts i = Some e
(1 K' K' K)
nsteps (prim_step_nofork) K' (e, sσ') (e', sσ'')
(to_validity (Refine master (cs' ++ [(ts', sσ')]) ixs') : refine_cmra) #
(to_validity (Refine snapshot {[i]} (cs ++ [(ts, sσ)]) ixs) : refine_cmra) ~~>>:
(λ r rl, cs'' ts'' ixs'',
nth_error ts'' i = Some e'
r to_validity (Refine master (cs'' ++ [(ts'', sσ'')]) ixs'')
rl to_validity (Refine snapshot {[i]} (cs'' ++ [(ts'', sσ'')]) ixs'')).
Proof.
intros Hlookup K_bounds K'_steps n z.
rewrite (comm _ (to_validity _)).
intros Hval.
inversion Hval as (Hvalop&?&Hdisj_prod_z).
inversion Hvalop as (Hval_snap&Hval_master&Hdisj_xy).
inversion Hdisj_xy as [ | ?????? Hinter Hvalid_ext (Heqt&Heqcs_ext) (Heqcs&Heqcs') |].
subst.
rewrite //= -Heqcs' in Hdisj_prod_z.
rewrite prefix_of_op in Hdisj_prod_z; last (eexists; auto).
rewrite //= right_id_L in Hdisj_prod_z.
inversion Hdisj_prod_z as [ | |
?????? Hinter_z Hvalid_ext_z [Heqt_z Heqcs_ext_z Heqixs_ext_z]
(Heq_vz)].
subst.
edestruct Hval_master as (_&Hval_cfg_master); simpl in *.
rewrite -Heqcs' in Hval_cfg_master.
edestruct (nth_error_split ts) as (ts1&ts2&Heq_ts&Hlen); eauto.
rewrite Heq_ts in Hval_cfg_master.
edestruct (nostep_fixed_extension) as (ts1'&ts2'&sσ0'&Hlen'&Hlast'); first (rewrite assoc); eauto.
{ edestruct Hval_snap. simpl in *. symmetry; eapply valid_cfg_idx_length4; eauto. }
{ set_solver. }
edestruct (prim_step_nofork_valid_cfg K' ts1' ts2') as
(cstep&ixstep&Hval_step&Hlen_step&Hidxs_step); eauto.
{ omega. }
assert (sσ0' = sσ') as ->.
{ rewrite -Heq_ts in Hlast'. rewrite app_assoc Heqcs' in Hlast'.
rewrite last_snoc in Hlast'. inversion Hlast'; auto. }
exists (to_validity {| view := master; tids := ;
cfgs := cs ++ [(ts1 ++ e :: ts2, sσ)] ++ cs2 ++ cstep
++ [(ts1' ++ e' :: ts2', sσ'')];
idxs := ixs ++ is2 ++ ixstep |}).
exists (to_validity {| view := snapshot; tids := {[i]};
cfgs := cs ++ [(ts1 ++ e :: ts2, sσ)] ++ cs2 ++ cstep
++ [(ts1' ++ e' :: ts2', sσ'')];
idxs := ixs ++ is2 ++ ixstep |}).
split_and!.
- exists (cs ++ [(ts1 ++ e :: ts2, sσ)] ++ cs2 ++ cstep).
exists (ts1' ++ e' :: ts2').
exists (ixs ++ is2 ++ ixstep).
split_and!.
* rewrite nth_error_app2. replace (i - length ts1') with 0 by omega.
auto. omega.
* rewrite ?app_assoc. reflexivity.
* rewrite ?app_assoc. reflexivity.
- split_and!.
* constructor; split_and!.
** simpl. rewrite ?app_assoc app_comm_cons ?app_assoc last_snoc. set_solver+.
** rewrite /cfgs /idxs.
eapply valid_seq_join' in Hval_cfg_master; eauto.
*** rewrite ?app_assoc in Hval_cfg_master *. auto.
*** rewrite -?app_assoc. auto.
** split_and!.
*** simpl. rewrite ?app_assoc app_comm_cons ?app_assoc last_snoc. set_unfold.
intros ? ->. rewrite app_length. simpl. omega.
*** rewrite /cfgs /idxs.
eapply valid_seq_join' in Hval_cfg_master; eauto.
**** rewrite ?app_assoc in Hval_cfg_master *. auto.
**** rewrite -?app_assoc. auto.
** simpl.
rewrite -[P in {| view := _; tids := _; cfgs := P |}]app_nil_r.
rewrite -[P in {| view := _; tids := _; cfgs := _; idxs := P |}]app_nil_r.
eapply (master_snapshot_disjoint _ _ _ [] _ []).
*** set_solver.
*** set_solver.
* auto.
* simpl. rewrite prefix_of_op; simpl; last (exists []; rewrite ?app_nil_r; done).
rewrite -Heq_vz.
rewrite ?assoc.
rewrite -Heqixs_ext_z.
rewrite app_comm_cons.
rewrite assoc.
rewrite app_comm_cons. rewrite assoc.
rewrite -assoc //= Heq_ts in Heqcs_ext_z .
rewrite -Heqcs_ext_z.
rewrite -?app_assoc.
econstructor.
** set_solver.
** set_solver.
- rewrite Heq_ts. econstructor.
* split; intros Hval'.
** econstructor.
*** simpl. rewrite ?app_assoc app_comm_cons ?app_assoc last_snoc. set_unfold.
intros ? ->. rewrite app_length. simpl. omega.
*** rewrite /cfgs /idxs.
eapply valid_seq_join' in Hval_cfg_master; eauto.
**** rewrite ?app_assoc in Hval_cfg_master *. auto.
**** rewrite -?app_assoc. auto.
** rewrite -Heq_ts. auto.
* intros Hval'.
rewrite /validity_car /to_validity.
eapply (snap_spec_step {[i]} {[i]} cs _ cs2 _ ixs is2).
** rewrite -assoc in Hval_cfg_master. eapply valid_seq_split in Hval_cfg_master; eauto.
destruct Hval' as (?&Hval_cfg'); eapply valid_cfg_idx_length4; eauto.
** clear -Hvalid_ext. set_solver.
** assert (exists cs0, cs ++ [(ts1 ++ e :: ts2, sσ)] ++ cs2 =
cs0 ++ [(ts1' ++ e :: ts2', sσ')]) as (cs0'&Heq_cs0').
{ destruct cs2 as [| c' cs2'] using rev_ind.
- rewrite ?app_nil_r last_snoc in Hlast' *. inversion Hlast'. subst.
eexists; eauto.
- rewrite ?app_assoc last_snoc in Hlast'. inversion Hlast'. subst.
rewrite ?assoc. eexists; eauto.
}
rewrite Heq_cs0'.
rewrite ?app_assoc. rewrite -(app_assoc cs) Heq_cs0'.
rewrite -?app_assoc. rewrite -[P in _ {| view := _; tids := P; |}]right_id_L.
rewrite (app_assoc ixs).
eapply snap_block_step; eauto.
*** clear -Hidxs_step Hlen'. set_solver.
***
Check count_occ.
intros. transitivity (length (ixstep)); first eapply count_occ_le_length.
omega.
*** set_solver.
*** split.
**** set_solver+.
**** clear. rewrite ?app_length //=. omega.
Qed.
Lemma valid_seq_tp_monotone_last c' cs1 cs2 c'' is1:
valid_cfg_idx_seq (cs1 ++ [c'] ++ cs2) is1
last (cs1 ++ [c'] ++ cs2) = Some c''
length (fst c') length (fst c'').
Proof.
destruct cs2 as [| c''' cs2'] using rev_ind.
- simpl. rewrite ?last_snoc. inversion 2. auto.
- rewrite ?app_assoc last_snoc. intros Hval. inversion 1. subst.
eapply valid_seq_tp_monotone_all_tl; eauto. set_solver.
Qed.
Lemma snap_master_simple_fork i e ef e' ts ts' sσ sσ' sσ'' cs cs' ixs ixs':
K <> 0
nth_error ts i = Some e
prim_step e sσ' e' sσ'' (Some ef)
(to_validity (Refine master (cs' ++ [(ts', sσ')]) ixs') : refine_cmra) #
(to_validity (Refine snapshot {[i]} (cs ++ [(ts, sσ)]) ixs) : refine_cmra) ~~>>:
(λ r rl, i' cs'' ts'' ixs'',
nth_error ts'' i = Some e'
nth_error ts'' i' = Some ef
r to_validity (Refine master (cs'' ++ [(ts'', sσ'')]) ixs'')
rl (to_validity (Refine snapshot {[i]} (cs'' ++ [(ts'', sσ'')]) ixs'') : refine_cmra)
to_validity (Refine snapshot {[i']} (cs'' ++ [(ts'', sσ'')]) ixs'')).
Proof.
intros Knz Hlookup step_fork n z.
rewrite (comm _ (to_validity _)).
intros Hval.
inversion Hval as (Hvalop&Hvalz&Hdisj_prod_z).
inversion Hvalop as (Hval_snap&Hval_master&Hdisj_xy).
inversion Hdisj_xy as [ | ?????? Hinter Hvalid_ext (Heqt&Heqcs_ext) (Heqcs&Heqcs') |].
subst.
rewrite //= -Heqcs' in Hdisj_prod_z.
rewrite prefix_of_op in Hdisj_prod_z; last (eexists; auto).
rewrite //= right_id_L in Hdisj_prod_z.
inversion Hdisj_prod_z as [ | |
?????? Hinter_z Hvalid_ext_z [Heqt_z Heqcs_ext_z Heqixs_ext_z]
(Heq_vz)].
subst.
edestruct Hval_master as (Hmaximal&Hval_cfg_master); simpl in *.
rewrite -Heqcs' in Hval_cfg_master.
edestruct (nth_error_split ts) as (ts1&ts2&Heq_ts&Hlen); eauto.
rewrite Heq_ts in Hval_cfg_master.
edestruct (nostep_fixed_extension) as (ts1'&ts2'&sσ0'&Hlen'&Hlast'); first (rewrite assoc); eauto.
{ edestruct Hval_snap. simpl in *. symmetry; eapply valid_cfg_idx_length4; eauto. }
{ set_solver. }
exists (to_validity {| view := master; tids := ;
cfgs := cs ++ [(ts1 ++ e :: ts2, sσ)] ++ cs2
++ [(ts1' ++ e' :: ts2' ++ [ef], sσ'')];
idxs := ixs ++ is2 ++ [i] |}).
exists (to_validity {| view := snapshot; tids := {[i]} {[length (ts1' ++ e' :: ts2')]};
cfgs := cs ++ [(ts1 ++ e :: ts2, sσ)] ++ cs2
++ [(ts1' ++ e' :: ts2' ++ [ef], sσ'')];
idxs := ixs ++ is2 ++ [i] |}).
assert (sσ0' = sσ') as ->.
{ rewrite -Heq_ts in Hlast'. rewrite app_assoc Heqcs' in Hlast'.
rewrite last_snoc in Hlast'. inversion Hlast'; auto. }
split_and!.
- exists (length (ts1' ++ e' :: ts2')).
exists (cs ++ [(ts1 ++ e :: ts2, sσ)] ++ cs2).
exists (ts1' ++ e' :: ts2' ++ [ef]).
exists (ixs ++ is2 ++ [i]).
split_and!.
* rewrite nth_error_app2. replace (i - length ts1') with 0 by omega.
auto. omega.
* rewrite app_comm_cons. rewrite app_assoc. rewrite nth_error_app2.
replace (length (ts1' ++ e' :: ts2') - length (ts1' ++ e' :: ts2')) with 0 by omega.
auto. omega.
* rewrite ?app_assoc. reflexivity.
* rewrite ?app_assoc.
econstructor.
** split.
*** intros Hval'.
econstructor. destruct Hval' as (Hval1&Hval2). simpl in *. econstructor.
**** rewrite ?last_snoc in Hval1 *. set_solver.
**** simpl. auto.
**** split; auto.
edestruct Hval' as (Hval1&Hval2). simpl in *. econstructor; auto.
rewrite ?last_snoc in Hval1 *. set_solver.
simpl. econstructor. set_unfold. rewrite ?app_length. simpl.
intros ?. omega.
left. econstructor. eauto. exists []. split; eauto using app_nil_r.
set_solver+.
*** intros Hval_op. destruct Hval_op as ((Hl1&Hval1)&(Hl2&Hval2)&?Hdisj). econstructor; auto.
rewrite ?last_snoc //= in Hl1 Hl2 *.
set_solver.
** intros ?Hval. simpl. rewrite ?prefix_of_op //=.
-
assert (valid_cfg_idx_seq ((ts1' ++ e :: ts2', sσ') :: (ts1' ++ e' :: ts2' ++ [ef], sσ'') :: nil)
[i]).
{ econstructor. econstructor; eauto. simpl; eauto.
econstructor. }
split_and!.
* constructor; split_and!.
** rewrite /cfgs /tids.
rewrite ?app_assoc last_snoc. set_solver+.
** rewrite /cfgs /idxs.
eapply valid_seq_join' in Hval_cfg_master; rewrite ?app_assoc; eauto.
*** rewrite -?app_assoc. auto.
** split_and!.
*** rewrite /cfgs /tids ?app_assoc ?last_snoc. set_unfold.
intros ? [->| ->]; rewrite ?app_length //= ?app_length //=;
omega.
*** rewrite /cfgs /idxs.
eapply valid_seq_join' in Hval_cfg_master; rewrite ?app_assoc; eauto.
**** rewrite -?app_assoc. auto.
** simpl.
rewrite -[P in {| view := _; tids := _; cfgs := P |}]app_nil_r.
rewrite -[P in {| view := _; tids := _; cfgs := _; idxs := P |}]app_nil_r.
eapply (master_snapshot_disjoint _ _ _ [] _ []).
*** set_solver.
*** set_solver.
* auto.
* simpl. rewrite prefix_of_op; simpl; last (exists []; rewrite ?app_nil_r; done).
rewrite -Heq_vz.
rewrite ?app_assoc.
rewrite -Heqixs_ext_z.
rewrite app_comm_cons.
rewrite app_comm_cons. rewrite app_assoc.
rewrite -assoc //= Heq_ts in Heqcs_ext_z .
rewrite app_assoc.
rewrite -Heqcs_ext_z.
rewrite -?app_assoc.
econstructor.
** clear -Heq_ts Hval_cfg_master Heqcs_ext_z Heqcs' Hinter_z Heq_vz Hvalz Hlast'.
assert ( validity_car z) as Hval_vcz by (destruct z; auto).
rewrite -Heq_vz in Hval_vcz.
destruct Hval_vcz as (Hmaximal&Hval_cs1). simpl in Hmaximal, Hval_cs1.
destruct cs1 as [| c1' cs1' _] using rev_ind.
*** simpl in *; set_solver.
*** rewrite last_snoc in Hmaximal. rewrite -?assoc //= -Heqcs_ext_z in Hval_cfg_master.
assert (length (c1'.1) length (ts1' ++ e :: ts2')).
rewrite -?app_assoc in Hval_cfg_master.
eapply valid_seq_tp_monotone_last in Hval_cfg_master; last first.
**** rewrite assoc Heqcs_ext_z. rewrite //= in Hlast'. rewrite Hlast'. auto.
**** auto.
**** rewrite ?left_id. set_unfold. intros i' (Hnot1&[->| ->]).
set_solver.
Check le_not_gt.
edestruct le_not_lt; eauto.
specialize (Hmaximal _ Hnot1). rewrite ?app_length //= in Hmaximal *.
** set_solver.
-
assert (valid_cfg_idx_seq ((ts1' ++ e :: ts2', sσ') :: (ts1' ++ e' :: ts2' ++ [ef], sσ'') :: nil)
[i]).
{ econstructor. econstructor; eauto. simpl; eauto.
econstructor. }
rewrite Heq_ts. econstructor.
* split; intros Hval'.
** econstructor.
*** rewrite ?app_assoc last_snoc /tids. set_unfold.
rewrite ?app_length //= ?app_length //=. intros ? [-> | ->]; omega.
*** rewrite /cfgs /idxs.
eapply valid_seq_join' in Hval_cfg_master; rewrite ?app_assoc; eauto.
**** rewrite -?app_assoc. auto.
** rewrite -Heq_ts. auto.
* intros Hval'.
rewrite /validity_car /to_validity.
eapply (snap_spec_step {[i]} ({[i]} {[length (ts1' ++ e' :: ts2')]}) cs _ cs2 _ ixs is2).
** rewrite -assoc in Hval_cfg_master. eapply valid_seq_split in Hval_cfg_master; eauto.
destruct Hval' as (?&Hval_cfg'); eapply valid_cfg_idx_length4; eauto.
** clear -Hvalid_ext. set_solver.
** assert (exists cs0, cs ++ [(ts1 ++ e :: ts2, sσ)] ++ cs2 =
cs0 ++ [(ts1' ++ e :: ts2', sσ')]) as (cs0'&Heq_cs0').
{ destruct cs2 as [| c' cs2'] using rev_ind.
- rewrite ?app_nil_r last_snoc in Hlast' *. inversion Hlast'. subst.
eexists; eauto.
- rewrite ?app_assoc last_snoc in Hlast'. inversion Hlast'. subst.
rewrite ?assoc. eexists; eauto.
}
rewrite Heq_cs0'.
rewrite ?app_assoc. rewrite -(app_assoc cs) Heq_cs0'.
rewrite -?app_assoc. rewrite -[P in _ {| view := _; tids := P; |}]right_id_L.
rewrite (app_assoc ixs).
rewrite right_id_L.
rewrite app_assoc.
rewrite -(app_nil_l [(ts1' ++ e' :: ts2' ++ [ef], sσ'')]).
rewrite -app_assoc.
eapply (snap_block_step {[i]} {[length (ts1' ++ e' :: ts2')]}); eauto.
*** set_solver+.
*** simpl. intros; destruct nat_eq_dec. omega. omega.
*** set_solver+.