Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
10
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Open sidebar
Pierre-Marie Pédrot
Iris
Commits
2e426d3f
Unverified
Commit
2e426d3f
authored
Jan 24, 2019
by
Maxime Dénès
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Make trivial instances explicit
This is in preparation for coq/coq#9274.
parent
455fec93
Changes
39
Hide whitespace changes
Inline
Side-by-side
Showing
39 changed files
with
127 additions
and
127 deletions
+127
-127
theories/algebra/agree.v
theories/algebra/agree.v
+1
-1
theories/algebra/auth.v
theories/algebra/auth.v
+3
-3
theories/algebra/big_op.v
theories/algebra/big_op.v
+5
-5
theories/algebra/cmra.v
theories/algebra/cmra.v
+13
-13
theories/algebra/cofe_solver.v
theories/algebra/cofe_solver.v
+1
-1
theories/algebra/csum.v
theories/algebra/csum.v
+4
-4
theories/algebra/excl.v
theories/algebra/excl.v
+2
-2
theories/algebra/frac_auth.v
theories/algebra/frac_auth.v
+2
-2
theories/algebra/functions.v
theories/algebra/functions.v
+2
-2
theories/algebra/local_updates.v
theories/algebra/local_updates.v
+1
-1
theories/algebra/ofe.v
theories/algebra/ofe.v
+7
-7
theories/algebra/sts.v
theories/algebra/sts.v
+3
-3
theories/algebra/updates.v
theories/algebra/updates.v
+2
-2
theories/base_logic/lib/auth.v
theories/base_logic/lib/auth.v
+3
-3
theories/base_logic/lib/boxes.v
theories/base_logic/lib/boxes.v
+4
-4
theories/base_logic/lib/cancelable_invariants.v
theories/base_logic/lib/cancelable_invariants.v
+2
-2
theories/base_logic/lib/invariants.v
theories/base_logic/lib/invariants.v
+2
-2
theories/base_logic/lib/na_invariants.v
theories/base_logic/lib/na_invariants.v
+2
-2
theories/base_logic/lib/own.v
theories/base_logic/lib/own.v
+2
-2
theories/base_logic/lib/saved_prop.v
theories/base_logic/lib/saved_prop.v
+1
-1
theories/base_logic/lib/sts.v
theories/base_logic/lib/sts.v
+4
-4
theories/base_logic/lib/viewshifts.v
theories/base_logic/lib/viewshifts.v
+1
-1
theories/base_logic/lib/wsat.v
theories/base_logic/lib/wsat.v
+4
-4
theories/base_logic/upred.v
theories/base_logic/upred.v
+1
-1
theories/bi/big_op.v
theories/bi/big_op.v
+1
-1
theories/bi/derived_connectives.v
theories/bi/derived_connectives.v
+12
-12
theories/bi/embedding.v
theories/bi/embedding.v
+1
-1
theories/bi/interface.v
theories/bi/interface.v
+14
-14
theories/bi/lib/core.v
theories/bi/lib/core.v
+1
-1
theories/bi/monpred.v
theories/bi/monpred.v
+1
-1
theories/bi/plainly.v
theories/bi/plainly.v
+3
-3
theories/bi/tactics.v
theories/bi/tactics.v
+5
-5
theories/bi/updates.v
theories/bi/updates.v
+2
-2
theories/bi/weakestpre.v
theories/bi/weakestpre.v
+2
-2
theories/program_logic/hoare.v
theories/program_logic/hoare.v
+1
-1
theories/program_logic/ownp.v
theories/program_logic/ownp.v
+1
-1
theories/proofmode/class_instances_bi.v
theories/proofmode/class_instances_bi.v
+1
-1
theories/proofmode/environments.v
theories/proofmode/environments.v
+5
-5
theories/proofmode/ltac_tactics.v
theories/proofmode/ltac_tactics.v
+5
-5
No files found.
theories/algebra/agree.v
View file @
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
.
...
...
theories/algebra/auth.v
View file @
2e426d3f
...
...
@@ -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
).
...
...
theories/algebra/big_op.v
View file @
2e426d3f
...
...
@@ -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
:
...
...
theories/algebra/cmra.v
View file @
2e426d3f
...
...
@@ -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
.
...
...
theories/algebra/cofe_solver.v
View file @
2e426d3f
...
...
@@ -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
).
...
...
theories/algebra/csum.v
View file @
2e426d3f
...
...
@@ -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
.
...
...
theories/algebra/excl.v
View file @
2e426d3f
...
...
@@ -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
)).
...
...
theories/algebra/frac_auth.v
View file @
2e426d3f
...
...
@@ -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"
).
...
...
theories/algebra/functions.v
View file @
2e426d3f
...
...
@@ -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
}.
...
...
theories/algebra/local_updates.v
View file @
2e426d3f
...
...
@@ -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
.
...
...
theories/algebra/ofe.v
View file @
2e426d3f
...
...
@@ -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
(
f
◎
g
,
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
}.
...
...
theories/algebra/sts.v
View file @
2e426d3f
...
...
@@ -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
.
...
...
theories/algebra/updates.v
View file @
2e426d3f
...
...
@@ -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
}.
...
...
theories/base_logic/lib/auth.v
View file @
2e426d3f
...
...
@@ -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
}.
...
...
theories/base_logic/lib/boxes.v
View file @
2e426d3f
...
...
@@ -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
).
...
...
theories/base_logic/lib/cancelable_invariants.v
View file @
2e426d3f
...
...
@@ -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
)
...
...
theories/base_logic/lib/invariants.v
View file @
2e426d3f
...
...
@@ -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
)
...
...
theories/base_logic/lib/na_invariants.v
View file @
2e426d3f
...
...
@@ -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
)
...
...
theories/base_logic/lib/own.v
View file @
2e426d3f
...
...
@@ -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 *)
...
...
theories/base_logic/lib/saved_prop.v
View file @
2e426d3f
...
...
@@ -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
}.
...
...
theories/base_logic/lib/sts.v
View file @
2e426d3f
...
...
@@ -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
}.
...
...
theories/base_logic/lib/viewshifts.v
View file @
2e426d3f
...
...
@@ -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
.
...
...
theories/base_logic/lib/wsat.v
View file @
2e426d3f
...
...
@@ -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
Σ
),
...
...
theories/base_logic/upred.v
View file @
2e426d3f
...
...
@@ -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
}.
...
...
theories/bi/big_op.v
View file @
2e426d3f
...
...
@@ -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
.
...
...
theories/bi/derived_connectives.v
View file @
2e426d3f
...
...
@@ -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
:
=
{}
.