Commit fd3aa446 authored by Ralf Jung's avatar Ralf Jung
Browse files

upred: move the primes in the always lemmas to the more specific versions

parent 3367bd23
...@@ -724,7 +724,7 @@ Proof. ...@@ -724,7 +724,7 @@ Proof.
intros x n ??; apply uPred_weaken with (unit x) n; intros x n ??; apply uPred_weaken with (unit x) n;
eauto using cmra_included_unit. eauto using cmra_included_unit.
Qed. Qed.
Lemma always_intro P Q : P Q P Q. Lemma always_intro' P Q : P Q P Q.
Proof. Proof.
intros HPQ x n ??; apply HPQ; simpl in *; auto using cmra_unit_validN. intros HPQ x n ??; apply HPQ; simpl in *; auto using cmra_unit_validN.
by rewrite cmra_unit_idemp. by rewrite cmra_unit_idemp.
...@@ -751,7 +751,7 @@ Proof. done. Qed. ...@@ -751,7 +751,7 @@ Proof. done. Qed.
(* Always derived *) (* Always derived *)
Lemma always_mono P Q : P Q P Q. Lemma always_mono P Q : P Q P Q.
Proof. intros. apply always_intro. by rewrite always_elim. Qed. Proof. intros. apply always_intro'. by rewrite always_elim. Qed.
Hint Resolve always_mono. Hint Resolve always_mono.
Global Instance always_mono' : Proper (() ==> ()) (@uPred_always M). Global Instance always_mono' : Proper (() ==> ()) (@uPred_always M).
Proof. intros P Q; apply always_mono. Qed. Proof. intros P Q; apply always_mono. Qed.
...@@ -769,26 +769,26 @@ Proof. ...@@ -769,26 +769,26 @@ Proof.
Qed. Qed.
Lemma always_and_sep P Q : ( (P Q))%I ( (P Q))%I. Lemma always_and_sep P Q : ( (P Q))%I ( (P Q))%I.
Proof. apply (anti_symm ()); auto using always_and_sep_1. Qed. Proof. apply (anti_symm ()); auto using always_and_sep_1. Qed.
Lemma always_and_sep_l P Q : ( P Q)%I ( P Q)%I. Lemma always_and_sep_l' P Q : ( P Q)%I ( P Q)%I.
Proof. apply (anti_symm ()); auto using always_and_sep_l_1. Qed. Proof. apply (anti_symm ()); auto using always_and_sep_l_1. Qed.
Lemma always_and_sep_r P Q : (P Q)%I (P Q)%I. Lemma always_and_sep_r' P Q : (P Q)%I (P Q)%I.
Proof. by rewrite !(comm _ P) always_and_sep_l. Qed. Proof. by rewrite !(comm _ P) always_and_sep_l'. Qed.
Lemma always_sep P Q : ( (P Q))%I ( P Q)%I. Lemma always_sep P Q : ( (P Q))%I ( P Q)%I.
Proof. by rewrite -always_and_sep -always_and_sep_l always_and. Qed. Proof. by rewrite -always_and_sep -always_and_sep_l' always_and. Qed.
Lemma always_wand P Q : (P - Q) ( P - Q). Lemma always_wand P Q : (P - Q) ( P - Q).
Proof. by apply wand_intro_r; rewrite -always_sep wand_elim_l. Qed. Proof. by apply wand_intro_r; rewrite -always_sep wand_elim_l. Qed.
Lemma always_sep_dup P : ( P)%I ( P P)%I. Lemma always_sep_dup' P : ( P)%I ( P P)%I.
Proof. by rewrite -always_sep -always_and_sep (idemp _). Qed. Proof. by rewrite -always_sep -always_and_sep (idemp _). Qed.
Lemma always_wand_impl P Q : ( (P - Q))%I ( (P Q))%I. Lemma always_wand_impl P Q : ( (P - Q))%I ( (P Q))%I.
Proof. Proof.
apply (anti_symm ()); [|by rewrite -impl_wand]. apply (anti_symm ()); [|by rewrite -impl_wand].
apply always_intro, impl_intro_r. apply always_intro', impl_intro_r.
by rewrite always_and_sep_l always_elim wand_elim_l. by rewrite always_and_sep_l' always_elim wand_elim_l.
Qed. Qed.
Lemma always_entails_l P Q : (P Q) P ( Q P). Lemma always_entails_l' P Q : (P Q) P ( Q P).
Proof. intros; rewrite -always_and_sep_l; auto. Qed. Proof. intros; rewrite -always_and_sep_l'; auto. Qed.
Lemma always_entails_r P Q : (P Q) P (P Q). Lemma always_entails_r' P Q : (P Q) P (P Q).
Proof. intros; rewrite -always_and_sep_r; auto. Qed. Proof. intros; rewrite -always_and_sep_r'; auto. Qed.
(* Own and valid *) (* Own and valid *)
Lemma ownM_op (a1 a2 : M) : Lemma ownM_op (a1 a2 : M) :
...@@ -922,7 +922,7 @@ Local Notation AS := AlwaysStable. ...@@ -922,7 +922,7 @@ Local Notation AS := AlwaysStable.
Global Instance const_always_stable φ : AS ( φ : uPred M)%I. Global Instance const_always_stable φ : AS ( φ : uPred M)%I.
Proof. by rewrite /AlwaysStable always_const. Qed. Proof. by rewrite /AlwaysStable always_const. Qed.
Global Instance always_always_stable P : AS ( P). Global Instance always_always_stable P : AS ( P).
Proof. by intros; apply always_intro. Qed. Proof. by intros; apply always_intro'. Qed.
Global Instance and_always_stable P Q: AS P AS Q AS (P Q). Global Instance and_always_stable P Q: AS P AS Q AS (P Q).
Proof. by intros; rewrite /AlwaysStable always_and; apply and_mono. Qed. Proof. by intros; rewrite /AlwaysStable always_and; apply and_mono. Qed.
Global Instance or_always_stable P Q : AS P AS Q AS (P Q). Global Instance or_always_stable P Q : AS P AS Q AS (P Q).
...@@ -967,17 +967,17 @@ Proof. unfold ASL=> ?; revert ys; induction xs=> -[|??]; constructor; auto. Qed. ...@@ -967,17 +967,17 @@ Proof. unfold ASL=> ?; revert ys; induction xs=> -[|??]; constructor; auto. Qed.
(* Derived lemmas for always stable *) (* Derived lemmas for always stable *)
Lemma always_always P `{!AlwaysStable P} : ( P)%I P. Lemma always_always P `{!AlwaysStable P} : ( P)%I P.
Proof. apply (anti_symm ()); auto using always_elim. Qed. Proof. apply (anti_symm ()); auto using always_elim. Qed.
Lemma always_intro' P Q `{!AlwaysStable P} : P Q P Q. Lemma always_intro P Q `{!AlwaysStable P} : P Q P Q.
Proof. rewrite -(always_always P); apply always_intro. Qed. Proof. rewrite -(always_always P); apply always_intro'. Qed.
Lemma always_and_sep_l' P Q `{!AlwaysStable P} : (P Q)%I (P Q)%I. Lemma always_and_sep_l P Q `{!AlwaysStable P} : (P Q)%I (P Q)%I.
Proof. by rewrite -(always_always P) always_and_sep_l. Qed. Proof. by rewrite -(always_always P) always_and_sep_l'. Qed.
Lemma always_and_sep_r' P Q `{!AlwaysStable Q} : (P Q)%I (P Q)%I. Lemma always_and_sep_r P Q `{!AlwaysStable Q} : (P Q)%I (P Q)%I.
Proof. by rewrite -(always_always Q) always_and_sep_r. Qed. Proof. by rewrite -(always_always Q) always_and_sep_r'. Qed.
Lemma always_sep_dup' P `{!AlwaysStable P} : P (P P)%I. Lemma always_sep_dup P `{!AlwaysStable P} : P (P P)%I.
Proof. by rewrite -(always_always P) -always_sep_dup. Qed. Proof. by rewrite -(always_always P) -always_sep_dup'. Qed.
Lemma always_entails_l' P Q `{!AlwaysStable Q} : (P Q) P (Q P). Lemma always_entails_l P Q `{!AlwaysStable Q} : (P Q) P (Q P).
Proof. by rewrite -(always_always Q); apply always_entails_l. Qed. Proof. by rewrite -(always_always Q); apply always_entails_l'. Qed.
Lemma always_entails_r' P Q `{!AlwaysStable Q} : (P Q) P (P Q). Lemma always_entails_r P Q `{!AlwaysStable Q} : (P Q) P (P Q).
Proof. by rewrite -(always_always Q); apply always_entails_r. Qed. Proof. by rewrite -(always_always Q); apply always_entails_r'. Qed.
End uPred_logic. End uPred. End uPred_logic. End uPred.
...@@ -36,7 +36,7 @@ Proof. ...@@ -36,7 +36,7 @@ Proof.
apply sep_mono, later_mono; first done. apply sep_mono, later_mono; first done.
apply forall_intro=>e2; apply forall_intro=>σ2; apply forall_intro=>ef. apply forall_intro=>e2; apply forall_intro=>σ2; apply forall_intro=>ef.
apply wand_intro_l. apply wand_intro_l.
rewrite always_and_sep_l' -assoc -always_and_sep_l'. rewrite always_and_sep_l -assoc -always_and_sep_l.
apply const_elim_l=>-[l [-> [-> [-> ?]]]]. apply const_elim_l=>-[l [-> [-> [-> ?]]]].
by rewrite (forall_elim l) right_id const_equiv // left_id wand_elim_r. by rewrite (forall_elim l) right_id const_equiv // left_id wand_elim_r.
Qed. Qed.
......
...@@ -32,7 +32,7 @@ Section auth. ...@@ -32,7 +32,7 @@ Section auth.
rewrite [(_ φ _)%I]comm -assoc. apply sep_mono; first done. rewrite [(_ φ _)%I]comm -assoc. apply sep_mono; first done.
rewrite /auth_own -own_op auth_both_op. done. } rewrite /auth_own -own_op auth_both_op. done. }
rewrite (inv_alloc N) /auth_ctx pvs_frame_r. apply pvs_mono. rewrite (inv_alloc N) /auth_ctx pvs_frame_r. apply pvs_mono.
by rewrite always_and_sep_l'. by rewrite always_and_sep_l.
Qed. Qed.
Context {Hφ : n, Proper (dist n ==> dist n) φ}. Context {Hφ : n, Proper (dist n ==> dist n) φ}.
......
...@@ -77,7 +77,7 @@ Proof. ...@@ -77,7 +77,7 @@ Proof.
rewrite /own ownG_valid; apply valid_mono=> ?; apply to_globalF_validN. rewrite /own ownG_valid; apply valid_mono=> ?; apply to_globalF_validN.
Qed. Qed.
Lemma own_valid_r γ a : own i γ a (own i γ a a). Lemma own_valid_r γ a : own i γ a (own i γ a a).
Proof. apply (uPred.always_entails_r' _ _), own_valid. Qed. Proof. apply (uPred.always_entails_r _ _), own_valid. Qed.
Global Instance own_timeless γ a : Timeless a TimelessP (own i γ a). Global Instance own_timeless γ a : Timeless a TimelessP (own i γ a).
Proof. unfold own; apply _. Qed. Proof. unfold own; apply _. Qed.
......
...@@ -32,14 +32,14 @@ Proof. by intros P P' HP e ? <- Q Q' HQ; apply ht_mono. Qed. ...@@ -32,14 +32,14 @@ Proof. by intros P P' HP e ? <- Q Q' HQ; apply ht_mono. Qed.
Lemma ht_val E v : Lemma ht_val E v :
{{ True : iProp Λ Σ }} of_val v @ E {{ λ v', v = v' }}. {{ True : iProp Λ Σ }} of_val v @ E {{ λ v', v = v' }}.
Proof. Proof.
apply (always_intro' _ _), impl_intro_l. apply (always_intro _ _), impl_intro_l.
by rewrite -wp_value; apply const_intro. by rewrite -wp_value; apply const_intro.
Qed. Qed.
Lemma ht_vs E P P' Q Q' e : Lemma ht_vs E P P' Q Q' e :
((P ={E}=> P') {{ P' }} e @ E {{ Q' }} v, Q' v ={E}=> Q v) ((P ={E}=> P') {{ P' }} e @ E {{ Q' }} v, Q' v ={E}=> Q v)
{{ P }} e @ E {{ Q }}. {{ P }} e @ E {{ Q }}.
Proof. Proof.
apply (always_intro' _ _), impl_intro_l. apply (always_intro _ _), impl_intro_l.
rewrite (assoc _ P) {1}/vs always_elim impl_elim_r. rewrite (assoc _ P) {1}/vs always_elim impl_elim_r.
rewrite assoc pvs_impl_r pvs_always_r wp_always_r. rewrite assoc pvs_impl_r pvs_always_r wp_always_r.
rewrite -(pvs_wp E e Q) -(wp_pvs E e Q); apply pvs_mono, wp_mono=> v. rewrite -(pvs_wp E e Q) -(wp_pvs E e Q); apply pvs_mono, wp_mono=> v.
...@@ -50,7 +50,7 @@ Lemma ht_atomic E1 E2 P P' Q Q' e : ...@@ -50,7 +50,7 @@ Lemma ht_atomic E1 E2 P P' Q Q' e :
((P ={E1,E2}=> P') {{ P' }} e @ E2 {{ Q' }} v, Q' v ={E2,E1}=> Q v) ((P ={E1,E2}=> P') {{ P' }} e @ E2 {{ Q' }} v, Q' v ={E2,E1}=> Q v)
{{ P }} e @ E1 {{ Q }}. {{ P }} e @ E1 {{ Q }}.
Proof. Proof.
intros ??; apply (always_intro' _ _), impl_intro_l. intros ??; apply (always_intro _ _), impl_intro_l.
rewrite (assoc _ P) {1}/vs always_elim impl_elim_r. rewrite (assoc _ P) {1}/vs always_elim impl_elim_r.
rewrite assoc pvs_impl_r pvs_always_r wp_always_r. rewrite assoc pvs_impl_r pvs_always_r wp_always_r.
rewrite -(wp_atomic E1 E2) //; apply pvs_mono, wp_mono=> v. rewrite -(wp_atomic E1 E2) //; apply pvs_mono, wp_mono=> v.
...@@ -60,7 +60,7 @@ Lemma ht_bind `{LanguageCtx Λ K} E P Q Q' e : ...@@ -60,7 +60,7 @@ Lemma ht_bind `{LanguageCtx Λ K} E P Q Q' e :
({{ P }} e @ E {{ Q }} v, {{ Q v }} K (of_val v) @ E {{ Q' }}) ({{ P }} e @ E {{ Q }} v, {{ Q v }} K (of_val v) @ E {{ Q' }})
{{ P }} K e @ E {{ Q' }}. {{ P }} K e @ E {{ Q' }}.
Proof. Proof.
intros; apply (always_intro' _ _), impl_intro_l. intros; apply (always_intro _ _), impl_intro_l.
rewrite (assoc _ P) {1}/ht always_elim impl_elim_r. rewrite (assoc _ P) {1}/ht always_elim impl_elim_r.
rewrite wp_always_r -wp_bind //; apply wp_mono=> v. rewrite wp_always_r -wp_bind //; apply wp_mono=> v.
by rewrite (forall_elim v) /ht always_elim impl_elim_r. by rewrite (forall_elim v) /ht always_elim impl_elim_r.
...@@ -71,7 +71,7 @@ Proof. intros. by apply always_mono, impl_mono, wp_mask_frame_mono. Qed. ...@@ -71,7 +71,7 @@ Proof. intros. by apply always_mono, impl_mono, wp_mask_frame_mono. Qed.
Lemma ht_frame_l E P Q R e : Lemma ht_frame_l E P Q R e :
{{ P }} e @ E {{ Q }} {{ R P }} e @ E {{ λ v, R Q v }}. {{ P }} e @ E {{ Q }} {{ R P }} e @ E {{ λ v, R Q v }}.
Proof. Proof.
apply always_intro, impl_intro_l. apply always_intro', impl_intro_l.
rewrite always_and_sep_r -assoc (sep_and P) always_elim impl_elim_r. rewrite always_and_sep_r -assoc (sep_and P) always_elim impl_elim_r.
by rewrite wp_frame_l. by rewrite wp_frame_l.
Qed. Qed.
...@@ -82,7 +82,7 @@ Lemma ht_frame_later_l E P R e Q : ...@@ -82,7 +82,7 @@ Lemma ht_frame_later_l E P R e Q :
to_val e = None to_val e = None
{{ P }} e @ E {{ Q }} {{ R P }} e @ E {{ λ v, R Q v }}. {{ P }} e @ E {{ Q }} {{ R P }} e @ E {{ λ v, R Q v }}.
Proof. Proof.
intros; apply always_intro, impl_intro_l. intros; apply always_intro', impl_intro_l.
rewrite always_and_sep_r -assoc (sep_and P) always_elim impl_elim_r. rewrite always_and_sep_r -assoc (sep_and P) always_elim impl_elim_r.
by rewrite wp_frame_later_l //; apply wp_mono=>v; rewrite pvs_frame_l. by rewrite wp_frame_later_l //; apply wp_mono=>v; rewrite pvs_frame_l.
Qed. Qed.
......
...@@ -26,14 +26,14 @@ Lemma ht_lift_step E1 E2 ...@@ -26,14 +26,14 @@ Lemma ht_lift_step E1 E2
{{ Q2 e2 σ2 ef }} ef ?@ coPset_all {{ λ _, True }}) {{ Q2 e2 σ2 ef }} ef ?@ coPset_all {{ λ _, True }})
{{ P }} e1 @ E2 {{ R }}. {{ P }} e1 @ E2 {{ R }}.
Proof. Proof.
intros ?? Hsafe Hstep; apply (always_intro' _ _), impl_intro_l. intros ?? Hsafe Hstep; apply (always_intro _ _), impl_intro_l.
rewrite (assoc _ P) {1}/vs always_elim impl_elim_r pvs_always_r. rewrite (assoc _ P) {1}/vs always_elim impl_elim_r pvs_always_r.
rewrite -(wp_lift_step E1 E2 φ _ e1 σ1) //; apply pvs_mono. rewrite -(wp_lift_step E1 E2 φ _ e1 σ1) //; apply pvs_mono.
rewrite always_and_sep_r' -assoc; apply sep_mono; first done. rewrite always_and_sep_r -assoc; apply sep_mono; first done.
rewrite (later_intro ( _, _)) -later_sep; apply later_mono. rewrite (later_intro ( _, _)) -later_sep; apply later_mono.
apply forall_intro=>e2; apply forall_intro=>σ2; apply forall_intro=>ef. apply forall_intro=>e2; apply forall_intro=>σ2; apply forall_intro=>ef.
rewrite (forall_elim e2) (forall_elim σ2) (forall_elim ef). rewrite (forall_elim e2) (forall_elim σ2) (forall_elim ef).
apply wand_intro_l; rewrite !always_and_sep_l'. apply wand_intro_l; rewrite !always_and_sep_l.
rewrite (assoc _ _ P') -(assoc _ _ _ P') assoc. rewrite (assoc _ _ P') -(assoc _ _ _ P') assoc.
rewrite {1}/vs -always_wand_impl always_elim wand_elim_r. rewrite {1}/vs -always_wand_impl always_elim wand_elim_r.
rewrite pvs_frame_r; apply pvs_mono. rewrite pvs_frame_r; apply pvs_mono.
...@@ -62,15 +62,15 @@ Proof. ...@@ -62,15 +62,15 @@ Proof.
apply and_intro; [by rewrite -vs_reflexive; apply const_intro|]. apply and_intro; [by rewrite -vs_reflexive; apply const_intro|].
apply forall_mono=>e2; apply forall_mono=>σ2; apply forall_mono=>ef. apply forall_mono=>e2; apply forall_mono=>σ2; apply forall_mono=>ef.
apply and_intro; [|apply and_intro; [|done]]. apply and_intro; [|apply and_intro; [|done]].
* rewrite -vs_impl; apply (always_intro' _ _),impl_intro_l;rewrite and_elim_l. * rewrite -vs_impl; apply (always_intro _ _),impl_intro_l; rewrite and_elim_l.
rewrite !assoc; apply sep_mono; last done. rewrite !assoc; apply sep_mono; last done.
rewrite -!always_and_sep_l' -!always_and_sep_r'; apply const_elim_l=>-[??]. rewrite -!always_and_sep_l -!always_and_sep_r; apply const_elim_l=>-[??].
by repeat apply and_intro; try apply const_intro. by repeat apply and_intro; try apply const_intro.
* apply (always_intro' _ _), impl_intro_l; rewrite and_elim_l. * apply (always_intro _ _), impl_intro_l; rewrite and_elim_l.
rewrite -always_and_sep_r'; apply const_elim_r=>-[[v Hv] ?]. rewrite -always_and_sep_r; apply const_elim_r=>-[[v Hv] ?].
rewrite -(of_to_val e2 v) // -wp_value. rewrite -(of_to_val e2 v) // -wp_value.
rewrite -(exist_intro σ2) -(exist_intro ef) (of_to_val e2) //. rewrite -(exist_intro σ2) -(exist_intro ef) (of_to_val e2) //.
by rewrite -always_and_sep_r'; apply and_intro; try apply const_intro. by rewrite -always_and_sep_r; apply and_intro; try apply const_intro.
Qed. Qed.
Lemma ht_lift_pure_step E (φ : expr Λ option (expr Λ) Prop) P P' Q e1 : Lemma ht_lift_pure_step E (φ : expr Λ option (expr Λ) Prop) P P' Q e1 :
...@@ -82,12 +82,12 @@ Lemma ht_lift_pure_step E (φ : expr Λ → option (expr Λ) → Prop) P P' Q e1 ...@@ -82,12 +82,12 @@ Lemma ht_lift_pure_step E (φ : expr Λ → option (expr Λ) → Prop) P P' Q e1
{{ φ e2 ef P' }} ef ?@ coPset_all {{ λ _, True }}) {{ φ e2 ef P' }} ef ?@ coPset_all {{ λ _, True }})
{{ (P P') }} e1 @ E {{ Q }}. {{ (P P') }} e1 @ E {{ Q }}.
Proof. Proof.
intros ? Hsafe Hstep; apply (always_intro' _ _), impl_intro_l. intros ? Hsafe Hstep; apply (always_intro _ _), impl_intro_l.
rewrite -(wp_lift_pure_step E φ _ e1) //. rewrite -(wp_lift_pure_step E φ _ e1) //.
rewrite (later_intro ( _, _)) -later_and; apply later_mono. rewrite (later_intro ( _, _)) -later_and; apply later_mono.
apply forall_intro=>e2; apply forall_intro=>ef; apply impl_intro_l. apply forall_intro=>e2; apply forall_intro=>ef; apply impl_intro_l.
rewrite (forall_elim e2) (forall_elim ef). rewrite (forall_elim e2) (forall_elim ef).
rewrite always_and_sep_l' !always_and_sep_r' {1}(always_sep_dup' ( _)). rewrite always_and_sep_l !always_and_sep_r {1}(always_sep_dup ( _)).
rewrite {1}(assoc _ (_ _)%I) -(assoc _ ( _)%I). rewrite {1}(assoc _ (_ _)%I) -(assoc _ ( _)%I).
rewrite (assoc _ ( _)%I P) -{1}(comm _ P) -(assoc _ P). rewrite (assoc _ ( _)%I P) -{1}(comm _ P) -(assoc _ P).
rewrite (assoc _ ( _)%I) assoc -(assoc _ ( _ P))%I. rewrite (assoc _ ( _)%I) assoc -(assoc _ ( _ P))%I.
...@@ -111,11 +111,11 @@ Proof. ...@@ -111,11 +111,11 @@ Proof.
rewrite -(ht_lift_pure_step _ (λ e2' ef', e2 = e2' ef = ef')); eauto. rewrite -(ht_lift_pure_step _ (λ e2' ef', e2 = e2' ef = ef')); eauto.
apply forall_intro=>e2'; apply forall_intro=>ef'; apply and_mono. apply forall_intro=>e2'; apply forall_intro=>ef'; apply and_mono.
* apply (always_intro' _ _), impl_intro_l. * apply (always_intro' _ _), impl_intro_l.
rewrite -always_and_sep_l' -assoc; apply const_elim_l=>-[??]; subst. rewrite -always_and_sep_l -assoc; apply const_elim_l=>-[??]; subst.
by rewrite /ht always_elim impl_elim_r. by rewrite /ht always_elim impl_elim_r.
* destruct ef' as [e'|]; simpl; [|by apply const_intro]. * destruct ef' as [e'|]; simpl; [|by apply const_intro].
apply (always_intro' _ _), impl_intro_l. apply (always_intro _ _), impl_intro_l.
rewrite -always_and_sep_l' -assoc; apply const_elim_l=>-[??]; subst. rewrite -always_and_sep_l -assoc; apply const_elim_l=>-[??]; subst.
by rewrite /= /ht always_elim impl_elim_r. by rewrite /= /ht always_elim impl_elim_r.
Qed. Qed.
......
...@@ -72,16 +72,16 @@ Lemma inv_fsa {A : Type} {FSA} (FSAs : FrameShiftAssertion (A:=A) FSA) ...@@ -72,16 +72,16 @@ Lemma inv_fsa {A : Type} {FSA} (FSAs : FrameShiftAssertion (A:=A) FSA)
Proof. Proof.
move=>HN. move=>HN.
rewrite /inv sep_exist_r. apply exist_elim=>i. rewrite /inv sep_exist_r. apply exist_elim=>i.
rewrite always_and_sep_l' -assoc. apply const_elim_sep_l=>HiN. rewrite always_and_sep_l -assoc. apply const_elim_sep_l=>HiN.
rewrite -(fsa_trans3 E (E {[encode i]})) //; last by solve_elem_of+. rewrite -(fsa_trans3 E (E {[encode i]})) //; last by solve_elem_of+.
(* Add this to the local context, so that solve_elem_of finds it. *) (* Add this to the local context, so that solve_elem_of finds it. *)
assert ({[encode i]} nclose N) by eauto. assert ({[encode i]} nclose N) by eauto.
rewrite (always_sep_dup' (ownI _ _)). rewrite (always_sep_dup (ownI _ _)).
rewrite {1}pvs_openI !pvs_frame_r. rewrite {1}pvs_openI !pvs_frame_r.
apply pvs_mask_frame_mono ; [solve_elem_of..|]. apply pvs_mask_frame_mono ; [solve_elem_of..|].
rewrite (comm _ (_)%I) -assoc wand_elim_r fsa_frame_l. rewrite (comm _ (_)%I) -assoc wand_elim_r fsa_frame_l.
apply fsa_mask_frame_mono; [solve_elem_of..|]. intros a. apply fsa_mask_frame_mono; [solve_elem_of..|]. intros a.
rewrite assoc -always_and_sep_l' pvs_closeI pvs_frame_r left_id. rewrite assoc -always_and_sep_l pvs_closeI pvs_frame_r left_id.
apply pvs_mask_frame'; solve_elem_of. apply pvs_mask_frame'; solve_elem_of.
Qed. Qed.
......
...@@ -71,7 +71,7 @@ Proof. ...@@ -71,7 +71,7 @@ Proof.
rewrite -pvs_intro. apply sep_mono, later_mono; first done. rewrite -pvs_intro. apply sep_mono, later_mono; first done.
apply forall_intro=>e2'; apply forall_intro=>σ2'. apply forall_intro=>e2'; apply forall_intro=>σ2'.
apply forall_intro=>ef; apply wand_intro_l. apply forall_intro=>ef; apply wand_intro_l.
rewrite always_and_sep_l' -assoc -always_and_sep_l'. rewrite always_and_sep_l -assoc -always_and_sep_l.
apply const_elim_l=>-[v2' [Hv ?]] /=. apply const_elim_l=>-[v2' [Hv ?]] /=.
rewrite -pvs_intro. rewrite -pvs_intro.
rewrite (forall_elim v2') (forall_elim σ2') (forall_elim ef) const_equiv //. rewrite (forall_elim v2') (forall_elim σ2') (forall_elim ef) const_equiv //.
...@@ -90,7 +90,7 @@ Proof. ...@@ -90,7 +90,7 @@ Proof.
apply sep_mono, later_mono; first done. apply sep_mono, later_mono; first done.
apply forall_intro=>e2'; apply forall_intro=>σ2'; apply forall_intro=>ef'. apply forall_intro=>e2'; apply forall_intro=>σ2'; apply forall_intro=>ef'.
apply wand_intro_l. apply wand_intro_l.
rewrite always_and_sep_l' -assoc -always_and_sep_l'. rewrite always_and_sep_l -assoc -always_and_sep_l.
apply const_elim_l=>-[-> [-> ->]] /=. by rewrite wand_elim_r. apply const_elim_l=>-[-> [-> ->]] /=. by rewrite wand_elim_r.
Qed. Qed.
......
...@@ -33,7 +33,7 @@ Qed. ...@@ -33,7 +33,7 @@ Qed.
Global Instance ownI_always_stable i P : AlwaysStable (ownI i P). Global Instance ownI_always_stable i P : AlwaysStable (ownI i P).
Proof. by rewrite /AlwaysStable always_ownI. Qed. Proof. by rewrite /AlwaysStable always_ownI. Qed.
Lemma ownI_sep_dup i P : ownI i P (ownI i P ownI i P)%I. Lemma ownI_sep_dup i P : ownI i P (ownI i P ownI i P)%I.
Proof. apply (uPred.always_sep_dup' _). Qed. Proof. apply (uPred.always_sep_dup _). Qed.
(* physical state *) (* physical state *)
Lemma ownP_twice σ1 σ2 : (ownP σ1 ownP σ2 : iProp Λ Σ) False. Lemma ownP_twice σ1 σ2 : (ownP σ1 ownP σ2 : iProp Λ Σ) False.
...@@ -58,7 +58,7 @@ Qed. ...@@ -58,7 +58,7 @@ Qed.
Lemma ownG_valid m : (ownG m) ( m). Lemma ownG_valid m : (ownG m) ( m).
Proof. by rewrite /ownG uPred.ownM_valid; apply uPred.valid_mono=> n [? []]. Qed. Proof. by rewrite /ownG uPred.ownM_valid; apply uPred.valid_mono=> n [? []]. Qed.
Lemma ownG_valid_r m : (ownG m) (ownG m m). Lemma ownG_valid_r m : (ownG m) (ownG m m).
Proof. apply (uPred.always_entails_r' _ _), ownG_valid. Qed. Proof. apply (uPred.always_entails_r _ _), ownG_valid. Qed.
Global Instance ownG_timeless m : Timeless m TimelessP (ownG m). Global Instance ownG_timeless m : Timeless m TimelessP (ownG m).
Proof. rewrite /ownG; apply _. Qed. Proof. rewrite /ownG; apply _. Qed.
......
...@@ -138,10 +138,10 @@ Lemma pvs_frame_l E1 E2 P Q : (P ★ pvs E1 E2 Q) ⊑ pvs E1 E2 (P ★ Q). ...@@ -138,10 +138,10 @@ Lemma pvs_frame_l E1 E2 P Q : (P ★ pvs E1 E2 Q) ⊑ pvs E1 E2 (P ★ Q).
Proof. rewrite !(comm _ P); apply pvs_frame_r. Qed. Proof. rewrite !(comm _ P); apply pvs_frame_r. Qed.
Lemma pvs_always_l E1 E2 P Q `{!AlwaysStable P} : Lemma pvs_always_l E1 E2 P Q `{!AlwaysStable P} :
(P pvs E1 E2 Q) pvs E1 E2 (P Q). (P pvs E1 E2 Q) pvs E1 E2 (P Q).
Proof. by rewrite !always_and_sep_l' pvs_frame_l. Qed. Proof. by rewrite !always_and_sep_l pvs_frame_l. Qed.
Lemma pvs_always_r E1 E2 P Q `{!AlwaysStable Q} : Lemma pvs_always_r E1 E2 P Q `{!AlwaysStable Q} :
(pvs E1 E2 P Q) pvs E1 E2 (P Q). (pvs E1 E2 P Q) pvs E1 E2 (P Q).
Proof. by rewrite !always_and_sep_r' pvs_frame_r. Qed. Proof. by rewrite !always_and_sep_r pvs_frame_r. Qed.
Lemma pvs_impl_l E1 E2 P Q : ( (P Q) pvs E1 E2 P) pvs E1 E2 Q. Lemma pvs_impl_l E1 E2 P Q : ( (P Q) pvs E1 E2 P) pvs E1 E2 Q.
Proof. by rewrite pvs_always_l always_elim impl_elim_l. Qed. Proof. by rewrite pvs_always_l always_elim impl_elim_l. Qed.
Lemma pvs_impl_r E1 E2 P Q : (pvs E1 E2 P (P Q)) pvs E1 E2 Q. Lemma pvs_impl_r E1 E2 P Q : (pvs E1 E2 P (P Q)) pvs E1 E2 Q.
......
...@@ -23,7 +23,7 @@ Implicit Types P Q R : iProp Λ Σ. ...@@ -23,7 +23,7 @@ Implicit Types P Q R : iProp Λ Σ.
Lemma vs_alt E1 E2 P Q : (P pvs E1 E2 Q) P ={E1,E2}=> Q. Lemma vs_alt E1 E2 P Q : (P pvs E1 E2 Q) P ={E1,E2}=> Q.
Proof. Proof.
intros; rewrite -{1}always_const; apply always_intro, impl_intro_l. intros; rewrite -{1}always_const. apply (always_intro _ _), impl_intro_l.
by rewrite always_const right_id. by rewrite always_const right_id.
Qed. Qed.
...@@ -50,7 +50,7 @@ Proof. by intros ?; apply vs_alt, pvs_timeless. Qed. ...@@ -50,7 +50,7 @@ Proof. by intros ?; apply vs_alt, pvs_timeless. Qed.
Lemma vs_transitive E1 E2 E3 P Q R : Lemma vs_transitive E1 E2 E3 P Q R :
E2 E1 E3 ((P ={E1,E2}=> Q) (Q ={E2,E3}=> R)) (P ={E1,E3}=> R). E2 E1 E3 ((P ={E1,E2}=> Q) (Q ={E2,E3}=> R)) (P ={E1,E3}=> R).
Proof. Proof.
intros; rewrite -always_and; apply always_intro, impl_intro_l. intros; rewrite -always_and; apply (always_intro _ _), impl_intro_l.
rewrite always_and assoc (always_elim (P _)) impl_elim_r. rewrite always_and assoc (always_elim (P _)) impl_elim_r.
by rewrite pvs_impl_r; apply pvs_trans. by rewrite pvs_impl_r; apply pvs_trans.
Qed. Qed.
...@@ -62,13 +62,13 @@ Proof. apply vs_alt, pvs_intro. Qed. ...@@ -62,13 +62,13 @@ Proof. apply vs_alt, pvs_intro. Qed.
Lemma vs_impl E P Q : (P Q) (P ={E}=> Q). Lemma vs_impl E P Q : (P Q) (P ={E}=> Q).
Proof. Proof.
apply always_intro, impl_intro_l. apply always_intro', impl_intro_l.
by rewrite always_elim impl_elim_r -pvs_intro. by rewrite always_elim impl_elim_r -pvs_intro.
Qed. Qed.
Lemma vs_frame_l E1 E2 P Q R : (P ={E1,E2}=> Q) (R P ={E1,E2}=> R Q). Lemma vs_frame_l E1 E2 P Q R : (P ={E1,E2}=> Q) (R P ={E1,E2}=> R Q).
Proof. Proof.
apply always_intro, impl_intro_l. apply always_intro', impl_intro_l.
rewrite -pvs_frame_l always_and_sep_r -always_wand_impl -assoc. rewrite -pvs_frame_l always_and_sep_r -always_wand_impl -assoc.
by rewrite always_elim wand_elim_r. by rewrite always_elim wand_elim_r.
Qed. Qed.
...@@ -79,7 +79,7 @@ Proof. rewrite !(comm _ _ R); apply vs_frame_l. Qed. ...@@ -79,7 +79,7 @@ Proof. rewrite !(comm _ _ R); apply vs_frame_l. Qed.
Lemma vs_mask_frame E1 E2 Ef P Q : Lemma vs_mask_frame E1 E2 Ef P Q :
Ef (E1 E2) = (P ={E1,E2}=> Q) (P ={E1 Ef,E2 Ef}=> Q). Ef (E1 E2) = (P ={E1,E2}=> Q) (P ={E1 Ef,E2 Ef}=> Q).
Proof. Proof.
intros ?; apply always_intro, impl_intro_l; rewrite (pvs_mask_frame _ _ Ef)//.