Skip to content

GitLab

Commit 664196f6 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

Merge branch 'gen_proofmode' of gitlab.mpi-sws.org:FP/iris-coq into gen_proofmode

parents 0b84351c 6d9e7847
Pipeline #7222 passed with stage
in 22 minutes and 32 seconds
Expand all Hide whitespace changes
Inline Side-by-side
ProofMode.md
View file @ 664196f6
......@@ -117,7 +117,7 @@ Modalities
- `iModIntro mod` : introduction of a modality. The type class `FromModal` is
used to specify which modalities this tactic should introduce. Instances of
that type class include: later, except 0, basic update and fancy update,
persistently, affinely, plainly, absorbingly, absolutely, and relatively.
persistently, affinely, plainly, absorbingly, objectively, and subjectively.
The optional argument `mod` can be used to specify what modality to introduce
in case of ambiguity, e.g. `⎡|==> P⎤`.
- `iAlways` : a deprecated alias of `iModIntro`.
......
theories/base_logic/derived.v
View file @ 664196f6
......@@ -16,8 +16,7 @@ Notation "P ⊢ Q" := (bi_entails (PROP:=uPredI M) P%I Q%I).
Notation "P ⊣⊢ Q" := (equiv (A:=uPredI M) P%I Q%I).
(* Own and valid derived *)
Lemma persistently_cmra_valid_1 {A : cmraT} (a : A) :
✓ a ⊢ bi_persistently (✓ a : uPred M).
Lemma persistently_cmra_valid_1 {A : cmraT} (a : A) : ✓ a ⊢ <pers> (✓ a : uPred M).
Proof. by rewrite {1}plainly_cmra_valid_1 plainly_elim_persistently. Qed.
Lemma affinely_persistently_ownM (a : M) : CoreId a → □ uPred_ownM a ⊣⊢ uPred_ownM a.
Proof.
......
theories/base_logic/upred.v
View file @ 664196f6
......@@ -457,21 +457,21 @@ Proof.
- (* (P ⊢ Q -∗ R) → P ∗ Q ⊢ R *)
intros P Q R. unseal=> HPQR. split; intros n x ? (?&?&?&?&?). ofe_subst.
eapply HPQR; eauto using cmra_validN_op_l.
- (* (P ⊢ Q) → bi_persistently P ⊢ bi_persistently Q *)
- (* (P ⊢ Q) → <pers> P ⊢ <pers> Q *)
intros P QR HP. unseal; split=> n x ? /=. by apply HP, cmra_core_validN.
- (* bi_persistently P ⊢ bi_persistently (bi_persistently P) *)
- (* <pers> P ⊢ <pers> <pers> P *)
intros P. unseal; split=> n x ?? /=. by rewrite cmra_core_idemp.
- (* P ⊢ bi_persistently emp (ADMISSIBLE) *)
- (* P ⊢ <pers> emp (ADMISSIBLE) *)
by unseal.
- (* (∀ a, bi_persistently (Ψ a)) ⊢ bi_persistently (∀ a, Ψ a) *)
- (* (∀ a, <pers> (Ψ a)) ⊢ <pers> (∀ a, Ψ a) *)
by unseal.
- (* bi_persistently (∃ a, Ψ a) ⊢ ∃ a, bi_persistently (Ψ a) *)
- (* <pers> (∃ a, Ψ a) ⊢ ∃ a, <pers> (Ψ a) *)
by unseal.
- (* bi_persistently P ∗ Q ⊢ bi_persistently P (ADMISSIBLE) *)
- (* <pers> P ∗ Q ⊢ <pers> P (ADMISSIBLE) *)
intros P Q. move: (uPred_persistently P)=> P'.
unseal; split; intros n x ? (x1&x2&?&?&_); ofe_subst;
eauto using uPred_mono, cmra_includedN_l.
- (* bi_persistently P ∧ Q ⊢ P ∗ Q *)
- (* <pers> P ∧ Q ⊢ P ∗ Q *)
intros P Q. unseal; split=> n x ? [??]; simpl in *.
exists (core x), x; rewrite ?cmra_core_l; auto.
Qed.
......@@ -523,9 +523,9 @@ Proof.
- (* ▷ P ∗ ▷ Q ⊢ ▷ (P ∗ Q) *)
intros P Q. unseal; split=> -[|n] x ? /=; [done|intros (x1&x2&Hx&?&?)].
exists x1, x2; eauto using dist_S.
- (* ▷ bi_persistently P ⊢ bi_persistently (▷ P) *)
- (* ▷ <pers> P ⊢ <pers> ▷ P *)
by unseal.
- (* bi_persistently (▷ P) ⊢ ▷ bi_persistently P *)
- (* <pers> ▷ P ⊢ ▷ <pers> P *)
by unseal.
- (* ▷ P ⊢ ▷ False ∨ (▷ False → P) *)
intros P. unseal; split=> -[|n] x ? /= HP; [by left|right].
......@@ -552,13 +552,13 @@ Proof.
unseal; split=> n' x; split; apply HP; eauto using @ucmra_unit_validN.
- (* (P ⊢ Q) → ■ P ⊢ ■ Q *)
intros P QR HP. unseal; split=> n x ? /=. by apply HP, ucmra_unit_validN.
- (* ■ P ⊢ bi_persistently P *)
- (* ■ P ⊢ <pers> P *)
unseal; split; simpl; eauto using uPred_mono, @ucmra_unit_leastN.
- (* ■ P ⊢ ■ ■ P *)
unseal; split=> n x ?? //.
- (* (∀ a, ■ (Ψ a)) ⊢ ■ (∀ a, Ψ a) *)
by unseal.
- (* (■ P → bi_persistently Q) ⊢ bi_persistently (■ P → Q) *)
- (* (■ P → <pers> Q) ⊢ <pers> (■ P → Q) *)
unseal; split=> /= n x ? HPQ n' x' ????.
eapply uPred_mono with n' (core x)=>//; [|by apply cmra_included_includedN].
apply (HPQ n' x); eauto using cmra_validN_le.
......@@ -665,8 +665,7 @@ Proof.
by rewrite (assoc op _ z1) -(comm op z1) (assoc op z1)
-(assoc op _ a2) (comm op z1) -Hy1 -Hy2.
Qed.
Lemma persistently_ownM_core (a : M) :
uPred_ownM a ⊢ bi_persistently (uPred_ownM (core a)).
Lemma persistently_ownM_core (a : M) : uPred_ownM a ⊢ <pers> uPred_ownM (core a).
Proof.
rewrite /bi_persistently /=. unseal.
split=> n x Hx /=. by apply cmra_core_monoN.
......
theories/bi/big_op.v
View file @ 664196f6
......@@ -127,8 +127,7 @@ Section sep_list.
Proof. auto using and_intro, big_sepL_mono, and_elim_l, and_elim_r. Qed.
Lemma big_sepL_persistently `{BiAffine PROP} Φ l :
bi_persistently ([∗ list] k↦x ∈ l, Φ k x) ⊣⊢
[∗ list] k↦x ∈ l, bi_persistently (Φ k x).
<pers> ([∗ list] k↦x ∈ l, Φ k x) ⊣⊢ [∗ list] k↦x ∈ l, <pers> (Φ k x).
Proof. apply (big_opL_commute _). Qed.
Lemma big_sepL_forall `{BiAffine PROP} Φ l :
......@@ -266,8 +265,7 @@ Section and_list.
Proof. auto using and_intro, big_andL_mono, and_elim_l, and_elim_r. Qed.
Lemma big_andL_persistently Φ l :
bi_persistently ([∧ list] k↦x ∈ l, Φ k x) ⊣⊢
[∧ list] k↦x ∈ l, bi_persistently (Φ k x).
<pers> ([∧ list] k↦x ∈ l, Φ k x) ⊣⊢ [∧ list] k↦x ∈ l, <pers> (Φ k x).
Proof. apply (big_opL_commute _). Qed.
Lemma big_andL_forall `{BiAffine PROP} Φ l :
......@@ -398,8 +396,7 @@ Section gmap.
Proof. auto using and_intro, big_sepM_mono, and_elim_l, and_elim_r. Qed.
Lemma big_sepM_persistently `{BiAffine PROP} Φ m :
(bi_persistently ([∗ map] k↦x ∈ m, Φ k x)) ⊣⊢
([∗ map] k↦x ∈ m, bi_persistently (Φ k x)).
(<pers> ([∗ map] k↦x ∈ m, Φ k x)) ⊣⊢ ([∗ map] k↦x ∈ m, <pers> (Φ k x)).
Proof. apply (big_opM_commute _). Qed.
Lemma big_sepM_forall `{BiAffine PROP} Φ m :
......@@ -564,7 +561,7 @@ Section gset.
Proof. auto using and_intro, big_sepS_mono, and_elim_l, and_elim_r. Qed.
Lemma big_sepS_persistently `{BiAffine PROP} Φ X :
bi_persistently ([∗ set] y ∈ X, Φ y) ⊣⊢ [∗ set] y ∈ X, bi_persistently (Φ y).
<pers> ([∗ set] y ∈ X, Φ y) ⊣⊢ [∗ set] y ∈ X, <pers> (Φ y).
Proof. apply (big_opS_commute _). Qed.
Lemma big_sepS_forall `{BiAffine PROP} Φ X :
......@@ -672,8 +669,7 @@ Section gmultiset.
Proof. auto using and_intro, big_sepMS_mono, and_elim_l, and_elim_r. Qed.
Lemma big_sepMS_persistently `{BiAffine PROP} Φ X :
bi_persistently ([∗ mset] y ∈ X, Φ y) ⊣⊢
[∗ mset] y ∈ X, bi_persistently (Φ y).
<pers> ([∗ mset] y ∈ X, Φ y) ⊣⊢ [∗ mset] y ∈ X, <pers> (Φ y).
Proof. apply (big_opMS_commute _). Qed.
Global Instance big_sepMS_empty_persistent Φ :
......
theories/bi/derived_connectives.v
View file @ 664196f6
......@@ -13,7 +13,7 @@ Arguments bi_wand_iff {_} _%I _%I : simpl never.
Instance: Params (@bi_wand_iff) 1.
Infix "∗-∗" := bi_wand_iff (at level 95, no associativity) : bi_scope.
Class Persistent {PROP : bi} (P : PROP) := persistent : P ⊢ bi_persistently P.
Class Persistent {PROP : bi} (P : PROP) := persistent : P ⊢ <pers> P.
Arguments Persistent {_} _%I : simpl never.
Arguments persistent {_} _%I {_}.
Hint Mode Persistent + ! : typeclass_instances.
......@@ -23,7 +23,10 @@ Definition bi_affinely {PROP : bi} (P : PROP) : PROP := (emp ∧ P)%I.
Arguments bi_affinely {_} _%I : simpl never.
Instance: Params (@bi_affinely) 1.
Typeclasses Opaque bi_affinely.
Notation "□ P" := (bi_affinely (bi_persistently P))%I
Notation "'<affine>' P" := (bi_affinely P)
(at level 20, right associativity) : bi_scope.
Notation "□ P" := (<affine> <pers> P)%I
(at level 20, right associativity) : bi_scope.
Class Affine {PROP : bi} (Q : PROP) := affine : Q ⊢ emp.
......@@ -36,31 +39,40 @@ Hint Mode BiAffine ! : typeclass_instances.
Existing Instance absorbing_bi | 0.
Class BiPositive (PROP : bi) :=
bi_positive (P Q : PROP) : bi_affinely (P ∗ Q) ⊢ bi_affinely P ∗ Q.
bi_positive (P Q : PROP) : <affine> (P ∗ Q) ⊢ <affine> P ∗ Q.
Hint Mode BiPositive ! : typeclass_instances.
Definition bi_absorbingly {PROP : bi} (P : PROP) : PROP := (True ∗ P)%I.
Arguments bi_absorbingly {_} _%I : simpl never.
Instance: Params (@bi_absorbingly) 1.
Typeclasses Opaque bi_absorbingly.
Notation "'<absorb>' P" := (bi_absorbingly P)
(at level 20, right associativity) : bi_scope.
Class Absorbing {PROP : bi} (P : PROP) := absorbing : bi_absorbingly P ⊢ P.
Class Absorbing {PROP : bi} (P : PROP) := absorbing : <absorb> P ⊢ P.
Arguments Absorbing {_} _%I : simpl never.
Arguments absorbing {_} _%I.
Hint Mode Absorbing + ! : typeclass_instances.
Definition bi_persistently_if {PROP : bi} (p : bool) (P : PROP) : PROP :=
(if p then bi_persistently P else P)%I.
(if p then <pers> P else P)%I.
Arguments bi_persistently_if {_} !_ _%I /.
Instance: Params (@bi_persistently_if) 2.
Typeclasses Opaque bi_persistently_if.
Notation "'<pers>?' p P" := (bi_persistently_if p P)
(at level 20, p at level 9, P at level 20,
right associativity, format "'<pers>?' p P") : bi_scope.
Definition bi_affinely_if {PROP : bi} (p : bool) (P : PROP) : PROP :=
(if p then bi_affinely P else P)%I.
(if p then <affine> P else P)%I.
Arguments bi_affinely_if {_} !_ _%I /.
Instance: Params (@bi_affinely_if) 2.
Typeclasses Opaque bi_affinely_if.
Notation "□? p P" := (bi_affinely_if p (bi_persistently_if p P))%I
Notation "'<affine>?' p P" := (bi_affinely_if p P)
(at level 20, p at level 9, P at level 20,
right associativity, format "'<affine>?' p P") : bi_scope.
Notation "□? p P" := (<affine>?p <pers>?p P)%I
(at level 20, p at level 9, P at level 20,
right associativity, format "□? p P") : bi_scope.
......
theories/bi/derived_laws.v
View file @ 664196f6
This diff is collapsed.
theories/bi/embedding.v
View file @ 664196f6
......@@ -22,7 +22,7 @@ Record BiEmbedMixin (PROP1 PROP2 : bi) `(Embed PROP1 PROP2) := {
bi_embed_mixin_exist_1 A (Φ : A → PROP1) : ⎡∃ x, Φ x⎤ ⊢ ∃ x, ⎡Φ x⎤;
bi_embed_mixin_sep P Q : ⎡P ∗ Q⎤ ⊣⊢ ⎡P⎤ ∗ ⎡Q⎤;
bi_embed_mixin_wand_2 P Q : (⎡P⎤ -∗ ⎡Q⎤) ⊢ ⎡P -∗ Q⎤;
bi_embed_mixin_persistently P : ⎡bi_persistently P⎤ ⊣⊢ bi_persistently ⎡P⎤
bi_embed_mixin_persistently P : ⎡<pers> P⎤ ⊣⊢ <pers> ⎡P⎤
}.
Class BiEmbed (PROP1 PROP2 : bi) := {
......@@ -79,7 +79,7 @@ Section embed_laws.
Proof. eapply bi_embed_mixin_sep, bi_embed_mixin. Qed.
Lemma embed_wand_2 P Q : (⎡P⎤ -∗ ⎡Q⎤) ⊢ ⎡P -∗ Q⎤.
Proof. eapply bi_embed_mixin_wand_2, bi_embed_mixin. Qed.
Lemma embed_persistently P : ⎡bi_persistently P⎤ ⊣⊢ bi_persistently ⎡P⎤.
Lemma embed_persistently P : ⎡<pers> P⎤ ⊣⊢ <pers> ⎡P⎤.
Proof. eapply bi_embed_mixin_persistently, bi_embed_mixin. Qed.
End embed_laws.
......@@ -141,14 +141,13 @@ Section embed.
Proof. by rewrite embed_and !embed_impl. Qed.
Lemma embed_wand_iff P Q : ⎡P ∗-∗ Q⎤ ⊣⊢ (⎡P⎤ ∗-∗ ⎡Q⎤).
Proof. by rewrite embed_and !embed_wand. Qed.
Lemma embed_affinely P : ⎡bi_affinely P⎤ ⊣⊢ bi_affinely ⎡P⎤.
Lemma embed_affinely P : ⎡<affine> P⎤ ⊣⊢ <affine> ⎡P⎤.
Proof. by rewrite embed_and embed_emp. Qed.
Lemma embed_absorbingly P : ⎡bi_absorbingly P⎤ ⊣⊢ bi_absorbingly ⎡P⎤.
Lemma embed_absorbingly P : ⎡<absorb> P⎤ ⊣⊢ <absorb> ⎡P⎤.
Proof. by rewrite embed_sep embed_pure. Qed.
Lemma embed_persistently_if P b :
⎡bi_persistently_if b P⎤ ⊣⊢ bi_persistently_if b ⎡P⎤.
Lemma embed_persistently_if P b : ⎡<pers>?b P⎤ ⊣⊢ <pers>?b ⎡P⎤.
Proof. destruct b; simpl; auto using embed_persistently. Qed.
Lemma embed_affinely_if P b : ⎡bi_affinely_if b P⎤ ⊣⊢ bi_affinely_if b ⎡P⎤.
Lemma embed_affinely_if P b : ⎡<affine>?b P⎤ ⊣⊢ <affine>?b ⎡P⎤.
Proof. destruct b; simpl; auto using embed_affinely. Qed.
Lemma embed_hforall {As} (Φ : himpl As PROP1):
⎡bi_hforall Φ⎤ ⊣⊢ bi_hforall (hcompose embed Φ).
......@@ -233,6 +232,6 @@ End sbi_embed.
(* Not defined using an ordinary [Instance] because the default
[class_apply @bi_embed_plainly] shelves the [BiPlainly] premise, making proof
search for the other premises fail. See the proof of [monPred_absolutely_plain]
search for the other premises fail. See the proof of [monPred_objectively_plain]
for an example where it would fail with a regular [Instance].*)
Hint Extern 4 (Plain ⎡_⎤) => eapply @embed_plain : typeclass_instances.
theories/bi/fixpoint.v
View file @ 664196f6
......@@ -6,7 +6,7 @@ Import bi.
(** Least and greatest fixpoint of a monotone function, defined entirely inside
the logic. *)
Class BiMonoPred {PROP : bi} {A : ofeT} (F : (A → PROP) → (A → PROP)) := {
bi_mono_pred Φ Ψ : ((bi_persistently (∀ x, Φ x -∗ Ψ x)) → ∀ x, F Φ x -∗ F Ψ x)%I;
bi_mono_pred Φ Ψ : (<pers> (∀ x, Φ x -∗ Ψ x) → ∀ x, F Φ x -∗ F Ψ x)%I;
bi_mono_pred_ne Φ : NonExpansive Φ → NonExpansive (F Φ)
}.
Arguments bi_mono_pred {_ _ _ _} _ _.
......@@ -14,11 +14,11 @@ Local Existing Instance bi_mono_pred_ne.
Definition bi_least_fixpoint {PROP : bi} {A : ofeT}
(F : (A → PROP) → (A → PROP)) (x : A) : PROP :=
(∀ Φ : A -n> PROP, bi_persistently (∀ x, F Φ x -∗ Φ x) → Φ x)%I.
(∀ Φ : A -n> PROP, <pers> (∀ x, F Φ x -∗ Φ x) → Φ x)%I.
Definition bi_greatest_fixpoint {PROP : bi} {A : ofeT}
(F : (A → PROP) → (A → PROP)) (x : A) : PROP :=
(∃ Φ : A -n> PROP, bi_persistently (∀ x, Φ x -∗ F Φ x) ∧ Φ x)%I.
(∃ Φ : A -n> PROP, <pers> (∀ x, Φ x -∗ F Φ x) ∧ Φ x)%I.
Section least.
Context {PROP : bi} {A : ofeT} (F : (A → PROP) → (A → PROP)) `{!BiMonoPred F}.
......
theories/bi/interface.v
View file @ 664196f6
......@@ -6,6 +6,7 @@ Reserved Notation "'emp'".
Reserved Notation "'⌜' φ '⌝'" (at level 1, φ at level 200, format "⌜ φ ⌝").
Reserved Notation "P ∗ Q" (at level 80, right associativity).
Reserved Notation "P -∗ Q" (at level 99, Q at level 200, right associativity).
Reserved Notation "'<pers>' P" (at level 20, right associativity).
Reserved Notation "▷ P" (at level 20, right associativity).
Section bi_mixin.
......@@ -38,6 +39,7 @@ Section bi_mixin.
(bi_exist _ (λ x, .. (bi_exist _ (λ y, P)) ..)).
Local Infix "∗" := bi_sep.
Local Infix "-∗" := bi_wand.
Local Notation "'<pers>' P" := (bi_persistently P).
Local Notation "x ≡ y" := (sbi_internal_eq _ x y).
Local Notation "▷ P" := (sbi_later P).
......@@ -102,27 +104,23 @@ Section bi_mixin.
(* Persistently *)
(* In the ordered RA model: Holds without further assumptions. *)
bi_mixin_persistently_mono P Q :
(P ⊢ Q) → bi_persistently P ⊢ bi_persistently Q;
bi_mixin_persistently_mono P Q : (P ⊢ Q) → <pers> P ⊢ <pers> Q;
(* In the ordered RA model: `core` is idempotent *)
bi_mixin_persistently_idemp_2 P :
bi_persistently P ⊢ bi_persistently (bi_persistently P);
bi_mixin_persistently_idemp_2 P : <pers> P ⊢ <pers> <pers> P;
(* In the ordered RA model: `ε ≼ core x` *)
bi_mixin_persistently_emp_intro P : P ⊢ bi_persistently emp;
bi_mixin_persistently_emp_intro P : P ⊢ <pers> emp;
bi_mixin_persistently_forall_2 {A} (Ψ : A → PROP) :
(∀ a, bi_persistently (Ψ a)) ⊢ bi_persistently (∀ a, Ψ a);
(∀ a, <pers> (Ψ a)) ⊢ <pers> (∀ a, Ψ a);
bi_mixin_persistently_exist_1 {A} (Ψ : A → PROP) :
bi_persistently (∃ a, Ψ a) ⊢ ∃ a, bi_persistently (Ψ a);
<pers> (∃ a, Ψ a) ⊢ ∃ a, <pers> (Ψ a);
(* In the ordered RA model: [core x ≼ core (x ⋅ y)].
Note that this implies that the core is monotone. *)
bi_mixin_persistently_absorbing P Q :
bi_persistently P ∗ Q ⊢ bi_persistently P;
bi_mixin_persistently_absorbing P Q : <pers> P ∗ Q ⊢ <pers> P;
(* In the ordered RA model: [x ⋅ core x = core x]. *)
bi_mixin_persistently_and_sep_elim P Q :
bi_persistently P ∧ Q ⊢ P ∗ Q;
bi_mixin_persistently_and_sep_elim P Q : <pers> P ∧ Q ⊢ P ∗ Q;
}.
Record SbiMixin := {
......@@ -149,10 +147,8 @@ Section bi_mixin.
(▷ ∃ a, Φ a) ⊢ ▷ False ∨ (∃ a, ▷ Φ a);
sbi_mixin_later_sep_1 P Q : ▷ (P ∗ Q) ⊢ ▷ P ∗ ▷ Q;
sbi_mixin_later_sep_2 P Q : ▷ P ∗ ▷ Q ⊢ ▷ (P ∗ Q);
sbi_mixin_later_persistently_1 P :
▷ bi_persistently P ⊢ bi_persistently (▷ P);
sbi_mixin_later_persistently_2 P :
bi_persistently (▷ P) ⊢ ▷ bi_persistently P;
sbi_mixin_later_persistently_1 P : ▷ <pers> P ⊢ <pers> ▷ P;
sbi_mixin_later_persistently_2 P : <pers> ▷ P ⊢ ▷ <pers> P;
sbi_mixin_later_false_em P : ▷ P ⊢ ▷ False ∨ (▷ False → P);
}.
......@@ -292,6 +288,7 @@ Notation "∀ x .. y , P" :=
(bi_forall (λ x, .. (bi_forall (λ y, P)) ..)%I) : bi_scope.
Notation "∃ x .. y , P" :=
(bi_exist (λ x, .. (bi_exist (λ y, P)) ..)%I) : bi_scope.
Notation "'<pers>' P" := (bi_persistently P) : bi_scope.
Infix "≡" := sbi_internal_eq : bi_scope.
Notation "▷ P" := (sbi_later P) : bi_scope.
......@@ -391,25 +388,24 @@ Lemma wand_elim_l' P Q R : (P ⊢ Q -∗ R) → P ∗ Q ⊢ R.
Proof. eapply bi_mixin_wand_elim_l', bi_bi_mixin. Qed.
(* Persistently *)
Lemma persistently_mono P Q : (P ⊢ Q) → bi_persistently P ⊢ bi_persistently Q.
Lemma persistently_mono P Q : (P ⊢ Q) → <pers> P ⊢ <pers> Q.
Proof. eapply bi_mixin_persistently_mono, bi_bi_mixin. Qed.
Lemma persistently_idemp_2 P :
bi_persistently P ⊢ bi_persistently (bi_persistently P).
Lemma persistently_idemp_2 P : <pers> P ⊢ <pers> <pers> P.
Proof. eapply bi_mixin_persistently_idemp_2, bi_bi_mixin. Qed.
Lemma persistently_emp_intro P : P ⊢ bi_persistently emp.
Lemma persistently_emp_intro P : P ⊢ <pers> emp.
Proof. eapply bi_mixin_persistently_emp_intro, bi_bi_mixin. Qed.
Lemma persistently_forall_2 {A} (Ψ : A → PROP) :
(∀ a, bi_persistently (Ψ a)) ⊢ bi_persistently (∀ a, Ψ a).
(∀ a, <pers> (Ψ a)) ⊢ <pers> (∀ a, Ψ a).
Proof. eapply bi_mixin_persistently_forall_2, bi_bi_mixin. Qed.
Lemma persistently_exist_1 {A} (Ψ : A → PROP) :
bi_persistently (∃ a, Ψ a) ⊢ ∃ a, bi_persistently (Ψ a).
<pers> (∃ a, Ψ a) ⊢ ∃ a, <pers> (Ψ a).
Proof. eapply bi_mixin_persistently_exist_1, bi_bi_mixin. Qed.
Lemma persistently_absorbing P Q : bi_persistently P ∗ Q ⊢ bi_persistently P.
Lemma persistently_absorbing P Q : <pers> P ∗ Q ⊢ <pers> P.
Proof. eapply (bi_mixin_persistently_absorbing bi_entails), bi_bi_mixin. Qed.
Lemma persistently_and_sep_elim P Q : bi_persistently P ∧ Q ⊢ P ∗ Q.
Lemma persistently_and_sep_elim P Q : <pers> P ∧ Q ⊢ P ∗ Q.
Proof. eapply (bi_mixin_persistently_and_sep_elim bi_entails), bi_bi_mixin. Qed.
End bi_laws.
......@@ -459,9 +455,9 @@ Lemma later_sep_1 P Q : ▷ (P ∗ Q) ⊢ ▷ P ∗ ▷ Q.
Proof. eapply sbi_mixin_later_sep_1, sbi_sbi_mixin. Qed.
Lemma later_sep_2 P Q : ▷ P ∗ ▷ Q ⊢ ▷ (P ∗ Q).
Proof. eapply sbi_mixin_later_sep_2, sbi_sbi_mixin. Qed.
Lemma later_persistently_1 P : ▷ bi_persistently P ⊢ bi_persistently (▷ P).
Lemma later_persistently_1 P : ▷ <pers> P ⊢ <pers> ▷ P.
Proof. eapply (sbi_mixin_later_persistently_1 bi_entails), sbi_sbi_mixin. Qed.
Lemma later_persistently_2 P : bi_persistently (▷ P) ⊢ ▷ bi_persistently P.
Lemma later_persistently_2 P : <pers> ▷ P ⊢ ▷ <pers> P.
Proof. eapply (sbi_mixin_later_persistently_2 bi_entails), sbi_sbi_mixin. Qed.
Lemma later_false_em P : ▷ P ⊢ ▷ False ∨ (▷ False → P).
......
theories/bi/monpred.v
View file @ 664196f6
This diff is collapsed.
theories/bi/plainly.v
View file @ 664196f6
......@@ -13,7 +13,7 @@ Record BiPlainlyMixin (PROP : sbi) `(Plainly PROP) := {
bi_plainly_mixin_plainly_ne : NonExpansive plainly;
bi_plainly_mixin_plainly_mono P Q : (P ⊢ Q) → ■ P ⊢ ■ Q;
bi_plainly_mixin_plainly_elim_persistently P : ■ P ⊢ bi_persistently P;
bi_plainly_mixin_plainly_elim_persistently P : ■ P ⊢ <pers> P;
bi_plainly_mixin_plainly_idemp_2 P : ■ P ⊢ ■ ■ P;
bi_plainly_mixin_plainly_forall_2 {A} (Ψ : A → PROP) :
......@@ -23,7 +23,7 @@ Record BiPlainlyMixin (PROP : sbi) `(Plainly PROP) := {
for persistently and plainly, but for any modality defined as `M P n x :=
∀ y, R x y → P n y`. *)
bi_plainly_mixin_persistently_impl_plainly P Q :
(■ P → bi_persistently Q) ⊢ bi_persistently (■ P → Q);
(■ P → <pers> Q) ⊢ <pers> (■ P → Q);
bi_plainly_mixin_plainly_impl_plainly P Q : (■ P → ■ Q) ⊢ ■ (■ P → Q);
bi_plainly_mixin_plainly_emp_intro P : P ⊢ ■ emp;
......@@ -59,14 +59,13 @@ Section plainly_laws.
Lemma plainly_mono P Q : (P ⊢ Q) → ■ P ⊢ ■ Q.
Proof. eapply bi_plainly_mixin_plainly_mono, bi_plainly_mixin. Qed.
Lemma plainly_elim_persistently P : ■ P ⊢ bi_persistently P.
Lemma plainly_elim_persistently P : ■ P ⊢ <pers> P.
Proof. eapply bi_plainly_mixin_plainly_elim_persistently, bi_plainly_mixin. Qed.
Lemma plainly_idemp_2 P : ■ P ⊢ ■ ■ P.
Proof. eapply bi_plainly_mixin_plainly_idemp_2, bi_plainly_mixin. Qed.
Lemma plainly_forall_2 {A} (Ψ : A → PROP) : (∀ a, ■ (Ψ a)) ⊢ ■ (∀ a, Ψ a).
Proof. eapply bi_plainly_mixin_plainly_forall_2, bi_plainly_mixin. Qed.
Lemma persistently_impl_plainly P Q :
(■ P → bi_persistently Q) ⊢ bi_persistently (■ P → Q).
Lemma persistently_impl_plainly P Q : (■ P → <pers> Q) ⊢ <pers> (■ P → Q).
Proof. eapply bi_plainly_mixin_persistently_impl_plainly, bi_plainly_mixin. Qed.
Lemma plainly_impl_plainly P Q : (■ P → ■ Q) ⊢ ■ (■ P → Q).
Proof. eapply bi_plainly_mixin_plainly_impl_plainly, bi_plainly_mixin. Qed.
......@@ -119,19 +118,19 @@ Global Instance plainly_flip_mono' :
Proper (flip (⊢) ==> flip (⊢)) (@plainly PROP _).
Proof. intros P Q; apply plainly_mono. Qed.
Lemma affinely_plainly_elim P : bi_affinely (■ P) ⊢ P.
Lemma affinely_plainly_elim P : <affine> ■ P ⊢ P.
Proof. by rewrite plainly_elim_persistently affinely_persistently_elim. Qed.
Lemma persistently_plainly P : bi_persistently (■ P) ⊣⊢ ■ P.
Lemma persistently_plainly P : <pers> ■ P ⊣⊢ ■ P.
Proof.
apply (anti_symm _).
- by rewrite persistently_elim_absorbingly /bi_absorbingly comm plainly_absorb.
- by rewrite {1}plainly_idemp_2 plainly_elim_persistently.
Qed.
Lemma persistently_if_plainly P p : bi_persistently_if p (■ P) ⊣⊢ ■ P.
Lemma persistently_if_plainly P p : <pers>?p ■ P ⊣⊢ ■ P.
Proof. destruct p; last done. exact: persistently_plainly. Qed.
Lemma plainly_persistently P : ■ (bi_persistently P) ⊣⊢ ■ P.
Lemma plainly_persistently P : ■ <pers> P ⊣⊢ ■ P.
Proof.
apply (anti_symm _).
- rewrite -{1}(left_id True%I bi_and (■ _)%I) (plainly_emp_intro True%I).
......@@ -140,7 +139,7 @@ Proof.
- by rewrite {1}plainly_idemp_2 (plainly_elim_persistently P).
Qed.
Lemma absorbingly_plainly P : bi_absorbingly (■ P) ⊣⊢ ■ P.
Lemma absorbingly_plainly P : <absorb> ■ P ⊣⊢ ■ P.
Proof. by rewrite -(persistently_plainly P) absorbingly_persistently. Qed.
Lemma plainly_and_sep_elim P Q : ■ P ∧ Q -∗ (emp ∧ P) ∗ Q.
......@@ -149,7 +148,7 @@ Lemma plainly_and_sep_assoc P Q R : ■ P ∧ (Q ∗ R) ⊣⊢ (■ P ∧ Q) ∗
Proof. by rewrite -(persistently_plainly P) persistently_and_sep_assoc. Qed.
Lemma plainly_and_emp_elim P : emp ∧ ■ P ⊢ P.
Proof. by rewrite plainly_elim_persistently persistently_and_emp_elim. Qed.
Lemma plainly_elim_absorbingly P : ■ P ⊢ bi_absorbingly P.
Lemma plainly_elim_absorbingly P : ■ P ⊢ <absorb> P.
Proof. by rewrite plainly_elim_persistently persistently_elim_absorbingly. Qed.
Lemma plainly_elim P `{!Absorbing P} : ■ P ⊢ P.
Proof. by rewrite plainly_elim_persistently persistently_elim. Qed.
......@@ -214,7 +213,7 @@ Proof.
by rewrite plainly_and_sep_assoc (comm bi_and) plainly_and_emp_elim.
Qed.
Lemma plainly_affinely P : ■ (bi_affinely P) ⊣⊢ ■ P.
Lemma plainly_affinely P : ■ <affine> P ⊣⊢ ■ P.
Proof. by rewrite /bi_affinely plainly_and -plainly_True_emp plainly_pure left_id. Qed.
Lemma and_sep_plainly P Q : ■ P ∧ ■ Q ⊣⊢ ■ P ∗ ■ Q.
......@@ -252,7 +251,7 @@ Qed.
Lemma impl_wand_plainly_2 P Q : (■ P -∗ Q) ⊢ (■ P → Q).
Proof. apply impl_intro_l. by rewrite plainly_and_sep_l_1 wand_elim_r. Qed.
Lemma impl_wand_affinely_plainly P Q : (■ P → Q) ⊣⊢ (bi_affinely (■ P) -∗ Q).
Lemma impl_wand_affinely_plainly P Q : (■ P → Q) ⊣⊢ (<affine> ■ P -∗ Q).
Proof. by rewrite -(persistently_plainly P) impl_wand_affinely_persistently. Qed.
Section plainly_affine_bi.
......@@ -351,7 +350,7 @@ Proof. by rewrite /Persistent persistently_plainly. Qed.
Global Instance wand_persistent P Q :
Plain P → Persistent Q → Absorbing Q → Persistent (P -∗ Q).
Proof.
intros. rewrite /Persistent {2}(plain P). trans (bi_persistently (■ P → Q)%I).
intros. rewrite /Persistent {2}(plain P). trans (<pers> (■ P → Q))%I.
- rewrite -persistently_impl_plainly impl_wand_affinely_plainly -(persistent Q).
by rewrite affinely_plainly_elim.
- apply persistently_mono, wand_intro_l. by rewrite sep_and impl_elim_r.
......@@ -428,13 +427,13 @@ Proof. intros. by rewrite /Plain -plainly_sep_2 -!plain. Qed.
Global Instance plainly_plain P : Plain (■ P).
Proof. by rewrite /Plain plainly_idemp. Qed.
Global Instance persistently_plain P : Plain P → Plain (bi_persistently P).
Global Instance persistently_plain P : Plain P → Plain (<pers> P).
Proof.
rewrite /Plain=> HP. rewrite {1}HP plainly_persistently persistently_plainly //.
Qed.
Global Instance affinely_plain P : Plain P → Plain (bi_affinely P).
Global Instance affinely_plain P : Plain P → Plain (<affine> P).
Proof. rewrite /bi_affinely. apply _. Qed.
Global Instance absorbingly_plain P : Plain P → Plain (bi_absorbingly P).
Global Instance absorbingly_plain P : Plain P → Plain (<absorb> P).
Proof. rewrite /bi_absorbingly. apply _. Qed.
Global Instance from_option_plain {A} P (Ψ : A → PROP) (mx : option A) :
(∀ x, Plain (Ψ x)) → Plain P → Plain (from_option Ψ P mx).
......@@ -449,7 +448,7 @@ Proof.
rewrite -(internal_eq_refl True%I a) plainly_pure; auto.
Qed.
Lemma plainly_alt P : ■ P ⊣⊢ bi_affinely P ≡ emp.
Lemma plainly_alt P : ■ P ⊣⊢ <affine> P ≡ emp.
Proof.
rewrite -plainly_affinely. apply (anti_symm (⊢)).
- rewrite -prop_ext. apply plainly_mono, and_intro; apply wand_intro_l.
......
theories/program_logic/total_adequacy.v
View file @ 664196f6
......@@ -17,7 +17,7 @@ Definition twptp_pre (twptp : list (expr Λ) → iProp Σ)
state_interp σ1 ={⊤}=∗ state_interp σ2 ∗ twptp t2)%I.
Lemma twptp_pre_mono (twptp1 twptp2 : list (expr Λ) → iProp Σ) :
((bi_persistently (∀ t, twptp1 t -∗ twptp2 t)) →
(<pers> (∀ t, twptp1 t -∗ twptp2 t) →
∀ t, twptp_pre twptp1 t -∗ twptp_pre twptp2 t)%I.