Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
George Pirlea
Iris
Commits
936db861
Commit
936db861
authored
Aug 11, 2016
by
Ralf Jung
Browse files
Merge branch 'master' of gitlab.mpisws.org:FP/iriscoq
parents
4e0b7781
76a28786
Changes
3
Hide whitespace changes
Inline
Sidebyside
algebra/frac.v
View file @
936db861
From
Coq
.
QArith
Require
Import
Qcanon
.
From
iris
.
algebra
Require
Export
cmra
.
From
iris
.
algebra
Require
Import
upred
.
Notation
frac
:
=
Qp
(
only
parsing
).
...
...
@@ 20,12 +19,6 @@ Qed.
Canonical
Structure
fracR
:
=
discreteR
frac
frac_ra_mixin
.
End
frac
.
(** Internalized properties *)
Lemma
frac_equivI
{
M
}
(
x
y
:
frac
)
:
x
≡
y
⊣
⊢
(
x
=
y
:
uPred
M
).
Proof
.
by
uPred
.
unseal
.
Qed
.
Lemma
frac_validI
{
M
}
(
x
:
frac
)
:
✓
x
⊣
⊢
(
■
(
x
≤
1
)%
Qc
:
uPred
M
).
Proof
.
by
uPred
.
unseal
.
Qed
.
(** Exclusive *)
Global
Instance
frac_full_exclusive
:
Exclusive
1
%
Qp
.
Proof
.
...
...
heap_lang/heap.v
View file @
936db861
...
...
@@ 118,7 +118,7 @@ Section heap.
rewrite
heap_mapsto_eq

auth_own_op
op_singleton
pair_op
dec_agree_ne
//.
apply
(
anti_symm
(
⊢
))
;
last
by
apply
pure_elim_l
.
rewrite
auth_own_valid
gmap_validI
(
forall_elim
l
)
lookup_singleton
.
rewrite
option_validI
prod_validI
frac_validI
discrete_valid
.
rewrite
option_validI
prod_validI
!
discrete_valid
/=
.
by
apply
pure_elim_r
.
Qed
.
...
...
program_logic/model.v
View file @
936db861
...
...
@@ 71,9 +71,9 @@ Notation "#[ Σ1 ; .. ; Σn ]" :=
(** * Subfunctors *)
(** In order to make proofs in the Iris logic modular, they are not done with
respect to some concrete list of functors [Σ], but are instead parametrized by
an arbitrary list of functors [Σ] that contains atleast certain functors. For
example, the lock library is parametrized by a functor [Σ] that should have
:
the functors corresponding to
:
the heap and the exclusive monoid to manage to
an arbitrary list of functors [Σ] that contains at
least certain functors. For
example, the lock library is paramet
e
rized by a functor [Σ] that should have
the functors corresponding to the heap and the exclusive monoid to manage to
lock invariant.
The contraints to can be expressed using the type class [subG Σ1 Σ2], which
...
...
@@ 109,7 +109,7 @@ Qed.
(** * Solution of the recursive domain equation *)
(** We first declare a module type and then an instance of it so as to seall of
(** We first declare a module type and then an instance of it so as to seal
al
l of
the construction, this way we are sure we do not use any properties of the
construction, and also avoid Coq from blindly unfolding it. *)
Module
Type
iProp_solution_sig
.
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Attach a 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