Commit 2ca5469a authored by Robbert Krebbers's avatar Robbert Krebbers Committed by Jacques-Henri Jourdan

More consistent naming, e.g. bare_later -> later_bare_2.

(All the later lemmas are now prefixed by later_, and dito for
laterN, and except_0).
parent 43048a39
......@@ -1419,15 +1419,13 @@ Proof. apply wand_intro_l. by rewrite -later_sep wand_elim_r. Qed.
Lemma later_iff P Q : (P Q) P Q.
Proof. by rewrite /bi_iff later_and !later_impl. Qed.
Lemma later_persistently P : P P.
Proof.
apply (anti_symm _); auto using later_persistently_1, later_persistently_2.
Qed.
Lemma bare_later P : P P.
Proof. apply (anti_symm _); auto using later_persistently_1, later_persistently_2. Qed.
Lemma later_bare_2 P : P P.
Proof. rewrite /bi_bare later_and. auto using later_intro. Qed.
Lemma bare_persistently_later P : P P.
Proof. by rewrite -later_persistently bare_later. Qed.
Lemma bare_persistently_if_later p P : ?p P ?p P.
Proof. destruct p; simpl; auto using bare_persistently_later. Qed.
Lemma later_bare_persistently_2 P : P P.
Proof. by rewrite -later_persistently later_bare_2. Qed.
Lemma later_bare_persistently_if_2 p P : ?p P ?p P.
Proof. destruct p; simpl; auto using later_bare_persistently_2. Qed.
Global Instance later_persistent P : Persistent P Persistent ( P).
Proof.
......@@ -1490,12 +1488,12 @@ Lemma laterN_iff n P Q : ▷^n (P ↔ Q) ⊢ ▷^n P ↔ ▷^n Q.
Proof. by rewrite /bi_iff laterN_and !laterN_impl. Qed.
Lemma laterN_persistently n P : ^n P ^n P.
Proof. induction n as [|n IH]; simpl; auto. by rewrite IH later_persistently. Qed.
Lemma bare_laterN n P : ^n P ^n P.
Lemma laterN_bare_2 n P : ^n P ^n P.
Proof. rewrite /bi_bare laterN_and. auto using laterN_intro. Qed.
Lemma bare_persistently_laterN n P : ^n P ^n P.
Proof. by rewrite -laterN_persistently bare_laterN. Qed.
Lemma bare_persistently_if_laterN n p P : ?p ^n P ^n ?p P.
Proof. destruct p; simpl; auto using bare_persistently_laterN. Qed.
Lemma laterN_bare_persistently_2 n P : ^n P ^n P.
Proof. by rewrite -laterN_persistently laterN_bare_2. Qed.
Lemma laterN_bare_persistently_if_2 n p P : ?p ^n P ^n ?p P.
Proof. destruct p; simpl; auto using laterN_bare_persistently_2. Qed.
Global Instance laterN_persistent n P : Persistent P Persistent (^n P).
Proof. induction n; apply _. Qed.
......@@ -1550,15 +1548,13 @@ Qed.
Lemma except_0_later P : P P.
Proof. by rewrite /bi_except_0 -later_or False_or. Qed.
Lemma except_0_persistently P : P P.
Proof.
by rewrite /bi_except_0 persistently_or -later_persistently persistently_pure.
Qed.
Lemma bare_except_0 P : P P.
Proof. by rewrite /bi_except_0 persistently_or -later_persistently persistently_pure. Qed.
Lemma except_0_bare_2 P : P P.
Proof. rewrite /bi_bare except_0_and. auto using except_0_intro. Qed.
Lemma bare_persistently_except_0 P : P P.
Proof. by rewrite -except_0_persistently bare_except_0. Qed.
Lemma bare_persistently_if_except_0 p P : ?p P ?p P.
Proof. destruct p; simpl; auto using bare_persistently_except_0. Qed.
Lemma except_0_bare_persistently_2 P : P P.
Proof. by rewrite -except_0_persistently except_0_bare_2. Qed.
Lemma except_0_bare_persistently_if_2 p P : ?p P ?p P.
Proof. destruct p; simpl; auto using except_0_bare_persistently_2. Qed.
Lemma except_0_frame_l P Q : P Q (P Q).
Proof. by rewrite {1}(except_0_intro P) except_0_sep. Qed.
......
......@@ -682,27 +682,27 @@ Proof. rewrite /FromPure=> ->. apply except_0_intro. Qed.
Global Instance into_wand_later p q R P Q :
IntoWand p q R P Q IntoWand p q ( R) ( P) ( Q).
Proof.
rewrite /IntoWand /= => HR. by rewrite !bare_persistently_if_later -later_wand HR.
rewrite /IntoWand /= => HR. by rewrite !later_bare_persistently_if_2 -later_wand HR.
Qed.
Global Instance into_wand_later_args p q R P Q :
IntoWand p q R P Q IntoWand' p q R ( P) ( Q).
Proof.
rewrite /IntoWand' /IntoWand /= => HR.
by rewrite !bare_persistently_if_later (later_intro (?p R)%I) -later_wand HR.
by rewrite !later_bare_persistently_if_2 (later_intro (?p R)%I) -later_wand HR.
Qed.
Global Instance into_wand_laterN n p q R P Q :
IntoWand p q R P Q IntoWand p q (^n R) (^n P) (^n Q).
Proof.
rewrite /IntoWand /= => HR. by rewrite !bare_persistently_if_laterN -laterN_wand HR.
rewrite /IntoWand /= => HR. by rewrite !laterN_bare_persistently_if_2 -laterN_wand HR.
Qed.
Global Instance into_wand_laterN_args n p q R P Q :
IntoWand p q R P Q IntoWand' p q R (^n P) (^n Q).
Proof.
rewrite /IntoWand' /IntoWand /= => HR.
by rewrite !bare_persistently_if_laterN (laterN_intro _ (?p R)%I) -laterN_wand HR.
by rewrite !laterN_bare_persistently_if_2 (laterN_intro _ (?p R)%I) -laterN_wand HR.
Qed.
(* FromAnd *)
......@@ -732,19 +732,19 @@ Global Instance into_and_later p P Q1 Q2 :
IntoAnd p P Q1 Q2 IntoAnd p ( P) ( Q1) ( Q2).
Proof.
rewrite /IntoAnd=> HP. apply bare_persistently_if_intro'.
by rewrite bare_persistently_if_later HP bare_persistently_if_elim later_and.
by rewrite later_bare_persistently_if_2 HP bare_persistently_if_elim later_and.
Qed.
Global Instance into_and_laterN n p P Q1 Q2 :
IntoAnd p P Q1 Q2 IntoAnd p (^n P) (^n Q1) (^n Q2).
Proof.
rewrite /IntoAnd=> HP. apply bare_persistently_if_intro'.
by rewrite bare_persistently_if_laterN HP bare_persistently_if_elim laterN_and.
by rewrite laterN_bare_persistently_if_2 HP bare_persistently_if_elim laterN_and.
Qed.
Global Instance into_and_except_0 p P Q1 Q2 :
IntoAnd p P Q1 Q2 IntoAnd p ( P) ( Q1) ( Q2).
Proof.
rewrite /IntoAnd=> HP. apply bare_persistently_if_intro'.
by rewrite bare_persistently_if_except_0 HP bare_persistently_if_elim except_0_and.
by rewrite except_0_bare_persistently_if_2 HP bare_persistently_if_elim except_0_and.
Qed.
(* IntoSep *)
......@@ -860,7 +860,7 @@ Global Instance frame_later p R R' P Q Q' :
IntoLaterN 1 R' R Frame p R P Q MakeLater Q Q' Frame p R' ( P) Q'.
Proof.
rewrite /Frame /MakeLater /IntoLaterN=>-> <- <- /=.
by rewrite bare_persistently_if_later later_sep.
by rewrite later_bare_persistently_if_2 later_sep.
Qed.
Class MakeLaterN (n : nat) (P lP : PROP) := make_laterN : ^n P lP.
......@@ -875,7 +875,7 @@ Global Instance frame_laterN p n R R' P Q Q' :
IntoLaterN n R' R Frame p R P Q MakeLaterN n Q Q' Frame p R' (^n P) Q'.
Proof.
rewrite /Frame /MakeLaterN /IntoLaterN=>-> <- <-.
by rewrite bare_persistently_if_laterN laterN_sep.
by rewrite laterN_bare_persistently_if_2 laterN_sep.
Qed.
Class MakeExcept0 (P Q : PROP) := make_except_0 : P Q.
......
......@@ -1044,7 +1044,7 @@ Lemma into_laterN_env_sound n Δ1 Δ2 :
IntoLaterNEnvs n Δ1 Δ2 Δ1 ^n (Δ2 : bi_car _).
Proof.
intros [Hp Hs]; rewrite /of_envs /= !laterN_and !laterN_sep.
rewrite -{1}laterN_intro -bare_persistently_laterN.
rewrite -{1}laterN_intro -laterN_bare_persistently_2.
apply and_mono, sep_mono.
- apply pure_mono; destruct 1; constructor;
naive_solver eauto using env_Forall2_wf, env_Forall2_fresh.
......
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