Commit 08b69a69 authored by Ralf Jung's avatar Ralf Jung

add tactic aliases: trans -> transitivity; etrans -> etransitivity

parent 709da735
...@@ -40,8 +40,8 @@ Proof. ...@@ -40,8 +40,8 @@ Proof.
+ by split. + by split.
+ by intros x y Hxy; split; intros; symmetry; apply Hxy; auto; apply Hxy. + by intros x y Hxy; split; intros; symmetry; apply Hxy; auto; apply Hxy.
+ intros x y z Hxy Hyz; split; intros n'; intros. + intros x y z Hxy Hyz; split; intros n'; intros.
* transitivity (agree_is_valid y n'). by apply Hxy. by apply Hyz. * trans (agree_is_valid y n'). by apply Hxy. by apply Hyz.
* transitivity (y n'). by apply Hxy. by apply Hyz, Hxy. * trans (y n'). by apply Hxy. by apply Hyz, Hxy.
- intros n x y Hxy; split; intros; apply Hxy; auto. - intros n x y Hxy; split; intros; apply Hxy; auto.
- intros n c; apply and_wlog_r; intros; - intros n c; apply and_wlog_r; intros;
symmetry; apply (chain_cauchy c); naive_solver. symmetry; apply (chain_cauchy c); naive_solver.
...@@ -74,8 +74,8 @@ Proof. ...@@ -74,8 +74,8 @@ Proof.
intros n x y1 y2 [Hy' Hy]; split; [|done]. intros n x y1 y2 [Hy' Hy]; split; [|done].
split; intros (?&?&Hxy); repeat (intro || split); split; intros (?&?&Hxy); repeat (intro || split);
try apply Hy'; eauto using agree_valid_le. try apply Hy'; eauto using agree_valid_le.
- etransitivity; [apply Hxy|apply Hy]; eauto using agree_valid_le. - etrans; [apply Hxy|apply Hy]; eauto using agree_valid_le.
- etransitivity; [apply Hxy|symmetry; apply Hy, Hy']; - etrans; [apply Hxy|symmetry; apply Hy, Hy'];
eauto using agree_valid_le. eauto using agree_valid_le.
Qed. Qed.
Instance: Proper (dist n ==> dist n ==> dist n) (@op (agree A) _). Instance: Proper (dist n ==> dist n ==> dist n) (@op (agree A) _).
......
...@@ -44,7 +44,7 @@ Proof. ...@@ -44,7 +44,7 @@ Proof.
- intros n; split. - intros n; split.
+ by intros ?; split. + by intros ?; split.
+ by intros ?? [??]; split; symmetry. + by intros ?? [??]; split; symmetry.
+ intros ??? [??] [??]; split; etransitivity; eauto. + intros ??? [??] [??]; split; etrans; eauto.
- by intros ? [??] [??] [??]; split; apply dist_S. - by intros ? [??] [??] [??]; split; apply dist_S.
- intros n c; split. apply (conv_compl n (chain_map authoritative c)). - intros n c; split. apply (conv_compl n (chain_map authoritative c)).
apply (conv_compl n (chain_map own c)). apply (conv_compl n (chain_map own c)).
......
...@@ -250,7 +250,7 @@ Qed. ...@@ -250,7 +250,7 @@ Qed.
Global Instance cmra_included_preorder: PreOrder (@included A _ _). Global Instance cmra_included_preorder: PreOrder (@included A _ _).
Proof. Proof.
split; red; intros until 0; rewrite !cmra_included_includedN; first done. split; red; intros until 0; rewrite !cmra_included_includedN; first done.
intros; etransitivity; eauto. intros; etrans; eauto.
Qed. Qed.
Lemma cmra_validN_includedN n x y : {n} y x {n} y {n} x. Lemma cmra_validN_includedN n x y : {n} y x {n} y {n} x.
Proof. intros Hyv [z ?]; cofe_subst y; eauto using cmra_validN_op_l. Qed. Proof. intros Hyv [z ?]; cofe_subst y; eauto using cmra_validN_op_l. Qed.
...@@ -391,7 +391,7 @@ Section identity_updates. ...@@ -391,7 +391,7 @@ Section identity_updates.
Lemma cmra_update_empty x : x ~~> . Lemma cmra_update_empty x : x ~~> .
Proof. intros n z; rewrite left_id; apply cmra_validN_op_r. Qed. Proof. intros n z; rewrite left_id; apply cmra_validN_op_r. Qed.
Lemma cmra_update_empty_alt y : ~~> y x, x ~~> y. Lemma cmra_update_empty_alt y : ~~> y x, x ~~> y.
Proof. split; [intros; transitivity |]; auto using cmra_update_empty. Qed. Proof. split; [intros; trans |]; auto using cmra_update_empty. Qed.
End identity_updates. End identity_updates.
End cmra. End cmra.
......
...@@ -23,7 +23,7 @@ Proof. ...@@ -23,7 +23,7 @@ Proof.
induction 1 as [|x xs1 xs2 ? IH|x y xs|xs1 xs2 xs3]; simpl; auto. induction 1 as [|x xs1 xs2 ? IH|x y xs|xs1 xs2 xs3]; simpl; auto.
- by rewrite IH. - by rewrite IH.
- by rewrite !assoc (comm _ x). - by rewrite !assoc (comm _ x).
- by transitivity (big_op xs2). - by trans (big_op xs2).
Qed. Qed.
Global Instance big_op_proper : Proper (() ==> ()) big_op. Global Instance big_op_proper : Proper (() ==> ()) big_op.
Proof. by induction 1; simpl; repeat apply (_ : Proper (_ ==> _ ==> _) op). Qed. Proof. by induction 1; simpl; repeat apply (_ : Proper (_ ==> _ ==> _) op). Qed.
......
...@@ -99,13 +99,13 @@ Section cofe. ...@@ -99,13 +99,13 @@ Section cofe.
split. split.
- by intros x; rewrite equiv_dist. - by intros x; rewrite equiv_dist.
- by intros x y; rewrite !equiv_dist. - by intros x y; rewrite !equiv_dist.
- by intros x y z; rewrite !equiv_dist; intros; transitivity y. - by intros x y z; rewrite !equiv_dist; intros; trans y.
Qed. Qed.
Global Instance dist_ne n : Proper (dist n ==> dist n ==> iff) (@dist A _ n). Global Instance dist_ne n : Proper (dist n ==> dist n ==> iff) (@dist A _ n).
Proof. Proof.
intros x1 x2 ? y1 y2 ?; split; intros. intros x1 x2 ? y1 y2 ?; split; intros.
- by transitivity x1; [|transitivity y1]. - by trans x1; [|trans y1].
- by transitivity x2; [|transitivity y2]. - by trans x2; [|trans y2].
Qed. Qed.
Global Instance dist_proper n : Proper (() ==> () ==> iff) (@dist A _ n). Global Instance dist_proper n : Proper (() ==> () ==> iff) (@dist A _ n).
Proof. Proof.
...@@ -217,7 +217,7 @@ Section cofe_mor. ...@@ -217,7 +217,7 @@ Section cofe_mor.
- intros n; split. - intros n; split.
+ by intros f x. + by intros f x.
+ by intros f g ? x. + by intros f g ? x.
+ by intros f g h ?? x; transitivity (g x). + by intros f g h ?? x; trans (g x).
- by intros n f g ? x; apply dist_S. - by intros n f g ? x; apply dist_S.
- intros n c x; simpl. - intros n c x; simpl.
by rewrite (conv_compl n (fun_chain c x)) /=. by rewrite (conv_compl n (fun_chain c x)) /=.
...@@ -352,7 +352,7 @@ Section later. ...@@ -352,7 +352,7 @@ Section later.
- intros [|n]; [by split|split]; unfold dist, later_dist. - intros [|n]; [by split|split]; unfold dist, later_dist.
+ by intros [x]. + by intros [x].
+ by intros [x] [y]. + by intros [x] [y].
+ by intros [x] [y] [z] ??; transitivity y. + by intros [x] [y] [z] ??; trans y.
- intros [|n] [x] [y] ?; [done|]; unfold dist, later_dist; by apply dist_S. - intros [|n] [x] [y] ?; [done|]; unfold dist, later_dist; by apply dist_S.
- intros [|n] c; [done|by apply (conv_compl n (later_chain c))]. - intros [|n] c; [done|by apply (conv_compl n (later_chain c))].
Qed. Qed.
......
...@@ -71,7 +71,7 @@ Proof. ...@@ -71,7 +71,7 @@ Proof.
- intros k; split. - intros k; split.
+ by intros X n. + by intros X n.
+ by intros X Y ? n. + by intros X Y ? n.
+ by intros X Y Z ?? n; transitivity (Y n). + by intros X Y Z ?? n; trans (Y n).
- intros k X Y HXY n; apply dist_S. - intros k X Y HXY n; apply dist_S.
by rewrite -(g_tower X) (HXY (S n)) g_tower. by rewrite -(g_tower X) (HXY (S n)) g_tower.
- intros n c k; rewrite /= (conv_compl n (tower_chain c k)). - intros n c k; rewrite /= (conv_compl n (tower_chain c k)).
...@@ -209,7 +209,7 @@ Proof. ...@@ -209,7 +209,7 @@ Proof.
- move=> X /=. - move=> X /=.
rewrite equiv_dist; intros n k; unfold unfold, fold; simpl. rewrite equiv_dist; intros n k; unfold unfold, fold; simpl.
rewrite -g_tower -(gg_tower _ n); apply (_ : Proper (_ ==> _) (g _)). rewrite -g_tower -(gg_tower _ n); apply (_ : Proper (_ ==> _) (g _)).
transitivity (map (ff n, gg n) (X (S (n + k)))). trans (map (ff n, gg n) (X (S (n + k)))).
{ rewrite /unfold (conv_compl n (unfold_chain X)). { rewrite /unfold (conv_compl n (unfold_chain X)).
rewrite -(chain_cauchy (unfold_chain X) n (S (n + k))) /=; last lia. rewrite -(chain_cauchy (unfold_chain X) n (S (n + k))) /=; last lia.
rewrite -(dist_le _ _ _ _ (f_tower (n + k) _)); last lia. rewrite -(dist_le _ _ _ _ (f_tower (n + k) _)); last lia.
...@@ -234,6 +234,6 @@ Proof. ...@@ -234,6 +234,6 @@ Proof.
apply (contractive_ne map); split => Y /=. apply (contractive_ne map); split => Y /=.
+ apply dist_le with n; last omega. + apply dist_le with n; last omega.
rewrite f_tower. apply dist_S. by rewrite embed_tower. rewrite f_tower. apply dist_S. by rewrite embed_tower.
+ etransitivity; [apply embed_ne, equiv_dist, g_tower|apply embed_tower]. + etrans; [apply embed_ne, equiv_dist, g_tower|apply embed_tower].
Qed. Qed.
End solver. End solver. End solver. End solver.
...@@ -60,7 +60,7 @@ Proof. ...@@ -60,7 +60,7 @@ Proof.
- by intros [x px ?]; simpl. - by intros [x px ?]; simpl.
- intros [x px ?] [y py ?]; naive_solver. - intros [x px ?] [y py ?]; naive_solver.
- intros [x px ?] [y py ?] [z pz ?] [? Hxy] [? Hyz]; simpl in *. - intros [x px ?] [y py ?] [z pz ?] [? Hxy] [? Hyz]; simpl in *.
split; [|intros; transitivity y]; tauto. split; [|intros; trans y]; tauto.
Qed. Qed.
Instance dra_valid_proper' : Proper (() ==> iff) (valid : A Prop). Instance dra_valid_proper' : Proper (() ==> iff) (valid : A Prop).
Proof. by split; apply dra_valid_proper. Qed. Proof. by split; apply dra_valid_proper. Qed.
......
...@@ -56,7 +56,7 @@ Proof. ...@@ -56,7 +56,7 @@ Proof.
- intros n; split. - intros n; split.
+ by intros [x| |]; constructor. + by intros [x| |]; constructor.
+ by destruct 1; constructor. + by destruct 1; constructor.
+ destruct 1; inversion_clear 1; constructor; etransitivity; eauto. + destruct 1; inversion_clear 1; constructor; etrans; eauto.
- by inversion_clear 1; constructor; apply dist_S. - by inversion_clear 1; constructor; apply dist_S.
- intros n c; unfold compl, excl_compl. - intros n c; unfold compl, excl_compl.
destruct (Some_dec (maybe Excl (c 1))) as [[x Hx]|]. destruct (Some_dec (maybe Excl (c 1))) as [[x Hx]|].
......
...@@ -22,7 +22,7 @@ Proof. ...@@ -22,7 +22,7 @@ Proof.
- intros n; split. - intros n; split.
+ by intros m k. + by intros m k.
+ by intros m1 m2 ? k. + by intros m1 m2 ? k.
+ by intros m1 m2 m3 ?? k; transitivity (m2 !! k). + by intros m1 m2 m3 ?? k; trans (m2 !! k).
- by intros n m1 m2 ? k; apply dist_S. - by intros n m1 m2 ? k; apply dist_S.
- intros n c k; rewrite /compl /map_compl lookup_imap. - intros n c k; rewrite /compl /map_compl lookup_imap.
feed inversion (λ H, chain_cauchy c 0 (S n) H k); simpl; auto with lia. feed inversion (λ H, chain_cauchy c 0 (S n) H k); simpl; auto with lia.
......
...@@ -35,7 +35,7 @@ Section iprod_cofe. ...@@ -35,7 +35,7 @@ Section iprod_cofe.
- intros n; split. - intros n; split.
+ by intros f x. + by intros f x.
+ by intros f g ? x. + by intros f g ? x.
+ by intros f g h ?? x; transitivity (g x). + by intros f g h ?? x; trans (g x).
- intros n f g Hfg x; apply dist_S, Hfg. - intros n f g Hfg x; apply dist_S, Hfg.
- intros n c x. - intros n c x.
rewrite /compl /iprod_compl (conv_compl n (iprod_chain c x)). rewrite /compl /iprod_compl (conv_compl n (iprod_chain c x)).
......
...@@ -29,7 +29,7 @@ Proof. ...@@ -29,7 +29,7 @@ Proof.
- intros n; split. - intros n; split.
+ by intros [x|]; constructor. + by intros [x|]; constructor.
+ by destruct 1; constructor. + by destruct 1; constructor.
+ destruct 1; inversion_clear 1; constructor; etransitivity; eauto. + destruct 1; inversion_clear 1; constructor; etrans; eauto.
- by inversion_clear 1; constructor; apply dist_S. - by inversion_clear 1; constructor; apply dist_S.
- intros n c; unfold compl, option_compl. - intros n c; unfold compl, option_compl.
destruct (Some_dec (c 1)) as [[x Hx]|]. destruct (Some_dec (c 1)) as [[x Hx]|].
......
...@@ -224,7 +224,7 @@ Proof. ...@@ -224,7 +224,7 @@ Proof.
split. split.
- by intros []; constructor. - by intros []; constructor.
- by destruct 1; constructor. - by destruct 1; constructor.
- destruct 1; inversion_clear 1; constructor; etransitivity; eauto. - destruct 1; inversion_clear 1; constructor; etrans; eauto.
Qed. Qed.
Global Instance sts_dra : DRA (car sts). Global Instance sts_dra : DRA (car sts).
Proof. Proof.
...@@ -366,7 +366,7 @@ Lemma sts_op_frag S1 S2 T1 T2 : ...@@ -366,7 +366,7 @@ Lemma sts_op_frag S1 S2 T1 T2 :
Proof. Proof.
intros HT HS1 HS2. rewrite /sts_frag. intros HT HS1 HS2. rewrite /sts_frag.
(* FIXME why does rewrite not work?? *) (* FIXME why does rewrite not work?? *)
etransitivity; last eapply to_validity_op; try done; []. etrans; last eapply to_validity_op; try done; [].
intros Hval. constructor; last set_solver. eapply closed_ne, Hval. intros Hval. constructor; last set_solver. eapply closed_ne, Hval.
Qed. Qed.
......
From algebra Require Export cmra. From algebra Require Export cmra.
Local Hint Extern 1 (_ _) => etransitivity; [eassumption|]. Local Hint Extern 1 (_ _) => etrans; [eassumption|].
Local Hint Extern 1 (_ _) => etransitivity; [|eassumption]. Local Hint Extern 1 (_ _) => etrans; [|eassumption].
Local Hint Extern 10 (_ _) => omega. Local Hint Extern 10 (_ _) => omega.
Record uPred (M : cmraT) : Type := IProp { Record uPred (M : cmraT) : Type := IProp {
...@@ -40,7 +40,7 @@ Section cofe. ...@@ -40,7 +40,7 @@ Section cofe.
- intros n; split. - intros n; split.
+ by intros P x i. + by intros P x i.
+ by intros P Q HPQ x i ??; symmetry; apply HPQ. + by intros P Q HPQ x i ??; symmetry; apply HPQ.
+ by intros P Q Q' HP HQ i x ??; transitivity (Q i x);[apply HP|apply HQ]. + by intros P Q Q' HP HQ i x ??; trans (Q i x);[apply HP|apply HQ].
- intros n P Q HPQ i x ??; apply HPQ; auto. - intros n P Q HPQ i x ??; apply HPQ; auto.
- intros n c i x ??; symmetry; apply (chain_cauchy c i (S n)); auto. - intros n c i x ??; symmetry; apply (chain_cauchy c i (S n)); auto.
Qed. Qed.
...@@ -243,8 +243,8 @@ Global Instance entails_proper : ...@@ -243,8 +243,8 @@ Global Instance entails_proper :
Proper (() ==> () ==> iff) (() : relation (uPred M)). Proper (() ==> () ==> iff) (() : relation (uPred M)).
Proof. Proof.
move => P1 P2 /equiv_spec [HP1 HP2] Q1 Q2 /equiv_spec [HQ1 HQ2]; split; intros. move => P1 P2 /equiv_spec [HP1 HP2] Q1 Q2 /equiv_spec [HQ1 HQ2]; split; intros.
- by transitivity P1; [|transitivity Q1]. - by trans P1; [|trans Q1].
- by transitivity P2; [|transitivity Q2]. - by trans P2; [|trans Q2].
Qed. Qed.
(** Non-expansiveness and setoid morphisms *) (** Non-expansiveness and setoid morphisms *)
...@@ -734,7 +734,7 @@ Proof. by rewrite /uPred_iff later_and !later_impl. Qed. ...@@ -734,7 +734,7 @@ Proof. by rewrite /uPred_iff later_and !later_impl. Qed.
Lemma löb_strong P Q : (P Q) Q P Q. Lemma löb_strong P Q : (P Q) Q P Q.
Proof. Proof.
intros Hlöb. apply impl_entails. intros Hlöb. apply impl_entails.
etransitivity; last by eapply löb. etrans; last by eapply löb.
apply impl_intro_l, impl_intro_l. rewrite right_id -{2}Hlöb. apply impl_intro_l, impl_intro_l. rewrite right_id -{2}Hlöb.
apply and_intro; first by eauto. apply and_intro; first by eauto.
by rewrite {1}(later_intro P) later_impl impl_elim_r. by rewrite {1}(later_intro P) later_impl impl_elim_r.
......
...@@ -61,14 +61,14 @@ Proof. ...@@ -61,14 +61,14 @@ Proof.
induction 1 as [|P Ps Qs ? IH|P Q Ps|]; simpl; auto. induction 1 as [|P Ps Qs ? IH|P Q Ps|]; simpl; auto.
- by rewrite IH. - by rewrite IH.
- by rewrite !assoc (comm _ P). - by rewrite !assoc (comm _ P).
- etransitivity; eauto. - etrans; eauto.
Qed. Qed.
Global Instance big_sep_perm : Proper (() ==> ()) (@uPred_big_sep M). Global Instance big_sep_perm : Proper (() ==> ()) (@uPred_big_sep M).
Proof. Proof.
induction 1 as [|P Ps Qs ? IH|P Q Ps|]; simpl; auto. induction 1 as [|P Ps Qs ? IH|P Q Ps|]; simpl; auto.
- by rewrite IH. - by rewrite IH.
- by rewrite !assoc (comm _ P). - by rewrite !assoc (comm _ P).
- etransitivity; eauto. - etrans; eauto.
Qed. Qed.
Lemma big_and_app Ps Qs : (Π (Ps ++ Qs))%I (Π Ps Π Qs)%I. Lemma big_and_app Ps Qs : (Π (Ps ++ Qs))%I (Π Ps Π Qs)%I.
...@@ -103,7 +103,7 @@ Section gmap. ...@@ -103,7 +103,7 @@ Section gmap.
m2 m1 ( x k, m2 !! k = Some x Φ k x Ψ k x) m2 m1 ( x k, m2 !! k = Some x Φ k x Ψ k x)
(Π★{map m1} Φ) (Π★{map m2} Ψ). (Π★{map m1} Φ) (Π★{map m2} Ψ).
Proof. Proof.
intros HX HΦ. transitivity (Π★{map m2} Φ)%I. intros HX HΦ. trans (Π★{map m2} Φ)%I.
- by apply big_sep_contains, fmap_contains, map_to_list_contains. - by apply big_sep_contains, fmap_contains, map_to_list_contains.
- apply big_sep_mono', Forall2_fmap, Forall2_Forall. - apply big_sep_mono', Forall2_fmap, Forall2_Forall.
apply Forall_forall=> -[i x] ? /=. by apply HΦ, elem_of_map_to_list. apply Forall_forall=> -[i x] ? /=. by apply HΦ, elem_of_map_to_list.
...@@ -163,7 +163,7 @@ Section gset. ...@@ -163,7 +163,7 @@ Section gset.
Lemma big_sepS_mono Φ Ψ X Y : Lemma big_sepS_mono Φ Ψ X Y :
Y X ( x, x Y Φ x Ψ x) (Π★{set X} Φ) (Π★{set Y} Ψ). Y X ( x, x Y Φ x Ψ x) (Π★{set X} Φ) (Π★{set Y} Ψ).
Proof. Proof.
intros HX HΦ. transitivity (Π★{set Y} Φ)%I. intros HX HΦ. trans (Π★{set Y} Φ)%I.
- by apply big_sep_contains, fmap_contains, elements_contains. - by apply big_sep_contains, fmap_contains, elements_contains.
- apply big_sep_mono', Forall2_fmap, Forall2_Forall. - apply big_sep_mono', Forall2_fmap, Forall2_Forall.
apply Forall_forall=> x ? /=. by apply HΦ, elem_of_elements. apply Forall_forall=> x ? /=. by apply HΦ, elem_of_elements.
......
...@@ -157,7 +157,7 @@ Section proof. ...@@ -157,7 +157,7 @@ Section proof.
{ by eapply (saved_prop_alloc _ P). } { by eapply (saved_prop_alloc _ P). }
rewrite pvs_frame_l. apply pvs_strip_pvs. rewrite sep_exist_l. rewrite pvs_frame_l. apply pvs_strip_pvs. rewrite sep_exist_l.
apply exist_elim=>i. apply exist_elim=>i.
transitivity (pvs (heap_ctx heapN (barrier_inv l P (State Low {[ i ]})) saved_prop_own i P)). trans (pvs (heap_ctx heapN (barrier_inv l P (State Low {[ i ]})) saved_prop_own i P)).
- rewrite -pvs_intro. rewrite [(_ heap_ctx _)%I]comm -!assoc. apply sep_mono_r. - rewrite -pvs_intro. rewrite [(_ heap_ctx _)%I]comm -!assoc. apply sep_mono_r.
rewrite {1}[saved_prop_own _ _]always_sep_dup !assoc. apply sep_mono_l. rewrite {1}[saved_prop_own _ _]always_sep_dup !assoc. apply sep_mono_l.
rewrite /barrier_inv /waiting -later_intro. apply sep_mono_r. rewrite /barrier_inv /waiting -later_intro. apply sep_mono_r.
...@@ -215,7 +215,7 @@ Section proof. ...@@ -215,7 +215,7 @@ Section proof.
apply const_elim_sep_l=>Hs. destruct p; last done. apply const_elim_sep_l=>Hs. destruct p; last done.
rewrite {1}/barrier_inv =>/={Hs}. rewrite later_sep. rewrite {1}/barrier_inv =>/={Hs}. rewrite later_sep.
eapply wp_store; eauto with I ndisj. eapply wp_store; eauto with I ndisj.
rewrite -!assoc. apply sep_mono_r. etransitivity; last eapply later_mono. rewrite -!assoc. apply sep_mono_r. etrans; last eapply later_mono.
{ (* Is this really the best way to strip the later? *) { (* Is this really the best way to strip the later? *)
erewrite later_sep. apply sep_mono_r. apply later_intro. } erewrite later_sep. apply sep_mono_r. apply later_intro. }
apply wand_intro_l. rewrite -(exist_intro (State High I)). apply wand_intro_l. rewrite -(exist_intro (State High I)).
...@@ -256,7 +256,7 @@ Section proof. ...@@ -256,7 +256,7 @@ Section proof.
apply const_elim_sep_l=>Hs. apply const_elim_sep_l=>Hs.
rewrite {1}/barrier_inv =>/=. rewrite later_sep. rewrite {1}/barrier_inv =>/=. rewrite later_sep.
eapply wp_load; eauto with I ndisj. eapply wp_load; eauto with I ndisj.
rewrite -!assoc. apply sep_mono_r. etransitivity; last eapply later_mono. rewrite -!assoc. apply sep_mono_r. etrans; last eapply later_mono.
{ (* Is this really the best way to strip the later? *) { (* Is this really the best way to strip the later? *)
erewrite later_sep. apply sep_mono_r. rewrite !assoc. erewrite later_sep. erewrite later_sep. apply sep_mono_r. rewrite !assoc. erewrite later_sep.
apply sep_mono_l, later_intro. } apply sep_mono_l, later_intro. }
...@@ -294,7 +294,7 @@ Section proof. ...@@ -294,7 +294,7 @@ Section proof.
rewrite [(sts_own _ _ _ _)%I]sep_elim_r [(sts_ctx _ _ _ _)%I]sep_elim_r. rewrite [(sts_own _ _ _ _)%I]sep_elim_r [(sts_ctx _ _ _ _)%I]sep_elim_r.
rewrite !assoc [(_ saved_prop_own i Q)%I]comm !assoc saved_prop_agree. rewrite !assoc [(_ saved_prop_own i Q)%I]comm !assoc saved_prop_agree.
wp_op>; last done. intros _. wp_op>; last done. intros _.
etransitivity; last eapply later_mono. etrans; last eapply later_mono.
{ (* Is this really the best way to strip the later? *) { (* Is this really the best way to strip the later? *)
erewrite later_sep. apply sep_mono; last apply later_intro. erewrite later_sep. apply sep_mono; last apply later_intro.
rewrite ->later_sep. apply sep_mono_l. rewrite ->later_sep. done. } rewrite ->later_sep. apply sep_mono_l. rewrite ->later_sep. done. }
......
...@@ -67,7 +67,7 @@ Section heap. ...@@ -67,7 +67,7 @@ Section heap.
authG heap_lang Σ heapRA nclose N E authG heap_lang Σ heapRA nclose N E
ownP σ (|={E}=> _ : heapG Σ, heap_ctx N Π★{map σ} heap_mapsto). ownP σ (|={E}=> _ : heapG Σ, heap_ctx N Π★{map σ} heap_mapsto).
Proof. Proof.
intros. rewrite -{1}(from_to_heap σ). etransitivity. intros. rewrite -{1}(from_to_heap σ). etrans.
{ rewrite [ownP _]later_intro. { rewrite [ownP _]later_intro.
apply (auth_alloc (ownP of_heap) E N (to_heap σ)); last done. apply (auth_alloc (ownP of_heap) E N (to_heap σ)); last done.
apply to_heap_valid. } apply to_heap_valid. }
...@@ -103,7 +103,7 @@ Section heap. ...@@ -103,7 +103,7 @@ Section heap.
P || Alloc e @ E {{ Φ }}. P || Alloc e @ E {{ Φ }}.
Proof. Proof.
rewrite /heap_ctx /heap_inv /heap_mapsto=> ?? Hctx HP. rewrite /heap_ctx /heap_inv /heap_mapsto=> ?? Hctx HP.
transitivity (|={E}=> auth_own heap_name P)%I. trans (|={E}=> auth_own heap_name P)%I.
{ by rewrite -pvs_frame_r -(auth_empty _ E) left_id. } { by rewrite -pvs_frame_r -(auth_empty _ E) left_id. }
apply wp_strip_pvs, (auth_fsa heap_inv (wp_fsa (Alloc e))) apply wp_strip_pvs, (auth_fsa heap_inv (wp_fsa (Alloc e)))
with N heap_name ; simpl; eauto with I. with N heap_name ; simpl; eauto with I.
......
...@@ -13,19 +13,19 @@ Ltac wp_strip_later := ...@@ -13,19 +13,19 @@ Ltac wp_strip_later :=
| |- _ _ => apply later_intro | |- _ _ => apply later_intro
| |- _ _ => reflexivity | |- _ _ => reflexivity
end end
in revert_intros ltac:(etransitivity; [|go]). in revert_intros ltac:(etrans; [|go]).
Ltac wp_bind K := Ltac wp_bind K :=
lazymatch eval hnf in K with lazymatch eval hnf in K with
| [] => idtac | [] => idtac
| _ => etransitivity; [|solve [ apply (wp_bind K) ]]; simpl | _ => etrans; [|solve [ apply (wp_bind K) ]]; simpl
end. end.
Ltac wp_finish := Ltac wp_finish :=
let rec go := let rec go :=
match goal with match goal with
| |- _ _ => etransitivity; [|apply later_mono; go; reflexivity] | |- _ _ => etrans; [|apply later_mono; go; reflexivity]
| |- _ wp _ _ _ => | |- _ wp _ _ _ =>
etransitivity; [|eapply wp_value_pvs; reflexivity]; etrans; [|eapply wp_value_pvs; reflexivity];
(* sometimes, we will have to do a final view shift, so only apply (* sometimes, we will have to do a final view shift, so only apply
wp_value if we obtain a consecutive wp *) wp_value if we obtain a consecutive wp *)
try (eapply pvs_intro; try (eapply pvs_intro;
...@@ -38,7 +38,7 @@ Tactic Notation "wp_rec" ">" := ...@@ -38,7 +38,7 @@ Tactic Notation "wp_rec" ">" :=
| |- _ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' => | |- _ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
match eval cbv in e' with match eval cbv in e' with
| App (Rec _ _ _) _ => | App (Rec _ _ _) _ =>
wp_bind K; etransitivity; [|eapply wp_rec; reflexivity]; wp_finish wp_bind K; etrans; [|eapply wp_rec; reflexivity]; wp_finish
end) end)
end. end.
Tactic Notation "wp_rec" := wp_rec>; wp_strip_later. Tactic Notation "wp_rec" := wp_rec>; wp_strip_later.
...@@ -48,7 +48,7 @@ Tactic Notation "wp_lam" ">" := ...@@ -48,7 +48,7 @@ Tactic Notation "wp_lam" ">" :=
| |- _ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' => | |- _ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
match eval cbv in e' with match eval cbv in e' with
| App (Rec "" _ _) _ => | App (Rec "" _ _) _ =>
wp_bind K; etransitivity; [|eapply wp_lam; reflexivity]; wp_finish wp_bind K; etrans; [|eapply wp_lam; reflexivity]; wp_finish
end) end)
end. end.
Tactic Notation "wp_lam" := wp_lam>; wp_strip_later. Tactic Notation "wp_lam" := wp_lam>; wp_strip_later.
...@@ -66,9 +66,9 @@ Tactic Notation "wp_op" ">" := ...@@ -66,9 +66,9 @@ Tactic Notation "wp_op" ">" :=
| BinOp LeOp _ _ => wp_bind K; apply wp_le; wp_finish | BinOp LeOp _ _ => wp_bind K; apply wp_le; wp_finish
| BinOp EqOp _ _ => wp_bind K; apply wp_eq; wp_finish | BinOp EqOp _ _ => wp_bind K; apply wp_eq; wp_finish
| BinOp _ _ _ => | BinOp _ _ _ =>