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

Drop positivity axiom of the BI canonical structure.

The absence of this axiom has two consequences:

- We no longer have `■ (P ∗ Q) ⊢ ■ P ∗ ■ Q` and `□ (P ∗ Q) ⊢ □ P ∗ □ Q`,
  and as a result, separating conjunctions in the unrestricted/persistent
  context cannot be eliminated.
- When having `(P -∗ ⬕ Q) ∗ P`, we do not get `⬕ Q ∗ P`. In the proof
  mode this means when having:

    H1 : P -∗ ⬕ Q
    H2 : P

  We cannot say `iDestruct ("H1" with "H2") as "#H1"` and keep `H2`.

However, there is now a type class `PositiveBI PROP`, and when there is an
instance of this type class, one gets the above reasoning principle back.

TODO: Can we describe positivity of individual propositions instead of the
whole BI? That way, we would get the above reasoning principles even when
the BI is not positive, but the propositions involved are.
parent 96501a4f
......@@ -185,8 +185,8 @@ Section proofmode_classes.
Context `{inG Σ A}.
Implicit Types a b : A.
Global Instance into_sep_own p γ a b1 b2 :
IsOp a b1 b2 IntoSep p (own γ a) (own γ b1) (own γ b2).
Global Instance into_sep_own γ a b1 b2 :
IsOp a b1 b2 IntoSep (own γ a) (own γ b1) (own γ b2).
Proof. intros. by rewrite /IntoSep (is_op a) own_op. Qed.
Global Instance into_and_own p γ a b1 b2 :
IsOp a b1 b2 IntoAnd p (own γ a) (own γ b1) (own γ b2).
......
......@@ -88,8 +88,8 @@ Proof.
intros. apply bare_persistently_if_mono. by rewrite (is_op a) ownM_op sep_and.
Qed.
Global Instance into_sep_ownM p (a b1 b2 : M) :
IsOp a b1 b2 IntoSep p (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
Global Instance into_sep_ownM (a b1 b2 : M) :
IsOp a b1 b2 IntoSep (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
Proof. intros. by rewrite /IntoSep (is_op a) ownM_op. Qed.
Global Instance from_sep_bupd P Q1 Q2 :
......
......@@ -438,9 +438,6 @@ 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.
- (* emp ∧ (Q ∗ R) ⊢ (emp ∧ Q) ∗ R (ADMISSIBLE) *)
intros Q R. unfold uPred_emp; unseal; split; intros n x ? [_ (x1&x2&?&?&?)].
exists x1, x2; simpl; auto.
- (* (P ⊢ Q) → □ P ⊢ □ Q *)
intros P QR HP. unseal; split=> n x ? /=. by apply HP, cmra_core_validN.
- (* □ P ⊢ □ □ P *)
......
This diff is collapsed.
......@@ -131,14 +131,14 @@ Section fractional.
FromSep Q P P.
Proof. rewrite /FromSep=>-[-> <-] [-> _]. by rewrite Qp_div_2. Qed.
Global Instance into_sep_fractional p P P1 P2 Φ q1 q2 :
Global Instance into_sep_fractional P P1 P2 Φ q1 q2 :
AsFractional P Φ (q1 + q2) AsFractional P1 Φ q1 AsFractional P2 Φ q2
IntoSep p P P1 P2.
IntoSep P P1 P2.
Proof. intros. rewrite /IntoSep [P]fractional_split //. Qed.
Global Instance into_sep_fractional_half p P Q Φ q :
Global Instance into_sep_fractional_half P Q Φ q :
AsFractional P Φ q AsFractional Q Φ (q/2)
IntoSep p P Q Q | 100.
IntoSep P Q Q | 100.
Proof. intros. rewrite /IntoSep [P]fractional_half //. Qed.
(* The instance [frame_fractional] can be tried at all the nodes of
......
......@@ -99,8 +99,6 @@ Section bi_mixin.
bi_mixin_wand_intro_r P Q R : (P Q R) P Q - R;
bi_mixin_wand_elim_l' P Q R : (P Q - R) P Q R;
bi_mixin_emp_and_sep_assoc_1 Q R : emp (Q R) (emp Q) R;
(* Persistently *)
bi_mixin_persistently_mono P Q : (P Q) P Q;
bi_mixin_persistently_idemp_2 P : P P;
......@@ -401,9 +399,6 @@ Proof. eapply bi_mixin_wand_intro_r, bi_bi_mixin. Qed.
Lemma wand_elim_l' P Q R : (P Q - R) P Q R.
Proof. eapply bi_mixin_wand_elim_l', bi_bi_mixin. Qed.
Lemma emp_and_sep_assoc_1 Q R : emp (Q R) (emp Q) R.
Proof. eapply bi_mixin_emp_and_sep_assoc_1, bi_bi_mixin. Qed.
(* Persistently *)
Lemma persistently_mono P Q : (P Q) P Q.
Proof. eapply bi_mixin_persistently_mono, bi_bi_mixin. Qed.
......
......@@ -185,8 +185,8 @@ Global Instance into_wand_impl_true_true P Q P' :
FromAssumption true P P' IntoWand true true (P' Q) P Q.
Proof.
rewrite /FromAssumption /IntoWand /= => <-. apply wand_intro_l.
rewrite -{1}(bare_persistently_idemp P) -bare_persistently_sep -persistently_and_sep.
by rewrite impl_elim_r bare_persistently_elim.
rewrite -{1}(bare_persistently_idemp P) -and_sep_bare_persistently.
by rewrite -bare_persistently_and impl_elim_r bare_persistently_elim.
Qed.
Global Instance into_wand_and_l p q R1 R2 P' Q' :
......@@ -266,10 +266,10 @@ Proof. by rewrite /FromSep pure_and sep_and. Qed.
Global Instance from_sep_bare P Q1 Q2 :
FromSep P Q1 Q2 FromSep ( P) ( Q1) ( Q2).
Proof. rewrite /FromSep=> <-. by rewrite bare_sep. Qed.
Proof. rewrite /FromSep=> <-. by rewrite bare_sep_2. Qed.
Global Instance from_sep_persistently P Q1 Q2 :
FromSep P Q1 Q2 FromSep ( P) ( Q1) ( Q2).
Proof. rewrite /FromSep=> <-. by rewrite persistently_sep. Qed.
Proof. rewrite /FromSep=> <-. by rewrite persistently_sep_2. Qed.
Global Instance from_sep_big_sepL_cons {A} (Φ : nat A PROP) x l :
FromSep ([ list] k y x :: l, Φ k y) (Φ 0 x) ([ list] k y l, Φ (S k) y).
......@@ -282,11 +282,8 @@ Proof. by rewrite /FromSep big_opL_app. Qed.
(* IntoAnd *)
Global Instance into_and_and p P Q : IntoAnd p (P Q) P Q.
Proof. by rewrite /IntoAnd bare_persistently_if_and. Qed.
Global Instance into_and_sep P Q : IntoAnd true (P Q) P Q.
Proof.
by rewrite /IntoAnd /= bare_persistently_sep -bare_persistently_sep
persistently_and_sep.
Qed.
Global Instance into_and_sep `{PositiveBI PROP} P Q : IntoAnd true (P Q) P Q.
Proof. by rewrite /IntoAnd /= persistently_sep -and_sep_persistently persistently_and. Qed.
Global Instance into_and_pure p φ ψ : @IntoAnd PROP p ⌜φ ψ⌝ ⌜φ⌝ ⌜ψ⌝.
Proof. by rewrite /IntoAnd pure_and bare_persistently_if_and. Qed.
......@@ -307,55 +304,44 @@ Proof.
Qed.
(* IntoSep *)
Global Instance into_sep_sep p P Q : IntoSep p (P Q) P Q.
Proof. by rewrite /IntoSep bare_persistently_if_sep. Qed.
Global Instance into_sep_and P Q : IntoSep true (P Q) P Q.
Proof. by rewrite /IntoSep /= persistently_and_sep. Qed.
Global Instance into_sep_sep P Q : IntoSep (P Q) P Q.
Proof. by rewrite /IntoSep. Qed.
Global Instance into_sep_and_persistent_l P P' Q :
Persistent P FromBare P' P IntoSep false (P Q) P' Q.
Persistent P FromBare P' P IntoSep (P Q) P' Q.
Proof.
rewrite /FromBare /IntoSep /=. intros ? <-.
by rewrite persistent_and_bare_sep_l_1.
Qed.
Global Instance into_sep_and_persistent_r P Q Q' :
Persistent Q FromBare Q' Q IntoSep false (P Q) P Q'.
Persistent Q FromBare Q' Q IntoSep (P Q) P Q'.
Proof.
rewrite /FromBare /IntoSep /=. intros ? <-.
by rewrite persistent_and_bare_sep_r_1.
Qed.
Global Instance into_sep_pure p φ ψ : @IntoSep PROP p ⌜φ ψ⌝ ⌜φ⌝ ⌜ψ⌝.
Proof.
by rewrite /IntoSep pure_and persistent_and_sep_1 bare_persistently_if_sep.
Qed.
Global Instance into_sep_bare p P Q1 Q2 :
IntoSep p P Q1 Q2 IntoSep p ( P) ( Q1) ( Q2).
Proof.
rewrite /IntoSep /=. destruct p; simpl.
- by rewrite -bare_sep !persistently_bare.
- intros ->. by rewrite bare_sep.
Qed.
Global Instance into_sep_persistently p P Q1 Q2 :
IntoSep p P Q1 Q2 IntoSep p ( P) ( Q1) ( Q2).
Proof.
rewrite /IntoSep /=. destruct p; simpl.
- by rewrite -persistently_sep !persistently_idemp.
- intros ->. by rewrite persistently_sep.
Qed.
Global Instance into_sep_pure φ ψ : @IntoSep PROP ⌜φ ψ⌝ ⌜φ⌝ ⌜ψ⌝.
Proof. by rewrite /IntoSep pure_and persistent_and_sep_1. Qed.
Global Instance into_sep_bare `{PositiveBI PROP} P Q1 Q2 :
IntoSep P Q1 Q2 IntoSep ( P) ( Q1) ( Q2).
Proof. rewrite /IntoSep /= => ->. by rewrite bare_sep. Qed.
Global Instance into_sep_persistently `{PositiveBI PROP} P Q1 Q2 :
IntoSep P Q1 Q2 IntoSep ( P) ( Q1) ( Q2).
Proof. rewrite /IntoSep /= => ->. by rewrite persistently_sep. Qed.
(* We use [IsCons] and [IsApp] to make sure that [frame_big_sepL_cons] and
[frame_big_sepL_app] cannot be applied repeatedly often when having
[ [∗ list] k ↦ x ∈ ?e, Φ k x] with [?e] an evar. *)
Global Instance into_sep_big_sepL_cons {A} p (Φ : nat A PROP) l x l' :
Global Instance into_sep_big_sepL_cons {A} (Φ : nat A PROP) l x l' :
IsCons l x l'
IntoSep p ([ list] k y l, Φ k y)
IntoSep ([ list] k y l, Φ k y)
(Φ 0 x) ([ list] k y l', Φ (S k) y).
Proof. rewrite /IsCons=>->. by rewrite /IntoSep big_sepL_cons. Qed.
Global Instance into_sep_big_sepL_app {A} p (Φ : nat A PROP) l l1 l2 :
Global Instance into_sep_big_sepL_app {A} (Φ : nat A PROP) l l1 l2 :
IsApp l l1 l2
IntoSep p ([ list] k y l, Φ k y)
IntoSep ([ list] k y l, Φ k y)
([ list] k y l1, Φ k y) ([ list] k y l2, Φ (length l1 + k) y).
Proof. rewrite /IsApp=>->. by rewrite /IntoSep big_sepL_app. Qed.
......@@ -499,7 +485,7 @@ Global Instance frame_sep_persistent_l R P1 P2 Q1 Q2 Q' :
Frame true R (P1 P2) Q' | 9.
Proof.
rewrite /Frame /MaybeFrame /MakeSep /= => <- <- <-.
rewrite {1}(persistently_sep_dup R) bare_sep. solve_sep_entails.
rewrite {1}(bare_persistently_sep_dup R). solve_sep_entails.
Qed.
Global Instance frame_sep_l R P1 P2 Q Q' :
Frame false R P1 Q MakeSep Q P2 Q' Frame false R (P1 P2) Q' | 9.
......@@ -602,7 +588,10 @@ Proof. by rewrite /MakeBare. Qed.
Global Instance frame_bare R P Q Q' :
Frame true R P Q MakeBare Q Q' Frame true R ( P) Q'.
Proof. rewrite /Frame /MakeBare=> <- <- /=. by rewrite bare_sep bare_idemp. Qed.
Proof.
rewrite /Frame /MakeBare=> <- <- /=.
by rewrite -{1}bare_idemp bare_sep_2.
Qed.
Class MakePersistently (P Q : PROP) := make_persistently : P Q.
Arguments MakePersistently _%I _%I.
......@@ -616,9 +605,9 @@ Proof. by rewrite /MakePersistently. Qed.
Global Instance frame_persistently R P Q Q' :
Frame true R P Q MakePersistently Q Q' Frame true R ( P) Q'.
Proof.
rewrite /Frame /MakePersistently=> <- <- /=.
by rewrite -persistently_and_bare_sep_l persistently_sep persistently_bare
persistently_idemp -persistently_and_sep_l_1.
rewrite /Frame /MakePersistently=> <- <- /=. rewrite -persistently_and_bare_sep_l.
by rewrite -persistently_sep_2 -persistently_and_sep_l_1 persistently_bare
persistently_idemp.
Qed.
Global Instance frame_exist {A} p R (Φ Ψ : A PROP) :
......@@ -722,24 +711,15 @@ Proof.
Qed.
(* IntoSep *)
Global Instance into_sep_later p P Q1 Q2 :
IntoSep p P Q1 Q2 IntoSep p ( P) ( Q1) ( Q2).
Proof.
rewrite /IntoSep=> HP. apply bare_persistently_if_intro'.
by rewrite bare_persistently_if_later HP bare_persistently_if_elim later_sep.
Qed.
Global Instance into_sep_laterN n p P Q1 Q2 :
IntoSep p P Q1 Q2 IntoSep p (^n P) (^n Q1) (^n Q2).
Proof.
rewrite /IntoSep=> HP. apply bare_persistently_if_intro'.
by rewrite bare_persistently_if_laterN HP bare_persistently_if_elim laterN_sep.
Qed.
Global Instance into_sep_except_0 p P Q1 Q2 :
IntoSep p P Q1 Q2 IntoSep p ( P) ( Q1) ( Q2).
Proof.
rewrite /IntoSep=> HP. apply bare_persistently_if_intro'.
by rewrite bare_persistently_if_except_0 HP bare_persistently_if_elim except_0_sep.
Qed.
Global Instance into_sep_later P Q1 Q2 :
IntoSep P Q1 Q2 IntoSep ( P) ( Q1) ( Q2).
Proof. rewrite /IntoSep=> ->. by rewrite later_sep. Qed.
Global Instance into_sep_laterN n P Q1 Q2 :
IntoSep P Q1 Q2 IntoSep (^n P) (^n Q1) (^n Q2).
Proof. rewrite /IntoSep=> ->. by rewrite laterN_sep. Qed.
Global Instance into_sep_except_0 P Q1 Q2 :
IntoSep P Q1 Q2 IntoSep ( P) ( Q1) ( Q2).
Proof. rewrite /IntoSep=> ->. by rewrite except_0_sep. Qed.
(* FromOr *)
Global Instance from_or_later P Q1 Q2 :
......
......@@ -121,11 +121,11 @@ Arguments IntoAnd {_} _ _%I _%I _%I : simpl never.
Arguments into_and {_} _ _%I _%I _%I {_}.
Hint Mode IntoAnd + + ! - - : typeclass_instances.
Class IntoSep {PROP : bi} (p : bool) (P Q1 Q2 : PROP) :=
into_sep : ?p P ?p (Q1 Q2).
Arguments IntoSep {_} _ _%I _%I _%I : simpl never.
Arguments into_sep {_} _ _%I _%I _%I {_}.
Hint Mode IntoAnd + + ! - - : typeclass_instances.
Class IntoSep {PROP : bi} (P Q1 Q2 : PROP) :=
into_sep : P Q1 Q2.
Arguments IntoSep {_} _%I _%I _%I : simpl never.
Arguments into_sep {_} _%I _%I _%I {_}.
Hint Mode IntoSep + ! - - : typeclass_instances.
Class FromOr {PROP : bi} (P Q1 Q2 : PROP) := from_or : Q1 Q2 P.
Arguments FromOr {_} _%I _%I _%I : simpl never.
......
This diff is collapsed.
......@@ -531,8 +531,9 @@ Tactic Notation "iSpecializeCore" open_constr(t) "as" constr(p) :=
quantifiers are instantiated. *)
let pat := spec_pat.parse pat in
lazymatch eval compute in
(bool_decide (pat []) && p && negb (existsb spec_pat_modal pat)) with
(p && bool_decide (pat []) && negb (existsb spec_pat_modal pat)) with
| true =>
(* FIXME: do something reasonable when the BI is not positive *)
eapply tac_specialize_persistent_helper with _ H _ _ _ _;
[env_reflexivity || fail "iSpecialize:" H "not found"
|iSpecializePat H pat; last (iExact H)
......@@ -540,7 +541,7 @@ Tactic Notation "iSpecializeCore" open_constr(t) "as" constr(p) :=
let Q := match goal with |- IntoPersistent _ ?Q _ => Q end in
fail "iSpecialize:" Q "not persistent"
|env_cbv; apply _ ||
let Q := match goal with |- Affine ?Q => Q end in
let Q := match goal with |- TCAnd _ (Affine ?Q) => Q end in
fail "iSpecialize:" Q "not affine"
|env_reflexivity
|(* goal *)]
......
......@@ -44,9 +44,9 @@ Lemma test_unfold_constants : bar.
Proof. iIntros (P) "HP //". Qed.
Lemma test_iRewrite {A : ofeT} (x y : A) P :
( z, P - (z y)) - (P - P (x,x) (y,x)).
( z, P - (z y)) - (P - P (x,x) (y,x)).
Proof.
iIntros "H1 H2".
iIntros "#H1 H2".
iRewrite (bi.internal_eq_sym x x with "[# //]").
iRewrite -("H1" $! _ with "[- //]").
auto.
......
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