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
George Pirlea
Iris
Commits
0aeb4cdc
Commit
0aeb4cdc
authored
May 17, 2018
by
Robbert Krebbers
Browse files
Merge branch 'master' into gen_proofmode
parents
bd60eade
463474fb
Changes
3
Hide whitespace changes
Inline
Side-by-side
CHANGELOG.md
View file @
0aeb4cdc
...
...
@@ -22,6 +22,8 @@ Changes in Coq:
-
`IntoLaterN'`
→
`IntoLaterN`
(this one _should_ strip a later)
-
`IntoLaterNEnv`
→
`MaybeIntoLaterNEnv`
-
`IntoLaterNEnvs`
→
`MaybeIntoLaterNEnvs`
*
Rename:
-
`frag_auth_op`
→
`frac_auth_frag_op`
*
`namespaces`
has been moved to std++.
## Iris 3.1.0 (released 2017-12-19)
...
...
theories/algebra/frac_auth.v
View file @
0aeb4cdc
...
...
@@ -81,13 +81,13 @@ Section frac_auth.
Lemma
frac_auth_frag_valid
q
a
:
✓
(
◯
!{
q
}
a
)
↔
✓
q
∧
✓
a
.
Proof
.
done
.
Qed
.
Lemma
fra
g
_auth_op
q1
q2
a1
a2
:
◯
!{
q1
+
q2
}
(
a1
⋅
a2
)
≡
◯
!{
q1
}
a1
⋅
◯
!{
q2
}
a2
.
Lemma
fra
c
_auth_
frag_
op
q1
q2
a1
a2
:
◯
!{
q1
+
q2
}
(
a1
⋅
a2
)
≡
◯
!{
q1
}
a1
⋅
◯
!{
q2
}
a2
.
Proof
.
done
.
Qed
.
Lemma
frac_auth_frag_validN_op_1_l
n
q
a
b
:
✓
{
n
}
(
◯
!{
1
}
a
⋅
◯
!{
q
}
b
)
→
False
.
Proof
.
rewrite
-
fra
g
_auth_op
frac_auth_frag_validN
=>
-[/
exclusiveN_l
[]].
Qed
.
Proof
.
rewrite
-
fra
c
_auth_
frag_
op
frac_auth_frag_validN
=>
-[/
exclusiveN_l
[]].
Qed
.
Lemma
frac_auth_frag_valid_op_1_l
q
a
b
:
✓
(
◯
!{
1
}
a
⋅
◯
!{
q
}
b
)
→
False
.
Proof
.
rewrite
-
fra
g
_auth_op
frac_auth_frag_valid
=>
-[/
exclusive_l
[]].
Qed
.
Proof
.
rewrite
-
fra
c
_auth_
frag_
op
frac_auth_frag_valid
=>
-[/
exclusive_l
[]].
Qed
.
Global
Instance
is_op_frac_auth
(
q
q1
q2
:
frac
)
(
a
a1
a2
:
A
)
:
IsOp
q
q1
q2
→
IsOp
a
a1
a2
→
IsOp'
(
◯
!{
q
}
a
)
(
◯
!{
q1
}
a1
)
(
◯
!{
q2
}
a2
).
...
...
@@ -97,7 +97,7 @@ Section frac_auth.
CoreId
a
→
IsOp
q
q1
q2
→
IsOp'
(
◯
!{
q
}
a
)
(
◯
!{
q1
}
a
)
(
◯
!{
q2
}
a
).
Proof
.
rewrite
/
IsOp'
/
IsOp
=>
?
/
leibniz_equiv_iff
->.
by
rewrite
-
fra
g
_auth_op
-
core_id_dup
.
by
rewrite
-
fra
c
_auth_
frag_
op
-
core_id_dup
.
Qed
.
Lemma
frac_auth_update
q
a
b
a'
b'
:
...
...
theories/heap_lang/lib/counter.v
View file @
0aeb4cdc
...
...
@@ -106,7 +106,7 @@ Section contrib_spec.
(** The main proofs. *)
Lemma
ccounter_op
γ
q1
q2
n1
n2
:
ccounter
γ
(
q1
+
q2
)
(
n1
+
n2
)
⊣
⊢
ccounter
γ
q1
n1
∗
ccounter
γ
q2
n2
.
Proof
.
by
rewrite
/
ccounter
fra
g
_auth_op
-
own_op
.
Qed
.
Proof
.
by
rewrite
/
ccounter
fra
c
_auth_
frag_
op
-
own_op
.
Qed
.
Lemma
newcounter_contrib_spec
(
R
:
iProp
Σ
)
:
{{{
True
}}}
newcounter
#()
...
...
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