Commit 5c797347 authored by Ralf Jung's avatar Ralf Jung

Merge branch 'instance-nobody-open-proof' into 'master'

Make trivial instances explicit

See merge request FP/iris-coq!204
parents 455fec93 2e426d3f
......@@ -249,7 +249,7 @@ Lemma to_agree_uninjI {M} x : ✓ x ⊢@{uPredI M} ∃ a, to_agree a ≡ x.
Proof. uPred.unseal. split=> n y _. exact: to_agree_uninjN. Qed.
End agree.
Instance: Params (@to_agree) 1.
Instance: Params (@to_agree) 1 := {}.
Arguments agreeC : clear implicits.
Arguments agreeR : clear implicits.
......
......@@ -8,9 +8,9 @@ Add Printing Constructor auth.
Arguments Auth {_} _ _.
Arguments authoritative {_} _.
Arguments auth_own {_} _.
Instance: Params (@Auth) 1.
Instance: Params (@authoritative) 1.
Instance: Params (@auth_own) 1.
Instance: Params (@Auth) 1 := {}.
Instance: Params (@authoritative) 1 := {}.
Instance: Params (@auth_own) 1 := {}.
Notation "◯ a" := (Auth None a) (at level 20).
Notation "● a" := (Auth (Excl' a) ε) (at level 20).
......
......@@ -25,7 +25,7 @@ Fixpoint big_opL `{Monoid M o} {A} (f : nat → A → M) (xs : list A) : M :=
| [] => monoid_unit
| x :: xs => o (f 0 x) (big_opL (λ n, f (S n)) xs)
end.
Instance: Params (@big_opL) 4.
Instance: Params (@big_opL) 4 := {}.
Arguments big_opL {M} o {_ A} _ !_ /.
Typeclasses Opaque big_opL.
Notation "'[^' o 'list]' k ↦ x ∈ l , P" := (big_opL o (λ k x, P) l)
......@@ -37,7 +37,7 @@ Notation "'[^' o 'list]' x ∈ l , P" := (big_opL o (λ _ x, P) l)
Definition big_opM `{Monoid M o} `{Countable K} {A} (f : K A M)
(m : gmap K A) : M := big_opL o (λ _, curry f) (map_to_list m).
Instance: Params (@big_opM) 7.
Instance: Params (@big_opM) 7 := {}.
Arguments big_opM {M} o {_ K _ _ A} _ _ : simpl never.
Typeclasses Opaque big_opM.
Notation "'[^' o 'map]' k ↦ x ∈ m , P" := (big_opM o (λ k x, P) m)
......@@ -49,7 +49,7 @@ Notation "'[^' o 'map]' x ∈ m , P" := (big_opM o (λ _ x, P) m)
Definition big_opS `{Monoid M o} `{Countable A} (f : A M)
(X : gset A) : M := big_opL o (λ _, f) (elements X).
Instance: Params (@big_opS) 6.
Instance: Params (@big_opS) 6 := {}.
Arguments big_opS {M} o {_ A _ _} _ _ : simpl never.
Typeclasses Opaque big_opS.
Notation "'[^' o 'set]' x ∈ X , P" := (big_opS o (λ x, P) X)
......@@ -58,7 +58,7 @@ Notation "'[^' o 'set]' x ∈ X , P" := (big_opS o (λ x, P) X)
Definition big_opMS `{Monoid M o} `{Countable A} (f : A M)
(X : gmultiset A) : M := big_opL o (λ _, f) (elements X).
Instance: Params (@big_opMS) 7.
Instance: Params (@big_opMS) 7 := {}.
Arguments big_opMS {M} o {_ A _ _} _ _ : simpl never.
Typeclasses Opaque big_opMS.
Notation "'[^' o 'mset]' x ∈ X , P" := (big_opMS o (λ x, P) X)
......@@ -417,7 +417,7 @@ Section homomorphisms.
[RewriteRelation] instance. For the purpose of this section, we want to
rewrite with arbitrary relations, so we declare any relation to be a
[RewriteRelation]. *)
Local Instance: {A} (R : relation A), RewriteRelation R.
Local Instance: {A} (R : relation A), RewriteRelation R := {}.
Lemma big_opL_commute {A} (h : M1 M2) `{!MonoidHomomorphism o1 o2 R h}
(f : nat A M1) l :
......
......@@ -4,11 +4,11 @@ Set Default Proof Using "Type".
Class PCore (A : Type) := pcore : A option A.
Hint Mode PCore ! : typeclass_instances.
Instance: Params (@pcore) 2.
Instance: Params (@pcore) 2 := {}.
Class Op (A : Type) := op : A A A.
Hint Mode Op ! : typeclass_instances.
Instance: Params (@op) 2.
Instance: Params (@op) 2 := {}.
Infix "⋅" := op (at level 50, left associativity) : stdpp_scope.
Notation "(⋅)" := op (only parsing) : stdpp_scope.
......@@ -21,23 +21,23 @@ Definition included `{Equiv A, Op A} (x y : A) := ∃ z, y ≡ x ⋅ z.
Infix "≼" := included (at level 70) : stdpp_scope.
Notation "(≼)" := included (only parsing) : stdpp_scope.
Hint Extern 0 (_ _) => reflexivity : core.
Instance: Params (@included) 3.
Instance: Params (@included) 3 := {}.
Class ValidN (A : Type) := validN : nat A Prop.
Hint Mode ValidN ! : typeclass_instances.
Instance: Params (@validN) 3.
Instance: Params (@validN) 3 := {}.
Notation "✓{ n } x" := (validN n x)
(at level 20, n at next level, format "✓{ n } x").
Class Valid (A : Type) := valid : A Prop.
Hint Mode Valid ! : typeclass_instances.
Instance: Params (@valid) 2.
Instance: Params (@valid) 2 := {}.
Notation "✓ x" := (valid x) (at level 20) : stdpp_scope.
Definition includedN `{Dist A, Op A} (n : nat) (x y : A) := z, y {n} x z.
Notation "x ≼{ n } y" := (includedN n x y)
(at level 70, n at next level, format "x ≼{ n } y") : stdpp_scope.
Instance: Params (@includedN) 4.
Instance: Params (@includedN) 4 := {}.
Hint Extern 0 (_ {_} _) => reflexivity : core.
Section mixin.
......@@ -147,27 +147,27 @@ Infix "⋅?" := opM (at level 50, left associativity) : stdpp_scope.
Class CoreId {A : cmraT} (x : A) := core_id : pcore x Some x.
Arguments core_id {_} _ {_}.
Hint Mode CoreId + ! : typeclass_instances.
Instance: Params (@CoreId) 1.
Instance: Params (@CoreId) 1 := {}.
(** * Exclusive elements (i.e., elements that cannot have a frame). *)
Class Exclusive {A : cmraT} (x : A) := exclusive0_l y : {0} (x y) False.
Arguments exclusive0_l {_} _ {_} _ _.
Hint Mode Exclusive + ! : typeclass_instances.
Instance: Params (@Exclusive) 1.
Instance: Params (@Exclusive) 1 := {}.
(** * Cancelable elements. *)
Class Cancelable {A : cmraT} (x : A) :=
cancelableN n y z : {n}(x y) x y {n} x z y {n} z.
Arguments cancelableN {_} _ {_} _ _ _ _.
Hint Mode Cancelable + ! : typeclass_instances.
Instance: Params (@Cancelable) 1.
Instance: Params (@Cancelable) 1 := {}.
(** * Identity-free elements. *)
Class IdFree {A : cmraT} (x : A) :=
id_free0_r y : {0}x x y {0} x False.
Arguments id_free0_r {_} _ {_} _ _.
Hint Mode IdFree + ! : typeclass_instances.
Instance: Params (@IdFree) 1.
Instance: Params (@IdFree) 1 := {}.
(** * CMRAs whose core is total *)
Class CmraTotal (A : cmraT) := cmra_total (x : A) : is_Some (pcore x).
......@@ -177,7 +177,7 @@ Hint Mode CmraTotal ! : typeclass_instances.
core. *)
Class Core (A : Type) := core : A A.
Hint Mode Core ! : typeclass_instances.
Instance: Params (@core) 2.
Instance: Params (@core) 2 := {}.
Instance core' `{PCore A} : Core A := λ x, default x (pcore x).
Arguments core' _ _ _ /.
......@@ -779,7 +779,7 @@ Structure rFunctor := RFunctor {
CmraMorphism (rFunctor_map fg)
}.
Existing Instances rFunctor_ne rFunctor_mor.
Instance: Params (@rFunctor_map) 5.
Instance: Params (@rFunctor_map) 5 := {}.
Delimit Scope rFunctor_scope with RF.
Bind Scope rFunctor_scope with rFunctor.
......@@ -812,7 +812,7 @@ Structure urFunctor := URFunctor {
CmraMorphism (urFunctor_map fg)
}.
Existing Instances urFunctor_ne urFunctor_mor.
Instance: Params (@urFunctor_map) 5.
Instance: Params (@urFunctor_map) 5 := {}.
Delimit Scope urFunctor_scope with URF.
Bind Scope urFunctor_scope with urFunctor.
......
......@@ -151,7 +151,7 @@ Qed.
Program Definition embed (k : nat) (x : A k) : T :=
{| tower_car n := embed_coerce n x |}.
Next Obligation. intros k x i. apply g_embed_coerce. Qed.
Instance: Params (@embed) 1.
Instance: Params (@embed) 1 := {}.
Instance embed_ne k : NonExpansive (embed k).
Proof. by intros n x y Hxy i; rewrite /= Hxy. Qed.
Definition embed' (k : nat) : A k -n> T := CofeMor (embed k).
......
......@@ -17,9 +17,9 @@ Arguments Cinl {_ _} _.
Arguments Cinr {_ _} _.
Arguments CsumBot {_ _}.
Instance: Params (@Cinl) 2.
Instance: Params (@Cinr) 2.
Instance: Params (@CsumBot) 2.
Instance: Params (@Cinl) 2 := {}.
Instance: Params (@Cinr) 2 := {}.
Instance: Params (@CsumBot) 2 := {}.
Instance maybe_Cinl {A B} : Maybe (@Cinl A B) := λ x,
match x with Cinl a => Some a | _ => None end.
......@@ -119,7 +119,7 @@ Definition csum_map {A A' B B'} (fA : A → A') (fB : B → B')
| Cinr b => Cinr (fB b)
| CsumBot => CsumBot
end.
Instance: Params (@csum_map) 4.
Instance: Params (@csum_map) 4 := {}.
Lemma csum_map_id {A B} (x : csum A B) : csum_map id id x = x.
Proof. by destruct x. Qed.
......
......@@ -10,8 +10,8 @@ Inductive excl (A : Type) :=
Arguments Excl {_} _.
Arguments ExclBot {_}.
Instance: Params (@Excl) 1.
Instance: Params (@ExclBot) 1.
Instance: Params (@Excl) 1 := {}.
Instance: Params (@ExclBot) 1 := {}.
Notation excl' A := (option (excl A)).
Notation Excl' x := (Some (Excl x)).
......
......@@ -14,8 +14,8 @@ Definition frac_auth_frag {A : cmraT} (q : frac) (x : A) : frac_authR A :=
Typeclasses Opaque frac_auth_auth frac_auth_frag.
Instance: Params (@frac_auth_auth) 1.
Instance: Params (@frac_auth_frag) 2.
Instance: Params (@frac_auth_auth) 1 := {}.
Instance: Params (@frac_auth_frag) 2 := {}.
Notation "●! a" := (frac_auth_auth a) (at level 10).
Notation "◯!{ q } a" := (frac_auth_frag q a) (at level 10, format "◯!{ q } a").
......
......@@ -6,11 +6,11 @@ Set Default Proof Using "Type".
Definition ofe_fun_insert `{EqDecision A} {B : A ofeT}
(x : A) (y : B x) (f : ofe_fun B) : ofe_fun B := λ x',
match decide (x = x') with left H => eq_rect _ B y _ H | right _ => f x' end.
Instance: Params (@ofe_fun_insert) 5.
Instance: Params (@ofe_fun_insert) 5 := {}.
Definition ofe_fun_singleton `{EqDecision A} {B : A ucmraT}
(x : A) (y : B x) : ofe_fun B := ofe_fun_insert x y ε.
Instance: Params (@ofe_fun_singleton) 5.
Instance: Params (@ofe_fun_singleton) 5 := {}.
Section ofe.
Context `{Heqdec : EqDecision A} {B : A ofeT}.
......
......@@ -4,7 +4,7 @@ Set Default Proof Using "Type".
(** * Local updates *)
Definition local_update {A : cmraT} (x y : A * A) := n mz,
{n} x.1 x.1 {n} x.2 ? mz {n} y.1 y.1 {n} y.2 ? mz.
Instance: Params (@local_update) 1.
Instance: Params (@local_update) 1 := {}.
Infix "~l~>" := local_update (at level 70).
Section updates.
......
......@@ -13,7 +13,7 @@ Set Primitive Projections.
(** Unbundeled version *)
Class Dist A := dist : nat relation A.
Instance: Params (@dist) 3.
Instance: Params (@dist) 3 := {}.
Notation "x ≡{ n }≡ y" := (dist n x y)
(at level 70, n at next level, format "x ≡{ n }≡ y").
Notation "x ≡{ n }@{ A }≡ y" := (dist (A:=A) n x y)
......@@ -102,7 +102,7 @@ Hint Extern 1 (_ ≡{_}≡ _) => apply equiv_dist; assumption : core.
Class Discrete {A : ofeT} (x : A) := discrete y : x {0} y x y.
Arguments discrete {_} _ {_} _ _.
Hint Mode Discrete + ! : typeclass_instances.
Instance: Params (@Discrete) 1.
Instance: Params (@Discrete) 1 := {}.
Class OfeDiscrete (A : ofeT) := ofe_discrete_discrete (x : A) :> Discrete x.
......@@ -573,13 +573,13 @@ Instance ofe_mor_inhabited {A B : ofeT} `{Inhabited B} :
(** Identity and composition and constant function *)
Definition cid {A} : A -n> A := CofeMor id.
Instance: Params (@cid) 1.
Instance: Params (@cid) 1 := {}.
Definition cconst {A B : ofeT} (x : B) : A -n> B := CofeMor (const x).
Instance: Params (@cconst) 2.
Instance: Params (@cconst) 2 := {}.
Definition ccompose {A B C}
(f : B -n> C) (g : A -n> B) : A -n> C := CofeMor (f g).
Instance: Params (@ccompose) 3.
Instance: Params (@ccompose) 3 := {}.
Infix "◎" := ccompose (at level 40, left associativity).
Global Instance ccompose_ne {A B C} :
NonExpansive2 (@ccompose A B C).
......@@ -676,7 +676,7 @@ Structure cFunctor := CFunctor {
cFunctor_map (fg, g'f') x cFunctor_map (g,g') (cFunctor_map (f,f') x)
}.
Existing Instance cFunctor_ne.
Instance: Params (@cFunctor_map) 5.
Instance: Params (@cFunctor_map) 5 := {}.
Delimit Scope cFunctor_scope with CF.
Bind Scope cFunctor_scope with cFunctor.
......@@ -995,7 +995,7 @@ Record later (A : Type) : Type := Next { later_car : A }.
Add Printing Constructor later.
Arguments Next {_} _.
Arguments later_car {_} _.
Instance: Params (@Next) 1.
Instance: Params (@Next) 1 := {}.
Section later.
Context {A : ofeT}.
......
......@@ -284,9 +284,9 @@ Section sts_definitions.
Definition sts_frag_up (s : sts.state sts) (T : sts.tokens sts) : stsR sts :=
sts_frag (sts.up s T) T.
End sts_definitions.
Instance: Params (@sts_auth) 2.
Instance: Params (@sts_frag) 1.
Instance: Params (@sts_frag_up) 2.
Instance: Params (@sts_auth) 2 := {}.
Instance: Params (@sts_frag) 1 := {}.
Instance: Params (@sts_frag_up) 2 := {}.
Section stsRA.
Import sts.
......
......@@ -8,13 +8,13 @@ Set Default Proof Using "Type".
*)
Definition cmra_updateP {A : cmraT} (x : A) (P : A Prop) := n mz,
{n} (x ? mz) y, P y {n} (y ? mz).
Instance: Params (@cmra_updateP) 1.
Instance: Params (@cmra_updateP) 1 := {}.
Infix "~~>:" := cmra_updateP (at level 70).
Definition cmra_update {A : cmraT} (x y : A) := n mz,
{n} (x ? mz) {n} (y ? mz).
Infix "~~>" := cmra_update (at level 70).
Instance: Params (@cmra_update) 1.
Instance: Params (@cmra_update) 1 := {}.
Section updates.
Context {A : cmraT}.
......
......@@ -55,9 +55,9 @@ Section definitions.
End definitions.
Typeclasses Opaque auth_own auth_inv auth_ctx.
Instance: Params (@auth_own) 4.
Instance: Params (@auth_inv) 5.
Instance: Params (@auth_ctx) 7.
Instance: Params (@auth_own) 4 := {}.
Instance: Params (@auth_inv) 5 := {}.
Instance: Params (@auth_ctx) 7 := {}.
Section auth.
Context `{invG Σ, authG Σ A}.
......
......@@ -40,10 +40,10 @@ Section box_defs.
inv N (slice_inv γ (Φ γ)))%I.
End box_defs.
Instance: Params (@box_own_prop) 3.
Instance: Params (@slice_inv) 3.
Instance: Params (@slice) 5.
Instance: Params (@box) 5.
Instance: Params (@box_own_prop) 3 := {}.
Instance: Params (@slice_inv) 3 := {}.
Instance: Params (@slice) 5 := {}.
Instance: Params (@box) 5 := {}.
Section box.
Context `{invG Σ, boxG Σ} (N : namespace).
......
......@@ -20,7 +20,7 @@ Section defs.
( P', (P P') inv N (P' cinv_own γ 1%Qp))%I.
End defs.
Instance: Params (@cinv) 5.
Instance: Params (@cinv) 5 := {}.
Section proofs.
Context `{invG Σ, cinvG Σ}.
......@@ -108,7 +108,7 @@ Section proofs.
iIntros "!> HP". iApply "H"; auto.
Qed.
Global Instance into_inv_cinv N γ P : IntoInv (cinv N γ P) N.
Global Instance into_inv_cinv N γ P : IntoInv (cinv N γ P) N := {}.
Global Instance into_acc_cinv E N γ P p :
IntoAcc (X:=unit) (cinv N γ P)
......
......@@ -12,7 +12,7 @@ Definition inv_def `{invG Σ} (N : namespace) (P : iProp Σ) : iProp Σ :=
Definition inv_aux : seal (@inv_def). by eexists. Qed.
Definition inv {Σ i} := inv_aux.(unseal) Σ i.
Definition inv_eq : @inv = @inv_def := inv_aux.(seal_eq).
Instance: Params (@inv) 3.
Instance: Params (@inv) 3 := {}.
Typeclasses Opaque inv.
Section inv.
......@@ -107,7 +107,7 @@ Proof.
by rewrite left_id_L.
Qed.
Global Instance into_inv_inv N P : IntoInv (inv N P) N.
Global Instance into_inv_inv N P : IntoInv (inv N P) N := {}.
Global Instance into_acc_inv E N P :
IntoAcc (X:=unit) (inv N P)
......
......@@ -26,7 +26,7 @@ Section defs.
inv N (P own p (CoPset , GSet {[i]}) na_own p {[i]}))%I.
End defs.
Instance: Params (@na_inv) 3.
Instance: Params (@na_inv) 3 := {}.
Typeclasses Opaque na_own na_inv.
Section proofs.
......@@ -111,7 +111,7 @@ Section proofs.
- iDestruct (na_own_disjoint with "Htoki Htoki2") as %?. set_solver.
Qed.
Global Instance into_inv_na p N P : IntoInv (na_inv p N P) N.
Global Instance into_inv_na p N P : IntoInv (na_inv p N P) N := {}.
Global Instance into_acc_na p F E N P :
IntoAcc (X:=unit) (na_inv p N P)
......
......@@ -49,14 +49,14 @@ Ltac solve_inG :=
(** * Definition of the connective [own] *)
Definition iRes_singleton `{i : inG Σ A} (γ : gname) (a : A) : iResUR Σ :=
ofe_fun_singleton (inG_id i) {[ γ := cmra_transport inG_prf a ]}.
Instance: Params (@iRes_singleton) 4.
Instance: Params (@iRes_singleton) 4 := {}.
Definition own_def `{inG Σ A} (γ : gname) (a : A) : iProp Σ :=
uPred_ownM (iRes_singleton γ a).
Definition own_aux : seal (@own_def). by eexists. Qed.
Definition own {Σ A i} := own_aux.(unseal) Σ A i.
Definition own_eq : @own = @own_def := own_aux.(seal_eq).
Instance: Params (@own) 4.
Instance: Params (@own) 4 := {}.
Typeclasses Opaque own.
(** * Properties about ghost ownership *)
......
......@@ -21,7 +21,7 @@ Definition saved_anything_own `{savedAnythingG Σ F}
(γ : gname) (x : F (iProp Σ)) : iProp Σ :=
own γ (to_agree $ (cFunctor_map F (iProp_fold, iProp_unfold) x)).
Typeclasses Opaque saved_anything_own.
Instance: Params (@saved_anything_own) 4.
Instance: Params (@saved_anything_own) 4 := {}.
Section saved_anything.
Context `{savedAnythingG Σ F}.
......
......@@ -51,10 +51,10 @@ Section definitions.
Proof. apply _. Qed.
End definitions.
Instance: Params (@sts_inv) 4.
Instance: Params (@sts_ownS) 4.
Instance: Params (@sts_own) 5.
Instance: Params (@sts_ctx) 6.
Instance: Params (@sts_inv) 4 := {}.
Instance: Params (@sts_ownS) 4 := {}.
Instance: Params (@sts_own) 5 := {}.
Instance: Params (@sts_ctx) 6 := {}.
Section sts.
Context `{invG Σ, stsG Σ sts}.
......
......@@ -6,7 +6,7 @@ Definition vs `{invG Σ} (E1 E2 : coPset) (P Q : iProp Σ) : iProp Σ :=
( (P - |={E1,E2}=> Q))%I.
Arguments vs {_ _} _ _ _%I _%I.
Instance: Params (@vs) 4.
Instance: Params (@vs) 4 := {}.
Notation "P ={ E1 , E2 }=> Q" := (vs E1 E2 P Q)
(at level 99, E1,E2 at level 50, Q at level 200,
format "P ={ E1 , E2 }=> Q") : bi_scope.
......
......@@ -39,18 +39,18 @@ Definition ownI `{invG Σ} (i : positive) (P : iProp Σ) : iProp Σ :=
own invariant_name ( {[ i := invariant_unfold P ]}).
Arguments ownI {_ _} _ _%I.
Typeclasses Opaque ownI.
Instance: Params (@invariant_unfold) 1.
Instance: Params (@ownI) 3.
Instance: Params (@invariant_unfold) 1 := {}.
Instance: Params (@ownI) 3 := {}.
Definition ownE `{invG Σ} (E : coPset) : iProp Σ :=
own enabled_name (CoPset E).
Typeclasses Opaque ownE.
Instance: Params (@ownE) 3.
Instance: Params (@ownE) 3 := {}.
Definition ownD `{invG Σ} (E : gset positive) : iProp Σ :=
own disabled_name (GSet E).
Typeclasses Opaque ownD.
Instance: Params (@ownD) 3.
Instance: Params (@ownD) 3 := {}.
Definition wsat `{invG Σ} : iProp Σ :=
locked ( I : gmap positive (iProp Σ),
......
......@@ -56,7 +56,7 @@ Record uPred (M : ucmraT) : Type := UPred {
Bind Scope bi_scope with uPred.
Arguments uPred_holds {_} _%I _ _ : simpl never.
Add Printing Constructor uPred.
Instance: Params (@uPred_holds) 3.
Instance: Params (@uPred_holds) 3 := {}.
Section cofe.
Context {M : ucmraT}.
......
......@@ -15,7 +15,7 @@ Fixpoint big_sepL2 {PROP : bi} {A B}
| x1 :: l1, x2 :: l2 => Φ 0 x1 x2 big_sepL2 (λ n, Φ (S n)) l1 l2
| _, _ => False
end%I.
Instance: Params (@big_sepL2) 3.
Instance: Params (@big_sepL2) 3 := {}.
Arguments big_sepL2 {PROP A B} _ !_ !_ /.
Typeclasses Opaque big_sepL2.
......
......@@ -3,24 +3,24 @@ From iris.algebra Require Import monoid.
Definition bi_iff {PROP : bi} (P Q : PROP) : PROP := ((P Q) (Q P))%I.
Arguments bi_iff {_} _%I _%I : simpl never.
Instance: Params (@bi_iff) 1.
Instance: Params (@bi_iff) 1 := {}.
Infix "↔" := bi_iff : bi_scope.
Definition bi_wand_iff {PROP : bi} (P Q : PROP) : PROP :=
((P - Q) (Q - P))%I.
Arguments bi_wand_iff {_} _%I _%I : simpl never.
Instance: Params (@bi_wand_iff) 1.
Instance: Params (@bi_wand_iff) 1 := {}.
Infix "∗-∗" := bi_wand_iff : bi_scope.
Class Persistent {PROP : bi} (P : PROP) := persistent : P <pers> P.
Arguments Persistent {_} _%I : simpl never.
Arguments persistent {_} _%I {_}.
Hint Mode Persistent + ! : typeclass_instances.
Instance: Params (@Persistent) 1.
Instance: Params (@Persistent) 1 := {}.
Definition bi_affinely {PROP : bi} (P : PROP) : PROP := (emp P)%I.
Arguments bi_affinely {_} _%I : simpl never.
Instance: Params (@bi_affinely) 1.
Instance: Params (@bi_affinely) 1 := {}.
Typeclasses Opaque bi_affinely.
Notation "'<affine>' P" := (bi_affinely P) : bi_scope.
......@@ -39,7 +39,7 @@ 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.
Instance: Params (@bi_absorbingly) 1 := {}.
Typeclasses Opaque bi_absorbingly.
Notation "'<absorb>' P" := (bi_absorbingly P) : bi_scope.
......@@ -51,28 +51,28 @@ Hint Mode Absorbing + ! : typeclass_instances.
Definition bi_persistently_if {PROP : bi} (p : bool) (P : PROP) : PROP :=
(if p then <pers> P else P)%I.
Arguments bi_persistently_if {_} !_ _%I /.
Instance: Params (@bi_persistently_if) 2.
Instance: Params (@bi_persistently_if) 2 := {}.
Typeclasses Opaque bi_persistently_if.
Notation "'<pers>?' p P" := (bi_persistently_if p P) : bi_scope.
Definition bi_affinely_if {PROP : bi} (p : bool) (P : PROP) : PROP :=
(if p then <affine> P else P)%I.
Arguments bi_affinely_if {_} !_ _%I /.
Instance: Params (@bi_affinely_if) 2.
Instance: Params (@bi_affinely_if) 2 := {}.
Typeclasses Opaque bi_affinely_if.