Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Tej Chajed
iris
Commits
18729ff5
Commit
18729ff5
authored
Oct 05, 2018
by
JacquesHenri Jourdan
Browse files
Merge branch 'master' of gitlab.mpisws.org:FP/iriscoq
parents
a9f98603
e2a503e9
Changes
4
Hide whitespace changes
Inline
Sidebyside
CHANGELOG.md
View file @
18729ff5
...
...
@@ 17,13 +17,15 @@ Changes in and extensions of the theory:
*
[#] Add weakest preconditions for total program correctness.
*
[#] "(Potentially) stuck" weakest preconditions are no longer considered
experimental.
*
[#] The adequacy statement for weakest preconditions now also involves the
final state.
*
[#] The Löb rule is now a derived rule; it follows from laterintro, later
being contractive and the fact that we can take fixpoints of contractive
functions.
*
[#] Add atomic updates and logically atomic triples, including tactic support.
See
`heap_lang/lib/increment.v`
for an example.
*
[#]
H
eap
L
ang now uses righttoleft evaluation order. This makes
easier to
write specifications of curried functions.
*
[#]
h
eap
_l
ang now uses righttoleft evaluation order. This makes
it
significantly easier to
write specifications of curried functions.
Changes in Coq:
...
...
@@ 76,6 +78,7 @@ Changes in Coq:
*
`namespaces`
has been moved to std++.
*
Changed
`IntoVal`
to be directly usable for rewriting
`e`
into
`of_val v`
, and
changed
`AsVal`
to be usable for rewriting via the
`[v <]`
destruct pattern.
*
`wp_fork`
is now written in curried form.
## Iris 3.1.0 (released 20171219)
...
...
theories/algebra/cmra.v
View file @
18729ff5
...
...
@@ 1395,6 +1395,10 @@ Section option.
by
eapply
(
cmra_validN_le
n
)
;
last
lia
.

done
.
Qed
.
Global
Instance
option_cancelable
(
ma
:
option
A
)
:
(
∀
a
:
A
,
IdFree
a
)
→
(
∀
a
:
A
,
Cancelable
a
)
→
Cancelable
ma
.
Proof
.
destruct
ma
;
apply
_
.
Qed
.
End
option
.
Arguments
optionR
:
clear
implicits
.
...
...
theories/algebra/gmap.v
View file @
18729ff5
...
...
@@ 288,6 +288,12 @@ Proof.

by
rewrite
lookup_singleton_ne
//
!(
left_id
None
_
).
Qed
.
Global
Instance
gmap_cancelable
(
m
:
gmap
K
A
)
:
(
∀
x
:
A
,
IdFree
x
)
→
(
∀
x
:
A
,
Cancelable
x
)
→
Cancelable
m
.
Proof
.
intros
??
n
m1
m2
??
i
.
apply
(
cancelableN
(
m
!!
i
))
;
by
rewrite
!
lookup_op
.
Qed
.
Lemma
insert_op
m1
m2
i
x
y
:
<[
i
:
=
x
⋅
y
]>(
m1
⋅
m2
)
=
<[
i
:
=
x
]>
m1
⋅
<[
i
:
=
y
]>
m2
.
Proof
.
by
rewrite
(
insert_merge
(
⋅
)
m1
m2
i
(
x
⋅
y
)
x
y
).
Qed
.
...
...
theories/heap_lang/lang.v
View file @
18729ff5
...
...
@@ 4,6 +4,17 @@ From stdpp Require Export strings.
From
stdpp
Require
Import
gmap
.
Set
Default
Proof
Using
"Type"
.
(** heap_lang. A fairly simple language used for common Iris examples.
 This is a righttoleft evaluated language, like CakeML and OCaml. The reason
for this is that it makes curried functions usable: Given a WP for [f a b], we
know that any effects [f] might have to not matter until after *both* [a] and
[b] are evaluated. With lefttoright evaluation, that triple is basically
useless the user letexpands [b].
*)
Delimit
Scope
expr_scope
with
E
.
Delimit
Scope
val_scope
with
V
.
...
...
Write
Preview
Markdown
is supported
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