Skip to content

GitLab

Commit dd0444b8 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files
Options

Rename uPred_now_True → uPred_except_last. 

Following the time anology of later, the step-index 0 corresponds does
not correspond to 'now', but rather to the end of time (i.e. 'last').
parent 48679cc3
Hide whitespace changes
Inline Side-by-side
Showing with 87 additions and 87 deletions
algebra/upred.v
View file @ dd0444b8
......@@ -328,11 +328,11 @@ Arguments uPred_always_if _ !_ _/.
Notation "□? p P" := (uPred_always_if p P)
(at level 20, p at level 0, P at level 20, format "□? p P").
Definition uPred_now_True {M} (P : uPred M) : uPred M := ▷ False ∨ P.
Notation "◇ P" := (uPred_now_True P)
Definition uPred_except_last {M} (P : uPred M) : uPred M := ▷ False ∨ P.
Notation "◇ P" := (uPred_except_last P)
(at level 20, right associativity) : uPred_scope.
Instance: Params (@uPred_now_True) 1.
Typeclasses Opaque uPred_now_True.
Instance: Params (@uPred_except_last) 1.
Typeclasses Opaque uPred_except_last.
Class TimelessP {M} (P : uPred M) := timelessP : ▷ P ⊢ ◇ P.
Arguments timelessP {_} _ {_}.
......@@ -1063,50 +1063,50 @@ Lemma later_iff P Q : ▷ (P ↔ Q) ⊢ ▷ P ↔ ▷ Q.
Proof. by rewrite /uPred_iff later_and !later_impl. Qed.
(* True now *)
Global Instance now_True_ne n : Proper (dist n ==> dist n) (@uPred_now_True M).
Global Instance except_last_ne n : Proper (dist n ==> dist n) (@uPred_except_last M).
Proof. solve_proper. Qed.
Global Instance now_True_proper : Proper ((⊣⊢) ==> (⊣⊢)) (@uPred_now_True M).
Global Instance except_last_proper : Proper ((⊣⊢) ==> (⊣⊢)) (@uPred_except_last M).
Proof. solve_proper. Qed.
Global Instance now_True_mono' : Proper ((⊢) ==> (⊢)) (@uPred_now_True M).
Global Instance except_last_mono' : Proper ((⊢) ==> (⊢)) (@uPred_except_last M).
Proof. solve_proper. Qed.
Global Instance now_True_flip_mono' :
Proper (flip (⊢) ==> flip (⊢)) (@uPred_now_True M).
Global Instance except_last_flip_mono' :
Proper (flip (⊢) ==> flip (⊢)) (@uPred_except_last M).
Proof. solve_proper. Qed.
Lemma now_True_intro P : P ⊢ ◇ P.
Proof. rewrite /uPred_now_True; auto. Qed.
Lemma now_True_mono P Q : (P ⊢ Q) → ◇ P ⊢ ◇ Q.
Lemma except_last_intro P : P ⊢ ◇ P.
Proof. rewrite /uPred_except_last; auto. Qed.
Lemma except_last_mono P Q : (P ⊢ Q) → ◇ P ⊢ ◇ Q.
Proof. by intros ->. Qed.
Lemma now_True_idemp P : ◇ ◇ P ⊢ ◇ P.
Proof. rewrite /uPred_now_True; auto. Qed.
Lemma now_True_True : ◇ True ⊣⊢ True.
Proof. rewrite /uPred_now_True. apply (anti_symm _); auto. Qed.
Lemma now_True_or P Q : ◇ (P ∨ Q) ⊣⊢ ◇ P ∨ ◇ Q.
Proof. rewrite /uPred_now_True. apply (anti_symm _); auto. Qed.
Lemma now_True_and P Q : ◇ (P ∧ Q) ⊣⊢ ◇ P ∧ ◇ Q.
Proof. by rewrite /uPred_now_True or_and_l. Qed.
Lemma now_True_sep P Q : ◇ (P ★ Q) ⊣⊢ ◇ P ★ ◇ Q.
Proof.
rewrite /uPred_now_True. apply (anti_symm _).
Lemma except_last_idemp P : ◇ ◇ P ⊢ ◇ P.
Proof. rewrite /uPred_except_last; auto. Qed.
Lemma except_last_True : ◇ True ⊣⊢ True.
Proof. rewrite /uPred_except_last. apply (anti_symm _); auto. Qed.
Lemma except_last_or P Q : ◇ (P ∨ Q) ⊣⊢ ◇ P ∨ ◇ Q.
Proof. rewrite /uPred_except_last. apply (anti_symm _); auto. Qed.
Lemma except_last_and P Q : ◇ (P ∧ Q) ⊣⊢ ◇ P ∧ ◇ Q.
Proof. by rewrite /uPred_except_last or_and_l. Qed.
Lemma except_last_sep P Q : ◇ (P ★ Q) ⊣⊢ ◇ P ★ ◇ Q.
Proof.
rewrite /uPred_except_last. apply (anti_symm _).
- apply or_elim; last by auto.
by rewrite -!or_intro_l -always_pure -always_later -always_sep_dup'.
- rewrite sep_or_r sep_elim_l sep_or_l; auto.
Qed.
Lemma now_True_forall {A} (Φ : A → uPred M) : ◇ (∀ a, Φ a) ⊢ ∀ a, ◇ Φ a.
Lemma except_last_forall {A} (Φ : A → uPred M) : ◇ (∀ a, Φ a) ⊢ ∀ a, ◇ Φ a.
Proof. apply forall_intro=> a. by rewrite (forall_elim a). Qed.
Lemma now_True_exist {A} (Φ : A → uPred M) : (∃ a, ◇ Φ a) ⊢ ◇ ∃ a, Φ a.
Lemma except_last_exist {A} (Φ : A → uPred M) : (∃ a, ◇ Φ a) ⊢ ◇ ∃ a, Φ a.
Proof. apply exist_elim=> a. by rewrite (exist_intro a). Qed.
Lemma now_True_later P : ◇ ▷ P ⊢ ▷ P.
Proof. by rewrite /uPred_now_True -later_or False_or. Qed.
Lemma now_True_always P : ◇ □ P ⊣⊢ □ ◇ P.
Proof. by rewrite /uPred_now_True always_or always_later always_pure. Qed.
Lemma now_True_always_if p P : ◇ □?p P ⊣⊢ □?p ◇ P.
Proof. destruct p; simpl; auto using now_True_always. Qed.
Lemma now_True_frame_l P Q : P ★ ◇ Q ⊢ ◇ (P ★ Q).
Proof. by rewrite {1}(now_True_intro P) now_True_sep. Qed.
Lemma now_True_frame_r P Q : ◇ P ★ Q ⊢ ◇ (P ★ Q).
Proof. by rewrite {1}(now_True_intro Q) now_True_sep. Qed.
Lemma except_last_later P : ◇ ▷ P ⊢ ▷ P.
Proof. by rewrite /uPred_except_last -later_or False_or. Qed.
Lemma except_last_always P : ◇ □ P ⊣⊢ □ ◇ P.
Proof. by rewrite /uPred_except_last always_or always_later always_pure. Qed.
Lemma except_last_always_if p P : ◇ □?p P ⊣⊢ □?p ◇ P.
Proof. destruct p; simpl; auto using except_last_always. Qed.
Lemma except_last_frame_l P Q : P ★ ◇ Q ⊢ ◇ (P ★ Q).
Proof. by rewrite {1}(except_last_intro P) except_last_sep. Qed.
Lemma except_last_frame_r P Q : ◇ P ★ Q ⊢ ◇ (P ★ Q).
Proof. by rewrite {1}(except_last_intro Q) except_last_sep. Qed.
(* Own *)
Lemma ownM_op (a1 a2 : M) :
......@@ -1200,9 +1200,9 @@ Proof.
intros; rewrite (rvs_ownM_updateP _ (y =)); last by apply cmra_update_updateP.
by apply rvs_mono, exist_elim=> y'; apply pure_elim_l=> ->.
Qed.
Lemma now_True_rvs P : ◇ (|=r=> P) ⊢ (|=r=> ◇ P).
Lemma except_last_rvs P : ◇ (|=r=> P) ⊢ (|=r=> ◇ P).
Proof.
rewrite /uPred_now_True. apply or_elim; auto using rvs_mono.
rewrite /uPred_except_last. apply or_elim; auto using rvs_mono.
by rewrite -rvs_intro -or_intro_l.
Qed.
......@@ -1241,10 +1241,10 @@ Lemma timelessP_spec P : TimelessP P ↔ ∀ n x, ✓{n} x → P 0 x → P n x.
Proof.
split.
- intros HP n x ??; induction n as [|n]; auto.
move: HP; rewrite /TimelessP /uPred_now_True /=.
move: HP; rewrite /TimelessP /uPred_except_last /=.
unseal=> /uPred_in_entails /(_ (S n) x) /=.
by destruct 1; auto using cmra_validN_S.
- move=> HP; rewrite /TimelessP /uPred_now_True /=.
- move=> HP; rewrite /TimelessP /uPred_except_last /=.
unseal; split=> -[|n] x /=; auto.
right. apply HP, uPred_closed with n; eauto using cmra_validN_le.
Qed.
......@@ -1258,16 +1258,16 @@ Proof.
apply timelessP_spec; unseal=> n x /=. by rewrite -!cmra_discrete_valid_iff.
Qed.
Global Instance and_timeless P Q: TimelessP P → TimelessP Q → TimelessP (P ∧ Q).
Proof. intros; rewrite /TimelessP now_True_and later_and; auto. Qed.
Proof. intros; rewrite /TimelessP except_last_and later_and; auto. Qed.
Global Instance or_timeless P Q : TimelessP P → TimelessP Q → TimelessP (P ∨ Q).
Proof. intros; rewrite /TimelessP now_True_or later_or; auto. Qed.
Proof. intros; rewrite /TimelessP except_last_or later_or; auto. Qed.
Global Instance impl_timeless P Q : TimelessP Q → TimelessP (P → Q).
Proof.
rewrite !timelessP_spec; unseal=> HP [|n] x ? HPQ [|n'] x' ????; auto.
apply HP, HPQ, uPred_closed with (S n'); eauto using cmra_validN_le.
Qed.
Global Instance sep_timeless P Q: TimelessP P → TimelessP Q → TimelessP (P ★ Q).
Proof. intros; rewrite /TimelessP now_True_sep later_sep; auto. Qed.
Proof. intros; rewrite /TimelessP except_last_sep later_sep; auto. Qed.
Global Instance wand_timeless P Q : TimelessP Q → TimelessP (P -★ Q).
Proof.
rewrite !timelessP_spec; unseal=> HP [|n] x ? HPQ [|n'] x' ???; auto.
......@@ -1284,7 +1284,7 @@ Proof.
[|intros [a ?]; exists a; apply HΨ].
Qed.
Global Instance always_timeless P : TimelessP P → TimelessP (□ P).
Proof. intros; rewrite /TimelessP now_True_always -always_later; auto. Qed.
Proof. intros; rewrite /TimelessP except_last_always -always_later; auto. Qed.
Global Instance always_if_timeless p P : TimelessP P → TimelessP (□?p P).
Proof. destruct p; apply _. Qed.
Global Instance eq_timeless {A : cofeT} (a b : A) :
......
program_logic/invariants.v
View file @ dd0444b8
......@@ -39,7 +39,7 @@ Proof.
eapply nclose_infinite, (difference_finite_inv _ _), Hfin.
apply of_gset_finite.
- by iFrame.
- rewrite /uPred_now_True; eauto.
- rewrite /uPred_except_last; eauto.
Qed.
Lemma inv_open E N P :
......@@ -49,9 +49,9 @@ Proof.
iDestruct "Hi" as % ?%elem_of_subseteq_singleton.
rewrite {1 4}(union_difference_L (nclose N) E) // ownE_op; last set_solver.
rewrite {1 5}(union_difference_L {[ i ]} (nclose N)) // ownE_op; last set_solver.
iIntros "(Hw & [HE $] & $)"; iVsIntro; iApply now_True_intro.
iIntros "(Hw & [HE $] & $)"; iVsIntro; iApply except_last_intro.
iDestruct (ownI_open i P with "[Hw HE]") as "($ & $ & HD)"; first by iFrame.
iIntros "HP [Hw $] !==>"; iApply now_True_intro. iApply ownI_close; by iFrame.
iIntros "HP [Hw $] !==>"; iApply except_last_intro. iApply ownI_close; by iFrame.
Qed.
Lemma inv_open_timeless E N P `{!TimelessP P} :
......
program_logic/pviewshifts.v
View file @ dd0444b8
......@@ -44,17 +44,17 @@ Lemma pvs_intro' E1 E2 P : E2 ⊆ E1 → ((|={E2,E1}=> True) -★ P) ={E1,E2}=>
Proof.
intros (E1''&->&?)%subseteq_disjoint_union_L.
rewrite pvs_eq /pvs_def ownE_op //; iIntros "H ($ & $ & HE) !==>".
iApply now_True_intro. iApply "H".
iIntros "[$ $] !==>". by iApply now_True_intro.
iApply except_last_intro. iApply "H".
iIntros "[$ $] !==>". by iApply except_last_intro.
Qed.
Lemma now_True_pvs E1 E2 P : ◇ (|={E1,E2}=> P) ={E1,E2}=> P.
Lemma except_last_pvs E1 E2 P : ◇ (|={E1,E2}=> P) ={E1,E2}=> P.
Proof.
rewrite pvs_eq. iIntros "H [Hw HE]". iTimeless "H". iApply "H"; by iFrame.
Qed.
Lemma rvs_pvs E P : (|=r=> P) ={E}=> P.
Proof.
rewrite pvs_eq /pvs_def. iIntros "H [$ $]"; iVs "H".
iVsIntro. by iApply now_True_intro.
iVsIntro. by iApply except_last_intro.
Qed.
Lemma pvs_mono E1 E2 P Q : (P ⊢ Q) → (|={E1,E2}=> P) ={E1,E2}=> Q.
Proof.
......@@ -72,7 +72,7 @@ Proof.
intros. rewrite pvs_eq /pvs_def ownE_op //. iIntros "Hvs (Hw & HE1 &HEf)".
iVs ("Hvs" with "[Hw HE1]") as ">($ & HE2 & HP)"; first by iFrame.
iDestruct (ownE_op' with "[HE2 HEf]") as "[? $]"; first by iFrame.
iVsIntro; iApply now_True_intro. by iApply "HP".
iVsIntro; iApply except_last_intro. by iApply "HP".
Qed.
Lemma pvs_frame_r E1 E2 P Q : (|={E1,E2}=> P) ★ Q ={E1,E2}=> P ★ Q.
Proof. rewrite pvs_eq /pvs_def. by iIntros "[HwP $]". Qed.
......@@ -86,8 +86,8 @@ Proof. intros P Q; apply pvs_mono. Qed.
Lemma pvs_intro E P : P ={E}=> P.
Proof. iIntros "HP". by iApply rvs_pvs. Qed.
Lemma pvs_now_True E1 E2 P : (|={E1,E2}=> ◇ P) ={E1,E2}=> P.
Proof. by rewrite {1}(pvs_intro E2 P) now_True_pvs pvs_trans. Qed.
Lemma pvs_except_last E1 E2 P : (|={E1,E2}=> ◇ P) ={E1,E2}=> P.
Proof. by rewrite {1}(pvs_intro E2 P) except_last_pvs pvs_trans. Qed.
Lemma pvs_frame_l E1 E2 P Q : (P ★ |={E1,E2}=> Q) ={E1,E2}=> P ★ Q.
Proof. rewrite !(comm _ P); apply pvs_frame_r. Qed.
......
proofmode/class_instances.v
View file @ dd0444b8
......@@ -275,17 +275,17 @@ Proof.
rewrite /Frame /MakeLater=><- <-. by rewrite later_sep -(later_intro R).
Qed.
Class MakeNowTrue (P Q : uPred M) := make_now_True : ◇ P ⊣⊢ Q.
Global Instance make_now_True_True : MakeNowTrue True True.
Proof. by rewrite /MakeNowTrue now_True_True. Qed.
Global Instance make_now_True_default P : MakeNowTrue P (◇ P) | 100.
Class MakeExceptLast (P Q : uPred M) := make_except_last : ◇ P ⊣⊢ Q.
Global Instance make_except_last_True : MakeExceptLast True True.
Proof. by rewrite /MakeExceptLast except_last_True. Qed.
Global Instance make_except_last_default P : MakeExceptLast P (◇ P) | 100.
Proof. done. Qed.
Global Instance frame_now_true R P Q Q' :
Frame R P Q → MakeNowTrue Q Q' → Frame R (◇ P) Q'.
Global Instance frame_except_last R P Q Q' :
Frame R P Q → MakeExceptLast Q Q' → Frame R (◇ P) Q'.
Proof.
rewrite /Frame /MakeNowTrue=><- <-.
by rewrite now_True_sep -(now_True_intro R).
rewrite /Frame /MakeExceptLast=><- <-.
by rewrite except_last_sep -(except_last_intro R).
Qed.
Global Instance frame_exist {A} R (Φ Ψ : A → uPred M) :
......@@ -331,21 +331,21 @@ Global Instance into_exist_always {A} P (Φ : A → uPred M) :
IntoExist P Φ → IntoExist (□ P) (λ a, □ (Φ a))%I.
Proof. rewrite /IntoExist=> HP. by rewrite HP always_exist. Qed.
(* IntoNowTrue *)
Global Instance into_now_True_now_True P : IntoNowTrue (◇ P) P.
(* IntoExceptLast *)
Global Instance into_except_last_except_last P : IntoExceptLast (◇ P) P.
Proof. done. Qed.
Global Instance into_now_True_timeless P : TimelessP P → IntoNowTrue (▷ P) P.
Global Instance into_except_last_timeless P : TimelessP P → IntoExceptLast (▷ P) P.
Proof. done. Qed.
(* IsNowTrue *)
Global Instance is_now_True_now_True P : IsNowTrue (◇ P).
Proof. by rewrite /IsNowTrue now_True_idemp. Qed.
Global Instance is_now_True_later P : IsNowTrue (▷ P).
Proof. by rewrite /IsNowTrue now_True_later. Qed.
Global Instance is_now_True_rvs P : IsNowTrue P → IsNowTrue (|=r=> P).
(* IsExceptLast *)
Global Instance is_except_last_except_last P : IsExceptLast (◇ P).
Proof. by rewrite /IsExceptLast except_last_idemp. Qed.
Global Instance is_except_last_later P : IsExceptLast (▷ P).
Proof. by rewrite /IsExceptLast except_last_later. Qed.
Global Instance is_except_last_rvs P : IsExceptLast P → IsExceptLast (|=r=> P).
Proof.
rewrite /IsNowTrue=> HP.
by rewrite -{2}HP -(now_True_idemp P) -now_True_rvs -(now_True_intro P).
rewrite /IsExceptLast=> HP.
by rewrite -{2}HP -(except_last_idemp P) -except_last_rvs -(except_last_intro P).
Qed.
(* FromViewShift *)
......
proofmode/classes.v
View file @ dd0444b8
......@@ -59,11 +59,11 @@ Class IntoExist {A} (P : uPred M) (Φ : A → uPred M) :=
into_exist : P ⊢ ∃ x, Φ x.
Global Arguments into_exist {_} _ _ {_}.
Class IntoNowTrue (P Q : uPred M) := into_now_True : P ⊢ ◇ Q.
Global Arguments into_now_True : clear implicits.
Class IntoExceptLast (P Q : uPred M) := into_except_last : P ⊢ ◇ Q.
Global Arguments into_except_last : clear implicits.
Class IsNowTrue (Q : uPred M) := is_now_True : ◇ Q ⊢ Q.
Global Arguments is_now_True : clear implicits.
Class IsExpectLast (Q : uPred M) := is_except_last : ◇ Q ⊢ Q.
Global Arguments is_except_last : clear implicits.
Class FromVs (P Q : uPred M) := from_vs : (|=r=> Q) ⊢ P.
Global Arguments from_vs : clear implicits.
......
proofmode/coq_tactics.v
View file @ dd0444b8
......@@ -376,14 +376,14 @@ Proof.
Qed.
Lemma tac_timeless Δ Δ' i p P P' Q :
IsNowTrue Q →
envs_lookup i Δ = Some (p, P) → IntoNowTrue P P' →
IsExceptLast Q →
envs_lookup i Δ = Some (p, P) → IntoExceptLast P P' →
envs_simple_replace i p (Esnoc Enil i P') Δ = Some Δ' →
(Δ' ⊢ Q) → Δ ⊢ Q.
Proof.
intros ???? HQ. rewrite envs_simple_replace_sound //; simpl.
rewrite right_id HQ -{2}(is_now_True Q).
by rewrite (into_now_True P) -now_True_always_if now_True_frame_r wand_elim_r.
rewrite right_id HQ -{2}(is_except_last Q).
by rewrite (into_except_last P) -except_last_always_if except_last_frame_r wand_elim_r.
Qed.
(** * Always *)
......
proofmode/pviewshifts.v
View file @ dd0444b8
......@@ -40,8 +40,8 @@ Global Instance to_assert_pvs E1 E2 P Q :
IntoAssert P (|={E1,E2}=> Q) (|={E1}=> P).
Proof. intros. by rewrite /IntoAssert pvs_frame_r wand_elim_r pvs_trans. Qed.
Global Instance is_now_True_pvs E1 E2 P : IsNowTrue (|={E1,E2}=> P).
Proof. by rewrite /IsNowTrue now_True_pvs. Qed.
Global Instance is_except_last_pvs E1 E2 P : IsExceptLast (|={E1,E2}=> P).
Proof. by rewrite /IsExceptLast except_last_pvs. Qed.
Global Instance from_vs_pvs E P : FromVs (|={E}=> P) P.
Proof. by rewrite /FromVs -rvs_pvs. Qed.
......
proofmode/tactics.v
View file @ dd0444b8
......@@ -507,10 +507,10 @@ Tactic Notation "iNext":=
Tactic Notation "iTimeless" constr(H) :=
eapply tac_timeless with _ H _ _ _;
[let Q := match goal with |- IsNowTrue ?Q => Q end in
[let Q := match goal with |- IsExceptLast ?Q => Q end in
apply _ || fail "iTimeless: cannot remove later when goal is" Q
|env_cbv; reflexivity || fail "iTimeless:" H "not found"
|let P := match goal with |- IntoNowTrue ?P _ => P end in
|let P := match goal with |- IntoExceptLast ?P _ => P end in
apply _ || fail "iTimeless:" P "not timeless"
|env_cbv; reflexivity|].
......
proofmode/weakestpre.v
View file @ dd0444b8
......@@ -16,8 +16,8 @@ Global Instance to_assert_wp E e P Φ :
IntoAssert P (WP e @ E {{ Ψ }}) (|={E}=> P).
Proof. intros. by rewrite /IntoAssert pvs_frame_r wand_elim_r pvs_wp. Qed.
Global Instance is_now_True_wp E e Φ : IsNowTrue (WP e @ E {{ Φ }}).
Proof. by rewrite /IsNowTrue -{2}pvs_wp -now_True_pvs -pvs_intro. Qed.
Global Instance is_except_last_wp E e Φ : IsExceptLast (WP e @ E {{ Φ }}).
Proof. by rewrite /IsExceptLast -{2}pvs_wp -except_last_pvs -pvs_intro. Qed.
Global Instance elim_vs_rvs_wp E e P Φ :
ElimVs (|=r=> P) P (WP e @ E {{ Φ }}) (WP e @ E {{ Φ }}).
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment