From 1aaf42dff29454ac853ebbec9c3973ee6424cc4a Mon Sep 17 00:00:00 2001 From: keba4ok <77245196+keba4ok@users.noreply.github.com> Date: Fri, 10 Jan 2025 21:42:12 +0100 Subject: [PATCH] refactor --- src/reordering/ReordExecNaNb.v | 368 +++++++++++----------- src/reordering/ReorderingExecA.v | 134 ++++---- src/reordering/ReorderingExecB.v | 505 ++++++++++++++++--------------- 3 files changed, 506 insertions(+), 501 deletions(-) diff --git a/src/reordering/ReordExecNaNb.v b/src/reordering/ReordExecNaNb.v index d9921d2..8b1b44b 100644 --- a/src/reordering/ReordExecNaNb.v +++ b/src/reordering/ReordExecNaNb.v @@ -538,10 +538,10 @@ Proof using INV INV'. rewrite !seq_union_l, !seq_union_r. apply inclusion_union_l. { apply inclusion_union_l. - { destruct SIMREL. rewrite wf_sbE. + { rewrite wf_sbE. rewrite collect_rel_seqi. rewrite seqA. rewrite collect_rel_eqv. - rewrite rsr_codom. rewrite EXTRAOLD. + rewrite (rsr_codom SIMREL). rewrite EXTRAOLD. clear. basic_solver. } clear. basic_solver. } assert (BMAP : mapper b_t = a_t). @@ -657,9 +657,9 @@ Proof using INV INV'. { apply XmmCons.read_extent with (G_t := G_t') (sc_t := WCore.sc X_t') (a := b_t) (m := mapper'); eauto. { apply SIMREL'. } - { destruct SIMREL'. rewrite rsr_acts. + { rewrite (rsr_acts SIMREL'). rewrite EXTRA; clear; basic_solver. } - { destruct SIMREL'; vauto. } + { apply SIMREL'; vauto. } { arewrite ((WCore.G X_s') = G_s'). intros FALSE. destruct rsr_as_nacq with (X_s := X_s') (X_t := X_t') (a_t := a_t) (b_t := b_t) (mapper := mapper') (x := b_t); vauto. @@ -721,9 +721,8 @@ Proof using INV INV'. { rewrite seq_eqvC. rewrite <- seqA. rewrite seq_eqvC. basic_solver. } assert (SBSUB : ⦗(E_s ∪₁ eq e) \₁ eq b_t⦘ ⨾ sb G_s' ⨾ ⦗(E_s ∪₁ eq e) \₁ eq b_t⦘ ⊆ ⦗(E_s ∪₁ eq e) \₁ eq b_t⦘ ⨾ mapper' ↑ sb_t' ⨾ ⦗(E_s ∪₁ eq e) \₁ eq b_t⦘). - { destruct SIMREL'. - arewrite (G_s' = WCore.G X_s'). - rewrite rsr_sb. rewrite !seq_union_l, !seq_union_r. + { arewrite (G_s' = WCore.G X_s'). + rewrite (rsr_sb SIMREL'). rewrite !seq_union_l, !seq_union_r. apply inclusion_union_l. { apply inclusion_union_l. { unfold swap_rel. @@ -746,12 +745,11 @@ Proof using INV INV'. rewrite <- !id_inter. rewrite <- !seqA. rewrite <- !id_inter. rewrite !seqA. rewrite <- !set_interA. - destruct SIMREL. rewrite rsr_acts. + rewrite (rsr_acts SIMREL). rewrite EXTRAOLD. arewrite ((mapper ↑₁ E_t ∪₁ eq b_t ∪₁ eq e) \₁ eq b_t ⊆₁ mapper ↑₁ E_t ∪₁ eq e). { clear. basic_solver. } - rewrite MAPE. arewrite (mapper ↑₁ E_t ∪₁ eq (mapper' e) ⊆₁ mapper' ↑₁ E_t'). @@ -764,11 +762,11 @@ Proof using INV INV'. unfold collect_rel. exists x', x'. split; vauto. split; vauto. split; vauto. - destruct SIMREL'. split. + split. { unfold G_s' in COND1; ins. - unfold is_r. destruct rsr_lab0 with x'; vauto. } + unfold is_r. destruct (rsr_lab SIMREL') with x'; vauto. } unfold G_s' in COND2; ins. - unfold is_rlx. unfold mod. destruct rsr_lab0 with x'; vauto. } + unfold is_rlx. unfold mod. destruct (rsr_lab SIMREL') with x'; vauto. } arewrite (⦗mapper' ↑₁ E_t' ∩₁ F G_s' ∩₁ Acq G_s'⦘ ⊆ mapper' ↑ ⦗E_t' ∩₁ F G_t' ∩₁ Acq G_t'⦘). { intros x y COND. destruct COND as (EQ & COND); subst y. @@ -776,11 +774,11 @@ Proof using INV INV'. destruct INE as [x' [INE MAP]]. unfold collect_rel. exists x', x'. split; vauto. - split; vauto. destruct SIMREL'. split. + split; vauto. split. { split; vauto. - unfold is_f. destruct rsr_lab0 with x'; vauto. } + unfold is_f. destruct (rsr_lab SIMREL') with x'; vauto. } unfold is_acq. unfold mod. - destruct rsr_lab0 with x'; vauto. } + destruct (rsr_lab SIMREL') with x'; vauto. } arewrite (⦗Acq G_s' ∩₁ mapper' ↑₁ E_t'⦘ ⊆ mapper' ↑ ⦗Acq G_t' ∩₁ E_t'⦘). { intros x y COND. destruct COND as (EQ & COND); subst y. @@ -788,11 +786,11 @@ Proof using INV INV'. destruct INE as [x' [INE MAP]]. unfold set_collect. exists x', x'. split; vauto. - split; vauto. destruct SIMREL'. + split; vauto. split; vauto. unfold G_s' in COND1; ins. unfold is_acq. unfold mod. - destruct rsr_lab0 with x'; vauto. } + destruct (rsr_lab SIMREL') with x'; vauto. } arewrite (mapper' ↑ ⦗Acq G_t' ∩₁ E_t'⦘ ⨾ mapper' ↑ sb_t' ⨾ ⦗mapper' ↑₁ E_t'⦘ ⊆ mapper' ↑ ⦗Acq G_t' ∩₁ E_t'⦘ ⨾ mapper' ↑ sb_t' ⨾ mapper' ↑ ⦗E_t'⦘). { do 2 hahn_frame_l. rewrite collect_rel_eqv; vauto. } @@ -803,11 +801,11 @@ Proof using INV INV'. destruct INE as [x' [INE MAP]]. unfold set_collect. exists x', x'. split; vauto. - split; vauto. destruct SIMREL'. + split; vauto. split; vauto. unfold G_s' in COND1; ins. unfold is_rel. unfold mod. - destruct rsr_lab0 with x'; vauto. } + destruct (rsr_lab SIMREL') with x'; vauto. } arewrite (⦗mapper' ↑₁ E_t'⦘ ⨾ mapper' ↑ sb_t' ⨾ mapper' ↑ ⦗E_t' ∩₁ Rel G_t'⦘ ⊆ mapper' ↑ ⦗E_t'⦘ ⨾ mapper' ↑ sb_t' ⨾ mapper' ↑ ⦗E_t' ∩₁ Rel G_t'⦘). { do 2 hahn_frame_r. rewrite collect_rel_eqv; vauto. } @@ -818,11 +816,11 @@ Proof using INV INV'. destruct INE as [x' [INE MAP]]. unfold collect_rel. exists x', x'. split; vauto. - split; vauto. destruct SIMREL'. split; vauto. + split; vauto. split; vauto. split. - { unfold is_f. destruct rsr_lab0 with x'; vauto. } + { unfold is_f. destruct (rsr_lab SIMREL') with x'; vauto. } unfold is_rel. unfold mod. - destruct rsr_lab0 with x'; vauto. } + destruct (rsr_lab SIMREL') with x'; vauto. } arewrite (⦗(mapper' ↑₁ E_t') ∩₁ W G_s' ∩₁ Rlx G_s'⦘ ⊆ mapper' ↑ ⦗E_t' ∩₁ W G_t' ∩₁ Rlx G_t'⦘). { intros x y COND. destruct COND as (EQ & COND); subst y. @@ -830,11 +828,11 @@ Proof using INV INV'. destruct INE as [x' [INE MAP]]. unfold collect_rel. exists x', x'. split; vauto. - split; vauto. destruct SIMREL'. split. + split; vauto. split. { split; vauto. unfold G_s' in COND1; ins. - unfold is_w. destruct rsr_lab0 with x'; vauto. } + unfold is_w. destruct (rsr_lab SIMREL') with x'; vauto. } unfold G_s' in COND2; ins. - unfold is_rlx. unfold mod. destruct rsr_lab0 with x'; vauto. } + unfold is_rlx. unfold mod. destruct (rsr_lab SIMREL') with x'; vauto. } rewrite !collect_rel_union. apply union_more. { apply union_more. @@ -844,53 +842,55 @@ Proof using INV INV'. { rewrite wf_sbE. basic_solver. } assert (IN2 : dom_rel ⦗E_t' ∩₁ F G_t' ∩₁ Acq G_t'⦘ ⊆₁ E_t'). { basic_solver. } - rewrite IN1, IN2. destruct SIMREL'. - clear - rsr_inj0; basic_solver 8. } + rewrite IN1, IN2. + arewrite (E_t' ∪₁ E_t' ≡₁ E_t'); [basic_solver|]. + eapply (rsr_inj SIMREL'). } assert (IN1 : codom_rel ⦗R_t' ∩₁ Rlx G_t' ∩₁ E_t'⦘ ⊆₁ E_t'). { basic_solver. } assert (IN2 : dom_rel (sb_t' ⨾ ⦗E_t' ∩₁ F G_t' ∩₁ Acq G_t'⦘) ⊆₁ E_t'). { rewrite wf_sbE. basic_solver. } - rewrite IN1, IN2. destruct SIMREL'. - clear - rsr_inj0; basic_solver 8. } + rewrite IN1, IN2. + arewrite (E_t' ∪₁ E_t' ≡₁ E_t'); [basic_solver|]. + eapply (rsr_inj SIMREL'). } rewrite !collect_rel_seq; vauto. { assert (IN1 : codom_rel sb_t' ⊆₁ E_t'). { rewrite wf_sbE. basic_solver. } assert (IN2 : dom_rel ⦗E_t'⦘ ⊆₁ E_t'). { basic_solver. } - rewrite IN1, IN2. destruct SIMREL'. - clear - rsr_inj0; basic_solver 8. } + rewrite IN1, IN2. arewrite (E_t' ∪₁ E_t' ≡₁ E_t'); [basic_solver|]. + eapply (rsr_inj SIMREL'). } assert (IN1 : codom_rel ⦗Acq G_t' ∩₁ E_t'⦘ ⊆₁ E_t'). { basic_solver. } assert (IN2 : dom_rel (sb_t' ⨾ ⦗E_t'⦘) ⊆₁ E_t'). { rewrite wf_sbE. basic_solver. } - rewrite IN1, IN2. destruct SIMREL'. - clear - rsr_inj0; basic_solver 8. } + rewrite IN1, IN2. arewrite (E_t' ∪₁ E_t' ≡₁ E_t'); [basic_solver|]. + eapply (rsr_inj SIMREL'). } rewrite !collect_rel_seq; vauto. { assert (IN1 : codom_rel sb_t' ⊆₁ E_t'). { rewrite wf_sbE. basic_solver. } assert (IN2 : dom_rel ⦗E_t' ∩₁ Rel G_t'⦘ ⊆₁ E_t'). { basic_solver. } - rewrite IN1, IN2. destruct SIMREL'. - clear - rsr_inj0; basic_solver 8. } + rewrite IN1, IN2. arewrite (E_t' ∪₁ E_t' ≡₁ E_t'); [basic_solver|]. + eapply (rsr_inj SIMREL'). } assert (IN1 : codom_rel ⦗E_t'⦘ ⊆₁ E_t'). { basic_solver. } assert (IN2 : dom_rel (sb_t' ⨾ ⦗E_t' ∩₁ Rel G_t'⦘) ⊆₁ E_t'). { rewrite wf_sbE. basic_solver. } - rewrite IN1, IN2. destruct SIMREL'. - clear - rsr_inj0; basic_solver 8. } + rewrite IN1, IN2. arewrite (E_t' ∪₁ E_t' ≡₁ E_t'); [basic_solver|]. + eapply (rsr_inj SIMREL'). } rewrite !collect_rel_seq; vauto. { assert (IN1 : codom_rel sb_t' ⊆₁ E_t'). { rewrite wf_sbE. basic_solver. } assert (IN2 : dom_rel ⦗E_t' ∩₁ W_t' ∩₁ Rlx G_t'⦘ ⊆₁ E_t'). { basic_solver. } - rewrite IN1, IN2. destruct SIMREL'. - clear - rsr_inj0; basic_solver 8. } + rewrite IN1, IN2. arewrite (E_t' ∪₁ E_t' ≡₁ E_t'); [basic_solver|]. + eapply (rsr_inj SIMREL'). } assert (IN1 : codom_rel ⦗F G_t' ∩₁ Rel G_t' ∩₁ E_t'⦘ ⊆₁ E_t'). { basic_solver. } assert (IN2 : dom_rel (sb_t' ⨾ ⦗E_t' ∩₁ W_t' ∩₁ Rlx G_t'⦘) ⊆₁ E_t'). { rewrite wf_sbE. basic_solver. } - rewrite IN1, IN2. destruct SIMREL'. - clear - rsr_inj0; basic_solver 8. } + rewrite IN1, IN2. arewrite (E_t' ∪₁ E_t' ≡₁ E_t'); [basic_solver|]. + eapply (rsr_inj SIMREL'). } assert (IND2 : mapper' ↑ (rpo_imm G_t')⁺ ⨾ ⦗(E_s ∪₁ eq e) \₁ eq b_t⦘ ⨾ (rpo_imm G_s' ⨾ ⦗(E_s ∪₁ eq e) \₁ eq b_t⦘) ⊆ mapper' ↑ (rpo_imm G_t')⁺). { assert (TRIN : mapper' ↑ (rpo_imm G_t')⁺ ⨾ mapper' ↑ (rpo_imm G_t')⁺ @@ -901,7 +901,7 @@ Proof using INV INV'. destruct P2 as (x0'' & y' & (P2 & M3 & M4)). exists x', y'. splits; vauto. assert (EQ : x0'' = x0'). - { destruct SIMREL'. apply rsr_inj; vauto. + { apply (rsr_inj SIMREL'); vauto. { apply ct_begin in P2. destruct P2 as (x1 & P2 & P3). apply wf_rpo_immE in P2; vauto. @@ -970,8 +970,7 @@ Proof using INV INV'. unfold G_s'; ins. left. apply (rsr_acts SIMREL). right. apply EXTRAOLD; basic_solver. } clear - EMP. basic_solver. } - { destruct SIMREL'. - rewrite rsr_rf. apply union_more; vauto. + { rewrite (rsr_rf SIMREL'). apply union_more; vauto. apply seq_more; vauto. rewrite EXTRA. unfold is_r. arewrite (WCore.G X_s' = G_s'). @@ -981,8 +980,7 @@ Proof using INV INV'. { red; intros x COND. destruct COND as [COND1 COND2]; vauto. } red; intros x COND. split; vauto. } - { destruct SIMREL'. - rewrite rsr_co. unfold add_max. + { rewrite (rsr_co SIMREL'). unfold add_max. rewrite EXTRA. arewrite ((extra_co_D (acts_set (WCore.G X_s')) (lab (WCore.G X_s')) (loc (lab (WCore.G X_s')) b_t) \₁ eq b_t ∩₁ W (WCore.G X_s')) @@ -1001,7 +999,7 @@ Proof using INV INV'. apply XmmCons.write_extent with (G_t := G_t') (sc_t := WCore.sc X_t') (a := b_t) (m := mapper'); eauto. { apply SIMREL'. } - { destruct SIMREL'. rewrite rsr_acts. + { rewrite (rsr_acts SIMREL'). rewrite EXTRA; clear; basic_solver. } { destruct SIMREL'; vauto. } { rewrite EQACTS. @@ -1060,9 +1058,8 @@ Proof using INV INV'. { rewrite seq_eqvC. rewrite <- seqA. rewrite seq_eqvC. basic_solver. } assert (SBSUB : ⦗(E_s ∪₁ eq e) \₁ eq b_t⦘ ⨾ sb G_s' ⨾ ⦗(E_s ∪₁ eq e) \₁ eq b_t⦘ ⊆ ⦗(E_s ∪₁ eq e) \₁ eq b_t⦘ ⨾ mapper' ↑ sb_t' ⨾ ⦗(E_s ∪₁ eq e) \₁ eq b_t⦘). - { destruct SIMREL'. - arewrite (G_s' = WCore.G X_s'). - rewrite rsr_sb. rewrite !seq_union_l, !seq_union_r. + { arewrite (G_s' = WCore.G X_s'). + rewrite (rsr_sb SIMREL'). rewrite !seq_union_l, !seq_union_r. apply inclusion_union_l. { apply inclusion_union_l. { unfold swap_rel. @@ -1085,7 +1082,7 @@ Proof using INV INV'. rewrite <- !id_inter. rewrite <- !seqA. rewrite <- !id_inter. rewrite !seqA. rewrite <- !set_interA. - destruct SIMREL. rewrite rsr_acts. + rewrite (rsr_acts SIMREL). rewrite EXTRAOLD. arewrite ((mapper ↑₁ E_t ∪₁ eq b_t ∪₁ eq e) \₁ eq b_t ⊆₁ mapper ↑₁ E_t ∪₁ eq e). @@ -1102,11 +1099,11 @@ Proof using INV INV'. unfold collect_rel. exists x', x'. split; vauto. split; vauto. split; vauto. - destruct SIMREL'. split. + split. { unfold G_s' in COND1; ins. - unfold is_r. destruct rsr_lab0 with x'; vauto. } + unfold is_r. destruct (rsr_lab SIMREL') with x'; vauto. } unfold G_s' in COND2; ins. - unfold is_rlx. unfold mod. destruct rsr_lab0 with x'; vauto. } + unfold is_rlx. unfold mod. destruct (rsr_lab SIMREL') with x'; vauto. } arewrite (⦗mapper' ↑₁ E_t' ∩₁ F G_s' ∩₁ Acq G_s'⦘ ⊆ mapper' ↑ ⦗E_t' ∩₁ F G_t' ∩₁ Acq G_t'⦘). { intros x y COND. destruct COND as (EQ & COND); subst y. @@ -1114,11 +1111,11 @@ Proof using INV INV'. destruct INE as [x' [INE MAP]]. unfold collect_rel. exists x', x'. split; vauto. - split; vauto. destruct SIMREL'. split. + split; vauto. split. { split; vauto. - unfold is_f. destruct rsr_lab0 with x'; vauto. } + unfold is_f. destruct (rsr_lab SIMREL') with x'; vauto. } unfold is_acq. unfold mod. - destruct rsr_lab0 with x'; vauto. } + destruct (rsr_lab SIMREL') with x'; vauto. } arewrite (⦗Acq G_s' ∩₁ mapper' ↑₁ E_t'⦘ ⊆ mapper' ↑ ⦗Acq G_t' ∩₁ E_t'⦘). { intros x y COND. destruct COND as (EQ & COND); subst y. @@ -1126,11 +1123,11 @@ Proof using INV INV'. destruct INE as [x' [INE MAP]]. unfold set_collect. exists x', x'. split; vauto. - split; vauto. destruct SIMREL'. + split; vauto. split; vauto. unfold G_s' in COND1; ins. unfold is_acq. unfold mod. - destruct rsr_lab0 with x'; vauto. } + destruct (rsr_lab SIMREL') with x'; vauto. } arewrite (mapper' ↑ ⦗Acq G_t' ∩₁ E_t'⦘ ⨾ mapper' ↑ sb_t' ⨾ ⦗mapper' ↑₁ E_t'⦘ ⊆ mapper' ↑ ⦗Acq G_t' ∩₁ E_t'⦘ ⨾ mapper' ↑ sb_t' ⨾ mapper' ↑ ⦗E_t'⦘). { do 2 hahn_frame_l. rewrite collect_rel_eqv; vauto. } @@ -1141,11 +1138,11 @@ Proof using INV INV'. destruct INE as [x' [INE MAP]]. unfold set_collect. exists x', x'. split; vauto. - split; vauto. destruct SIMREL'. + split; vauto. split; vauto. unfold G_s' in COND1; ins. unfold is_rel. unfold mod. - destruct rsr_lab0 with x'; vauto. } + destruct (rsr_lab SIMREL') with x'; vauto. } arewrite (⦗mapper' ↑₁ E_t'⦘ ⨾ mapper' ↑ sb_t' ⨾ mapper' ↑ ⦗E_t' ∩₁ Rel G_t'⦘ ⊆ mapper' ↑ ⦗E_t'⦘ ⨾ mapper' ↑ sb_t' ⨾ mapper' ↑ ⦗E_t' ∩₁ Rel G_t'⦘). { do 2 hahn_frame_r. rewrite collect_rel_eqv; vauto. } @@ -1156,11 +1153,11 @@ Proof using INV INV'. destruct INE as [x' [INE MAP]]. unfold collect_rel. exists x', x'. split; vauto. - split; vauto. destruct SIMREL'. split; vauto. + split; vauto. split; vauto. split. - { unfold is_f. destruct rsr_lab0 with x'; vauto. } + { unfold is_f. destruct (rsr_lab SIMREL') with x'; vauto. } unfold is_rel. unfold mod. - destruct rsr_lab0 with x'; vauto. } + destruct (rsr_lab SIMREL') with x'; vauto. } arewrite (⦗(mapper' ↑₁ E_t') ∩₁ W G_s' ∩₁ Rlx G_s'⦘ ⊆ mapper' ↑ ⦗E_t' ∩₁ W G_t' ∩₁ Rlx G_t'⦘). { intros x y COND. destruct COND as (EQ & COND); subst y. @@ -1168,11 +1165,11 @@ Proof using INV INV'. destruct INE as [x' [INE MAP]]. unfold collect_rel. exists x', x'. split; vauto. - split; vauto. destruct SIMREL'. split. + split; vauto. split. { split; vauto. unfold G_s' in COND1; ins. - unfold is_w. destruct rsr_lab0 with x'; vauto. } + unfold is_w. destruct (rsr_lab SIMREL') with x'; vauto. } unfold G_s' in COND2; ins. - unfold is_rlx. unfold mod. destruct rsr_lab0 with x'; vauto. } + unfold is_rlx. unfold mod. destruct (rsr_lab SIMREL') with x'; vauto. } rewrite !collect_rel_union. apply union_more. { apply union_more. @@ -1182,53 +1179,53 @@ Proof using INV INV'. { rewrite wf_sbE. basic_solver. } assert (IN2 : dom_rel ⦗E_t' ∩₁ F G_t' ∩₁ Acq G_t'⦘ ⊆₁ E_t'). { basic_solver. } - rewrite IN1, IN2. destruct SIMREL'. - clear - rsr_inj0; basic_solver 8. } + rewrite IN1, IN2. arewrite (E_t' ∪₁ E_t' ≡₁ E_t'); [basic_solver|]. + eapply (rsr_inj SIMREL'). } assert (IN1 : codom_rel ⦗R_t' ∩₁ Rlx G_t' ∩₁ E_t'⦘ ⊆₁ E_t'). { basic_solver. } assert (IN2 : dom_rel (sb_t' ⨾ ⦗E_t' ∩₁ F G_t' ∩₁ Acq G_t'⦘) ⊆₁ E_t'). { rewrite wf_sbE. basic_solver. } - rewrite IN1, IN2. destruct SIMREL'. - clear - rsr_inj0; basic_solver 8. } + rewrite IN1, IN2. arewrite (E_t' ∪₁ E_t' ≡₁ E_t'); [basic_solver|]. + eapply (rsr_inj SIMREL'). } rewrite !collect_rel_seq; vauto. { assert (IN1 : codom_rel sb_t' ⊆₁ E_t'). { rewrite wf_sbE. basic_solver. } assert (IN2 : dom_rel ⦗E_t'⦘ ⊆₁ E_t'). { basic_solver. } - rewrite IN1, IN2. destruct SIMREL'. - clear - rsr_inj0; basic_solver 8. } + rewrite IN1, IN2. arewrite (E_t' ∪₁ E_t' ≡₁ E_t'); [basic_solver|]. + eapply (rsr_inj SIMREL'). } assert (IN1 : codom_rel ⦗Acq G_t' ∩₁ E_t'⦘ ⊆₁ E_t'). { basic_solver. } assert (IN2 : dom_rel (sb_t' ⨾ ⦗E_t'⦘) ⊆₁ E_t'). { rewrite wf_sbE. basic_solver. } - rewrite IN1, IN2. destruct SIMREL'. - clear - rsr_inj0; basic_solver 8. } + rewrite IN1, IN2. arewrite (E_t' ∪₁ E_t' ≡₁ E_t'); [basic_solver|]. + eapply (rsr_inj SIMREL'). } rewrite !collect_rel_seq; vauto. { assert (IN1 : codom_rel sb_t' ⊆₁ E_t'). { rewrite wf_sbE. basic_solver. } assert (IN2 : dom_rel ⦗E_t' ∩₁ Rel G_t'⦘ ⊆₁ E_t'). { basic_solver. } - rewrite IN1, IN2. destruct SIMREL'. - clear - rsr_inj0; basic_solver 8. } + rewrite IN1, IN2. arewrite (E_t' ∪₁ E_t' ≡₁ E_t'); [basic_solver|]. + eapply (rsr_inj SIMREL'). } assert (IN1 : codom_rel ⦗E_t'⦘ ⊆₁ E_t'). { basic_solver. } assert (IN2 : dom_rel (sb_t' ⨾ ⦗E_t' ∩₁ Rel G_t'⦘) ⊆₁ E_t'). { rewrite wf_sbE. basic_solver. } - rewrite IN1, IN2. destruct SIMREL'. - clear - rsr_inj0; basic_solver 8. } + rewrite IN1, IN2. arewrite (E_t' ∪₁ E_t' ≡₁ E_t'); [basic_solver|]. + eapply (rsr_inj SIMREL'). } rewrite !collect_rel_seq; vauto. { assert (IN1 : codom_rel sb_t' ⊆₁ E_t'). { rewrite wf_sbE. basic_solver. } assert (IN2 : dom_rel ⦗E_t' ∩₁ W_t' ∩₁ Rlx G_t'⦘ ⊆₁ E_t'). { basic_solver. } - rewrite IN1, IN2. destruct SIMREL'. - clear - rsr_inj0; basic_solver 8. } + rewrite IN1, IN2. arewrite (E_t' ∪₁ E_t' ≡₁ E_t'); [basic_solver|]. + eapply (rsr_inj SIMREL'). } assert (IN1 : codom_rel ⦗F G_t' ∩₁ Rel G_t' ∩₁ E_t'⦘ ⊆₁ E_t'). { basic_solver. } assert (IN2 : dom_rel (sb_t' ⨾ ⦗E_t' ∩₁ W_t' ∩₁ Rlx G_t'⦘) ⊆₁ E_t'). { rewrite wf_sbE. basic_solver. } - rewrite IN1, IN2. destruct SIMREL'. - clear - rsr_inj0; basic_solver 8. } + rewrite IN1, IN2. arewrite (E_t' ∪₁ E_t' ≡₁ E_t'); [basic_solver|]. + eapply (rsr_inj SIMREL'). } assert (IND2 : mapper' ↑ (rpo_imm G_t')⁺ ⨾ ⦗(E_s ∪₁ eq e) \₁ eq b_t⦘ ⨾ (rpo_imm G_s' ⨾ ⦗(E_s ∪₁ eq e) \₁ eq b_t⦘) ⊆ mapper' ↑ (rpo_imm G_t')⁺). { assert (TRIN : mapper' ↑ (rpo_imm G_t')⁺ ⨾ mapper' ↑ (rpo_imm G_t')⁺ @@ -1239,7 +1236,7 @@ Proof using INV INV'. destruct P2 as (x0'' & y' & (P2 & M3 & M4)). exists x', y'. splits; vauto. assert (EQ : x0'' = x0'). - { destruct SIMREL'. apply rsr_inj; vauto. + { apply (rsr_inj SIMREL'); vauto. { apply ct_begin in P2. destruct P2 as (x1 & P2 & P3). apply wf_rpo_immE in P2; vauto. @@ -1308,8 +1305,7 @@ Proof using INV INV'. unfold G_s'; ins. left. apply (rsr_acts SIMREL). right. apply EXTRAOLD; basic_solver. } clear - EMP. basic_solver. } - { destruct SIMREL'. - rewrite rsr_rf. split; [|basic_solver 8]. + { rewrite (rsr_rf SIMREL'). split; [|basic_solver 8]. rewrite EXTRA. unfold is_r. arewrite (WCore.G X_s' = G_s'). unfold G_s' at 2; ins. @@ -1320,8 +1316,7 @@ Proof using INV INV'. destruct COND2 as [EQ [P1 P2]]. subst. clear - WW P2 E_NOT_B. unfold is_w in WW. basic_solver. } - { destruct SIMREL'. - rewrite rsr_co. unfold add_max. + { rewrite (rsr_co SIMREL'). unfold add_max. rewrite EXTRA. apply union_more; vauto. apply cross_more. { unfold extra_co_D. unfold same_loc. @@ -1340,10 +1335,9 @@ Proof using INV INV'. assert (IND1 : (rpo_imm G_s') ⊆ mapper' ↑ (rpo_imm G_t')⁺). { unfold rpo_imm. assert (SIMRELD : reord_simrel X_s' X_t' a_t b_t mapper') by vauto. - destruct SIMREL'. arewrite (G_s' = WCore.G X_s'). rewrite wf_sbE. - rewrite rsr_sb. + rewrite (rsr_sb SIMREL'). rewrite EXTRA, cross_false_l, cross_false_r, union_false_r. rewrite !union_false_r. unfold swap_rel. rewrite !collect_rel_union. @@ -1356,29 +1350,29 @@ Proof using INV INV'. ⨾ ⦗acts_set G_s'⦘ ⨾ mapper' ↑ (eq a_t ∩₁ E_t') × (eq b_t ∩₁ E_t') ⨾ ⦗acts_set G_s'⦘ ⨾ ⦗F G_s' ∩₁ Acq G_s'⦘). - { arewrite (G_s' = WCore.G X_s'). rewrite rsr_acts. + { arewrite (G_s' = WCore.G X_s'). rewrite (rsr_acts SIMREL'). rewrite EXTRA. rels. arewrite_id (⦗R (WCore.G X_s') ∩₁ Rlx (WCore.G X_s')⦘). rels. destruct INV'. arewrite (eq b_t ∩₁ E_t' ⊆₁ eq b_t ∩₁ E_t' ∩₁ E_t'). { clear. basic_solver. } rewrite rsr_b_t_is_r_or_w0. - rewrite rsr_at. + rewrite (rsr_at SIMREL'). intros x y PATH. destruct PATH as [x0 [MAP [x1 [[C0 C1] [x2 [C2 C3]]]]]]. destruct C2 as (EQ & MAPA). subst x2. destruct C3 as (EQ & (FNC & ACQ)). destruct SIMRELD. - clear - C1 rsr_lab0 FNC. + clear - C1 rsr_lab FNC. destruct C1 as (x0' & LABS & MAPN). apply set_inter_union_l in LABS. destruct LABS as [LAB1 | LAB2]. { destruct LAB1 as (LAB1 & LAB2). unfold is_w, is_f in *. - unfold eq_dom in rsr_lab0. specialize (rsr_lab0 x0'). - apply rsr_lab0 in LAB2. rewrite <- LAB2 in LAB1. + unfold eq_dom in rsr_lab. specialize (rsr_lab x0'). + apply rsr_lab in LAB2. rewrite <- LAB2 in LAB1. unfold compose in LAB1. rewrite MAPN in LAB1. basic_solver. } destruct LAB2 as (LAB1 & LAB2). unfold is_r, is_f in *. - unfold eq_dom in rsr_lab0. specialize (rsr_lab0 x0'). - apply rsr_lab0 in LAB2. rewrite <- LAB2 in LAB1. + unfold eq_dom in rsr_lab. specialize (rsr_lab x0'). + apply rsr_lab in LAB2. rewrite <- LAB2 in LAB1. unfold compose in LAB1. rewrite MAPN in LAB1. basic_solver. } arewrite_false (⦗Acq G_s'⦘ @@ -1390,15 +1384,14 @@ Proof using INV INV'. ⨾ (mapper' ↑₁ (set_compl Acq G_t' ∩₁ E_t')) × (mapper' ↑₁ (eq b_t ∩₁ E_t'))). { hahn_frame_l. apply cross_mori; vauto. apply set_collect_mori; vauto. clear - INV'. - destruct INV'. arewrite (E_t' ⊆₁ E_t' ∩₁ E_t'). rewrite <- set_interA. - rewrite rsr_at_nacq. basic_solver. } + rewrite (rsr_at_nacq INV'). basic_solver. } intros x y COND. destruct COND as [z [[EQ ACQ] [C2 C3]]]; subst z. destruct C2 as [x0 [[P1 P2] MAP]]. destruct P1. rewrite <- MAP in ACQ. unfold is_acq in *. unfold mod in *. - rewrite <- rsr_lab; vauto. } + rewrite <- (rsr_lab SIMREL'); vauto. } arewrite_false (⦗acts_set G_s'⦘ ⨾ mapper' ↑ (eq a_t ∩₁ E_t') × (eq b_t ∩₁ E_t') ⨾ ⦗acts_set G_s'⦘ ⨾ ⦗Rel G_s'⦘). { arewrite (G_s' = WCore.G X_s'). @@ -1407,43 +1400,42 @@ Proof using INV INV'. ⨾ ⦗Rel (WCore.G X_s')⦘). { hahn_frame_r. apply cross_mori; vauto. apply set_collect_mori; vauto. clear - INV'. - destruct INV'. arewrite (E_t' ⊆₁ E_t' ∩₁ E_t'). rewrite <- set_interA. - rewrite rsr_bt_nrel. basic_solver. } + rewrite (rsr_bt_nrel INV'). basic_solver. } intros x y COND. destruct COND as [z [[EQ REL] [C2 C3]]]; subst z. destruct REL as [x0 [[P1 P2] MAP]]. destruct P1. rewrite <- MAP in C3. unfold is_rel in *. unfold mod in *. - rewrite <- rsr_lab; vauto. } + rewrite <- (rsr_lab SIMREL'); vauto. } arewrite_false (⦗F G_s' ∩₁ Rel G_s'⦘ ⨾ ⦗acts_set G_s'⦘ ⨾ mapper' ↑ (eq a_t ∩₁ E_t') × (eq b_t ∩₁ E_t') ⨾ ⦗acts_set G_s'⦘ ⨾ ⦗W G_s' ∩₁ Rlx G_s'⦘). - { arewrite (G_s' = WCore.G X_s'). rewrite rsr_acts. - rewrite EXTRA. rels. arewrite_id (⦗W (WCore.G X_s') ∩₁ Rlx (WCore.G X_s')⦘). + { arewrite (G_s' = WCore.G X_s'). rewrite (rsr_acts SIMREL'). + rewrite EXTRA. arewrite_id (⦗W (WCore.G X_s') ∩₁ Rlx (WCore.G X_s')⦘). rels. destruct INV'. arewrite (eq a_t ∩₁ E_t' ⊆₁ eq a_t ∩₁ E_t' ∩₁ E_t'). { clear. basic_solver. } rewrite rsr_a_t_is_r_or_w0. - rewrite rsr_bt. + rewrite (rsr_bt SIMREL'). intros x y PATH. destruct PATH as [x0 [MAP [x1 [[C0 C1] [x2 [C2 C3]]]]]]. destruct C2 as (EQ & MAPA). subst x0. destruct MAP as (EQQ & (FNC & REL)). destruct SIMRELD. - clear - C1 rsr_lab0 FNC EQ EQQ. + clear - C1 rsr_lab FNC EQ EQQ. destruct C1 as (x0' & LABS & MAPN). destruct EQ as (x1' & WR & INE). apply set_inter_union_l in WR. destruct WR as [LAB1 | LAB2]. { destruct LAB1 as (LAB1 & LAB2). unfold is_w, is_f in *. - unfold eq_dom in rsr_lab0. specialize (rsr_lab0 x1'). - apply rsr_lab0 in LAB2. rewrite <- LAB2 in LAB1. + unfold eq_dom in rsr_lab. specialize (rsr_lab x1'). + apply rsr_lab in LAB2. rewrite <- LAB2 in LAB1. unfold compose in LAB1. rewrite INE in LAB1. basic_solver. } destruct LAB2 as (LAB1 & LAB2). unfold is_r, is_f in *. - unfold eq_dom in rsr_lab0. specialize (rsr_lab0 x1'). - apply rsr_lab0 in LAB2. rewrite <- LAB2 in LAB1. + unfold eq_dom in rsr_lab. specialize (rsr_lab x1'). + apply rsr_lab in LAB2. rewrite <- LAB2 in LAB1. unfold compose in LAB1. rewrite INE in LAB1. basic_solver. } rewrite !union_false_r. @@ -1462,33 +1454,31 @@ Proof using INV INV'. split; vauto. split; vauto. split. { unfold G_s' in COND1; ins. - unfold is_r. destruct rsr_lab with x'; vauto. } + unfold is_r. destruct (rsr_lab SIMREL') with x'; vauto. } unfold G_s' in COND2; ins. - unfold is_rlx. unfold mod. destruct rsr_lab with x'; vauto. } + unfold is_rlx. unfold mod. destruct (rsr_lab SIMREL') with x'; vauto. } arewrite (⦗mapper' ↑₁ E_t' ∩₁ (F (WCore.G X_s') ∩₁ Acq (WCore.G X_s'))⦘ ⊆ mapper' ↑ ⦗(E_t' ∩₁ F G_t' ∩₁ Acq G_t')⦘). { intros x y COND. destruct COND as (EQ & COND); subst y. - destruct SIMREL. destruct COND as [INE [FACQ FAT]]. unfold set_collect. destruct INE as [x' [INE MAP]]. exists x'. exists x'. splits; vauto. split; vauto. split. { split; vauto. unfold G_s' in FACQ; ins. - unfold is_f. destruct rsr_lab with x'; vauto. } + unfold is_f. destruct (rsr_lab SIMREL') with x'; vauto. } unfold G_s' in FAT; ins. - unfold is_acq. unfold mod. destruct rsr_lab with x'; vauto. } + unfold is_acq. unfold mod. destruct (rsr_lab SIMREL') with x'; vauto. } arewrite (⦗Acq (WCore.G X_s') ∩₁ mapper' ↑₁ E_t'⦘ ⊆ mapper' ↑ ⦗(Acq G_t' ∩₁ E_t')⦘). { intros x y COND. destruct COND as (EQ & COND); subst y. - destruct SIMREL. destruct COND as [ACQ INE]. unfold set_collect. destruct INE as [x' [INE MAP]]. exists x'. exists x'. splits; vauto. split; vauto. split; vauto. unfold G_s' in ACQ; ins. - unfold is_acq. unfold mod. destruct rsr_lab with x'; vauto. } + unfold is_acq. unfold mod. destruct (rsr_lab SIMREL') with x'; vauto. } arewrite (mapper' ↑ ⦗(Acq G_t' ∩₁ E_t')⦘ ⨾ mapper' ↑ sb_t' ⨾ ⦗mapper' ↑₁ E_t'⦘ ⊆ mapper' ↑ ⦗(Acq G_t' ∩₁ E_t')⦘ ⨾ mapper' ↑ sb_t' ⨾ mapper' ↑ ⦗E_t'⦘). { do 2 hahn_frame_l. rewrite collect_rel_eqv; vauto. } @@ -1500,31 +1490,28 @@ Proof using INV INV'. arewrite (⦗mapper' ↑₁ E_t' ∩₁ Rel (WCore.G X_s')⦘ ⊆ mapper' ↑ ⦗E_t' ∩₁ Rel G_t'⦘). { intros x y COND. destruct COND as (EQ & COND); subst y. - destruct SIMREL. destruct COND as [INE REL]. unfold set_collect. destruct INE as [x' [INE MAP]]. exists x'. exists x'. splits; vauto. split; vauto. split; vauto. unfold G_s' in REL; ins. - unfold is_rel. unfold mod. destruct rsr_lab with x'; vauto. } + unfold is_rel. unfold mod. destruct (rsr_lab SIMREL') with x'; vauto. } arewrite (⦗F (WCore.G X_s') ∩₁ Rel (WCore.G X_s') ∩₁ mapper' ↑₁ E_t'⦘ ⊆ mapper' ↑ ⦗(F G_t' ∩₁ Rel G_t' ∩₁ E_t')⦘). { intros x y COND. destruct COND as (EQ & COND); subst y. - destruct SIMREL. destruct COND as [[FENC REL] INE]. unfold set_collect. destruct INE as [x' [INE MAP]]. exists x'. exists x'. splits; vauto. split; vauto. split; vauto. split. { unfold G_s' in FENC; ins. - unfold is_f. destruct rsr_lab with x'; vauto. } + unfold is_f. destruct (rsr_lab SIMREL') with x'; vauto. } unfold G_s' in FENC; ins. - unfold is_rel. unfold mod. destruct rsr_lab with x'; vauto. } + unfold is_rel. unfold mod. destruct (rsr_lab SIMREL') with x'; vauto. } arewrite (⦗mapper' ↑₁ E_t' ∩₁ (W (WCore.G X_s') ∩₁ Rlx (WCore.G X_s'))⦘ ⊆ mapper' ↑ ⦗(E_t' ∩₁ W G_t' ∩₁ Rlx G_t')⦘). { intros x y COND. destruct COND as (EQ & COND); subst y. - destruct SIMREL. destruct COND as [INE [WRLX INE']]. unfold set_collect. destruct INE as [x' [INE MAP]]. @@ -1533,9 +1520,9 @@ Proof using INV INV'. { split; vauto. unfold G_s' in WRLX; ins. unfold is_w. unfold is_rlx. unfold mod. - destruct rsr_lab with x'; vauto. } + destruct (rsr_lab SIMREL') with x'; vauto. } unfold G_s' in INE'; ins. - unfold is_rlx. unfold mod. destruct rsr_lab with x'; vauto. } + unfold is_rlx. unfold mod. destruct (rsr_lab SIMREL') with x'; vauto. } rewrite <- ct_step. assert (SBT : sb_t' ≡ ⦗E_t'⦘ ⨾ sb_t' ⨾ ⦗E_t'⦘). { rewrite wf_sbE. basic_solver. } @@ -1554,53 +1541,53 @@ Proof using INV INV'. { clear. rewrite wf_sbE. basic_solver. } assert (IN2 : dom_rel ⦗E_t' ∩₁ F G_t' ∩₁ Acq G_t'⦘ ⊆₁ E_t'). { clear. basic_solver. } - rewrite IN1, IN2. - clear - rsr_inj; basic_solver 8. } + rewrite IN1, IN2. arewrite (E_t' ∪₁ E_t' ≡₁ E_t'); [basic_solver|]. + eapply (rsr_inj SIMREL'). } assert (IN1 : codom_rel ⦗R_t' ∩₁ Rlx G_t' ∩₁ E_t'⦘ ⊆₁ E_t'). { clear. basic_solver. } assert (IN2 : dom_rel (sb_t' ⨾ ⦗E_t' ∩₁ F G_t' ∩₁ Acq G_t'⦘) ⊆₁ E_t'). { clear. rewrite wf_sbE. basic_solver. } - rewrite IN1, IN2. - clear - rsr_inj; basic_solver 8. } + rewrite IN1, IN2. arewrite (E_t' ∪₁ E_t' ≡₁ E_t'); [basic_solver|]. + eapply (rsr_inj SIMREL'). } rewrite !collect_rel_seq; vauto. { assert (IN1 : codom_rel sb_t' ⊆₁ E_t'). { clear. rewrite wf_sbE. basic_solver. } assert (IN2 : dom_rel ⦗E_t'⦘ ⊆₁ E_t'). { clear. basic_solver. } - rewrite IN1, IN2. - clear - rsr_inj; basic_solver 8. } + rewrite IN1, IN2. arewrite (E_t' ∪₁ E_t' ≡₁ E_t'); [basic_solver|]. + eapply (rsr_inj SIMREL'). } assert (IN1 : codom_rel ⦗Acq G_t' ∩₁ E_t'⦘ ⊆₁ E_t'). { clear. basic_solver. } assert (IN2 : dom_rel (sb_t' ⨾ ⦗E_t'⦘) ⊆₁ E_t'). { clear. rewrite wf_sbE. basic_solver. } - rewrite IN1, IN2. - clear - rsr_inj; basic_solver 8. } + rewrite IN1, IN2. arewrite (E_t' ∪₁ E_t' ≡₁ E_t'); [basic_solver|]. + eapply (rsr_inj SIMREL'). } rewrite !collect_rel_seq; vauto. { assert (IN1 : codom_rel sb_t' ⊆₁ E_t'). { clear. rewrite wf_sbE. basic_solver. } assert (IN2 : dom_rel ⦗E_t' ∩₁ Rel G_t'⦘ ⊆₁ E_t'). { clear. basic_solver. } - rewrite IN1, IN2. - clear - rsr_inj; basic_solver 8. } + rewrite IN1, IN2. arewrite (E_t' ∪₁ E_t' ≡₁ E_t'); [basic_solver|]. + eapply (rsr_inj SIMREL'). } assert (IN1 : codom_rel ⦗E_t'⦘ ⊆₁ E_t'). { clear. basic_solver. } assert (IN2 : dom_rel (sb_t' ⨾ ⦗E_t' ∩₁ Rel G_t'⦘) ⊆₁ E_t'). { clear. rewrite wf_sbE. basic_solver. } - rewrite IN1, IN2. - clear - rsr_inj; basic_solver 8. } + rewrite IN1, IN2. arewrite (E_t' ∪₁ E_t' ≡₁ E_t'); [basic_solver|]. + eapply (rsr_inj SIMREL'). } rewrite !collect_rel_seq; rewrite <- set_interA; vauto. { assert (IN1 : codom_rel sb_t' ⊆₁ E_t'). { clear. rewrite wf_sbE. basic_solver. } assert (IN2 : dom_rel ⦗E_t' ∩₁ W_t' ∩₁ Rlx G_t'⦘ ⊆₁ E_t'). { clear. basic_solver. } - rewrite IN1, IN2. - clear - rsr_inj; basic_solver 8. } + rewrite IN1, IN2. arewrite (E_t' ∪₁ E_t' ≡₁ E_t'); [basic_solver|]. + eapply (rsr_inj SIMREL'). } assert (IN1 : codom_rel ⦗F G_t' ∩₁ Rel G_t' ∩₁ E_t'⦘ ⊆₁ E_t'). { clear. basic_solver. } assert (IN2 : dom_rel (sb_t' ⨾ ⦗E_t' ∩₁ W_t' ∩₁ Rlx G_t'⦘) ⊆₁ E_t'). { clear. rewrite wf_sbE. basic_solver. } - rewrite IN1, IN2. - clear - rsr_inj; basic_solver 8. } + rewrite IN1, IN2. arewrite (E_t' ∪₁ E_t' ≡₁ E_t'); [basic_solver|]. + eapply (rsr_inj SIMREL'). } assert (IND2 : mapper' ↑ (rpo_imm G_t')⁺ ⨾ (rpo_imm G_s') ⊆ mapper' ↑ (rpo_imm G_t')⁺). { assert (TRIN : mapper' ↑ (rpo_imm G_t')⁺ ⨾ mapper' ↑ (rpo_imm G_t')⁺ @@ -1611,7 +1598,7 @@ Proof using INV INV'. destruct P2 as (x0'' & y' & (P2 & M3 & M4)). exists x', y'. splits; vauto. assert (EQ : x0'' = x0'). - { destruct SIMREL'. apply rsr_inj; vauto. + { apply (rsr_inj SIMREL'); vauto. { apply ct_begin in P2. destruct P2 as (x1 & P2 & P3). destruct INV. @@ -1641,9 +1628,8 @@ Proof using INV INV'. rewrite !collect_rel_union. repeat apply union_mori; vauto. { apply not_and_or in NEMP. destruct NEMP as [N1 | N2]. - { destruct SIMREL'. - arewrite (G_s' = WCore.G X_s'). - rewrite rsr_sb. rewrite !EXTRA. rels. + { arewrite (G_s' = WCore.G X_s'). + rewrite (rsr_sb SIMREL'). rewrite !EXTRA. rels. unfold swap_rel. rewrite collect_rel_union. rewrite inter_union_l. apply inclusion_union_l. @@ -1653,14 +1639,14 @@ Proof using INV INV'. unfold collect_rel. exists x0, y0. splits; vauto. split; vauto. unfold same_loc in *. unfold loc. unfold loc in PTH2. - rewrite <- rsr_lab; vauto. - { rewrite <- rsr_lab; vauto. + rewrite <- (rsr_lab SIMREL'); vauto. + { rewrite <- (rsr_lab SIMREL'); vauto. apply wf_sbE in SB. destruct SB as (x1 & INE1 & (y1 & SB & (EQ & INE2))); vauto. } apply wf_sbE in SB. destruct SB as (x1 & (EQ & INE) & RST); vauto. } rewrite collect_rel_cross. - rewrite rsr_bt, rsr_at. destruct INV'. + rewrite (rsr_bt SIMREL'), (rsr_at SIMREL'). destruct INV'. arewrite_false (eq b_t × eq a_t ∩ same_loc (lab (WCore.G X_s'))); vauto. intros x y COND. destruct COND as ((Q1 & Q2) & SL). subst x y. @@ -1673,17 +1659,16 @@ Proof using INV INV'. exists b_t. split; vauto. unfold same_loc in SL. unfold loc in SL. unfold same_loc, loc. - rewrite <- rsr_lab; vauto. - rewrite <- rsr_lab; vauto. + rewrite <- (rsr_lab SIMREL'); vauto. + rewrite <- (rsr_lab SIMREL'); vauto. unfold compose. assert (AEQ : mapper' a_t = b_t). { rewrite rsr_map_at with (X_s := X_s') (X_t := X_t') (b_t := b_t); vauto. } assert (BEQ : mapper' b_t = a_t). { rewrite rsr_map_bt with (X_s := X_s') (X_t := X_t') (a_t := a_t); vauto. } rewrite AEQ, BEQ. vauto. } - destruct SIMREL'. arewrite (G_s' = WCore.G X_s'). - rewrite rsr_sb. rewrite !EXTRA. rels. + rewrite (rsr_sb SIMREL'). rewrite !EXTRA. rels. unfold swap_rel. rewrite collect_rel_union. rewrite inter_union_l. assert (BEMP : eq b_t ∩₁ E_t' ≡₁ ∅). @@ -1695,16 +1680,16 @@ Proof using INV INV'. unfold collect_rel. exists x0, y0. splits; vauto. split; vauto. unfold same_loc in *. unfold loc. unfold loc in PTH2. - rewrite <- rsr_lab; vauto. - { rewrite <- rsr_lab; vauto. + rewrite <- (rsr_lab SIMREL'); vauto. + { rewrite <- (rsr_lab SIMREL'); vauto. apply wf_sbE in SB. destruct SB as (x1 & INE1 & (y1 & SB & (EQ & INE2))); vauto. } apply wf_sbE in SB. destruct SB as (x1 & (EQ & INE) & RST); vauto. } unfold sw. unfold release. unfold rs. - destruct SIMREL'. arewrite (G_s' = WCore.G X_s'). - rewrite rsr_rf. rewrite EXTRA. rewrite set_inter_empty_l. - rels. rewrite rsr_rmw. + arewrite (G_s' = WCore.G X_s'). + rewrite (rsr_rf SIMREL'). rewrite EXTRA. rewrite set_inter_empty_l. + rels. rewrite (rsr_rmw SIMREL'). arewrite ((mapper' ↑ rf_t' ⨾ mapper' ↑ rmw_t')＊ ⨾ mapper' ↑ rf_t' ⊆ ⦗mapper' ↑₁ E_t'⦘ ⨾ (mapper' ↑ rf_t' ⨾ mapper' ↑ rmw_t')＊ ⨾ mapper' ↑ rf_t' ⨾ ⦗mapper' ↑₁ E_t'⦘). { rewrite rtE. rewrite !seq_union_l. @@ -1724,7 +1709,7 @@ Proof using INV INV'. ⨾ ⦗W (WCore.G X_s')⦘ ⨾ ⦗mapper' ↑₁ E_t'⦘) by mode_solver 21. arewrite (⦗F (WCore.G X_s')⦘ ⨾ sb (WCore.G X_s') ⊆ ⦗F (WCore.G X_s')⦘ ⨾ ⦗mapper' ↑₁ E_t'⦘ ⨾ mapper' ↑ sb_t'). - { rewrite rsr_sb. rewrite !seq_union_r. + { rewrite (rsr_sb SIMREL'). rewrite !seq_union_r. apply inclusion_union_l. { apply inclusion_union_l. { unfold swap_rel. rewrite collect_rel_union. @@ -1732,11 +1717,11 @@ Proof using INV INV'. apply inclusion_union_l. { transitivity (⦗F (WCore.G X_s')⦘ ⨾ mapper' ↑ (sb_t')); [basic_solver 21|]. hahn_frame_l. rewrite wf_sbE. basic_solver. } - rewrite collect_rel_cross. rewrite rsr_bt. + rewrite collect_rel_cross. rewrite (rsr_bt SIMREL'). arewrite (eq a_t ∩₁ E_t' ≡₁ eq a_t ∩₁ E_t' ∩₁ E_t') by basic_solver. rewrite (rsr_a_t_is_r_or_w INV'). arewrite_false (⦗F (WCore.G X_s')⦘ ⨾ (mapper' ↑₁ ((W_t' ∪₁ R_t') ∩₁ E_t')) × eq a_t); vauto. - rewrite <- cross_inter_l. clear - rsr_lab. + rewrite <- cross_inter_l. destruct SIMREL'. clear - rsr_lab . intros x y COND. destruct COND as (LT & RT); subst. destruct LT as [FNC MAP]. destruct MAP as [x0 [CONDS MAP]]. rewrite <- MAP in FNC. unfold is_f in FNC. @@ -1774,7 +1759,7 @@ Proof using INV INV'. red. exists y0, y0. splits; vauto. red. split; vauto. split; vauto. unfold is_rel in *. unfold mod in *. - rewrite <- rsr_lab; vauto. } + rewrite <- (rsr_lab SIMREL'); vauto. } rewrite <- seqA. transitivity (mapper' ↑ (((⦗F G_t'⦘ ⨾ sb_t')^? ⨾ ⦗E_t'⦘) ⨾ ⦗E_t'⦘ ⨾ ⦗Rlx G_t'⦘ ⨾ ⦗W_t'⦘ ⨾ ⦗E_t'⦘ ⨾ (rf_t' ⨾ rmw_t')＊ @@ -1795,10 +1780,10 @@ Proof using INV INV'. exists z0. splits; vauto. apply crE. right. exists x1. splits. { red. splits; vauto. - unfold is_f in *. rewrite <- rsr_lab; vauto. } + unfold is_f in *. rewrite <- (rsr_lab SIMREL'); vauto. } destruct MAP as (x0 & x2 & (SB & M1 & M2)). - apply rsr_inj in M1. - { apply rsr_inj in M2. subst; vauto. + apply (rsr_inj SIMREL') in M1. + { apply (rsr_inj SIMREL') in M2. subst; vauto. { apply wf_sbE in SB. clear - SB. destruct SB as (y1 & INE & (y2 & SB & (EQ & INE'))); vauto. } vauto. } @@ -1823,10 +1808,10 @@ Proof using INV INV'. exists y0. splits. { red. splits; vauto. unfold is_rlx in *. unfold mod in *. - destruct rsr_lab with y0; vauto. } + destruct (rsr_lab SIMREL') with y0; vauto. } red. split; vauto. unfold is_w in *. - destruct rsr_lab with y0; vauto. } + destruct (rsr_lab SIMREL') with y0; vauto. } rewrite <- collect_rel_seq. { transitivity (mapper' ↑ ((⦗E_t'⦘ ⨾ (rf_t' ⨾ rmw_t')＊) ⨾ rf_t' @@ -1849,10 +1834,11 @@ Proof using INV INV'. assert (RESTR : rf_t' ⨾ rmw_t' ≡ restr_rel E_t' (rf_t' ⨾ rmw_t')). { rewrite restr_relE. rewrite wf_rmwE, wf_rfE; vauto. basic_solver 21. } assert (EQQ : mapper' ↑ (restr_rel E_t' (rf_t' ⨾ rmw_t'))⁺ ≡ (mapper' ↑ restr_rel E_t' (rf_t' ⨾ rmw_t'))⁺). - { apply collect_rel_ct_inj; vauto. } + { apply collect_rel_ct_inj; vauto. + apply SIMREL'. } rewrite <- RESTR in EQQ. apply EQQ in COND'. destruct COND' as (x4 & y4 & PTH' & M3 & M4). - apply rsr_inj in M3, M4; vauto. + apply (rsr_inj SIMREL') in M3, M4; vauto. { apply ct_end in PTH'. destruct PTH' as (x5 & PTH' & PTH''). destruct PTH'' as (x6 & P1 & P2). apply wf_rmwE in P2; vauto. clear - P2. @@ -1879,7 +1865,7 @@ Proof using INV INV'. exists y0. splits; vauto. red. split; vauto. unfold is_rlx in *. unfold mod in *. - rewrite <- rsr_lab; vauto. } + rewrite <- (rsr_lab SIMREL'); vauto. } arewrite (⦗mapper' ↑₁ E_t'⦘ ⨾ (sb (WCore.G X_s') ⨾ ⦗F (WCore.G X_s')⦘)^? ⊆ ⦗mapper' ↑₁ E_t'⦘ ⨾ (sb (WCore.G X_s') ⨾ ⦗F (WCore.G X_s')⦘)^? ⨾ ⦗mapper' ↑₁ E_t'⦘). { rewrite crE at 1. @@ -1888,7 +1874,7 @@ Proof using INV INV'. apply inclusion_union_r. right. rewrite seqA. arewrite (sb (WCore.G X_s') ⊆ sb (WCore.G X_s') ⨾ ⦗acts_set (WCore.G X_s')⦘). { rewrite wf_sbE. basic_solver. } - rewrite rsr_acts. rewrite EXTRA. basic_solver. } + rewrite (rsr_acts SIMREL'). rewrite EXTRA. basic_solver. } arewrite (⦗mapper' ↑₁ E_t'⦘ ⨾ (sb (WCore.G X_s') ⨾ ⦗F (WCore.G X_s')⦘)^? ⊆ ⦗mapper' ↑₁ E_t'⦘ ⨾ (mapper' ↑ sb_t' ⨾ ⦗mapper' ↑₁ E_t'⦘ ⨾ ⦗F (WCore.G X_s')⦘)^?). { rewrite crE at 1. rewrite seq_union_r. @@ -1896,10 +1882,10 @@ Proof using INV INV'. hahn_frame_l. arewrite (sb (WCore.G X_s') ⊆ sb (WCore.G X_s') ⨾ ⦗acts_set (WCore.G X_s')⦘). { rewrite wf_sbE. basic_solver. } - rewrite rsr_acts. rewrite EXTRA. rewrite set_union_empty_r. + rewrite (rsr_acts SIMREL'). rewrite EXTRA. rewrite set_union_empty_r. rewrite crE. apply inclusion_union_r. right. - rewrite rsr_sb. rewrite !seq_union_l. + rewrite (rsr_sb SIMREL'). rewrite !seq_union_l. repeat apply inclusion_union_l. { unfold swap_rel. rewrite collect_rel_union. rewrite seq_union_l. apply inclusion_union_l. @@ -1911,7 +1897,7 @@ Proof using INV INV'. arewrite_false ((mapper' ↑₁ (eq a_t ∩₁ E_t')) × (mapper' ↑₁ ((W_t' ∪₁ R_t') ∩₁ E_t')) ⨾ ⦗mapper' ↑₁ E_t'⦘ ⨾ ⦗F (WCore.G X_s')⦘); vauto. rewrite <- seqA. rewrite <- cross_inter_r. rewrite <- cross_inter_r. - clear - rsr_lab. + destruct SIMREL'. clear - rsr_lab. intros x y COND. destruct COND as (LT & RT); subst. destruct RT as [[MAP1 MAP2] FNC]. destruct MAP1 as [x0 [CONDS MAP]]. rewrite <- MAP in FNC. unfold is_f in FNC. @@ -1938,8 +1924,8 @@ Proof using INV INV'. exists x1. splits; vauto. apply crE. right. exists x4. splits. { destruct SB as (x5 & x6 & (SB & M1 & M2)). - apply rsr_inj in M1. - { apply rsr_inj in M2. subst; vauto. + apply (rsr_inj SIMREL') in M1. + { apply (rsr_inj SIMREL') in M2. subst; vauto. { apply wf_sbE in SB. clear - SB. destruct SB as (y1 & INE & (y2 & SB & (EQ & INE'))); vauto. } vauto. } @@ -1947,7 +1933,7 @@ Proof using INV INV'. destruct SB as (y1 & (EQ & INE') & RST); vauto. } vauto. } red. splits; vauto. - unfold is_f in *. rewrite <- rsr_lab; vauto. } + unfold is_f in *. rewrite <- (rsr_lab SIMREL'); vauto. } intros x y COND. destruct COND as (x0 & (EQ & (x1 & INE & EQ1)) & (EQ2 & COND)); subst. red. exists x1, x1. splits; vauto. @@ -1955,12 +1941,13 @@ Proof using INV INV'. exists x1. splits; vauto. red. splits; vauto. unfold is_acq in *. unfold mod in *. - destruct rsr_lab with x1; vauto. } + destruct (rsr_lab SIMREL') with x1; vauto. } assert (IN1 : codom_rel (⦗E_t'⦘ ⨾ (sb_t' ⨾ ⦗F G_t'⦘)^?) ⊆₁ E_t'). { clear. rewrite wf_sbE. basic_solver. } assert (IN2 : dom_rel (⦗E_t'⦘ ⨾ ⦗Acq G_t'⦘ ⨾ ⦗E_t'⦘) ⊆₁ E_t'). { clear. basic_solver. } - rewrite IN1, IN2; basic_solver. } + rewrite IN1, IN2. arewrite (E_t' ∪₁ E_t' ≡₁ E_t'); [basic_solver|]. + eapply (rsr_inj SIMREL'). } apply collect_rel_mori; vauto. rewrite !seqA; vauto. } assert (IN1 : codom_rel (⦗E_t'⦘ ⨾ ⦗Rlx G_t'⦘) ⊆₁ E_t'). @@ -1968,7 +1955,8 @@ Proof using INV INV'. assert (IN2 : dom_rel (⦗E_t'⦘ ⨾ (sb_t' ⨾ ⦗F G_t'⦘)^? ⨾ ⦗E_t'⦘ ⨾ ⦗Acq G_t'⦘ ⨾ ⦗E_t'⦘) ⊆₁ E_t'). { clear. basic_solver. } - rewrite IN1, IN2; basic_solver. } + rewrite IN1, IN2. arewrite (E_t' ∪₁ E_t' ≡₁ E_t'); [basic_solver|]. + eapply (rsr_inj SIMREL'). } apply collect_rel_mori; vauto. apply seqA. } assert (IN1 : codom_rel rf_t' ⊆₁ E_t'). @@ -1976,28 +1964,32 @@ Proof using INV INV'. assert (IN2 : dom_rel (⦗E_t'⦘ ⨾ ⦗Rlx G_t'⦘ ⨾ ⦗E_t'⦘ ⨾ (sb_t' ⨾ ⦗F G_t'⦘)^? ⨾ ⦗E_t'⦘ ⨾ ⦗Acq G_t'⦘ ⨾ ⦗E_t'⦘) ⊆₁ E_t'). { clear; basic_solver. } - rewrite IN1, IN2; basic_solver. } + rewrite IN1, IN2. arewrite (E_t' ∪₁ E_t' ≡₁ E_t'); [basic_solver|]. + eapply (rsr_inj SIMREL'). } assert (IN1 : codom_rel (⦗E_t'⦘ ⨾ (rf_t' ⨾ rmw_t')＊) ⊆₁ E_t'). { rewrite wf_rmwE; vauto. rewrite rtE. rewrite ct_end. basic_solver. } assert (IN2 : dom_rel (rf_t' ⨾ ⦗E_t'⦘ ⨾ ⦗Rlx G_t'⦘ ⨾ ⦗E_t'⦘ ⨾ (sb_t' ⨾ ⦗F G_t'⦘)^? ⨾ ⦗E_t'⦘ ⨾ ⦗Acq G_t'⦘ ⨾ ⦗E_t'⦘) ⊆₁ E_t'). { rewrite wf_rfE; basic_solver. } - rewrite IN1, IN2; basic_solver. } + rewrite IN1, IN2. arewrite (E_t' ∪₁ E_t' ≡₁ E_t'); [basic_solver|]. + eapply (rsr_inj SIMREL'). } apply collect_rel_mori; vauto. apply seqA. } assert (IN1 : codom_rel rf_t' ⊆₁ E_t'). { rewrite wf_rfE; basic_solver. } assert (IN2 : dom_rel rmw_t' ⊆₁ E_t'). { rewrite wf_rmwE; basic_solver. } - rewrite IN1, IN2; basic_solver. } + rewrite IN1, IN2. arewrite (E_t' ∪₁ E_t' ≡₁ E_t'); [basic_solver|]. + eapply (rsr_inj SIMREL'). } assert (IN1 : codom_rel (⦗E_t'⦘ ⨾ ⦗Rlx G_t'⦘ ⨾ ⦗W_t'⦘) ⊆₁ E_t'). { clear. basic_solver. } assert (IN2 : dom_rel (⦗E_t'⦘ ⨾ (rf_t' ⨾ rmw_t')＊ ⨾ rf_t' ⨾ ⦗E_t'⦘ ⨾ ⦗Rlx G_t'⦘ ⨾ ⦗E_t'⦘ ⨾ (sb_t' ⨾ ⦗F G_t'⦘)^? ⨾ ⦗E_t'⦘ ⨾ ⦗Acq G_t'⦘ ⨾ ⦗E_t'⦘) ⊆₁ E_t'). { clear. basic_solver. } - rewrite IN1, IN2; basic_solver. } + rewrite IN1, IN2. arewrite (E_t' ∪₁ E_t' ≡₁ E_t'); [basic_solver|]. + eapply (rsr_inj SIMREL'). } apply collect_rel_mori; vauto. rewrite !seqA; vauto. } assert (IN1 : codom_rel ((⦗F G_t'⦘ ⨾ sb_t')^? ⨾ ⦗E_t'⦘) ⊆₁ E_t'). @@ -2006,7 +1998,8 @@ Proof using INV INV'. ⨾ (rf_t' ⨾ rmw_t')＊ ⨾ rf_t' ⨾ ⦗E_t'⦘ ⨾ ⦗Rlx G_t'⦘ ⨾ ⦗E_t'⦘ ⨾ (sb_t' ⨾ ⦗F G_t'⦘)^? ⨾ ⦗E_t'⦘ ⨾ ⦗Acq G_t'⦘ ⨾ ⦗E_t'⦘) ⊆₁ E_t'). { clear. basic_solver. } - rewrite IN1, IN2; basic_solver. } + rewrite IN1, IN2. arewrite (E_t' ∪₁ E_t' ≡₁ E_t'); [basic_solver|]. + eapply (rsr_inj SIMREL'). } apply collect_rel_mori; vauto. rewrite seqA. arewrite (⦗E_t'⦘ ⨾ ⦗E_t'⦘ ⊆ ⦗E_t'⦘) by basic_solver. } @@ -2017,7 +2010,8 @@ Proof using INV INV'. ⨾ ⦗E_t'⦘ ⨾ ⦗Rlx G_t'⦘ ⨾ ⦗E_t'⦘ ⨾ (sb_t' ⨾ ⦗F G_t'⦘)^? ⨾ ⦗E_t'⦘ ⨾ ⦗Acq G_t'⦘ ⨾ ⦗E_t'⦘) ⊆₁ E_t'). { rewrite wf_sbE; vauto. clear. basic_solver. } - rewrite IN1, IN2; basic_solver. } + rewrite IN1, IN2. arewrite (E_t' ∪₁ E_t' ≡₁ E_t'); [basic_solver|]. + eapply (rsr_inj SIMREL'). } apply collect_rel_mori; vauto. clear. arewrite_id (⦗E_t'⦘). rels. } assert (IND2 : mapper' ↑ (sb_t' ∩ same_loc_t' ∪ rpo_t' ∪ sw G_t')⁺ @@ -2032,7 +2026,7 @@ Proof using INV INV'. destruct P2 as (x0'' & y' & (P2 & M3 & M4)). exists x', y'. splits; vauto. assert (EQ : x0'' = x0'). - { destruct SIMREL'. apply rsr_inj; vauto. + { apply (rsr_inj SIMREL'); vauto. { apply ct_begin in P2. destruct P2 as (x1 & P2 & P3). assert (P2' : rhb (G_t') x0'' x1) by vauto. diff --git a/src/reordering/ReorderingExecA.v b/src/reordering/ReorderingExecA.v index 46f00f2..045cb78 100644 --- a/src/reordering/ReorderingExecA.v +++ b/src/reordering/ReorderingExecA.v @@ -629,7 +629,7 @@ Proof using INV INV'. rewrite EVEQ. rewrite id_union. rewrite seq_union_r. rewrite dom_union. rewrite set_subset_union_l; split. - { destruct SIMREL. intros x COND. + { intros x COND. unfold dom_rel in COND. destruct COND as [y COND]. destruct COND as (z & SB & XIN & YIN); subst z y. unfold set_minus. splits. @@ -778,10 +778,9 @@ Proof using INV INV'. assert (IND1 : (rpo_imm G_s') ⊆ mapper' ↑ (rpo_imm G_t')⁺). { unfold rpo_imm. assert (SIMRELD : reord_simrel X_s' X_t' a_t b_t mapper') by vauto. - destruct SIMREL'. arewrite (G_s' = WCore.G X_s'). rewrite wf_sbE. - rewrite rsr_sb. + rewrite (rsr_sb SIMREL'). rewrite NOEXA, cross_false_l, cross_false_r, union_false_r. rewrite !union_false_r. arewrite (eq b_t ∩₁ E_t' ≡₁ eq b_t). @@ -797,7 +796,7 @@ Proof using INV INV'. ⨾ ⦗acts_set G_s'⦘ ⨾ mapper' ↑ eq a_t × eq b_t ⨾ ⦗acts_set G_s'⦘ ⨾ ⦗F G_s' ∩₁ Acq G_s'⦘). - { arewrite (G_s' = WCore.G X_s'). rewrite rsr_acts. + { arewrite (G_s' = WCore.G X_s'). rewrite (rsr_acts SIMREL'). rewrite NOEXA. rels. arewrite_id (⦗R (WCore.G X_s') ∩₁ Rlx (WCore.G X_s')⦘). rels. arewrite (mapper' b_t = a_t). @@ -809,7 +808,7 @@ Proof using INV INV'. (a_t := a_t) (b_t := b_t) (mapper := mapper') (x := a_t); vauto. { destruct C1. subst x1. destruct C2 as (x1 & (EQ & INE) & RT). - split; vauto. apply rsr_acts; vauto. } + split; vauto. apply (rsr_acts SIMREL'); vauto. } { destruct C2 as (x2 & (EQ & INE) & RT); subst x2. destruct C1. subst x1. destruct RT as (EQQ & (RT & LT)). @@ -823,7 +822,7 @@ Proof using INV INV'. arewrite_false (⦗Acq G_s'⦘ ⨾ ⦗acts_set G_s'⦘ ⨾ mapper' ↑ eq a_t × eq b_t ⨾ ⦗acts_set G_s'⦘). - { arewrite (G_s' = WCore.G X_s'). rewrite rsr_acts. + { arewrite (G_s' = WCore.G X_s'). rewrite (rsr_acts SIMREL'). rewrite NOEXA. rels. arewrite_id (⦗mapper' ↑₁ E_t'⦘). rels. arewrite (mapper' a_t = b_t). @@ -835,7 +834,7 @@ Proof using INV INV'. (a_t := a_t) (b_t := b_t) (mapper := mapper') (x := b_t); vauto. } arewrite_false (⦗acts_set G_s'⦘ ⨾ mapper' ↑ eq a_t × eq b_t ⨾ ⦗acts_set G_s'⦘ ⨾ ⦗Rel G_s'⦘). - { arewrite (G_s' = WCore.G X_s'). rewrite rsr_acts. + { arewrite (G_s' = WCore.G X_s'). rewrite (rsr_acts SIMREL'). rewrite NOEXA. rels. arewrite_id (⦗mapper' ↑₁ E_t'⦘). rels. arewrite (mapper' b_t = a_t). @@ -850,13 +849,13 @@ Proof using INV INV'. unfold G_s'; ins. arewrite (y = mapper' b_t). { rewrite rsr_map_bt with (X_s := X_s') (X_t := X_t') (a_t := y); vauto. } - apply rsr_acts. left. + apply (rsr_acts SIMREL'). left. clear - INB'. basic_solver. } arewrite_false (⦗F G_s' ∩₁ Rel G_s'⦘ ⨾ ⦗acts_set G_s'⦘ ⨾ mapper' ↑ eq a_t × eq b_t ⨾ ⦗acts_set G_s'⦘ ⨾ ⦗W G_s' ∩₁ Rlx G_s'⦘). - { arewrite (G_s' = WCore.G X_s'). rewrite rsr_acts. + { arewrite (G_s' = WCore.G X_s'). rewrite (rsr_acts SIMREL'). rewrite NOEXA. rels. arewrite_id (⦗mapper' ↑₁ E_t'⦘). rels. arewrite (mapper' a_t = b_t). @@ -886,33 +885,31 @@ Proof using INV INV'. split; vauto. split; vauto. split. { unfold G_s' in COND1; ins. - unfold is_r. destruct rsr_lab with x'; vauto. } + unfold is_r. destruct (rsr_lab SIMREL') with x'; vauto. } unfold G_s' in COND2; ins. - unfold is_rlx. unfold mod. destruct rsr_lab with x'; vauto. } + unfold is_rlx. unfold mod. destruct (rsr_lab SIMREL') with x'; vauto. } arewrite (⦗mapper' ↑₁ E_t' ∩₁ (F (WCore.G X_s') ∩₁ Acq (WCore.G X_s'))⦘ ⊆ mapper' ↑ ⦗(E_t' ∩₁ F G_t' ∩₁ Acq G_t')⦘). { intros x y COND. destruct COND as (EQ & COND); subst y. - destruct SIMREL. destruct COND as [INE [FACQ FAT]]. unfold set_collect. destruct INE as [x' [INE MAP]]. exists x'. exists x'. splits; vauto. split; vauto. split. { split; vauto. unfold G_s' in FACQ; ins. - unfold is_f. destruct rsr_lab with x'; vauto. } + unfold is_f. destruct (rsr_lab SIMREL') with x'; vauto. } unfold G_s' in FAT; ins. - unfold is_acq. unfold mod. destruct rsr_lab with x'; vauto. } + unfold is_acq. unfold mod. destruct (rsr_lab SIMREL') with x'; vauto. } arewrite (⦗Acq (WCore.G X_s') ∩₁ mapper' ↑₁ E_t'⦘ ⊆ mapper' ↑ ⦗(Acq G_t' ∩₁ E_t')⦘). { intros x y COND. destruct COND as (EQ & COND); subst y. - destruct SIMREL. destruct COND as [ACQ INE]. unfold set_collect. destruct INE as [x' [INE MAP]]. exists x'. exists x'. splits; vauto. split; vauto. split; vauto. unfold G_s' in ACQ; ins. - unfold is_acq. unfold mod. destruct rsr_lab with x'; vauto. } + unfold is_acq. unfold mod. destruct (rsr_lab SIMREL') with x'; vauto. } arewrite (mapper' ↑ ⦗(Acq G_t' ∩₁ E_t')⦘ ⨾ mapper' ↑ sb_t' ⨾ ⦗mapper' ↑₁ E_t'⦘ ⊆ mapper' ↑ ⦗(Acq G_t' ∩₁ E_t')⦘ ⨾ mapper' ↑ sb_t' ⨾ mapper' ↑ ⦗E_t'⦘). { do 2 hahn_frame_l. rewrite collect_rel_eqv; vauto. } @@ -924,31 +921,28 @@ Proof using INV INV'. arewrite (⦗mapper' ↑₁ E_t' ∩₁ Rel (WCore.G X_s')⦘ ⊆ mapper' ↑ ⦗E_t' ∩₁ Rel G_t'⦘). { intros x y COND. destruct COND as (EQ & COND); subst y. - destruct SIMREL. destruct COND as [INE REL]. unfold set_collect. destruct INE as [x' [INE MAP]]. exists x'. exists x'. splits; vauto. split; vauto. split; vauto. unfold G_s' in REL; ins. - unfold is_rel. unfold mod. destruct rsr_lab with x'; vauto. } + unfold is_rel. unfold mod. destruct (rsr_lab SIMREL') with x'; vauto. } arewrite (⦗F (WCore.G X_s') ∩₁ Rel (WCore.G X_s') ∩₁ mapper' ↑₁ E_t'⦘ ⊆ mapper' ↑ ⦗(F G_t' ∩₁ Rel G_t' ∩₁ E_t')⦘). { intros x y COND. destruct COND as (EQ & COND); subst y. - destruct SIMREL. destruct COND as [[FENC REL] INE]. unfold set_collect. destruct INE as [x' [INE MAP]]. exists x'. exists x'. splits; vauto. split; vauto. split; vauto. split. { unfold G_s' in FENC; ins. - unfold is_f. destruct rsr_lab with x'; vauto. } + unfold is_f. destruct (rsr_lab SIMREL') with x'; vauto. } unfold G_s' in FENC; ins. - unfold is_rel. unfold mod. destruct rsr_lab with x'; vauto. } + unfold is_rel. unfold mod. destruct (rsr_lab SIMREL') with x'; vauto. } arewrite (⦗mapper' ↑₁ E_t' ∩₁ (W (WCore.G X_s') ∩₁ Rlx (WCore.G X_s'))⦘ ⊆ mapper' ↑ ⦗(E_t' ∩₁ W G_t' ∩₁ Rlx G_t')⦘). { intros x y COND. destruct COND as (EQ & COND); subst y. - destruct SIMREL. destruct COND as [INE [WRLX INE']]. unfold set_collect. destruct INE as [x' [INE MAP]]. @@ -957,9 +951,9 @@ Proof using INV INV'. { split; vauto. unfold G_s' in WRLX; ins. unfold is_w. unfold is_rlx. unfold mod. - destruct rsr_lab with x'; vauto. } + destruct (rsr_lab SIMREL') with x'; vauto. } unfold G_s' in INE'; ins. - unfold is_rlx. unfold mod. destruct rsr_lab with x'; vauto. } + unfold is_rlx. unfold mod. destruct (rsr_lab SIMREL') with x'; vauto. } rewrite <- ct_step. assert (SBT : sb_t' ≡ ⦗E_t'⦘ ⨾ sb_t' ⨾ ⦗E_t'⦘). { rewrite wf_sbE. basic_solver. } @@ -978,53 +972,53 @@ Proof using INV INV'. { clear. rewrite wf_sbE. basic_solver. } assert (IN2 : dom_rel ⦗E_t' ∩₁ F G_t' ∩₁ Acq G_t'⦘ ⊆₁ E_t'). { clear. basic_solver. } - rewrite IN1, IN2. - clear - rsr_inj; basic_solver 8. } + rewrite IN1, IN2. arewrite (E_t' ∪₁ E_t' ≡₁ E_t'); [basic_solver|]. + eapply (rsr_inj SIMREL'). } assert (IN1 : codom_rel ⦗R_t' ∩₁ Rlx G_t' ∩₁ E_t'⦘ ⊆₁ E_t'). { clear. basic_solver. } assert (IN2 : dom_rel (sb_t' ⨾ ⦗E_t' ∩₁ F G_t' ∩₁ Acq G_t'⦘) ⊆₁ E_t'). { clear. rewrite wf_sbE. basic_solver. } - rewrite IN1, IN2. - clear - rsr_inj; basic_solver 8. } + rewrite IN1, IN2. arewrite (E_t' ∪₁ E_t' ≡₁ E_t'); [basic_solver|]. + eapply (rsr_inj SIMREL'). } rewrite !collect_rel_seq; vauto. { assert (IN1 : codom_rel sb_t' ⊆₁ E_t'). { clear. rewrite wf_sbE. basic_solver. } assert (IN2 : dom_rel ⦗E_t'⦘ ⊆₁ E_t'). { clear. basic_solver. } - rewrite IN1, IN2. - clear - rsr_inj; basic_solver 8. } + rewrite IN1, IN2. arewrite (E_t' ∪₁ E_t' ≡₁ E_t'); [basic_solver|]. + eapply (rsr_inj SIMREL'). } assert (IN1 : codom_rel ⦗Acq G_t' ∩₁ E_t'⦘ ⊆₁ E_t'). { clear. basic_solver. } assert (IN2 : dom_rel (sb_t' ⨾ ⦗E_t'⦘) ⊆₁ E_t'). { clear. rewrite wf_sbE. basic_solver. } - rewrite IN1, IN2. - clear - rsr_inj; basic_solver 8. } + rewrite IN1, IN2. arewrite (E_t' ∪₁ E_t' ≡₁ E_t'); [basic_solver|]. + eapply (rsr_inj SIMREL'). } rewrite !collect_rel_seq; vauto. { assert (IN1 : codom_rel sb_t' ⊆₁ E_t'). { clear. rewrite wf_sbE. basic_solver. } assert (IN2 : dom_rel ⦗E_t' ∩₁ Rel G_t'⦘ ⊆₁ E_t'). { clear. basic_solver. } - rewrite IN1, IN2. - clear - rsr_inj; basic_solver 8. } + rewrite IN1, IN2. arewrite (E_t' ∪₁ E_t' ≡₁ E_t'); [basic_solver|]. + eapply (rsr_inj SIMREL'). } assert (IN1 : codom_rel ⦗E_t'⦘ ⊆₁ E_t'). { clear. basic_solver. } assert (IN2 : dom_rel (sb_t' ⨾ ⦗E_t' ∩₁ Rel G_t'⦘) ⊆₁ E_t'). { clear. rewrite wf_sbE. basic_solver. } - rewrite IN1, IN2. - clear - rsr_inj; basic_solver 8. } + rewrite IN1, IN2. arewrite (E_t' ∪₁ E_t' ≡₁ E_t'); [basic_solver|]. + eapply (rsr_inj SIMREL'). } rewrite !collect_rel_seq; rewrite <- set_interA; vauto. { assert (IN1 : codom_rel sb_t' ⊆₁ E_t'). { clear. rewrite wf_sbE. basic_solver. } assert (IN2 : dom_rel ⦗E_t' ∩₁ W_t' ∩₁ Rlx G_t'⦘ ⊆₁ E_t'). { clear. basic_solver. } - rewrite IN1, IN2. - clear - rsr_inj; basic_solver 8. } + rewrite IN1, IN2. arewrite (E_t' ∪₁ E_t' ≡₁ E_t'); [basic_solver|]. + eapply (rsr_inj SIMREL'). } assert (IN1 : codom_rel ⦗F G_t' ∩₁ Rel G_t' ∩₁ E_t'⦘ ⊆₁ E_t'). { clear. basic_solver. } assert (IN2 : dom_rel (sb_t' ⨾ ⦗E_t' ∩₁ W_t' ∩₁ Rlx G_t'⦘) ⊆₁ E_t'). { clear. rewrite wf_sbE. basic_solver. } - rewrite IN1, IN2. - clear - rsr_inj; basic_solver 8. } + rewrite IN1, IN2. arewrite (E_t' ∪₁ E_t' ≡₁ E_t'); [basic_solver|]. + eapply (rsr_inj SIMREL'). } assert (IND2 : mapper' ↑ (rpo_imm G_t')⁺ ⨾ (rpo_imm G_s') ⊆ mapper' ↑ (rpo_imm G_t')⁺). { assert (TRIN : mapper' ↑ (rpo_imm G_t')⁺ ⨾ mapper' ↑ (rpo_imm G_t')⁺ @@ -1035,7 +1029,7 @@ Proof using INV INV'. destruct P2 as (x0'' & y' & (P2 & M3 & M4)). exists x', y'. splits; vauto. assert (EQ : x0'' = x0'). - { destruct SIMREL'. apply rsr_inj; vauto. + { apply (rsr_inj SIMREL'); vauto. { apply ct_begin in P2. destruct P2 as (x1 & P2 & P3). destruct INV. @@ -1072,14 +1066,14 @@ Proof using INV INV'. unfold collect_rel. exists x0, y0. splits; vauto. split; vauto. unfold same_loc in *. unfold loc. unfold loc in PTH2. - destruct SIMREL'. rewrite <- rsr_lab; vauto. - { rewrite <- rsr_lab; vauto. + rewrite <- (rsr_lab SIMREL'); vauto. + { rewrite <- (rsr_lab SIMREL'); vauto. apply wf_sbE in SB. destruct SB as (x1 & INE1 & (y1 & SB & (EQ & INE2))); vauto. } apply wf_sbE in SB. destruct SB as (x1 & (EQ & INE) & RST); vauto. } - destruct SIMREL'. rewrite collect_rel_cross. - rewrite rsr_bt, rsr_at. destruct INV'. + rewrite collect_rel_cross. + rewrite (rsr_bt SIMREL'), (rsr_at SIMREL'). destruct INV'. arewrite_false (eq b_t × eq a_t ∩ same_loc (lab G_s')); vauto. intros x y COND. destruct COND as ((Q1 & Q2) & SL). subst x y. destruct rsr_at_bt_loc with a_t b_t. @@ -1087,8 +1081,8 @@ Proof using INV INV'. exists b_t. split; vauto. unfold same_loc in SL. unfold loc in SL. unfold same_loc, loc. - rewrite <- rsr_lab; vauto. - rewrite <- rsr_lab; vauto. + rewrite <- (rsr_lab SIMREL'); vauto. + rewrite <- (rsr_lab SIMREL'); vauto. unfold compose. assert (AEQ : mapper' a_t = b_t). { rewrite rsr_map_at with (X_s := X_s') (X_t := X_t') (b_t := b_t); vauto. } @@ -1096,9 +1090,9 @@ Proof using INV INV'. { rewrite rsr_map_bt with (X_s := X_s') (X_t := X_t') (a_t := a_t); vauto. } rewrite AEQ, BEQ. vauto. } unfold sw. unfold release. unfold rs. - destruct SIMREL'. arewrite (G_s' = WCore.G X_s'). - rewrite rsr_rf. rewrite NOEXA. rewrite set_inter_empty_l. - rels. rewrite rsr_rmw. + arewrite (G_s' = WCore.G X_s'). + rewrite (rsr_rf SIMREL'). rewrite NOEXA. rewrite set_inter_empty_l. + rels. rewrite (rsr_rmw SIMREL'). arewrite ((mapper' ↑ rf_t' ⨾ mapper' ↑ rmw_t')＊ ⨾ mapper' ↑ rf_t' ⊆ ⦗mapper' ↑₁ E_t'⦘ ⨾ (mapper' ↑ rf_t' ⨾ mapper' ↑ rmw_t')＊ ⨾ mapper' ↑ rf_t' ⨾ ⦗mapper' ↑₁ E_t'⦘). { rewrite rtE. rewrite !seq_union_l. @@ -1118,7 +1112,7 @@ Proof using INV INV'. ⨾ ⦗W (WCore.G X_s')⦘ ⨾ ⦗mapper' ↑₁ E_t'⦘) by mode_solver 21. arewrite (⦗F (WCore.G X_s')⦘ ⨾ sb (WCore.G X_s') ⊆ ⦗F (WCore.G X_s')⦘ ⨾ ⦗mapper' ↑₁ E_t'⦘ ⨾ mapper' ↑ sb_t'). - { rewrite rsr_sb. rewrite !seq_union_r. + { rewrite (rsr_sb SIMREL'). rewrite !seq_union_r. apply inclusion_union_l. { apply inclusion_union_l. { unfold swap_rel. rewrite collect_rel_union. @@ -1126,11 +1120,11 @@ Proof using INV INV'. apply inclusion_union_l. { transitivity (⦗F (WCore.G X_s')⦘ ⨾ mapper' ↑ (sb_t')); [basic_solver 21|]. hahn_frame_l. rewrite wf_sbE. basic_solver. } - rewrite collect_rel_cross. rewrite rsr_bt. + rewrite collect_rel_cross. rewrite (rsr_bt SIMREL'). arewrite (eq a_t ∩₁ E_t' ≡₁ eq a_t ∩₁ E_t' ∩₁ E_t') by basic_solver. rewrite (rsr_a_t_is_r_or_w INV'). arewrite_false (⦗F (WCore.G X_s')⦘ ⨾ (mapper' ↑₁ ((W_t' ∪₁ R_t') ∩₁ E_t')) × eq a_t); vauto. - rewrite <- cross_inter_l. clear - rsr_lab. + rewrite <- cross_inter_l. destruct SIMREL'. clear - rsr_lab. intros x y COND. destruct COND as (LT & RT); subst. destruct LT as [FNC MAP]. destruct MAP as [x0 [CONDS MAP]]. rewrite <- MAP in FNC. unfold is_f in FNC. @@ -1168,7 +1162,7 @@ Proof using INV INV'. red. exists y0, y0. splits; vauto. red. split; vauto. split; vauto. unfold is_rel in *. unfold mod in *. - rewrite <- rsr_lab; vauto. } + rewrite <- (rsr_lab SIMREL'); vauto. } rewrite <- seqA. transitivity (mapper' ↑ (((⦗F G_t'⦘ ⨾ sb_t')^? ⨾ ⦗E_t'⦘) ⨾ ⦗E_t'⦘ ⨾ ⦗Rlx G_t'⦘ ⨾ ⦗W_t'⦘ ⨾ ⦗E_t'⦘ ⨾ (rf_t' ⨾ rmw_t')＊ @@ -1189,10 +1183,10 @@ Proof using INV INV'. exists z0. splits; vauto. apply crE. right. exists x1. splits. { red. splits; vauto. - unfold is_f in *. rewrite <- rsr_lab; vauto. } + unfold is_f in *. rewrite <- (rsr_lab SIMREL'); vauto. } destruct MAP as (x0 & x2 & (SB & M1 & M2)). - apply rsr_inj in M1. - { apply rsr_inj in M2. subst; vauto. + apply (rsr_inj SIMREL') in M1. + { apply (rsr_inj SIMREL') in M2. subst; vauto. { apply wf_sbE in SB. clear - SB. destruct SB as (y1 & INE & (y2 & SB & (EQ & INE'))); vauto. } vauto. } @@ -1217,10 +1211,10 @@ Proof using INV INV'. exists y0. splits. { red. splits; vauto. unfold is_rlx in *. unfold mod in *. - destruct rsr_lab with y0; vauto. } + destruct (rsr_lab SIMREL') with y0; vauto. } red. split; vauto. unfold is_w in *. - destruct rsr_lab with y0; vauto. } + destruct (rsr_lab SIMREL') with y0; vauto. } rewrite <- collect_rel_seq. { transitivity (mapper' ↑ ((⦗E_t'⦘ ⨾ (rf_t' ⨾ rmw_t')＊) ⨾ rf_t' @@ -1246,7 +1240,7 @@ Proof using INV INV'. { apply collect_rel_ct_inj; vauto. } rewrite <- RESTR in EQQ. apply EQQ in COND'. destruct COND' as (x4 & y4 & PTH' & M3 & M4). - apply rsr_inj in M3, M4; vauto. + apply (rsr_inj SIMREL') in M3, M4; vauto. { apply ct_end in PTH'. destruct PTH' as (x5 & PTH' & PTH''). destruct PTH'' as (x6 & P1 & P2). apply wf_rmwE in P2; vauto. clear - P2. @@ -1273,7 +1267,7 @@ Proof using INV INV'. exists y0. splits; vauto. red. split; vauto. unfold is_rlx in *. unfold mod in *. - rewrite <- rsr_lab; vauto. } + rewrite <- (rsr_lab SIMREL'); vauto. } arewrite (⦗mapper' ↑₁ E_t'⦘ ⨾ (sb (WCore.G X_s') ⨾ ⦗F (WCore.G X_s')⦘)^? ⊆ ⦗mapper' ↑₁ E_t'⦘ ⨾ (sb (WCore.G X_s') ⨾ ⦗F (WCore.G X_s')⦘)^? ⨾ ⦗mapper' ↑₁ E_t'⦘). { rewrite crE at 1. @@ -1282,7 +1276,7 @@ Proof using INV INV'. apply inclusion_union_r. right. rewrite seqA. arewrite (sb (WCore.G X_s') ⊆ sb (WCore.G X_s') ⨾ ⦗acts_set (WCore.G X_s')⦘). { rewrite wf_sbE. basic_solver. } - rewrite rsr_acts. rewrite NOEXA. basic_solver. } + rewrite (rsr_acts SIMREL'). rewrite NOEXA. basic_solver. } arewrite (⦗mapper' ↑₁ E_t'⦘ ⨾ (sb (WCore.G X_s') ⨾ ⦗F (WCore.G X_s')⦘)^? ⊆ ⦗mapper' ↑₁ E_t'⦘ ⨾ (mapper' ↑ sb_t' ⨾ ⦗mapper' ↑₁ E_t'⦘ ⨾ ⦗F (WCore.G X_s')⦘)^?). { rewrite crE at 1. rewrite seq_union_r. @@ -1290,10 +1284,10 @@ Proof using INV INV'. hahn_frame_l. arewrite (sb (WCore.G X_s') ⊆ sb (WCore.G X_s') ⨾ ⦗acts_set (WCore.G X_s')⦘). { rewrite wf_sbE. basic_solver. } - rewrite rsr_acts. rewrite NOEXA. rewrite set_union_empty_r. + rewrite (rsr_acts SIMREL'). rewrite NOEXA. rewrite set_union_empty_r. rewrite crE. apply inclusion_union_r. right. - rewrite rsr_sb. rewrite !seq_union_l. + rewrite (rsr_sb SIMREL'). rewrite !seq_union_l. repeat apply inclusion_union_l. { unfold swap_rel. rewrite collect_rel_union. rewrite seq_union_l. apply inclusion_union_l. @@ -1305,7 +1299,7 @@ Proof using INV INV'. arewrite_false ((mapper' ↑₁ (eq a_t ∩₁ E_t')) × (mapper' ↑₁ ((W_t' ∪₁ R_t') ∩₁ E_t')) ⨾ ⦗mapper' ↑₁ E_t'⦘ ⨾ ⦗F (WCore.G X_s')⦘); vauto. rewrite <- seqA. rewrite <- cross_inter_r. rewrite <- cross_inter_r. - clear - rsr_lab. + destruct SIMREL'. clear - rsr_lab. intros x y COND. destruct COND as (LT & RT); subst. destruct RT as [[MAP1 MAP2] FNC]. destruct MAP1 as [x0 [CONDS MAP]]. rewrite <- MAP in FNC. unfold is_f in FNC. @@ -1332,8 +1326,8 @@ Proof using INV INV'. exists x1. splits; vauto. apply crE. right. exists x4. splits. { destruct SB as (x5 & x6 & (SB & M1 & M2)). - apply rsr_inj in M1. - { apply rsr_inj in M2. subst; vauto. + apply (rsr_inj SIMREL') in M1. + { apply (rsr_inj SIMREL') in M2. subst; vauto. { apply wf_sbE in SB. clear - SB. destruct SB as (y1 & INE & (y2 & SB & (EQ & INE'))); vauto. } vauto. } @@ -1341,7 +1335,7 @@ Proof using INV INV'. destruct SB as (y1 & (EQ & INE') & RST); vauto. } vauto. } red. splits; vauto. - unfold is_f in *. rewrite <- rsr_lab; vauto. } + unfold is_f in *. rewrite <- (rsr_lab SIMREL'); vauto. } intros x y COND. destruct COND as (x0 & (EQ & (x1 & INE & EQ1)) & (EQ2 & COND)); subst. red. exists x1, x1. splits; vauto. @@ -1349,7 +1343,7 @@ Proof using INV INV'. exists x1. splits; vauto. red. splits; vauto. unfold is_acq in *. unfold mod in *. - destruct rsr_lab with x1; vauto. } + destruct (rsr_lab SIMREL') with x1; vauto. } assert (IN1 : codom_rel (⦗E_t'⦘ ⨾ (sb_t' ⨾ ⦗F G_t'⦘)^?) ⊆₁ E_t'). { clear. rewrite wf_sbE. basic_solver. } assert (IN2 : dom_rel (⦗E_t'⦘ ⨾ ⦗Acq G_t'⦘ ⨾ ⦗E_t'⦘) ⊆₁ E_t'). @@ -1426,7 +1420,7 @@ Proof using INV INV'. destruct P2 as (x0'' & y' & (P2 & M3 & M4)). exists x', y'. splits; vauto. assert (EQ : x0'' = x0'). - { destruct SIMREL'. apply rsr_inj; vauto. + { apply (rsr_inj SIMREL'); vauto. { apply ct_begin in P2. destruct P2 as (x1 & P2 & P3). assert (P2' : rhb (G_t') x0'' x1) by vauto. diff --git a/src/reordering/ReorderingExecB.v b/src/reordering/ReorderingExecB.v index 9c8255f..cb9b419 100644 --- a/src/reordering/ReorderingExecB.v +++ b/src/reordering/ReorderingExecB.v @@ -339,8 +339,7 @@ Proof using INV INV'. rewrite updo; ins. { apply (rsr_lab SIMREL); eauto. } intros FALSE. - destruct SIMREL. - destruct rsr_codom with (x := mapper x). + destruct (rsr_codom SIMREL) with (x := mapper x). { unfold set_collect. exists x; split; vauto. } rewrite FALSE in H0. unfold extra_a in H0. basic_solver 21. } @@ -388,13 +387,13 @@ Proof using INV INV'. apply rpo_in_sb. } arewrite (⦗eq b_t⦘ ⨾ sb G_s'' ≡ ∅₂). { split; [| basic_solver]. - unfold sb at 1. ins. destruct SIMREL. - rewrite NEWSB. rewrite rsr_sb. unfold swap_rel. + unfold sb at 1. ins. + rewrite NEWSB. rewrite (rsr_sb SIMREL). unfold swap_rel. arewrite (eq b_t ∩₁ E_t ≡₁ ∅). { split; basic_solver. } rels. unfold extra_a. desf. { destruct a. destruct BNOTIN; eauto. } - rels. rewrite wf_sbE. + rels. rewrite wf_sbE. destruct SIMREL. unfold extra_a in rsr_codom. desf. unfold WCore.sb_delta. rewrite seq_union_r. @@ -435,14 +434,13 @@ Proof using INV INV'. destruct l_a'. { apply XmmCons.read_extent with (G_t := G_t) (sc_t := WCore.sc X_t) (a := b_t) (m := mapper); eauto. - { destruct SIMREL; vauto. } - { unfold G_s''; ins. destruct SIMREL. - rewrite rsr_acts. unfold extra_a. basic_solver 12. } + { apply SIMREL; vauto. } + { unfold G_s''; ins. + rewrite (rsr_acts SIMREL). unfold extra_a. basic_solver 12. } { unfold G_s'', is_r. ins. rewrite upds. ins. } { admit. (*TODO : finish *) } - { destruct SIMREL. - rewrite rsr_codom. basic_solver 21. } + { rewrite (rsr_codom SIMREL). basic_solver 21. } { unfold G_s'' at 2; ins. rewrite set_minus_union_l. rels. rewrite set_minusK. rels. @@ -453,9 +451,9 @@ Proof using INV INV'. apply NOTIN; vauto. } assert (SBSUB : sb G_s'' ⨾ ⦗E_s⦘ ⊆ mapper ↑ sb_t). { unfold sb at 1. ins. rewrite NEWSB. - rewrite seq_union_l. destruct SIMREL. + rewrite seq_union_l. unfold WCore.sb_delta. apply inclusion_union_l. - { rewrite rsr_sb. arewrite_id ⦗E_s⦘; rels. + { rewrite (rsr_sb SIMREL). arewrite_id ⦗E_s⦘; rels. apply inclusion_union_l. { apply inclusion_union_l. { unfold swap_rel. basic_solver 8. } @@ -499,7 +497,7 @@ Proof using INV INV'. seq_rewrite <- !id_inter. arewrite (R G_s'' ∩₁ Rlx G_s'' ∩₁ mapper ↑₁ E_t ⊆₁ mapper ↑₁ (R_t ∩₁ Rlx G_t ∩₁ E_t)). - { intros x COND. destruct SIMREL. + { intros x COND. destruct COND as ((COND1 & COND2) & INE). destruct INE as [x' [INE MAP]]. unfold set_collect. @@ -507,28 +505,30 @@ Proof using INV INV'. split; vauto. split. { unfold G_s'' in COND1; ins. - unfold is_r. destruct rsr_lab with x'; vauto. + unfold is_r. destruct (rsr_lab SIMREL) with x'; vauto. unfold compose. unfold is_r in COND1. rewrite updo in COND1; vauto. intros FALSE. assert (INMAP : (mapper ↑₁ E_t) b_t). - { clear - FALSE INE rsr_codom. basic_solver. } - apply rsr_codom in INMAP. + { rewrite <- FALSE. unfold set_collect. + exists x'; vauto. } + apply (rsr_codom SIMREL) in INMAP. clear - INMAP NOTIN. unfold set_minus in INMAP. desf. } unfold G_s'' in COND2; ins. - unfold is_rlx. unfold mod. destruct rsr_lab with x'; vauto. + unfold is_rlx. unfold mod. destruct (rsr_lab SIMREL) with x'; vauto. unfold compose. unfold is_rlx in COND2. unfold mod in COND2. rewrite updo in COND2; vauto. intros FALSE. assert (INMAP : (mapper ↑₁ E_t) b_t). - { clear - FALSE INE rsr_codom. basic_solver. } - apply rsr_codom in INMAP. + { rewrite <- FALSE. unfold set_collect. + exists x'; vauto. } + apply (rsr_codom SIMREL) in INMAP. clear - INMAP NOTIN. unfold set_minus in INMAP. desf. } arewrite (mapper ↑₁ E_t ∩₁ (F G_s'' ∩₁ Acq G_s'') ⊆₁ mapper ↑₁ (E_t ∩₁ F G_t ∩₁ Acq G_t)). - { intros x COND. destruct SIMREL. + { intros x COND. destruct COND as (COND1 & COND2). destruct COND1 as [x' [INE MAP]]. unfold set_collect. @@ -538,24 +538,26 @@ Proof using INV INV'. { unfold G_s'' in COND2; ins. } destruct COND2 as (COND1 & COND2). { unfold G_s'' in COND1; ins. - unfold is_f. destruct rsr_lab with x'; vauto. + unfold is_f. destruct (rsr_lab SIMREL) with x'; vauto. unfold compose. unfold is_f in COND1. rewrite updo in COND1; vauto. intros FALSE. assert (INMAP : (mapper ↑₁ E_t) b_t). - { clear - FALSE INE rsr_codom. basic_solver. } - apply rsr_codom in INMAP. + { rewrite <- FALSE. unfold set_collect. + exists x'; vauto. } + apply (rsr_codom SIMREL) in INMAP. clear - INMAP NOTIN. unfold set_minus in INMAP. desf. } destruct COND2 as (COND1 & COND2). unfold G_s'' in COND2; ins. - unfold is_acq. unfold mod. destruct rsr_lab with x'; vauto. + unfold is_acq. unfold mod. destruct (rsr_lab SIMREL) with x'; vauto. unfold compose. unfold is_acq in COND2. unfold mod in COND2. rewrite updo in COND2; vauto. intros FALSE. assert (INMAP : (mapper ↑₁ E_t) b_t). - { clear - FALSE INE rsr_codom. basic_solver. } - apply rsr_codom in INMAP. + { rewrite <- FALSE. unfold set_collect. + exists x'; vauto. } + apply (rsr_codom SIMREL) in INMAP. clear - INMAP NOTIN. unfold set_minus in INMAP. desf. } rewrite !collect_rel_seq. @@ -564,32 +566,35 @@ Proof using INV INV'. { basic_solver. } assert (IN2 : codom_rel sb_t ⊆₁ E_t). { rewrite wf_sbE. basic_solver. } - rewrite IN1, IN2. destruct SIMREL. basic_solver. } + rewrite IN1, IN2. arewrite (E_t ∪₁ E_t ≡₁ E_t); [basic_solver|]. + eapply (rsr_inj SIMREL). } assert (IN1 : codom_rel ⦗R_t ∩₁ Rlx G_t ∩₁ E_t⦘ ⊆₁ E_t). { basic_solver 8. } assert (IN2 : dom_rel (sb_t ⨾ ⦗E_t ∩₁ (F G_t ∩₁ Acq G_t)⦘) ⊆₁ E_t). { rewrite wf_sbE. basic_solver 8. } - rewrite IN1, IN2. destruct SIMREL. basic_solver. } + rewrite IN1, IN2. arewrite (E_t ∪₁ E_t ≡₁ E_t); [basic_solver|]. + eapply (rsr_inj SIMREL). } { rewrite wf_sbE. rewrite 2! collect_rel_seqi. rewrite collect_rel_eqv. seq_rewrite <- !id_inter. arewrite (Acq G_s'' ∩₁ mapper ↑₁ E_t ⊆₁ mapper ↑₁ (Acq G_t ∩₁ E_t)). - { intros x COND. destruct SIMREL. + { intros x COND. destruct COND as (COND1 & COND2). destruct COND2 as [x' [INE MAP]]. unfold set_collect. exists x'. splits; vauto. split; vauto. unfold G_s'' in COND1; ins. - unfold is_acq. unfold mod. destruct rsr_lab with x'; vauto. + unfold is_acq. unfold mod. destruct (rsr_lab SIMREL) with x'; vauto. unfold compose. unfold is_acq in COND1. unfold mod in COND1. rewrite updo in COND1; vauto. intros FALSE. assert (INMAP : (mapper ↑₁ E_t) b_t). - { clear - FALSE INE rsr_codom. basic_solver. } - apply rsr_codom in INMAP. + { rewrite <- FALSE. unfold set_collect. + exists x'; vauto. } + apply (rsr_codom SIMREL) in INMAP. clear - INMAP NOTIN. unfold set_minus in INMAP. desf. } rewrite !collect_rel_seq. @@ -598,32 +603,35 @@ Proof using INV INV'. { basic_solver. } assert (IN2 : codom_rel sb_t ⊆₁ E_t). { rewrite wf_sbE. basic_solver. } - rewrite IN1, IN2. destruct SIMREL. basic_solver. } + rewrite IN1, IN2. arewrite (E_t ∪₁ E_t ≡₁ E_t); [basic_solver|]. + eapply (rsr_inj SIMREL). } assert (IN1 : codom_rel ⦗Acq G_t ∩₁ E_t⦘ ⊆₁ E_t). { basic_solver 8. } assert (IN2 : dom_rel (sb_t ⨾ ⦗E_t⦘) ⊆₁ E_t). { rewrite wf_sbE. basic_solver 8. } - rewrite IN1, IN2. destruct SIMREL. basic_solver. } + rewrite IN1, IN2. arewrite (E_t ∪₁ E_t ≡₁ E_t); [basic_solver|]. + eapply (rsr_inj SIMREL). } { rewrite wf_sbE. rewrite 2! collect_rel_seqi. rewrite collect_rel_eqv. rewrite !seqA. seq_rewrite <- !id_inter. arewrite (mapper ↑₁ E_t ∩₁ Rel G_s'' ⊆₁ mapper ↑₁ (E_t ∩₁ Rel G_t)). - { intros x COND. destruct SIMREL. + { intros x COND. destruct COND as (COND1 & COND2). destruct COND1 as [x' [INE MAP]]. unfold set_collect. exists x'. splits; vauto. split; vauto. unfold G_s'' in COND2; ins. - unfold is_rel, mod. destruct rsr_lab with x'; vauto. + unfold is_rel, mod. destruct (rsr_lab SIMREL) with x'; vauto. unfold compose. unfold is_rel, mod in COND2. rewrite updo in COND2; vauto. intros FALSE. assert (INMAP : (mapper ↑₁ E_t) b_t). - { clear - FALSE INE rsr_codom. basic_solver. } - apply rsr_codom in INMAP. + { rewrite <- FALSE. unfold set_collect. + exists x'; vauto. } + apply (rsr_codom SIMREL) in INMAP. clear - INMAP NOTIN. unfold set_minus in INMAP. desf. } rewrite !collect_rel_seq. @@ -632,19 +640,21 @@ Proof using INV INV'. { basic_solver. } assert (IN2 : codom_rel sb_t ⊆₁ E_t). { rewrite wf_sbE. basic_solver. } - rewrite IN1, IN2. destruct SIMREL. basic_solver. } + rewrite IN1, IN2. arewrite (E_t ∪₁ E_t ≡₁ E_t); [basic_solver|]. + eapply (rsr_inj SIMREL). } assert (IN1 : dom_rel (sb_t ⨾ ⦗E_t ∩₁ Rel G_t⦘) ⊆₁ E_t). { rewrite wf_sbE. basic_solver 8. } assert (IN2 : codom_rel ⦗E_t⦘ ⊆₁ E_t). { basic_solver 8. } - rewrite IN1, IN2. destruct SIMREL. basic_solver. } + rewrite IN1, IN2. arewrite (E_t ∪₁ E_t ≡₁ E_t); [basic_solver|]. + eapply (rsr_inj SIMREL). } rewrite wf_sbE. rewrite 2! collect_rel_seqi. rewrite collect_rel_eqv. rewrite !seqA. seq_rewrite <- !id_inter. arewrite (F G_s'' ∩₁ Rel G_s'' ∩₁ mapper ↑₁ E_t ⊆₁ mapper ↑₁ (F G_t ∩₁ Rel G_t ∩₁ E_t)). - { intros x COND. destruct SIMREL. + { intros x COND. destruct COND as (COND1 & (y & COND2)). destruct COND2 as (COND2 & COND3). destruct COND1 as [ISF INREL]. @@ -653,30 +663,32 @@ Proof using INV INV'. split; vauto. split. { unfold G_s'' in COND2; ins. - unfold is_f. destruct rsr_lab with y; vauto. + unfold is_f. destruct (rsr_lab SIMREL) with y; vauto. unfold compose. unfold is_f in ISF. rewrite updo in ISF; vauto. intros FALSE. assert (INMAP : (mapper ↑₁ E_t) b_t). - { clear - FALSE COND2 rsr_codom. basic_solver. } - apply rsr_codom in INMAP. + { rewrite <- FALSE. unfold set_collect. + exists y; vauto. } + apply (rsr_codom SIMREL) in INMAP. clear - INMAP NOTIN. unfold set_minus in INMAP. desf. } unfold is_rel, mod in INREL. unfold is_rel, mod. - destruct rsr_lab with y; vauto. + destruct (rsr_lab SIMREL) with y; vauto. unfold compose. unfold is_rel, mod in INREL. unfold G_s'' in INREL; ins. rewrite updo in INREL; vauto. intros FALSE. assert (INMAP : (mapper ↑₁ E_t) b_t). - { clear - FALSE COND2 rsr_codom. basic_solver. } - apply rsr_codom in INMAP. + { rewrite <- FALSE. unfold set_collect. + exists y; vauto. } + apply (rsr_codom SIMREL) in INMAP. clear - INMAP NOTIN. unfold set_minus in INMAP. desf. } arewrite (mapper ↑₁ E_t ∩₁ (W G_s'' ∩₁ Rlx G_s'') ⊆₁ mapper ↑₁ (E_t ∩₁ W G_t ∩₁ Rlx G_t)). - { intros x COND. destruct SIMREL. + { intros x COND. destruct COND as (COND1 & COND2). destruct COND1 as [x' [INE MAP]]. destruct COND2 as [ISW INRLX]. @@ -685,23 +697,25 @@ Proof using INV INV'. split. { split; vauto. unfold G_s'' in ISW; ins. - unfold is_w. destruct rsr_lab with x'; vauto. + unfold is_w. destruct (rsr_lab SIMREL) with x'; vauto. unfold compose. unfold is_w in ISW. rewrite updo in ISW; vauto. intros FALSE. assert (INMAP : (mapper ↑₁ E_t) b_t). - { clear - FALSE INE rsr_codom. basic_solver. } - apply rsr_codom in INMAP. + { rewrite <- FALSE. unfold set_collect. + exists x'; vauto. } + apply (rsr_codom SIMREL) in INMAP. clear - INMAP NOTIN. unfold set_minus in INMAP. desf. } unfold G_s'' in INRLX; ins. - unfold is_rlx. unfold mod. destruct rsr_lab with x'; vauto. + unfold is_rlx. unfold mod. destruct (rsr_lab SIMREL) with x'; vauto. unfold compose. unfold is_rlx in INRLX. unfold mod in INRLX. rewrite updo in INRLX; vauto. intros FALSE. assert (INMAP : (mapper ↑₁ E_t) b_t). - { clear - FALSE INE rsr_codom. basic_solver. } - apply rsr_codom in INMAP. + { rewrite <- FALSE. unfold set_collect. + exists x'; vauto. } + apply (rsr_codom SIMREL) in INMAP. clear - INMAP NOTIN. unfold set_minus in INMAP. desf. } rewrite !collect_rel_seq. @@ -710,12 +724,14 @@ Proof using INV INV'. { basic_solver. } assert (IN2 : codom_rel sb_t ⊆₁ E_t). { rewrite wf_sbE. basic_solver. } - rewrite IN1, IN2. destruct SIMREL. basic_solver. } + rewrite IN1, IN2. arewrite (E_t ∪₁ E_t ≡₁ E_t); [basic_solver|]. + eapply (rsr_inj SIMREL). } assert (IN1 : codom_rel ⦗F G_t ∩₁ Rel G_t ∩₁ E_t⦘ ⊆₁ E_t). { basic_solver 8. } assert (IN2 : dom_rel (sb_t ⨾ ⦗E_t ∩₁ (W_t ∩₁ Rlx G_t)⦘) ⊆₁ E_t). { rewrite wf_sbE. basic_solver 8. } - rewrite IN1, IN2. destruct SIMREL. basic_solver. } + rewrite IN1, IN2. arewrite (E_t ∪₁ E_t ≡₁ E_t); [basic_solver|]. + eapply (rsr_inj SIMREL). } assert (IND2 : mapper ↑ (rpo_imm G_t)⁺ ⨾ (rpo_imm G_s'' ⨾ ⦗E_s⦘) ⊆ mapper ↑ (rpo_imm G_t)⁺). { assert (TRIN : mapper ↑ (rpo_imm G_t)⁺ ⨾ mapper ↑ (rpo_imm G_t)⁺ @@ -726,7 +742,7 @@ Proof using INV INV'. destruct P2 as (x0'' & y' & (P2 & M3 & M4)). exists x', y'. splits; vauto. assert (EQ : x0'' = x0'). - { destruct SIMREL. apply rsr_inj; vauto. + { apply (rsr_inj SIMREL); vauto. { apply ct_begin in P2. destruct P2 as (x1 & P2 & P3). destruct INV. @@ -745,13 +761,13 @@ Proof using INV INV'. { split; [| basic_solver]. unfold sb at 1. ins. rewrite NEWSB. rewrite inter_union_l. rewrite seq_union_r. rewrite codom_union. - destruct SIMREL. rewrite rsr_sb. + rewrite (rsr_sb SIMREL). unfold swap_rel. arewrite (eq b_t ∩₁ E_t ≡₁ ∅). { split; basic_solver. } rels. unfold extra_a. desf. { destruct a. destruct BNOTIN; eauto. } - rels. rewrite wf_sbE. + rels. rewrite wf_sbE. destruct SIMREL. unfold extra_a in rsr_codom. desf. unfold WCore.sb_delta. assert (EMP1 : ⦗eq b_t⦘ ⨾ ((fun a : actid => is_init a) @@ -781,13 +797,13 @@ Proof using INV INV'. rewrite PROP1, PROP2; basic_solver. } { unfold sb at 1. ins. rewrite NEWSB. rewrite inter_union_l. - destruct SIMREL. rewrite rsr_sb. + rewrite (rsr_sb SIMREL). unfold swap_rel. arewrite (eq b_t ∩₁ E_t ≡₁ ∅). { split; basic_solver. } rels. unfold extra_a. desf. { destruct a. destruct BNOTIN; eauto. } - rels. rewrite wf_sbE. + rels. rewrite wf_sbE. destruct SIMREL. unfold extra_a in rsr_codom. desf. unfold WCore.sb_delta. arewrite (⦗(E_s ∪₁ eq b_t) \₁ eq b_t⦘ ⊆ ⦗E_s⦘). @@ -826,7 +842,7 @@ Proof using INV INV'. basic_solver 21. } { unfold G_s'' at 1; ins. unfold WCore.lab_is_r. desf. rewrite set_inter_full_r. - destruct SIMREL. rewrite rsr_rf. + rewrite (rsr_rf SIMREL). unfold extra_a. desf. { exfalso. eapply BNOTIN. apply a. } rewrite set_inter_empty_l; rels. @@ -836,20 +852,19 @@ Proof using INV INV'. rewrite SRF'; vauto. } { unfold G_s''; ins. unfold WCore.lab_is_w. desf. rewrite set_inter_empty_r. rels. - destruct SIMREL. rewrite rsr_co. + rewrite (rsr_co SIMREL). unfold add_max. unfold extra_a at 2. desf. { exfalso. eapply BNOTIN. apply a. } rewrite set_inter_empty_l; rels. } destruct INV; eauto. } { apply XmmCons.write_extent with (G_t := G_t) (sc_t := WCore.sc X_t) (a := b_t) (m := mapper); eauto. - { destruct SIMREL; vauto. } - { unfold G_s''; ins. destruct SIMREL. - rewrite rsr_acts. unfold extra_a. basic_solver 12. } + { apply SIMREL; vauto. } + { unfold G_s''; ins. + rewrite (rsr_acts SIMREL). unfold extra_a. basic_solver 12. } { unfold G_s''; ins. unfold upd. unfold is_w. basic_solver. } - { destruct SIMREL. - rewrite rsr_codom. basic_solver 21. } + { rewrite (rsr_codom SIMREL). basic_solver 21. } { unfold G_s'' at 2; ins. rewrite set_minus_union_l. rels. rewrite set_minusK. rels. @@ -860,9 +875,9 @@ Proof using INV INV'. apply NOTIN; vauto. } assert (SBSUB : sb G_s'' ⨾ ⦗E_s⦘ ⊆ mapper ↑ sb_t). { unfold sb at 1. ins. rewrite NEWSB. - rewrite seq_union_l. destruct SIMREL. + rewrite seq_union_l. unfold WCore.sb_delta. apply inclusion_union_l. - { rewrite rsr_sb. arewrite_id ⦗E_s⦘; rels. + { rewrite (rsr_sb SIMREL). arewrite_id ⦗E_s⦘; rels. apply inclusion_union_l. { apply inclusion_union_l. { unfold swap_rel. basic_solver 8. } @@ -906,7 +921,7 @@ Proof using INV INV'. seq_rewrite <- !id_inter. arewrite (R G_s'' ∩₁ Rlx G_s'' ∩₁ mapper ↑₁ E_t ⊆₁ mapper ↑₁ (R_t ∩₁ Rlx G_t ∩₁ E_t)). - { intros x COND. destruct SIMREL. + { intros x COND. destruct COND as ((COND1 & COND2) & INE). destruct INE as [x' [INE MAP]]. unfold set_collect. @@ -914,28 +929,30 @@ Proof using INV INV'. split; vauto. split. { unfold G_s'' in COND1; ins. - unfold is_r. destruct rsr_lab with x'; vauto. + unfold is_r. destruct (rsr_lab SIMREL) with x'; vauto. unfold compose. unfold is_r in COND1. rewrite updo in COND1; vauto. intros FALSE. assert (INMAP : (mapper ↑₁ E_t) b_t). - { clear - FALSE INE rsr_codom. basic_solver. } - apply rsr_codom in INMAP. + { rewrite <- FALSE. unfold set_collect. + exists x'; vauto. } + apply (rsr_codom SIMREL) in INMAP. clear - INMAP NOTIN. unfold set_minus in INMAP. desf. } unfold G_s'' in COND2; ins. - unfold is_rlx. unfold mod. destruct rsr_lab with x'; vauto. + unfold is_rlx. unfold mod. destruct (rsr_lab SIMREL) with x'; vauto. unfold compose. unfold is_rlx in COND2. unfold mod in COND2. rewrite updo in COND2; vauto. intros FALSE. assert (INMAP : (mapper ↑₁ E_t) b_t). - { clear - FALSE INE rsr_codom. basic_solver. } - apply rsr_codom in INMAP. + { rewrite <- FALSE. unfold set_collect. + exists x'; vauto. } + apply (rsr_codom SIMREL) in INMAP. clear - INMAP NOTIN. unfold set_minus in INMAP. desf. } arewrite (mapper ↑₁ E_t ∩₁ (F G_s'' ∩₁ Acq G_s'') ⊆₁ mapper ↑₁ (E_t ∩₁ F G_t ∩₁ Acq G_t)). - { intros x COND. destruct SIMREL. + { intros x COND. destruct COND as (COND1 & COND2). destruct COND1 as [x' [INE MAP]]. unfold set_collect. @@ -945,24 +962,26 @@ Proof using INV INV'. { unfold G_s'' in COND2; ins. } destruct COND2 as (COND1 & COND2). { unfold G_s'' in COND1; ins. - unfold is_f. destruct rsr_lab with x'; vauto. + unfold is_f. destruct (rsr_lab SIMREL) with x'; vauto. unfold compose. unfold is_f in COND1. rewrite updo in COND1; vauto. intros FALSE. assert (INMAP : (mapper ↑₁ E_t) b_t). - { clear - FALSE INE rsr_codom. basic_solver. } - apply rsr_codom in INMAP. + { rewrite <- FALSE. unfold set_collect. + exists x'; vauto. } + apply (rsr_codom SIMREL) in INMAP. clear - INMAP NOTIN. unfold set_minus in INMAP. desf. } destruct COND2 as (COND1 & COND2). unfold G_s'' in COND2; ins. - unfold is_acq. unfold mod. destruct rsr_lab with x'; vauto. + unfold is_acq. unfold mod. destruct (rsr_lab SIMREL) with x'; vauto. unfold compose. unfold is_acq in COND2. unfold mod in COND2. rewrite updo in COND2; vauto. intros FALSE. assert (INMAP : (mapper ↑₁ E_t) b_t). - { clear - FALSE INE rsr_codom. basic_solver. } - apply rsr_codom in INMAP. + { rewrite <- FALSE. unfold set_collect. + exists x'; vauto. } + apply (rsr_codom SIMREL) in INMAP. clear - INMAP NOTIN. unfold set_minus in INMAP. desf. } rewrite !collect_rel_seq. @@ -971,32 +990,35 @@ Proof using INV INV'. { basic_solver. } assert (IN2 : codom_rel sb_t ⊆₁ E_t). { rewrite wf_sbE. basic_solver. } - rewrite IN1, IN2. destruct SIMREL. basic_solver. } + rewrite IN1, IN2. arewrite (E_t ∪₁ E_t ≡₁ E_t); [basic_solver|]. + eapply (rsr_inj SIMREL). } assert (IN1 : codom_rel ⦗R_t ∩₁ Rlx G_t ∩₁ E_t⦘ ⊆₁ E_t). { basic_solver 8. } assert (IN2 : dom_rel (sb_t ⨾ ⦗E_t ∩₁ (F G_t ∩₁ Acq G_t)⦘) ⊆₁ E_t). { rewrite wf_sbE. basic_solver 8. } - rewrite IN1, IN2. destruct SIMREL. basic_solver. } + rewrite IN1, IN2. arewrite (E_t ∪₁ E_t ≡₁ E_t); [basic_solver|]. + eapply (rsr_inj SIMREL). } { rewrite wf_sbE. rewrite 2! collect_rel_seqi. rewrite collect_rel_eqv. seq_rewrite <- !id_inter. arewrite (Acq G_s'' ∩₁ mapper ↑₁ E_t ⊆₁ mapper ↑₁ (Acq G_t ∩₁ E_t)). - { intros x COND. destruct SIMREL. + { intros x COND. destruct COND as (COND1 & COND2). destruct COND2 as [x' [INE MAP]]. unfold set_collect. exists x'. splits; vauto. split; vauto. unfold G_s'' in COND1; ins. - unfold is_acq. unfold mod. destruct rsr_lab with x'; vauto. + unfold is_acq. unfold mod. destruct (rsr_lab SIMREL) with x'; vauto. unfold compose. unfold is_acq in COND1. unfold mod in COND1. rewrite updo in COND1; vauto. intros FALSE. assert (INMAP : (mapper ↑₁ E_t) b_t). - { clear - FALSE INE rsr_codom. basic_solver. } - apply rsr_codom in INMAP. + { rewrite <- FALSE. unfold set_collect. + exists x'; vauto. } + apply (rsr_codom SIMREL) in INMAP. clear - INMAP NOTIN. unfold set_minus in INMAP. desf. } rewrite !collect_rel_seq. @@ -1005,32 +1027,35 @@ Proof using INV INV'. { basic_solver. } assert (IN2 : codom_rel sb_t ⊆₁ E_t). { rewrite wf_sbE. basic_solver. } - rewrite IN1, IN2. destruct SIMREL. basic_solver. } + rewrite IN1, IN2. arewrite (E_t ∪₁ E_t ≡₁ E_t); [basic_solver|]. + eapply (rsr_inj SIMREL). } assert (IN1 : codom_rel ⦗Acq G_t ∩₁ E_t⦘ ⊆₁ E_t). { basic_solver 8. } assert (IN2 : dom_rel (sb_t ⨾ ⦗E_t⦘) ⊆₁ E_t). { rewrite wf_sbE. basic_solver 8. } - rewrite IN1, IN2. destruct SIMREL. basic_solver. } + rewrite IN1, IN2. arewrite (E_t ∪₁ E_t ≡₁ E_t); [basic_solver|]. + eapply (rsr_inj SIMREL). } { rewrite wf_sbE. rewrite 2! collect_rel_seqi. rewrite collect_rel_eqv. rewrite !seqA. seq_rewrite <- !id_inter. arewrite (mapper ↑₁ E_t ∩₁ Rel G_s'' ⊆₁ mapper ↑₁ (E_t ∩₁ Rel G_t)). - { intros x COND. destruct SIMREL. + { intros x COND. destruct COND as (COND1 & COND2). destruct COND1 as [x' [INE MAP]]. unfold set_collect. exists x'. splits; vauto. split; vauto. unfold G_s'' in COND2; ins. - unfold is_rel, mod. destruct rsr_lab with x'; vauto. + unfold is_rel, mod. destruct (rsr_lab SIMREL) with x'; vauto. unfold compose. unfold is_rel, mod in COND2. rewrite updo in COND2; vauto. intros FALSE. assert (INMAP : (mapper ↑₁ E_t) b_t). - { clear - FALSE INE rsr_codom. basic_solver. } - apply rsr_codom in INMAP. + { rewrite <- FALSE. unfold set_collect. + exists x'; vauto. } + apply (rsr_codom SIMREL) in INMAP. clear - INMAP NOTIN. unfold set_minus in INMAP. desf. } rewrite !collect_rel_seq. @@ -1039,19 +1064,21 @@ Proof using INV INV'. { basic_solver. } assert (IN2 : codom_rel sb_t ⊆₁ E_t). { rewrite wf_sbE. basic_solver. } - rewrite IN1, IN2. destruct SIMREL. basic_solver. } + rewrite IN1, IN2. arewrite (E_t ∪₁ E_t ≡₁ E_t); [basic_solver|]. + eapply (rsr_inj SIMREL). } assert (IN1 : dom_rel (sb_t ⨾ ⦗E_t ∩₁ Rel G_t⦘) ⊆₁ E_t). { rewrite wf_sbE. basic_solver 8. } assert (IN2 : codom_rel ⦗E_t⦘ ⊆₁ E_t). { basic_solver 8. } - rewrite IN1, IN2. destruct SIMREL. basic_solver. } + rewrite IN1, IN2. arewrite (E_t ∪₁ E_t ≡₁ E_t); [basic_solver|]. + eapply (rsr_inj SIMREL). } rewrite wf_sbE. rewrite 2! collect_rel_seqi. rewrite collect_rel_eqv. rewrite !seqA. seq_rewrite <- !id_inter. arewrite (F G_s'' ∩₁ Rel G_s'' ∩₁ mapper ↑₁ E_t ⊆₁ mapper ↑₁ (F G_t ∩₁ Rel G_t ∩₁ E_t)). - { intros x COND. destruct SIMREL. + { intros x COND. destruct COND as (COND1 & (y & COND2)). destruct COND2 as (COND2 & COND3). destruct COND1 as [ISF INREL]. @@ -1060,30 +1087,32 @@ Proof using INV INV'. split; vauto. split. { unfold G_s'' in COND2; ins. - unfold is_f. destruct rsr_lab with y; vauto. + unfold is_f. destruct (rsr_lab SIMREL) with y; vauto. unfold compose. unfold is_f in ISF. rewrite updo in ISF; vauto. intros FALSE. assert (INMAP : (mapper ↑₁ E_t) b_t). - { clear - FALSE COND2 rsr_codom. basic_solver. } - apply rsr_codom in INMAP. + { rewrite <- FALSE. unfold set_collect. + exists y; vauto. } + apply (rsr_codom SIMREL) in INMAP. clear - INMAP NOTIN. unfold set_minus in INMAP. desf. } unfold is_rel, mod in INREL. unfold is_rel, mod. - destruct rsr_lab with y; vauto. + destruct (rsr_lab SIMREL) with y; vauto. unfold compose. unfold is_rel, mod in INREL. unfold G_s'' in INREL; ins. rewrite updo in INREL; vauto. intros FALSE. assert (INMAP : (mapper ↑₁ E_t) b_t). - { clear - FALSE COND2 rsr_codom. basic_solver. } - apply rsr_codom in INMAP. + { rewrite <- FALSE. unfold set_collect. + exists y; vauto. } + apply (rsr_codom SIMREL) in INMAP. clear - INMAP NOTIN. unfold set_minus in INMAP. desf. } arewrite (mapper ↑₁ E_t ∩₁ (W G_s'' ∩₁ Rlx G_s'') ⊆₁ mapper ↑₁ (E_t ∩₁ W G_t ∩₁ Rlx G_t)). - { intros x COND. destruct SIMREL. + { intros x COND. destruct COND as (COND1 & COND2). destruct COND1 as [x' [INE MAP]]. destruct COND2 as [ISW INRLX]. @@ -1092,23 +1121,25 @@ Proof using INV INV'. split. { split; vauto. unfold G_s'' in ISW; ins. - unfold is_w. destruct rsr_lab with x'; vauto. + unfold is_w. destruct (rsr_lab SIMREL) with x'; vauto. unfold compose. unfold is_w in ISW. rewrite updo in ISW; vauto. intros FALSE. assert (INMAP : (mapper ↑₁ E_t) b_t). - { clear - FALSE INE rsr_codom. basic_solver. } - apply rsr_codom in INMAP. + { rewrite <- FALSE. unfold set_collect. + exists x'; vauto. } + apply (rsr_codom SIMREL) in INMAP. clear - INMAP NOTIN. unfold set_minus in INMAP. desf. } unfold G_s'' in INRLX; ins. - unfold is_rlx. unfold mod. destruct rsr_lab with x'; vauto. + unfold is_rlx. unfold mod. destruct (rsr_lab SIMREL) with x'; vauto. unfold compose. unfold is_rlx in INRLX. unfold mod in INRLX. rewrite updo in INRLX; vauto. intros FALSE. assert (INMAP : (mapper ↑₁ E_t) b_t). - { clear - FALSE INE rsr_codom. basic_solver. } - apply rsr_codom in INMAP. + { rewrite <- FALSE. unfold set_collect. + exists x'; vauto. } + apply (rsr_codom SIMREL) in INMAP. clear - INMAP NOTIN. unfold set_minus in INMAP. desf. } rewrite !collect_rel_seq. @@ -1117,12 +1148,14 @@ Proof using INV INV'. { basic_solver. } assert (IN2 : codom_rel sb_t ⊆₁ E_t). { rewrite wf_sbE. basic_solver. } - rewrite IN1, IN2. destruct SIMREL. basic_solver. } + rewrite IN1, IN2. arewrite (E_t ∪₁ E_t ≡₁ E_t); [basic_solver|]. + eapply (rsr_inj SIMREL). } assert (IN1 : codom_rel ⦗F G_t ∩₁ Rel G_t ∩₁ E_t⦘ ⊆₁ E_t). { basic_solver 8. } assert (IN2 : dom_rel (sb_t ⨾ ⦗E_t ∩₁ (W_t ∩₁ Rlx G_t)⦘) ⊆₁ E_t). { rewrite wf_sbE. basic_solver 8. } - rewrite IN1, IN2. destruct SIMREL. basic_solver. } + rewrite IN1, IN2. arewrite (E_t ∪₁ E_t ≡₁ E_t); [basic_solver|]. + eapply (rsr_inj SIMREL). } assert (IND2 : mapper ↑ (rpo_imm G_t)⁺ ⨾ (rpo_imm G_s'' ⨾ ⦗E_s⦘) ⊆ mapper ↑ (rpo_imm G_t)⁺). { assert (TRIN : mapper ↑ (rpo_imm G_t)⁺ ⨾ mapper ↑ (rpo_imm G_t)⁺ @@ -1133,7 +1166,7 @@ Proof using INV INV'. destruct P2 as (x0'' & y' & (P2 & M3 & M4)). exists x', y'. splits; vauto. assert (EQ : x0'' = x0'). - { destruct SIMREL. apply rsr_inj; vauto. + { apply (rsr_inj SIMREL); vauto. { apply ct_begin in P2. destruct P2 as (x1 & P2 & P3). destruct INV. @@ -1152,13 +1185,13 @@ Proof using INV INV'. { split; [| basic_solver]. unfold sb at 1. ins. rewrite NEWSB. rewrite inter_union_l. rewrite seq_union_r. rewrite codom_union. - destruct SIMREL. rewrite rsr_sb. + rewrite (rsr_sb SIMREL). unfold swap_rel. arewrite (eq b_t ∩₁ E_t ≡₁ ∅). { split; basic_solver. } rels. unfold extra_a. desf. { destruct a. destruct BNOTIN; eauto. } - rels. rewrite wf_sbE. + rels. rewrite wf_sbE. destruct SIMREL. unfold extra_a in rsr_codom. desf. unfold WCore.sb_delta. assert (EMP1 : ⦗eq b_t⦘ ⨾ ((fun a : actid => is_init a) @@ -1188,13 +1221,13 @@ Proof using INV INV'. rewrite PROP1, PROP2; basic_solver. } { unfold sb at 1. ins. rewrite NEWSB. rewrite inter_union_l. - destruct SIMREL. rewrite rsr_sb. + rewrite (rsr_sb SIMREL). unfold swap_rel. arewrite (eq b_t ∩₁ E_t ≡₁ ∅). { split; basic_solver. } rels. unfold extra_a. desf. { destruct a. destruct BNOTIN; eauto. } - rels. rewrite wf_sbE. + rels. rewrite wf_sbE. destruct SIMREL. unfold extra_a in rsr_codom. desf. unfold WCore.sb_delta. arewrite (⦗(E_s ∪₁ eq b_t) \₁ eq b_t⦘ ⊆ ⦗E_s⦘). @@ -1233,7 +1266,7 @@ Proof using INV INV'. basic_solver 21. } { unfold G_s'' at 1; ins. unfold WCore.lab_is_r. desf. rewrite set_inter_empty_r. rels. - destruct SIMREL. rewrite rsr_rf. + rewrite (rsr_rf SIMREL). split; vauto. apply inclusion_union_l; vauto. unfold extra_a. desf. { exfalso. eapply BNOTIN. apply a. } @@ -1863,12 +1896,12 @@ Proof using. basic_solver. } { apply XmmCons.read_extent with (G_t := G_t') (sc_t := WCore.sc X_t') (a := b_t) (m := mapper'); eauto. - { destruct SIMREL'; vauto. } - { unfold G_s'; ins. destruct SIMREL. - rewrite rsr_acts. rewrite OLDEXA. + { apply SIMREL'; vauto. } + { unfold G_s'; ins. + rewrite (rsr_acts SIMREL). rewrite OLDEXA. rewrite EQACTS. rewrite set_collect_union; eauto. rewrite MAPER_E. rewrite MAPSUB; basic_solver 12. } - { destruct SIMREL'; vauto. } + { apply SIMREL'; vauto. } { rewrite EQACTS. rewrite set_collect_union, MAPER_E, MAPSUB, (rsr_codom SIMREL). rewrite OLDEXA; rels. intros FLS. @@ -1908,11 +1941,11 @@ Proof using. destruct COND' as [COND' | COND']. { assert (COND'' : E_s y) by vauto. apply IHP2_1 in COND1; vauto. apply IHP2_2 in COND''; vauto. } - subst y. exfalso. destruct SIMREL'. + subst y. exfalso. apply rpo_imm_in_sb in P1. assert (GEQ : G_s' = WCore.G X_s') by vauto. rewrite GEQ in P1. - apply rsr_sb in P1. + apply (rsr_sb SIMREL') in P1. destruct P1 as [[P1 | P1] | P1]. { assert (AEQQ : eq a_t ∩₁ E_t' ≡₁ ∅). { clear - ANOTIN'. basic_solver. } @@ -1925,7 +1958,7 @@ Proof using. destruct C1' as (a0 & C1' & C1''). destruct C1' as (EQ & C1'). rewrite MAPE in C2; subst a0. - apply rsr_inj in C2; vauto. + apply (rsr_inj SIMREL') in C2; vauto. { destruct C1'' as (x1 & PTH & (EQ & INE)). subst x1. subst a'. destruct INV'. assert (C1'' : E_t' b_t) by vauto. @@ -1935,7 +1968,7 @@ Proof using. basic_solver 21. } apply EQACTS. basic_solver. } rewrite MAPE in C2. - apply rsr_inj in C2; vauto. + apply (rsr_inj SIMREL') in C2; vauto. { destruct C1 as (C1 & C1'). subst a'. clear - C1 ANOTB. destruct C1; vauto. } @@ -1951,7 +1984,7 @@ Proof using. subst a4. subst a3. destruct CD as (EQ1 & EQB). subst a2. subst a1. rewrite MAPE in MAP. - apply rsr_inj in MAP; vauto. + apply (rsr_inj SIMREL') in MAP; vauto. subst a0. apply sb_irr in EQ'. done. } destruct P1 as (P1 & P1'). apply NEWEXA in P1. clear - P1 ANOTB; vauto. } @@ -1973,9 +2006,8 @@ Proof using. ⦗F G_s' ∩₁ Rel G_s'⦘ ⨾ ⦗E_s⦘ ⨾ sb G_s' ⨾ ⦗E_s ∪₁ eq a_t⦘ ⨾ ⦗W G_s' ∩₁ Rlx G_s'⦘). { rewrite seq_eqvC. rewrite <- seqA. rewrite seq_eqvC. basic_solver. } assert (SBSUB : ⦗E_s⦘ ⨾ sb G_s' ⨾ ⦗E_s ∪₁ eq a_t⦘ ⊆ ⦗E_s⦘ ⨾ mapper' ↑ sb_t' ⨾ ⦗E_s ∪₁ eq a_t⦘). - { destruct SIMREL'. - arewrite (G_s' = WCore.G X_s'). - rewrite rsr_sb. unfold swap_rel. + { arewrite (G_s' = WCore.G X_s'). + rewrite (rsr_sb SIMREL'). unfold swap_rel. rewrite !NEWEXA. arewrite (eq a_t ∩₁ E_t' ≡₁ ∅). { clear - ANOTIN'. basic_solver. } @@ -2009,10 +2041,10 @@ Proof using. rewrite <- !id_inter. rewrite <- !seqA. rewrite <- !id_inter. rewrite !seqA. rewrite <- !set_interA. - destruct SIMREL. rewrite rsr_acts. + rewrite (rsr_acts SIMREL). rewrite OLDEXA. rewrite !set_union_empty_r. assert (NOTEQ : forall x , E_t x -> mapper x = x). - { intros x XINE. apply rsr_mid. + { intros x XINE. apply (rsr_mid SIMREL). clear - XINE ENOTIN ANOTIN. unfold set_minus. split. { split; vauto. intros FALSE. apply ANOTIN. @@ -2035,23 +2067,23 @@ Proof using. split. { split. { unfold G_s' in COND1; ins. - unfold is_r. destruct rsr_lab with x'; vauto. + unfold is_r. destruct (rsr_lab SIMREL) with x'; vauto. unfold compose. unfold is_r in COND1. rewrite !updo in COND1; vauto. { arewrite (lab_t' x' = lab_t x'). rewrite <- MAP in COND1. - destruct rsr_lab with x'; vauto. } + destruct (rsr_lab SIMREL) with x'; vauto. } { apply NOTEQ in INE. congruence. } intros FALSE. rewrite FALSE in MAP. assert (INEN : E_t x'); vauto. apply NOTEQ in INE. congruence. } unfold G_s' in COND2; ins. - unfold is_rlx. unfold mod. destruct rsr_lab with x'; vauto. + unfold is_rlx. unfold mod. destruct (rsr_lab SIMREL) with x'; vauto. unfold compose. unfold is_rlx in COND2. unfold mod in COND2. rewrite !updo in COND2; vauto. { arewrite (lab_t' x' = lab_t x'). rewrite <- MAP in COND2. - destruct rsr_lab with x'; vauto. } + destruct (rsr_lab SIMREL) with x'; vauto. } { apply NOTEQ in INE. congruence. } intros FALSE. rewrite FALSE in MAP. assert (INEN : E_t x'); vauto. @@ -2071,11 +2103,10 @@ Proof using. split; vauto. split; vauto. split. { split; vauto. - destruct SIMREL'. - unfold is_f. destruct rsr_lab0 with x'; vauto. + unfold is_f. destruct (rsr_lab SIMREL') with x'; vauto. unfold compose. rewrite MAP; vauto. } - unfold is_acq. unfold mod. destruct SIMREL'. - destruct rsr_lab0 with x'; vauto. + unfold is_acq. unfold mod. + destruct (rsr_lab SIMREL') with x'; vauto. unfold compose. unfold is_acq in COND2. unfold mod in COND2. rewrite MAP; vauto. } arewrite (⦗Acq G_s' ∩₁ mapper ↑₁ E_t⦘ @@ -2093,13 +2124,13 @@ Proof using. splits; vauto. split; vauto. split. { unfold G_s' in COND1; ins. - unfold is_acq. destruct rsr_lab with x'; vauto. + unfold is_acq. destruct (rsr_lab SIMREL) with x'; vauto. unfold compose. unfold is_acq in COND1. unfold mod in COND1. unfold mod. rewrite !updo in COND1; vauto. { arewrite (lab_t' x' = lab_t x'). rewrite <- MAP in COND1. - destruct rsr_lab with x'; vauto. } + destruct (rsr_lab SIMREL) with x'; vauto. } { apply NOTEQ in INE. congruence. } intros FALSE. rewrite FALSE in MAP. assert (INEN : E_t x'); vauto. @@ -2120,8 +2151,7 @@ Proof using. exists x', x'. splits; vauto. split; vauto. split; vauto. - destruct SIMREL'. - unfold is_rel. unfold mod. destruct rsr_lab0 with x'; vauto. + unfold is_rel. unfold mod. destruct (rsr_lab SIMREL') with x'; vauto. unfold compose. unfold is_rel in COND. unfold mod in COND. rewrite MAP; vauto. } arewrite (⦗mapper ↑₁ E_t⦘ ⨾ mapper' ↑ sb_t' ⨾ mapper' ↑ ⦗E_t' ∩₁ Rel G_t'⦘ @@ -2145,23 +2175,23 @@ Proof using. split. { split. { unfold G_s' in COND1; ins. - unfold is_f. destruct rsr_lab with x'; vauto. + unfold is_f. destruct (rsr_lab SIMREL) with x'; vauto. unfold compose. unfold is_f in COND1. rewrite !updo in COND1; vauto. { arewrite (lab_t' x' = lab_t x'). rewrite <- MAP in COND1. - destruct rsr_lab with x'; vauto. } + destruct (rsr_lab SIMREL) with x'; vauto. } { apply NOTEQ in INE. congruence. } intros FALSE. rewrite FALSE in MAP. assert (INEN : E_t x'); vauto. apply NOTEQ in INE. congruence. } unfold G_s' in COND2; ins. - unfold is_rel. unfold mod. destruct rsr_lab with x'; vauto. + unfold is_rel. unfold mod. destruct (rsr_lab SIMREL) with x'; vauto. unfold compose. unfold is_rel in COND2. unfold mod in COND2. rewrite !updo in COND2; vauto. { arewrite (lab_t' x' = lab_t x'). rewrite <- MAP in COND2. - destruct rsr_lab with x'; vauto. } + destruct (rsr_lab SIMREL) with x'; vauto. } { apply NOTEQ in INE. congruence. } intros FALSE. rewrite FALSE in MAP. assert (INEN : E_t x'); vauto. @@ -2178,12 +2208,10 @@ Proof using. splits; vauto. split; vauto. split. { split; vauto. - destruct SIMREL'. - unfold is_w. destruct rsr_lab0 with x'; vauto. + unfold is_w. destruct (rsr_lab SIMREL') with x'; vauto. unfold compose. unfold is_w in COND1. rewrite MAP; vauto. } - destruct SIMREL'. - unfold is_rlx. unfold mod. destruct rsr_lab0 with x'; vauto. + unfold is_rlx. unfold mod. destruct (rsr_lab SIMREL') with x'; vauto. unfold compose. unfold is_rlx in COND2. unfold mod in COND2. rewrite MAP; vauto. } rewrite !collect_rel_union. @@ -2195,53 +2223,53 @@ Proof using. { clear - ANOTINS. rewrite wf_sbE. basic_solver. } assert (IN2 : dom_rel ⦗E_t' ∩₁ F G_t' ∩₁ Acq G_t'⦘ ⊆₁ E_t'). { clear - ANOTINS. basic_solver. } - rewrite IN1, IN2. destruct SIMREL'. - clear - rsr_inj0; basic_solver 8. } + rewrite IN1, IN2. arewrite (E_t' ∪₁ E_t' ≡₁ E_t'); [basic_solver|]. + eapply (rsr_inj SIMREL'). } assert (IN1 : codom_rel ⦗R_t' ∩₁ Rlx G_t' ∩₁ E_t'⦘ ⊆₁ E_t'). { clear - ANOTINS. basic_solver. } assert (IN2 : dom_rel (sb_t' ⨾ ⦗E_t' ∩₁ F G_t' ∩₁ Acq G_t'⦘) ⊆₁ E_t'). { clear - ANOTINS. rewrite wf_sbE. basic_solver. } - rewrite IN1, IN2. destruct SIMREL'. - clear - rsr_inj0; basic_solver 8. } + rewrite IN1, IN2. arewrite (E_t' ∪₁ E_t' ≡₁ E_t'); [basic_solver|]. + eapply (rsr_inj SIMREL'). } rewrite !collect_rel_seq; vauto. { assert (IN1 : codom_rel sb_t' ⊆₁ E_t'). { clear - ANOTINS. rewrite wf_sbE. basic_solver. } assert (IN2 : dom_rel ⦗E_t'⦘ ⊆₁ E_t'). { clear - ANOTINS. basic_solver. } - rewrite IN1, IN2. destruct SIMREL'. - clear - rsr_inj0; basic_solver 8. } + rewrite IN1, IN2. arewrite (E_t' ∪₁ E_t' ≡₁ E_t'); [basic_solver|]. + eapply (rsr_inj SIMREL'). } assert (IN1 : codom_rel ⦗Acq G_t' ∩₁ E_t'⦘ ⊆₁ E_t'). { clear - ANOTINS. basic_solver. } assert (IN2 : dom_rel (sb_t' ⨾ ⦗E_t'⦘) ⊆₁ E_t'). { clear - ANOTINS. rewrite wf_sbE. basic_solver. } - rewrite IN1, IN2. destruct SIMREL'. - clear - rsr_inj0; basic_solver 8. } + rewrite IN1, IN2. arewrite (E_t' ∪₁ E_t' ≡₁ E_t'); [basic_solver|]. + eapply (rsr_inj SIMREL'). } rewrite !collect_rel_seq; vauto. { assert (IN1 : codom_rel sb_t' ⊆₁ E_t'). { clear - ANOTINS. rewrite wf_sbE. basic_solver. } assert (IN2 : dom_rel ⦗E_t' ∩₁ Rel G_t'⦘ ⊆₁ E_t'). { clear - ANOTINS. basic_solver. } - rewrite IN1, IN2. destruct SIMREL'. - clear - rsr_inj0; basic_solver 8. } + rewrite IN1, IN2. arewrite (E_t' ∪₁ E_t' ≡₁ E_t'); [basic_solver|]. + eapply (rsr_inj SIMREL'). } assert (IN1 : codom_rel ⦗E_t'⦘ ⊆₁ E_t'). { clear - ANOTINS. basic_solver. } assert (IN2 : dom_rel (sb_t' ⨾ ⦗E_t' ∩₁ Rel G_t'⦘) ⊆₁ E_t'). { clear - ANOTINS. rewrite wf_sbE. basic_solver. } - rewrite IN1, IN2. destruct SIMREL'. - clear - rsr_inj0; basic_solver 8. } + rewrite IN1, IN2. arewrite (E_t' ∪₁ E_t' ≡₁ E_t'); [basic_solver|]. + eapply (rsr_inj SIMREL'). } rewrite !collect_rel_seq; vauto. { assert (IN1 : codom_rel sb_t' ⊆₁ E_t'). { clear - ANOTINS. rewrite wf_sbE. basic_solver. } assert (IN2 : dom_rel ⦗E_t' ∩₁ W_t' ∩₁ Rlx G_t'⦘ ⊆₁ E_t'). { clear - ANOTINS. basic_solver. } - rewrite IN1, IN2. destruct SIMREL'. - clear - rsr_inj0; basic_solver 8. } + rewrite IN1, IN2. arewrite (E_t' ∪₁ E_t' ≡₁ E_t'); [basic_solver|]. + eapply (rsr_inj SIMREL'). } assert (IN1 : codom_rel ⦗F G_t' ∩₁ Rel G_t' ∩₁ E_t'⦘ ⊆₁ E_t'). { clear - ANOTINS. basic_solver. } assert (IN2 : dom_rel (sb_t' ⨾ ⦗E_t' ∩₁ W_t' ∩₁ Rlx G_t'⦘) ⊆₁ E_t'). { clear - ANOTINS. rewrite wf_sbE. basic_solver. } - rewrite IN1, IN2. destruct SIMREL'. - clear - rsr_inj0; basic_solver 8. } + rewrite IN1, IN2. arewrite (E_t' ∪₁ E_t' ≡₁ E_t'); [basic_solver|]. + eapply (rsr_inj SIMREL'). } assert (IND2 : mapper' ↑ (rpo_imm G_t')⁺ ⨾ ⦗E_s⦘ ⨾ (rpo_imm G_s' ⨾ ⦗E_s ∪₁ eq a_t⦘) ⊆ mapper' ↑ (rpo_imm G_t')⁺). { assert (TRIN : mapper' ↑ (rpo_imm G_t')⁺ ⨾ mapper' ↑ (rpo_imm G_t')⁺ @@ -2252,7 +2280,7 @@ Proof using. destruct P2 as (x0'' & y' & (P2 & M3 & M4)). exists x', y'. splits; vauto. assert (EQ : x0'' = x0'). - { destruct SIMREL'. apply rsr_inj; vauto. + { apply (rsr_inj SIMREL'); vauto. { apply ct_begin in P2. destruct P2 as (x1 & P2 & P3). apply wf_rpo_immE in P2; vauto. @@ -2309,9 +2337,8 @@ Proof using. rewrite !upds in LOC. apply NEQLOQ'. unfold WCore.lab_loc. congruence. } - { destruct SIMREL'. - arewrite (G_s' = WCore.G X_s'). - rewrite rsr_sb. rewrite !NEWEXA. + { arewrite (G_s' = WCore.G X_s'). + rewrite (rsr_sb SIMREL'). rewrite !NEWEXA. arewrite (eq a_t ∩₁ E_t' ≡₁ ∅). { clear - ANOTIN'. basic_solver. } arewrite (eq b_t ∩₁ E_t' ≡₁ eq b_t). @@ -2334,11 +2361,11 @@ Proof using. rewrite ACTEQ in SL. unfold same_loc. unfold loc. arewrite (lab_t' x' = lab G_s' x). - { destruct rsr_lab with x'. + { destruct (rsr_lab SIMREL') with x'. { destruct SB as (x0 & (C1 & EQ) & C2); vauto. } unfold compose. clear - M1; basic_solver. } arewrite (lab_t' z' = lab G_s' z). - { destruct rsr_lab with z'. + { destruct (rsr_lab SIMREL') with z'. { destruct SB as (x0 & C1 & (x2 & C2 & (IN & EQ))). clear - IN EQ. basic_solver. } unfold compose. clear - M2; basic_solver. } @@ -2355,9 +2382,8 @@ Proof using. exfalso. apply NEQLOQ'. unfold WCore.lab_loc. congruence. } - { destruct SIMREL'. - arewrite (G_s' = WCore.G X_s'). - rewrite rsr_rf. apply union_more; vauto. + { arewrite (G_s' = WCore.G X_s'). + rewrite (rsr_rf SIMREL'). apply union_more; vauto. apply seq_more; vauto. rewrite NEWEXA. split; [basic_solver|]. split. @@ -2365,9 +2391,8 @@ Proof using. split; vauto. { destruct H; vauto. } destruct H; subst x y; vauto. } - { destruct SIMREL'. - arewrite (G_s' = WCore.G X_s'). - rewrite rsr_co. unfold add_max. + { arewrite (G_s' = WCore.G X_s'). + rewrite (rsr_co SIMREL'). unfold add_max. rewrite NEWEXA. arewrite ((extra_co_D (acts_set (WCore.G X_s')) (lab (WCore.G X_s')) (loc (lab (WCore.G X_s')) b_t) \₁ eq b_t ∩₁ W (WCore.G X_s')) @@ -2380,12 +2405,12 @@ Proof using. (a_t := a_t) (b_t := b_t) (mapper := mapper'); vauto. } apply XmmCons.write_extent with (G_t := G_t') (sc_t := WCore.sc X_t') (a := b_t) (m := mapper'); eauto. - { destruct SIMREL'; vauto. } - { unfold G_s'; ins. destruct SIMREL. - rewrite rsr_acts. rewrite OLDEXA. + { apply SIMREL'; vauto. } + { unfold G_s'; ins. + rewrite (rsr_acts SIMREL). rewrite OLDEXA. rewrite EQACTS. rewrite set_collect_union; eauto. rewrite MAPER_E. rewrite MAPSUB; basic_solver 12. } - { destruct SIMREL'; vauto. } + { apply SIMREL'; vauto. } { rewrite EQACTS. rewrite set_collect_union, MAPER_E, MAPSUB, (rsr_codom SIMREL). rewrite OLDEXA; rels. intros FLS. @@ -2425,11 +2450,11 @@ Proof using. destruct COND' as [COND' | COND']. { assert (COND'' : E_s y) by vauto. apply IHP2_1 in COND1; vauto. apply IHP2_2 in COND''; vauto. } - subst y. exfalso. destruct SIMREL'. + subst y. exfalso. apply rpo_imm_in_sb in P1. assert (GEQ : G_s' = WCore.G X_s') by vauto. rewrite GEQ in P1. - apply rsr_sb in P1. + apply (rsr_sb SIMREL') in P1. destruct P1 as [[P1 | P1] | P1]. { assert (AEQQ : eq a_t ∩₁ E_t' ≡₁ ∅). { clear - ANOTIN'. basic_solver. } @@ -2442,7 +2467,7 @@ Proof using. destruct C1' as (a0 & C1' & C1''). destruct C1' as (EQ & C1'). rewrite MAPE in C2; subst a0. - apply rsr_inj in C2; vauto. + apply (rsr_inj SIMREL') in C2; vauto. { destruct C1'' as (x1 & PTH & (EQ & INE)). subst x1. subst a'. destruct INV'. assert (C1'' : E_t' b_t) by vauto. @@ -2452,7 +2477,7 @@ Proof using. basic_solver 21. } apply EQACTS. basic_solver. } rewrite MAPE in C2. - apply rsr_inj in C2; vauto. + apply (rsr_inj SIMREL') in C2; vauto. { destruct C1 as (C1 & C1'). subst a'. clear - C1 ANOTB. destruct C1; vauto. } @@ -2468,7 +2493,7 @@ Proof using. subst a4. subst a3. destruct CD as (EQ1 & EQB). subst a2. subst a1. rewrite MAPE in MAP. - apply rsr_inj in MAP; vauto. + apply (rsr_inj SIMREL') in MAP; vauto. subst a0. apply sb_irr in EQ'. done. } destruct P1 as (P1 & P1'). apply NEWEXA in P1. clear - P1 ANOTB; vauto. } @@ -2490,9 +2515,8 @@ Proof using. ⦗F G_s' ∩₁ Rel G_s'⦘ ⨾ ⦗E_s⦘ ⨾ sb G_s' ⨾ ⦗E_s ∪₁ eq a_t⦘ ⨾ ⦗W G_s' ∩₁ Rlx G_s'⦘). { rewrite seq_eqvC. rewrite <- seqA. rewrite seq_eqvC. basic_solver. } assert (SBSUB : ⦗E_s⦘ ⨾ sb G_s' ⨾ ⦗E_s ∪₁ eq a_t⦘ ⊆ ⦗E_s⦘ ⨾ mapper' ↑ sb_t' ⨾ ⦗E_s ∪₁ eq a_t⦘). - { destruct SIMREL'. - arewrite (G_s' = WCore.G X_s'). - rewrite rsr_sb. unfold swap_rel. + { arewrite (G_s' = WCore.G X_s'). + rewrite (rsr_sb SIMREL'). unfold swap_rel. rewrite !NEWEXA. arewrite (eq a_t ∩₁ E_t' ≡₁ ∅). { clear - ANOTIN'. basic_solver. } @@ -2526,10 +2550,10 @@ Proof using. rewrite <- !id_inter. rewrite <- !seqA. rewrite <- !id_inter. rewrite !seqA. rewrite <- !set_interA. - destruct SIMREL. rewrite rsr_acts. + rewrite (rsr_acts SIMREL). rewrite OLDEXA. rewrite !set_union_empty_r. assert (NOTEQ : forall x , E_t x -> mapper x = x). - { intros x XINE. apply rsr_mid. + { intros x XINE. apply (rsr_mid SIMREL). clear - XINE ENOTIN ANOTIN. unfold set_minus. split. { split; vauto. intros FALSE. apply ANOTIN. @@ -2552,23 +2576,23 @@ Proof using. split. { split. { unfold G_s' in COND1; ins. - unfold is_r. destruct rsr_lab with x'; vauto. + unfold is_r. destruct (rsr_lab SIMREL) with x'; vauto. unfold compose. unfold is_r in COND1. rewrite !updo in COND1; vauto. { arewrite (lab_t' x' = lab_t x'). rewrite <- MAP in COND1. - destruct rsr_lab with x'; vauto. } + destruct (rsr_lab SIMREL) with x'; vauto. } { apply NOTEQ in INE. congruence. } intros FALSE. rewrite FALSE in MAP. assert (INEN : E_t x'); vauto. apply NOTEQ in INE. congruence. } unfold G_s' in COND2; ins. - unfold is_rlx. unfold mod. destruct rsr_lab with x'; vauto. + unfold is_rlx. unfold mod. destruct (rsr_lab SIMREL) with x'; vauto. unfold compose. unfold is_rlx in COND2. unfold mod in COND2. rewrite !updo in COND2; vauto. { arewrite (lab_t' x' = lab_t x'). rewrite <- MAP in COND2. - destruct rsr_lab with x'; vauto. } + destruct (rsr_lab SIMREL) with x'; vauto. } { apply NOTEQ in INE. congruence. } intros FALSE. rewrite FALSE in MAP. assert (INEN : E_t x'); vauto. @@ -2588,11 +2612,10 @@ Proof using. split; vauto. split; vauto. split. { split; vauto. - destruct SIMREL'. - unfold is_f. destruct rsr_lab0 with x'; vauto. + unfold is_f. destruct (rsr_lab SIMREL') with x'; vauto. unfold compose. rewrite MAP; vauto. } - unfold is_acq. unfold mod. destruct SIMREL'. - destruct rsr_lab0 with x'; vauto. + unfold is_acq. unfold mod. + destruct (rsr_lab SIMREL') with x'; vauto. unfold compose. unfold is_acq in COND2. unfold mod in COND2. rewrite MAP; vauto. } arewrite (⦗Acq G_s' ∩₁ mapper ↑₁ E_t⦘ @@ -2610,13 +2633,13 @@ Proof using. splits; vauto. split; vauto. split. { unfold G_s' in COND1; ins. - unfold is_acq. destruct rsr_lab with x'; vauto. + unfold is_acq. destruct (rsr_lab SIMREL) with x'; vauto. unfold compose. unfold is_acq in COND1. unfold mod in COND1. unfold mod. rewrite !updo in COND1; vauto. { arewrite (lab_t' x' = lab_t x'). rewrite <- MAP in COND1. - destruct rsr_lab with x'; vauto. } + destruct (rsr_lab SIMREL) with x'; vauto. } { apply NOTEQ in INE. congruence. } intros FALSE. rewrite FALSE in MAP. assert (INEN : E_t x'); vauto. @@ -2637,8 +2660,7 @@ Proof using. exists x', x'. splits; vauto. split; vauto. split; vauto. - destruct SIMREL'. - unfold is_rel. unfold mod. destruct rsr_lab0 with x'; vauto. + unfold is_rel. unfold mod. destruct (rsr_lab SIMREL') with x'; vauto. unfold compose. unfold is_rel in COND. unfold mod in COND. rewrite MAP; vauto. } arewrite (⦗mapper ↑₁ E_t⦘ ⨾ mapper' ↑ sb_t' ⨾ mapper' ↑ ⦗E_t' ∩₁ Rel G_t'⦘ @@ -2662,23 +2684,23 @@ Proof using. split. { split. { unfold G_s' in COND1; ins. - unfold is_f. destruct rsr_lab with x'; vauto. + unfold is_f. destruct (rsr_lab SIMREL) with x'; vauto. unfold compose. unfold is_f in COND1. rewrite !updo in COND1; vauto. { arewrite (lab_t' x' = lab_t x'). rewrite <- MAP in COND1. - destruct rsr_lab with x'; vauto. } + destruct (rsr_lab SIMREL) with x'; vauto. } { apply NOTEQ in INE. congruence. } intros FALSE. rewrite FALSE in MAP. assert (INEN : E_t x'); vauto. apply NOTEQ in INE. congruence. } unfold G_s' in COND2; ins. - unfold is_rel. unfold mod. destruct rsr_lab with x'; vauto. + unfold is_rel. unfold mod. destruct (rsr_lab SIMREL) with x'; vauto. unfold compose. unfold is_rel in COND2. unfold mod in COND2. rewrite !updo in COND2; vauto. { arewrite (lab_t' x' = lab_t x'). rewrite <- MAP in COND2. - destruct rsr_lab with x'; vauto. } + destruct (rsr_lab SIMREL) with x'; vauto. } { apply NOTEQ in INE. congruence. } intros FALSE. rewrite FALSE in MAP. assert (INEN : E_t x'); vauto. @@ -2695,12 +2717,10 @@ Proof using. splits; vauto. split; vauto. split. { split; vauto. - destruct SIMREL'. - unfold is_w. destruct rsr_lab0 with x'; vauto. + unfold is_w. destruct (rsr_lab SIMREL') with x'; vauto. unfold compose. unfold is_w in COND1. rewrite MAP; vauto. } - destruct SIMREL'. - unfold is_rlx. unfold mod. destruct rsr_lab0 with x'; vauto. + unfold is_rlx. unfold mod. destruct (rsr_lab SIMREL') with x'; vauto. unfold compose. unfold is_rlx in COND2. unfold mod in COND2. rewrite MAP; vauto. } rewrite !collect_rel_union. @@ -2712,53 +2732,53 @@ Proof using. { clear - ANOTINS. rewrite wf_sbE. basic_solver. } assert (IN2 : dom_rel ⦗E_t' ∩₁ F G_t' ∩₁ Acq G_t'⦘ ⊆₁ E_t'). { clear - ANOTINS. basic_solver. } - rewrite IN1, IN2. destruct SIMREL'. - clear - rsr_inj0; basic_solver 8. } + rewrite IN1, IN2. arewrite (E_t' ∪₁ E_t' ≡₁ E_t'); [basic_solver|]. + eapply (rsr_inj SIMREL'). } assert (IN1 : codom_rel ⦗R_t' ∩₁ Rlx G_t' ∩₁ E_t'⦘ ⊆₁ E_t'). { clear - ANOTINS. basic_solver. } assert (IN2 : dom_rel (sb_t' ⨾ ⦗E_t' ∩₁ F G_t' ∩₁ Acq G_t'⦘) ⊆₁ E_t'). { clear - ANOTINS. rewrite wf_sbE. basic_solver. } - rewrite IN1, IN2. destruct SIMREL'. - clear - rsr_inj0; basic_solver 8. } + rewrite IN1, IN2. arewrite (E_t' ∪₁ E_t' ≡₁ E_t'); [basic_solver|]. + eapply (rsr_inj SIMREL'). } rewrite !collect_rel_seq; vauto. { assert (IN1 : codom_rel sb_t' ⊆₁ E_t'). { clear - ANOTINS. rewrite wf_sbE. basic_solver. } assert (IN2 : dom_rel ⦗E_t'⦘ ⊆₁ E_t'). { clear - ANOTINS. basic_solver. } - rewrite IN1, IN2. destruct SIMREL'. - clear - rsr_inj0; basic_solver 8. } + rewrite IN1, IN2. arewrite (E_t' ∪₁ E_t' ≡₁ E_t'); [basic_solver|]. + eapply (rsr_inj SIMREL'). } assert (IN1 : codom_rel ⦗Acq G_t' ∩₁ E_t'⦘ ⊆₁ E_t'). { clear - ANOTINS. basic_solver. } assert (IN2 : dom_rel (sb_t' ⨾ ⦗E_t'⦘) ⊆₁ E_t'). { clear - ANOTINS. rewrite wf_sbE. basic_solver. } - rewrite IN1, IN2. destruct SIMREL'. - clear - rsr_inj0; basic_solver 8. } + rewrite IN1, IN2. arewrite (E_t' ∪₁ E_t' ≡₁ E_t'); [basic_solver|]. + eapply (rsr_inj SIMREL'). } rewrite !collect_rel_seq; vauto. { assert (IN1 : codom_rel sb_t' ⊆₁ E_t'). { clear - ANOTINS. rewrite wf_sbE. basic_solver. } assert (IN2 : dom_rel ⦗E_t' ∩₁ Rel G_t'⦘ ⊆₁ E_t'). { clear - ANOTINS. basic_solver. } - rewrite IN1, IN2. destruct SIMREL'. - clear - rsr_inj0; basic_solver 8. } + rewrite IN1, IN2. arewrite (E_t' ∪₁ E_t' ≡₁ E_t'); [basic_solver|]. + eapply (rsr_inj SIMREL'). } assert (IN1 : codom_rel ⦗E_t'⦘ ⊆₁ E_t'). { clear - ANOTINS. basic_solver. } assert (IN2 : dom_rel (sb_t' ⨾ ⦗E_t' ∩₁ Rel G_t'⦘) ⊆₁ E_t'). { clear - ANOTINS. rewrite wf_sbE. basic_solver. } - rewrite IN1, IN2. destruct SIMREL'. - clear - rsr_inj0; basic_solver 8. } + rewrite IN1, IN2. arewrite (E_t' ∪₁ E_t' ≡₁ E_t'); [basic_solver|]. + eapply (rsr_inj SIMREL'). } rewrite !collect_rel_seq; vauto. { assert (IN1 : codom_rel sb_t' ⊆₁ E_t'). { clear - ANOTINS. rewrite wf_sbE. basic_solver. } assert (IN2 : dom_rel ⦗E_t' ∩₁ W_t' ∩₁ Rlx G_t'⦘ ⊆₁ E_t'). { clear - ANOTINS. basic_solver. } - rewrite IN1, IN2. destruct SIMREL'. - clear - rsr_inj0; basic_solver 8. } + rewrite IN1, IN2. arewrite (E_t' ∪₁ E_t' ≡₁ E_t'); [basic_solver|]. + eapply (rsr_inj SIMREL'). } assert (IN1 : codom_rel ⦗F G_t' ∩₁ Rel G_t' ∩₁ E_t'⦘ ⊆₁ E_t'). { clear - ANOTINS. basic_solver. } assert (IN2 : dom_rel (sb_t' ⨾ ⦗E_t' ∩₁ W_t' ∩₁ Rlx G_t'⦘) ⊆₁ E_t'). { clear - ANOTINS. rewrite wf_sbE. basic_solver. } - rewrite IN1, IN2. destruct SIMREL'. - clear - rsr_inj0; basic_solver 8. } + rewrite IN1, IN2. arewrite (E_t' ∪₁ E_t' ≡₁ E_t'); [basic_solver|]. + eapply (rsr_inj SIMREL'). } assert (IND2 : mapper' ↑ (rpo_imm G_t')⁺ ⨾ ⦗E_s⦘ ⨾ (rpo_imm G_s' ⨾ ⦗E_s ∪₁ eq a_t⦘) ⊆ mapper' ↑ (rpo_imm G_t')⁺). { assert (TRIN : mapper' ↑ (rpo_imm G_t')⁺ ⨾ mapper' ↑ (rpo_imm G_t')⁺ @@ -2769,7 +2789,7 @@ Proof using. destruct P2 as (x0'' & y' & (P2 & M3 & M4)). exists x', y'. splits; vauto. assert (EQ : x0'' = x0'). - { destruct SIMREL'. apply rsr_inj; vauto. + { apply (rsr_inj SIMREL'); vauto. { apply ct_begin in P2. destruct P2 as (x1 & P2 & P3). apply wf_rpo_immE in P2; vauto. @@ -2826,9 +2846,8 @@ Proof using. rewrite !upds in LOC. apply NEQLOQ'. unfold WCore.lab_loc. congruence. } - { destruct SIMREL'. - arewrite (G_s' = WCore.G X_s'). - rewrite rsr_sb. rewrite !NEWEXA. + { arewrite (G_s' = WCore.G X_s'). + rewrite (rsr_sb SIMREL'). rewrite !NEWEXA. arewrite (eq a_t ∩₁ E_t' ≡₁ ∅). { clear - ANOTIN'. basic_solver. } arewrite (eq b_t ∩₁ E_t' ≡₁ eq b_t). @@ -2851,11 +2870,11 @@ Proof using. rewrite ACTEQ in SL. unfold same_loc. unfold loc. arewrite (lab_t' x' = lab G_s' x). - { destruct rsr_lab with x'. + { destruct (rsr_lab SIMREL') with x'. { destruct SB as (x0 & (C1 & EQ) & C2); vauto. } unfold compose. clear - M1; basic_solver. } arewrite (lab_t' z' = lab G_s' z). - { destruct rsr_lab with z'. + { destruct (rsr_lab SIMREL') with z'. { destruct SB as (x0 & C1 & (x2 & C2 & (IN & EQ))). clear - IN EQ. basic_solver. } unfold compose. clear - M2; basic_solver. } @@ -2872,17 +2891,15 @@ Proof using. exfalso. apply NEQLOQ'. unfold WCore.lab_loc. congruence. } - { destruct SIMREL'. - arewrite (G_s' = WCore.G X_s'). - rewrite rsr_rf. rewrite NEWEXA. + { arewrite (G_s' = WCore.G X_s'). + rewrite (rsr_rf SIMREL'). rewrite NEWEXA. arewrite (eq b_t ∩₁ R (WCore.G X_s') ≡₁ ∅). { split; [| basic_solver]. intros x (EQ & ISR); subst x. unfold is_w, is_r in *; basic_solver. } basic_solver 8. } - { destruct SIMREL'. - arewrite (G_s' = WCore.G X_s'). - rewrite rsr_co. unfold add_max. + { arewrite (G_s' = WCore.G X_s'). + rewrite (rsr_co SIMREL'). unfold add_max. rewrite NEWEXA. apply union_more; vauto. arewrite (eq b_t ∩₁ W (WCore.G X_s') ≡₁ eq b_t). { split; [basic_solver |].