Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Joshua Yanovski
iris-coq
Commits
8dc73363
Commit
8dc73363
authored
Nov 16, 2015
by
Robbert Krebbers
Browse files
Use qualified module names and coqc -Q instead of -R.
parent
19cca411
Changes
44
Hide whitespace changes
Inline
Side-by-side
SConstruct
View file @
8dc73363
...
...
@@ -3,7 +3,7 @@
import
os
,
glob
,
string
modules
=
[
"prelude"
,
"iris"
]
Rs
=
'
-R . iris'
Rs
=
'
'
.
join
([
'-Q '
+
x
+
' '
+
x
for
x
in
modules
])
env
=
DefaultEnvironment
(
ENV
=
os
.
environ
,
tools
=
[
'default'
,
'Coq'
],
COQFLAGS
=
Rs
)
# Coq dependencies
...
...
@@ -15,4 +15,4 @@ ParseDepends('deps')
for
v
in
vs
:
env
.
Coq
(
v
)
# Coqidescript
env
.
CoqIdeScript
(
'coqidescript'
,
[])
env
.
CoqIdeScript
(
'coqidescript'
,
[]
,
COQFLAGS
=
Rs
)
iris/agree.v
View file @
8dc73363
Require
Export
cmra
.
Require
Export
iris
.
cmra
.
Local
Hint
Extern
10
(
_
≤
_
)
=>
omega
.
Record
agree
A
`
{
Dist
A
}
:=
Agree
{
...
...
iris/auth.v
View file @
8dc73363
Require
Export
excl
.
Require
Export
iris
.
excl
.
Local
Arguments
disjoint
_
_
!
_
!
_
/
.
Local
Arguments
included
_
_
!
_
!
_
/
.
...
...
iris/cmra.v
View file @
8dc73363
Require
Export
ra
cofe
cofe_instances
.
Require
Export
iris
.
ra
iris
.
cofe
.
Class
ValidN
(
A
:
Type
)
:=
validN
:
nat
→
A
→
Prop
.
Instance:
Params
(
@
validN
)
3.
...
...
iris/cofe.v
View file @
8dc73363
Require
Export
prelude
.
Require
Export
prelude
.
prelude
.
Obligation
Tactic
:=
idtac
.
(
**
Unbundeled
version
*
)
...
...
iris/cofe_instances.v
View file @
8dc73363
Require
Export
cofe
.
Require
Import
fin_maps
p
map
nmap
zmap
stringmap
.
Require
Export
iris
.
cofe
.
Require
Import
prelude
.
fin_maps
p
relude
.
pmap
prelude
.
nmap
prelude
.
zmap
prelude
.
stringmap
.
(
**
Discrete
cofe
*
)
Section
discrete_cofe
.
...
...
iris/cofe_solver.v
View file @
8dc73363
Require
Export
cofe
.
Require
Export
iris
.
cofe
.
Section
solver
.
Context
(
F
:
cofeT
→
cofeT
→
cofeT
).
...
...
iris/dra.v
View file @
8dc73363
Require
Export
ra
.
Require
Export
iris
.
ra
.
(
**
From
disjoint
pcm
*
)
Record
validity
{
A
}
(
P
:
A
→
Prop
)
:
Type
:=
Validity
{
...
...
iris/excl.v
View file @
8dc73363
Require
Export
cmra
.
Require
Export
iris
.
cmra
.
Local
Arguments
disjoint
_
_
!
_
!
_
/
.
Local
Arguments
included
_
_
!
_
!
_
/
.
...
...
iris/logic.v
View file @
8dc73363
Require
Import
cmra
cofe_instances
.
Require
Import
iris
.
cmra
.
Local
Hint
Extern
1
(
_
≼
_
)
=>
etransitivity
;
[
eassumption
|
].
Local
Hint
Extern
1
(
_
≼
_
)
=>
etransitivity
;
[
|
eassumption
].
Local
Hint
Extern
10
(
_
≤
_
)
=>
omega
.
...
...
iris/ra.v
View file @
8dc73363
Require
Export
collections
relations
.
Require
Export
prelude
.
collections
prelude
.
relations
.
Class
Valid
(
A
:
Type
)
:=
valid
:
A
→
Prop
.
Instance:
Params
(
@
valid
)
2.
...
...
iris/sts.v
View file @
8dc73363
Require
Export
ra
.
Require
Import
sets
stringmap
dra
.
Require
Export
iris
.
ra
.
Require
Import
prelude
.
sets
prelude
.
stringmap
iris
.
dra
.
Local
Arguments
valid
_
_
!
_
/
.
Local
Arguments
op
_
_
!
_
!
_
/
.
Local
Arguments
unit
_
_
!
_
/
.
...
...
prelude/assoc.v
View file @
8dc73363
...
...
@@ -6,8 +6,8 @@ main advantage of these association lists compared to search trees, is that it
has
canonical
representatives
and
thus
extensional
Leibniz
equality
.
Compared
to
a
naive
unordered
association
list
,
the
merge
operation
(
used
for
unions
,
intersections
,
and
difference
)
is
also
linear
-
time
.
*
)
Require
Import
mapset
.
Require
Export
fin_maps
.
Require
Import
prelude
.
mapset
.
Require
Export
prelude
.
fin_maps
.
(
**
Because
the
association
list
is
sorted
using
[
strict
lexico
]
instead
of
[
lexico
],
it
automatically
guarantees
that
no
duplicates
exist
.
*
)
...
...
prelude/collections.v
View file @
8dc73363
...
...
@@ -3,7 +3,7 @@
(
**
This
file
collects
definitions
and
theorems
on
collections
.
Most
importantly
,
it
implements
some
tactics
to
automatically
solve
goals
involving
collections
.
*
)
Require
Export
base
tactics
orders
.
Require
Export
prelude
.
base
prelude
.
tactics
prelude
.
orders
.
Instance
collection_subseteq
`
{
ElemOf
A
C
}
:
SubsetEq
C
:=
λ
X
Y
,
∀
x
,
x
∈
X
→
x
∈
Y
.
...
...
prelude/countable.v
View file @
8dc73363
(
*
Copyright
(
c
)
2012
-
2015
,
Robbert
Krebbers
.
*
)
(
*
This
file
is
distributed
under
the
terms
of
the
BSD
license
.
*
)
Require
Export
list
.
Require
Export
prelude
.
list
.
Local
Obligation
Tactic
:=
idtac
.
Local
Open
Scope
positive
.
...
...
prelude/decidable.v
View file @
8dc73363
...
...
@@ -3,7 +3,7 @@
(
**
This
file
collects
theorems
,
definitions
,
tactics
,
related
to
propositions
with
a
decidable
equality
.
Such
propositions
are
collected
by
the
[
Decision
]
type
class
.
*
)
Require
Export
proof_irrel
.
Require
Export
prelude
.
proof_irrel
.
Hint
Extern
200
(
Decision
_
)
=>
progress
(
lazy
beta
)
:
typeclass_instances
.
...
...
prelude/error.v
View file @
8dc73363
(
*
Copyright
(
c
)
2012
-
2015
,
Robbert
Krebbers
.
*
)
(
*
This
file
is
distributed
under
the
terms
of
the
BSD
license
.
*
)
Require
Export
list
.
Require
Export
prelude
.
list
.
Definition
error
(
S
E
A
:
Type
)
:
Type
:=
S
→
E
+
(
A
*
S
).
...
...
prelude/fin_collections.v
View file @
8dc73363
...
...
@@ -3,8 +3,8 @@
(
**
This
file
collects
definitions
and
theorems
on
finite
collections
.
Most
importantly
,
it
implements
a
fold
and
size
function
and
some
useful
induction
principles
on
finite
collections
.
*
)
Require
Import
Permutation
relations
listset
.
Require
Export
numbers
collections
.
Require
Import
Permutation
prelude
.
relations
prelude
.
listset
.
Require
Export
prelude
.
numbers
prelude
.
collections
.
Instance
collection_size
`
{
Elements
A
C
}
:
Size
C
:=
length
∘
elements
.
Definition
collection_fold
`
{
Elements
A
C
}
{
B
}
...
...
prelude/fin_map_dom.v
View file @
8dc73363
...
...
@@ -3,7 +3,7 @@
(
**
This
file
provides
an
axiomatization
of
the
domain
function
of
finite
maps
.
We
provide
such
an
axiomatization
,
instead
of
implementing
the
domain
function
in
a
generic
way
,
to
allow
more
efficient
implementations
.
*
)
Require
Export
collections
fin_maps
.
Require
Export
prelude
.
collections
prelude
.
fin_maps
.
Class
FinMapDom
K
M
D
`
{
FMap
M
,
∀
A
,
Lookup
K
A
(
M
A
),
∀
A
,
Empty
(
M
A
),
∀
A
,
PartialAlter
K
A
(
M
A
),
...
...
prelude/fin_maps.v
View file @
8dc73363
...
...
@@ -5,7 +5,7 @@ finite maps and collects some theory on it. Most importantly, it proves useful
induction
principles
for
finite
maps
and
implements
the
tactic
[
simplify_map_equality
]
to
simplify
goals
involving
finite
maps
.
*
)
Require
Import
Permutation
.
Require
Export
relations
vector
orders
.
Require
Export
prelude
.
relations
prelude
.
vector
prelude
.
orders
.
(
**
*
Axiomatization
of
finite
maps
*
)
(
**
We
require
Leibniz
equality
to
be
extensional
on
finite
maps
.
This
of
...
...
Prev
1
2
3
Next
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment