Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
7
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Open sidebar
Tej Chajed
iris
Commits
f351a117
Commit
f351a117
authored
Jan 25, 2017
by
Ralf Jung
Browse files
Options
Browse Files
Download
Plain Diff
Merge branch 'master' of
https://gitlab.mpisws.org/FP/iriscoq
parents
b4edc070
76fb6fa5
Changes
43
Show whitespace changes
Inline
Sidebyside
Showing
43 changed files
with
147 additions
and
84 deletions
+147
84
ProofMode.md
ProofMode.md
+0
1
theories/algebra/ofe.v
theories/algebra/ofe.v
+15
20
theories/heap_lang/lib/par.v
theories/heap_lang/lib/par.v
+1
1
theories/prelude/base.v
theories/prelude/base.v
+1
1
theories/prelude/bset.v
theories/prelude/bset.v
+1
1
theories/prelude/coPset.v
theories/prelude/coPset.v
+1
1
theories/prelude/collections.v
theories/prelude/collections.v
+1
1
theories/prelude/countable.v
theories/prelude/countable.v
+1
1
theories/prelude/decidable.v
theories/prelude/decidable.v
+1
1
theories/prelude/fin_collections.v
theories/prelude/fin_collections.v
+1
1
theories/prelude/fin_map_dom.v
theories/prelude/fin_map_dom.v
+1
1
theories/prelude/fin_maps.v
theories/prelude/fin_maps.v
+1
1
theories/prelude/finite.v
theories/prelude/finite.v
+1
1
theories/prelude/gmap.v
theories/prelude/gmap.v
+1
1
theories/prelude/hashset.v
theories/prelude/hashset.v
+1
1
theories/prelude/lexico.v
theories/prelude/lexico.v
+1
1
theories/prelude/list.v
theories/prelude/list.v
+1
1
theories/prelude/listset.v
theories/prelude/listset.v
+1
1
theories/prelude/listset_nodup.v
theories/prelude/listset_nodup.v
+1
1
theories/prelude/mapset.v
theories/prelude/mapset.v
+1
1
theories/prelude/natmap.v
theories/prelude/natmap.v
+1
1
theories/prelude/nmap.v
theories/prelude/nmap.v
+1
1
theories/prelude/numbers.v
theories/prelude/numbers.v
+1
1
theories/prelude/option.v
theories/prelude/option.v
+1
1
theories/prelude/orders.v
theories/prelude/orders.v
+1
1
theories/prelude/pmap.v
theories/prelude/pmap.v
+1
1
theories/prelude/prelude.v
theories/prelude/prelude.v
+1
1
theories/prelude/pretty.v
theories/prelude/pretty.v
+1
1
theories/prelude/proof_irrel.v
theories/prelude/proof_irrel.v
+1
1
theories/prelude/relations.v
theories/prelude/relations.v
+1
1
theories/prelude/set.v
theories/prelude/set.v
+1
1
theories/prelude/sorting.v
theories/prelude/sorting.v
+1
1
theories/prelude/streams.v
theories/prelude/streams.v
+1
1
theories/prelude/stringmap.v
theories/prelude/stringmap.v
+1
1
theories/prelude/strings.v
theories/prelude/strings.v
+1
1
theories/prelude/tactics.v
theories/prelude/tactics.v
+1
1
theories/prelude/vector.v
theories/prelude/vector.v
+1
1
theories/prelude/zmap.v
theories/prelude/zmap.v
+1
1
theories/program_logic/adequacy.v
theories/program_logic/adequacy.v
+1
1
theories/program_logic/ownp.v
theories/program_logic/ownp.v
+3
3
theories/program_logic/weakestpre.v
theories/program_logic/weakestpre.v
+2
2
theories/proofmode/class_instances.v
theories/proofmode/class_instances.v
+6
0
theories/proofmode/tactics.v
theories/proofmode/tactics.v
+84
21
No files found.
ProofMode.md
View file @
f351a117
...
...
@@ 251,7 +251,6 @@ _specification patterns_ to express splitting of hypotheses:
`P`
, as well the remaining goal.

`[%]`
: This pattern can be used when eliminating
`P ★ Q`
when
`P`
is pure.
It will generate a Coq goal for
`P`
and does not consume any hypotheses.

`*`
: instantiate all toplevel universal quantifiers with meta variables.
For example, given:
...
...
theories/algebra/ofe.v
View file @
f351a117
...
...
@@ 1030,28 +1030,25 @@ End limit_preserving.
Section
sigma
.
Context
{
A
:
ofeT
}
{
P
:
A
→
Prop
}.
Implicit
Types
x
:
sig
P
.
(* TODO: Find a better place for this Equiv instance. It also
should not depend on A being an OFE. *)
Instance
sig_equiv
:
Equiv
(
sig
P
)
:
=
λ
x1
x2
,
(
proj1_sig
x1
)
≡
(
proj1_sig
x2
).
Instance
sig_dist
:
Dist
(
sig
P
)
:
=
λ
n
x1
x2
,
(
proj1_sig
x1
)
≡
{
n
}
≡
(
proj1_sig
x2
).
Lemma
exist_ne
:
∀
n
x1
x2
,
x1
≡
{
n
}
≡
x2
→
∀
(
H1
:
P
x1
)
(
H2
:
P
x2
),
(
exist
P
x1
H1
)
≡
{
n
}
≡
(
exist
P
x2
H2
).
Proof
.
intros
n
??
Hx
??.
exact
Hx
.
Qed
.
Instance
sig_equiv
:
Equiv
(
sig
P
)
:
=
λ
x1
x2
,
`
x1
≡
`
x2
.
Instance
sig_dist
:
Dist
(
sig
P
)
:
=
λ
n
x1
x2
,
`
x1
≡
{
n
}
≡
`
x2
.
Lemma
exist_ne
n
a1
a2
(
H1
:
P
a1
)
(
H2
:
P
a2
)
:
a1
≡
{
n
}
≡
a2
→
a1
↾
H1
≡
{
n
}
≡
a2
↾
H2
.
Proof
.
done
.
Qed
.
Global
Instance
proj1_sig_ne
:
Proper
(
dist
n
==>
dist
n
)
(@
proj1_sig
_
P
).
Proof
.
intros
n
[
]
[]
?.
done
.
Qed
.
Proof
.
by
intros
n
[
a
Ha
]
[
b
Hb
]
?
.
Qed
.
Definition
sig_ofe_mixin
:
OfeMixin
(
sig
P
).
Proof
.
split
.

intros
x
y
.
unfold
dist
,
sig_dist
,
equiv
,
sig_equiv
.
destruct
x
,
y
.
apply
equiv_dist
.

unfold
dist
,
sig_dist
.
intros
n
.
split
;
[
intros
[]

intros
[]
[]

intros
[]
[]
[]]
;
simpl
;
try
done
.
intros
.
by
etrans
.

intros
n
[??]
[??].
unfold
dist
,
sig_dist
.
simpl
.
apply
dist_S
.

intros
[
a
?]
[
b
?].
rewrite
/
dist
/
sig_dist
/
equiv
/
sig_equiv
/=.
apply
equiv_dist
.

intros
n
.
rewrite
/
dist
/
sig_dist
.
split
;
[
intros
[]
intros
[]
[]
intros
[]
[]
[]]=>
//=
>
//.

intros
n
[
a
?]
[
b
?].
rewrite
/
dist
/
sig_dist
/=.
apply
dist_S
.
Qed
.
Canonical
Structure
sigC
:
ofeT
:
=
OfeT
(
sig
P
)
sig_ofe_mixin
.
...
...
@@ 1059,13 +1056,11 @@ Section sigma.
suddenly becomes explicit...? *)
Program
Definition
sig_compl
`
{
LimitPreserving
_
P
}
:
Compl
sigC
:
=
λ
c
,
exist
P
(
compl
(
chain_map
proj1_sig
c
))
_
.
Next
Obligation
.
intros
?
Hlim
c
.
apply
Hlim
.
move
=>
n
/=.
destruct
(
c
n
).
done
.
Qed
.
Program
Definition
sig_cofe
`
{
LimitPreserving
_
P
}
:
Cofe
sigC
:
=
Next
Obligation
.
intros
?
Hlim
c
.
apply
Hlim
=>
n
/=.
by
destruct
(
c
n
).
Qed
.
Program
Definition
sig_cofe
`
{
Cofe
A
,
!
LimitPreserving
P
}
:
Cofe
sigC
:
=
{
compl
:
=
sig_compl
}.
Next
Obligation
.
intros
?
Hlim
n
c
.
apply
(
conv_compl
n
(
chain_map
proj1_sig
c
)).
intros
?
?
n
c
.
apply
(
conv_compl
n
(
chain_map
proj1_sig
c
)).
Qed
.
Global
Instance
sig_timeless
(
x
:
sig
P
)
:
...
...
theories/heap_lang/lib/par.v
View file @
f351a117
...
...
@@ 33,7 +33,7 @@ Proof.
iIntros
(
l
)
"Hl"
.
wp_let
.
wp_proj
.
wp_bind
(
f2
_
).
iApply
(
wp_wand
with
"Hf2"
)
;
iIntros
(
v
)
"H2"
.
wp_let
.
wp_apply
(
join_spec
with
"[$Hl]"
).
iIntros
(
w
)
"H1"
.
iSpecialize
(
"HΦ"
with
"
*
[]"
)
;
first
by
iSplitL
"H1"
.
by
wp_let
.
iSpecialize
(
"HΦ"
with
"[]"
)
;
first
by
iSplitL
"H1"
.
by
wp_let
.
Qed
.
Lemma
wp_par
(
Ψ
1
Ψ
2
:
val
→
iProp
Σ
)
...
...
theories/prelude/base.v
View file @
f351a117
(* Copyright (c) 2012201
5
, Robbert Krebbers. *)
(* Copyright (c) 2012201
7
, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file collects type class interfaces, notations, and general theorems
that are used throughout the whole development. Most importantly it contains
...
...
theories/prelude/bset.v
View file @
f351a117
(* Copyright (c) 2012201
5
, Robbert Krebbers. *)
(* Copyright (c) 2012201
7
, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file implements bsets as functions into Prop. *)
From
iris
.
prelude
Require
Export
prelude
.
...
...
theories/prelude/coPset.v
View file @
f351a117
(* Copyright (c) 2012201
5
, Robbert Krebbers. *)
(* Copyright (c) 2012201
7
, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This files implements the type [coPset] of efficient finite/cofinite sets
of positive binary naturals [positive]. These sets are:
...
...
theories/prelude/collections.v
View file @
f351a117
(* Copyright (c) 2012201
5
, Robbert Krebbers. *)
(* Copyright (c) 2012201
7
, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file collects definitions and theorems on collections. Most
importantly, it implements some tactics to automatically solve goals involving
...
...
theories/prelude/countable.v
View file @
f351a117
(* Copyright (c) 2012201
5
, Robbert Krebbers. *)
(* Copyright (c) 2012201
7
, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
From
iris
.
prelude
Require
Export
list
.
Set
Default
Proof
Using
"Type"
.
...
...
theories/prelude/decidable.v
View file @
f351a117
(* Copyright (c) 2012201
5
, Robbert Krebbers. *)
(* Copyright (c) 2012201
7
, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file collects theorems, definitions, tactics, related to propositions
with a decidable equality. Such propositions are collected by the [Decision]
...
...
theories/prelude/fin_collections.v
View file @
f351a117
(* Copyright (c) 2012201
5
, Robbert Krebbers. *)
(* Copyright (c) 2012201
7
, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file collects definitions and theorems on finite collections. Most
importantly, it implements a fold and size function and some useful induction
...
...
theories/prelude/fin_map_dom.v
View file @
f351a117
(* Copyright (c) 2012201
5
, Robbert Krebbers. *)
(* Copyright (c) 2012201
7
, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file provides an axiomatization of the domain function of finite
maps. We provide such an axiomatization, instead of implementing the domain
...
...
theories/prelude/fin_maps.v
View file @
f351a117
(* Copyright (c) 2012201
5
, Robbert Krebbers. *)
(* Copyright (c) 2012201
7
, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
(** Finite maps associate data to keys. This file defines an interface for
finite maps and collects some theory on it. Most importantly, it proves useful
...
...
theories/prelude/finite.v
View file @
f351a117
(* Copyright (c) 2012201
5
, Robbert Krebbers. *)
(* Copyright (c) 2012201
7
, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
From
iris
.
prelude
Require
Export
countable
vector
.
Set
Default
Proof
Using
"Type"
.
...
...
theories/prelude/gmap.v
View file @
f351a117
(* Copyright (c) 2012201
5
, Robbert Krebbers. *)
(* Copyright (c) 2012201
7
, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file implements finite maps and finite sets with keys of any countable
type. The implementation is based on [Pmap]s, radix2 search trees. *)
...
...
theories/prelude/hashset.v
View file @
f351a117
(* Copyright (c) 2012201
5
, Robbert Krebbers. *)
(* Copyright (c) 2012201
7
, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file implements finite set using hash maps. Hash sets are represented
using radix2 search trees. Each hash bucket is thus indexed using an binary
...
...
theories/prelude/lexico.v
View file @
f351a117
(* Copyright (c) 2012201
5
, Robbert Krebbers. *)
(* Copyright (c) 2012201
7
, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This files defines a lexicographic order on various common data structures
and proves that it is a partial order having a strong variant of trichotomy. *)
...
...
theories/prelude/list.v
View file @
f351a117
(* Copyright (c) 2012201
5
, Robbert Krebbers. *)
(* Copyright (c) 2012201
7
, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file collects general purpose definitions and theorems on lists that
are not in the Coq standard library. *)
...
...
theories/prelude/listset.v
View file @
f351a117
(* Copyright (c) 2012201
5
, Robbert Krebbers. *)
(* Copyright (c) 2012201
7
, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file implements finite set as unordered lists without duplicates
removed. This implementation forms a monad. *)
...
...
theories/prelude/listset_nodup.v
View file @
f351a117
(* Copyright (c) 2012201
5
, Robbert Krebbers. *)
(* Copyright (c) 2012201
7
, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file implements finite as unordered lists without duplicates.
Although this implementation is slow, it is very useful as decidable equality
...
...
theories/prelude/mapset.v
View file @
f351a117
(* Copyright (c) 2012201
5
, Robbert Krebbers. *)
(* Copyright (c) 2012201
7
, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This files gives an implementation of finite sets using finite maps with
elements of the unit type. Since maps enjoy extensional equality, the
...
...
theories/prelude/natmap.v
View file @
f351a117
(* Copyright (c) 2012201
5
, Robbert Krebbers. *)
(* Copyright (c) 2012201
7
, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This files implements a type [natmap A] of finite maps whose keys range
over Coq's data type of unary natural numbers [nat]. The implementation equips
...
...
theories/prelude/nmap.v
View file @
f351a117
(* Copyright (c) 2012201
5
, Robbert Krebbers. *)
(* Copyright (c) 2012201
7
, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This files extends the implementation of finite over [positive] to finite
maps whose keys range over Coq's data type of binary naturals [N]. *)
...
...
theories/prelude/numbers.v
View file @
f351a117
(* Copyright (c) 2012201
5
, Robbert Krebbers. *)
(* Copyright (c) 2012201
7
, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file collects some trivial facts on the Coq types [nat] and [N] for
natural numbers, and the type [Z] for integers. It also declares some useful
...
...
theories/prelude/option.v
View file @
f351a117
(* Copyright (c) 2012201
5
, Robbert Krebbers. *)
(* Copyright (c) 2012201
7
, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file collects general purpose definitions and theorems on the option
data type that are not in the Coq standard library. *)
...
...
theories/prelude/orders.v
View file @
f351a117
(* Copyright (c) 2012201
5
, Robbert Krebbers. *)
(* Copyright (c) 2012201
7
, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
(** Properties about arbitrary pre, partial, and total orders. We do not use
the relation [⊆] because we often have multiple orders on the same structure *)
...
...
theories/prelude/pmap.v
View file @
f351a117
(* Copyright (c) 2012201
5
, Robbert Krebbers. *)
(* Copyright (c) 2012201
7
, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This files implements an efficient implementation of finite maps whose keys
range over Coq's data type of positive binary naturals [positive]. The
...
...
theories/prelude/prelude.v
View file @
f351a117
(* Copyright (c) 2012201
5
, Robbert Krebbers. *)
(* Copyright (c) 2012201
7
, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
From
iris
.
prelude
Require
Export
base
...
...
theories/prelude/pretty.v
View file @
f351a117
(* Copyright (c) 2012201
5
, Robbert Krebbers. *)
(* Copyright (c) 2012201
7
, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
From
iris
.
prelude
Require
Export
strings
.
From
iris
.
prelude
Require
Import
relations
.
...
...
theories/prelude/proof_irrel.v
View file @
f351a117
(* Copyright (c) 2012201
5
, Robbert Krebbers. *)
(* Copyright (c) 2012201
7
, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file collects facts on proof irrelevant types/propositions. *)
From
iris
.
prelude
Require
Export
base
.
...
...
theories/prelude/relations.v
View file @
f351a117
(* Copyright (c) 2012201
5
, Robbert Krebbers. *)
(* Copyright (c) 2012201
7
, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file collects definitions and theorems on abstract rewriting systems.
These are particularly useful as we define the operational semantics as a
...
...
theories/prelude/set.v
View file @
f351a117
(* Copyright (c) 2012201
5
, Robbert Krebbers. *)
(* Copyright (c) 2012201
7
, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file implements sets as functions into Prop. *)
From
iris
.
prelude
Require
Export
collections
.
...
...
theories/prelude/sorting.v
View file @
f351a117
(* Copyright (c) 2012201
5
, Robbert Krebbers. *)
(* Copyright (c) 2012201
7
, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
(** Merge sort. Adapted from the implementation of Hugo Herbelin in the Coq
standard library, but without using the module system. *)
...
...
theories/prelude/streams.v
View file @
f351a117
(* Copyright (c) 2012201
5
, Robbert Krebbers. *)
(* Copyright (c) 2012201
7
, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
From
iris
.
prelude
Require
Export
tactics
.
Set
Default
Proof
Using
"Type"
.
...
...
theories/prelude/stringmap.v
View file @
f351a117
(* Copyright (c) 2012201
5
, Robbert Krebbers. *)
(* Copyright (c) 2012201
7
, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This files implements an efficient implementation of finite maps whose keys
range over Coq's data type of strings [string]. The implementation uses radix2
...
...
theories/prelude/strings.v
View file @
f351a117
(* Copyright (c) 2012201
5
, Robbert Krebbers. *)
(* Copyright (c) 2012201
7
, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
From
Coq
Require
Import
Ascii
.
From
Coq
Require
Export
String
.
...
...
theories/prelude/tactics.v
View file @
f351a117
(* Copyright (c) 2012201
5
, Robbert Krebbers. *)
(* Copyright (c) 2012201
7
, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file collects general purpose tactics that are used throughout
the development. *)
...
...
theories/prelude/vector.v
View file @
f351a117
(* Copyright (c) 2012201
5
, Robbert Krebbers. *)
(* Copyright (c) 2012201
7
, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file collects general purpose definitions and theorems on vectors
(lists of fixed length) and the fin type (bounded naturals). It uses the
...
...
theories/prelude/zmap.v
View file @
f351a117
(* Copyright (c) 2012201
5
, Robbert Krebbers. *)
(* Copyright (c) 2012201
7
, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This files extends the implementation of finite over [positive] to finite
maps whose keys range over Coq's data type of binary naturals [Z]. *)
...
...
theories/program_logic/adequacy.v
View file @
f351a117
...
...
@@ 134,7 +134,7 @@ Lemma wp_safe e σ Φ :
Proof
.
rewrite
wp_unfold
/
wp_pre
.
iIntros
"[(Hw&HE&Hσ) H]"
.
destruct
(
to_val
e
)
as
[
v
]
eqn
:
?
;
[
eauto
10
].
rewrite
fupd_eq
.
iMod
(
"H"
with
"
*
Hσ []"
)
as
">(?&?&%&?)"
;
first
by
iFrame
.
rewrite
fupd_eq
.
iMod
(
"H"
with
"Hσ []"
)
as
">(?&?&%&?)"
;
first
by
iFrame
.
eauto
10
.
Qed
.
...
...
theories/program_logic/ownp.v
View file @
f351a117
...
...
@@ 96,7 +96,7 @@ Section lifting.
iMod
(
own_update_2
with
"Hσ Hσf"
)
as
"[Hσ Hσf]"
.
{
by
apply
auth_update
,
option_local_update
,
(
exclusive_local_update
_
(
Excl
σ
2
)).
}
iFrame
"Hσ"
.
iApply
(
"H"
with
"
*
[]"
)
;
eauto
.
iFrame
"Hσ"
.
iApply
(
"H"
with
"[]"
)
;
eauto
.
Qed
.
Lemma
ownP_lift_pure_step
`
{
Inhabited
(
state
Λ
)}
E
Φ
e1
:
...
...
@@ 171,7 +171,7 @@ Section ectx_lifting.
iIntros
"H"
.
iApply
(
ownP_lift_step
E
)
;
try
done
.
iMod
"H"
as
(
σ
1
)
"(%&Hσ1&Hwp)"
.
iModIntro
.
iExists
σ
1
.
iSplit
;
first
by
eauto
.
iFrame
.
iNext
.
iIntros
(
e2
σ
2
efs
)
"% ?"
.
iApply
(
"Hwp"
with
"
*
[]"
)
;
by
eauto
.
iApply
(
"Hwp"
with
"[]"
)
;
eauto
.
Qed
.
Lemma
ownP_lift_pure_head_step
E
Φ
e1
:
...
...
@@ 193,7 +193,7 @@ Section ectx_lifting.
⊢
WP
e1
@
E
{{
Φ
}}.
Proof
.
iIntros
(?)
"[? H]"
.
iApply
ownP_lift_atomic_step
;
eauto
.
iFrame
.
iNext
.
iIntros
(???)
"% ?"
.
iApply
(
"H"
with
"
*
[]"
)
;
eauto
.
iIntros
(???)
"% ?"
.
iApply
(
"H"
with
"[]"
)
;
eauto
.
Qed
.
Lemma
ownP_lift_atomic_det_head_step
{
E
Φ
e1
}
σ
1
v2
σ
2
efs
:
...
...
theories/program_logic/weakestpre.v
View file @
f351a117
...
...
@@ 155,10 +155,10 @@ Proof.
{
by
iDestruct
"H"
as
">>> $"
.
}
iIntros
(
σ
1
)
"Hσ"
.
iMod
"H"
.
iMod
(
"H"
$!
σ
1
with
"Hσ"
)
as
"[$ H]"
.
iModIntro
.
iNext
.
iIntros
(
e2
σ
2
efs
Hstep
).
iMod
(
"H"
with
"
*
[]"
)
as
"(Hphy & H & $)"
;
first
done
.
iMod
(
"H"
with
"[]"
)
as
"(Hphy & H & $)"
;
first
done
.
rewrite
!
wp_unfold
/
wp_pre
.
destruct
(
to_val
e2
)
as
[
v2
]
eqn
:
He2
.

iDestruct
"H"
as
">> $"
.
iFrame
.
eauto
.

iMod
(
"H"
with
"
*
Hphy"
)
as
"[H _]"
.

iMod
(
"H"
with
"Hphy"
)
as
"[H _]"
.
iDestruct
"H"
as
%(?
&
?
&
?
&
?).
by
edestruct
(
Hatomic
_
_
_
_
Hstep
).
Qed
.
...
...
theories/proofmode/class_instances.v
View file @
f351a117
...
...
@@ 21,6 +21,9 @@ Proof. rewrite /FromAssumption=><. by rewrite always_always. Qed.
Global
Instance
from_assumption_bupd
p
P
Q
:
FromAssumption
p
P
Q
→
FromAssumption
p
P
(==>
Q
)%
I
.
Proof
.
rewrite
/
FromAssumption
=>>.
apply
bupd_intro
.
Qed
.
Global
Instance
from_assumption_forall
{
A
}
p
(
Φ
:
A
→
uPred
M
)
Q
x
:
FromAssumption
p
(
Φ
x
)
Q
→
FromAssumption
p
(
∀
x
,
Φ
x
)
Q
.
Proof
.
rewrite
/
FromAssumption
=>
<.
by
rewrite
forall_elim
.
Qed
.
(* IntoPure *)
Global
Instance
into_pure_pure
φ
:
@
IntoPure
M
⌜φ⌝
φ
.
...
...
@@ 217,6 +220,9 @@ Proof. by apply and_elim_l', impl_wand. Qed.
Global
Instance
into_wand_iff_r
P
Q
:
IntoWand
(
P
↔
Q
)
Q
P
.
Proof
.
apply
and_elim_r'
,
impl_wand
.
Qed
.
Global
Instance
into_wand_forall
{
A
}
(
Φ
:
A
→
uPred
M
)
P
Q
x
:
IntoWand
(
Φ
x
)
P
Q
→
IntoWand
(
∀
x
,
Φ
x
)
P
Q
.
Proof
.
rewrite
/
IntoWand
=>
<.
apply
forall_elim
.
Qed
.
Global
Instance
into_wand_always
R
P
Q
:
IntoWand
R
P
Q
→
IntoWand
(
□
R
)
P
Q
.
Proof
.
rewrite
/
IntoWand
=>
>.
apply
always_elim
.
Qed
.
...
...
theories/proofmode/tactics.v
View file @
f351a117
...
...
@@ 285,7 +285,9 @@ Local Tactic Notation "iSpecializePat" constr(H) constr(pat) :=
let
rec
go
H1
pats
:
=
lazymatch
pats
with

[]
=>
idtac

SForall
::
?pats
=>
try
(
iSpecializeArgs
H1
(
hcons
_
_
))
;
go
H1
pats

SForall
::
?pats
=>
idtac
"the * specialization pattern is deprecated because it is applied implicitly"
;
go
H1
pats

SName
?H2
::
?pats
=>
eapply
tac_specialize
with
_
_
H2
_
H1
_
_
_
_;
(* (j:=H1) (i:=H2) *)
[
env_cbv
;
reflexivity

fail
"iSpecialize:"
H2
"not found"
...
...
@@ 333,6 +335,8 @@ introduction pattern, which will be coerced into [true] when it solely contains
`#` or `%` patterns at the toplevel. *)
Tactic
Notation
"iSpecializeCore"
open_constr
(
t
)
"as"
constr
(
p
)
:
=
let
p
:
=
intro_pat_persistent
p
in
let
t
:
=
match
type
of
t
with
string
=>
constr
:
(
ITrm
t
hnil
""
)

_
=>
t
end
in
lazymatch
t
with

ITrm
?H
?xs
?pat
=>
lazymatch
type
of
H
with
...
...
@@ 349,6 +353,7 @@ Tactic Notation "iSpecializeCore" open_constr(t) "as" constr(p) :=
end

_
=>
fail
"iSpecialize:"
H
"should be a hypothesis, use iPoseProof instead"
end

_
=>
fail
"iSpecialize:"
t
"should be a proof mode term"
end
.
Tactic
Notation
"iSpecialize"
open_constr
(
t
)
:
=
...
...
@@ 421,11 +426,6 @@ Tactic Notation "iPoseProof" open_constr(lem) "as" constr(H) :=
(** * Apply *)
Tactic
Notation
"iApply"
open_constr
(
lem
)
:
=
let
lem
:
=
(* add a `*` to specialize all toplevel foralls *)
lazymatch
lem
with

ITrm
?t
?xs
?pat
=>
constr
:
(
ITrm
t
xs
(
"*"
+
:
+
pat
))

_
=>
constr
:
(
ITrm
lem
hnil
"*"
)
end
in
let
rec
go
H
:
=
first
[
eapply
tac_apply
with
_
H
_
_
_;
[
env_cbv
;
reflexivity
...
...
@@ 961,27 +961,59 @@ Tactic Notation "iRevertIntros" "(" ident(x1) ident(x2) ident(x3) ident(x4)
iRevertIntros
(
x1
x2
x3
x4
x5
x6
x7
x8
)
""
with
tac
.
(** * Destruct tactic *)
Class
CopyDestruct
{
M
}
(
P
:
uPred
M
).
Hint
Mode
CopyDestruct
+
!
:
typeclass_instances
.
Instance
copy_destruct_forall
{
M
A
}
(
Φ
:
A
→
uPred
M
)
:
CopyDestruct
(
∀
x
,
Φ
x
).
Instance
copy_destruct_impl
{
M
}
(
P
Q
:
uPred
M
)
:
CopyDestruct
Q
→
CopyDestruct
(
P
→
Q
).
Instance
copy_destruct_wand
{
M
}
(
P
Q
:
uPred
M
)
:
CopyDestruct
Q
→
CopyDestruct
(
P

∗
Q
).
Instance
copy_destruct_always
{
M
}
(
P
:
uPred
M
)
:
CopyDestruct
P
→
CopyDestruct
(
□
P
).
Tactic
Notation
"iDestructCore"
open_constr
(
lem
)
"as"
constr
(
p
)
tactic
(
tac
)
:
=
let
hyp_name
:
=
lazymatch
type
of
lem
with

string
=>
constr
:
(
Some
lem
)

iTrm
=>
lazymatch
lem
with

@
iTrm
string
?H
_
_
=>
constr
:
(
Some
H
)

_
=>
constr
:
(@
None
string
)
end

_
=>
constr
:
(@
None
string
)
end
in
let
intro_destruct
n
:
=
let
rec
go
n'
:
=
lazymatch
n'
with

0
=>
fail
"iDestruct: cannot introduce"
n
"hypotheses"

1
=>
repeat
iIntroForall
;
let
H
:
=
iFresh
in
iIntro
H
;
tac
H

S
?n'
=>
repeat
iIntroForall
;
let
H
:
=
iFresh
in
iIntro
H
;
go
n'
end
in
intros
;
iStartProof
;
go
n
in
end
in
intros
;
iStartProof
;
go
n
in
lazymatch
type
of
lem
with

nat
=>
intro_destruct
lem

Z
=>
(* to make it work in Z_scope. We should just be able to bind
tactic notation arguments to notation scopes. *)
let
n
:
=
eval
compute
in
(
Z
.
to_nat
lem
)
in
intro_destruct
n

string
=>
tac
lem

iTrm
=>
(* only copy the hypothesis when universal quantifiers are instantiated *)
lazymatch
lem
with

@
iTrm
string
?H
_
hnil
?pat
=>
iSpecializeCore
lem
as
p
;
last
tac

_
=>
iPoseProofCore
lem
as
p
false
tac

_
=>
(* Only copy the hypothesis in case there is a [CopyDestruct] instance.
Also, rule out cases in which it does not make sense to copy, namely when
destructing a lemma (instead of a hypothesis) or a spatial hyopthesis
(which cannot be kept). *)
lazymatch
hyp_name
with

None
=>
iPoseProofCore
lem
as
p
false
tac

Some
?H
=>
iTypeOf
H
(
fun
q
P
=>
lazymatch
q
with

true
=>
(* persistent hypothesis, check for a CopyDestruct instance *)
tryif
(
let
dummy
:
=
constr
:
(
_
:
CopyDestruct
P
)
in
idtac
)
then
(
iPoseProofCore
lem
as
p
false
tac
)
else
(
iSpecializeCore
lem
as
p
;
last
(
tac
H
))

false
=>
(* spatial hypothesis, cannot copy *)
iSpecializeCore
lem
as
p
;
last
(
tac
H
)
end
)
end

_
=>
iPoseProofCore
lem
as
p
false
tac
end
.
Tactic
Notation
"iDestruct"
open_constr
(
lem
)
"as"
constr
(
pat
)
:
=
...
...
@@ 1166,8 +1198,8 @@ Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ident(x2)
(** * Assert *)
(* The argument [p] denotes whether [Q] is persistent. It can either be a
Boolean or an introduction pattern, which will be coerced into [true]
when
it
only contains `#` or `%` patterns at the toplevel. *)
Boolean or an introduction pattern, which will be coerced into [true]
if
it
only contains `#` or `%` patterns at the toplevel
, and [false] otherwise
. *)
Tactic
Notation
"iAssertCore"
open_constr
(
Q
)
"with"
constr
(
Hs
)
"as"
constr
(
p
)
tactic
(
tac
)
:
=
iStartProof
;
...
...
@@ 1205,15 +1237,46 @@ Tactic Notation "iAssertCore" open_constr(Q)
end

?pat
=>
fail
"iAssert: invalid pattern"
pat
end
.
Tactic
Notation
"iAssertCore"
open_constr
(
Q
)
"as"
constr
(
p
)
tactic
(
tac
)
:
=
let
p
:
=
intro_pat_persistent
p
in
match
p
with

true
=>
iAssertCore
Q
with
"[]"
as
p
tac

false
=>
iAssertCore
Q
with
"[]"
as
p
tac
end
.
Tactic
Notation
"iAssert"
open_constr
(
Q
)
"with"
constr
(
Hs
)
"as"
constr
(
pat
)
:
=
iAssertCore
Q
with
Hs
as
pat
(
fun
H
=>
iDestructHyp
H
as
pat
).
Tactic
Notation
"iAssert"
open_constr
(
Q
)
"with"
constr
(
Hs
)
"as"
"("
simple_intropattern
(
x1
)
")"
constr
(
pat
)
:
=
iAssertCore
Q
with
Hs
as
pat
(
fun
H
=>
iDestructHyp
H
as
(
x1
)
pat
).
Tactic
Notation
"iAssert"
open_constr
(
Q
)
"with"
constr
(
Hs
)
"as"
"("
simple_intropattern
(
x1
)
simple_intropattern
(
x2
)
")"
constr
(
pat
)
:
=
iAssertCore
Q
with
Hs
as
pat
(
fun
H
=>
iDestructHyp
H
as
(
x1
x2
)
pat
).
Tactic
Notation
"iAssert"
open_constr
(
Q
)
"with"
constr
(
Hs
)
"as"
"("
simple_intropattern
(
x1
)
simple_intropattern
(
x2
)
simple_intropattern
(
x3
)
")"
constr
(
pat
)
:
=
iAssertCore
Q
with
Hs
as
pat
(
fun
H
=>
iDestructHyp
H
as
(
x1
x2
x3
)
pat
).
Tactic
Notation
"iAssert"
open_constr
(
Q
)
"with"
constr
(
Hs
)
"as"
"("
simple_intropattern
(
x1
)
simple_intropattern
(
x2
)
simple_intropattern
(
x3
)
simple_intropattern
(
x4
)
")"
constr
(
pat
)
:
=
iAssertCore
Q
with
Hs
as
pat
(
fun
H
=>
iDestructHyp
H
as
(
x1
x2
x3
x4
)
pat
).
Tactic
Notation
"iAssert"
open_constr
(
Q
)
"as"
constr
(
pat
)
:
=
let
p
:
=
intro_pat_persistent
pat
in
match
p
with

true
=>
iAssert
Q
with
"[]"
as
pat

false
=>
iAssert
Q
with
"[]"
as
pat
end
.
iAssertCore
Q
as
pat
(
fun
H
=>
iDestructHyp
H
as
pat
).
Tactic
Notation
"iAssert"
open_constr
(
Q
)
"as"
"("
simple_intropattern
(
x1
)
")"
constr
(
pat
)
:
=
iAssertCore
Q
as
pat
(
fun
H
=>
iDestructHyp
H
as
(
x1
)
pat
).
Tactic
Notation
"iAssert"
open_constr
(
Q
)
"as"
"("
simple_intropattern
(
x1
)
simple_intropattern
(
x2
)
")"
constr
(
pat
)
:
=
iAssertCore
Q
as
pat
(
fun
H
=>
iDestructHyp
H
as
(
x1
x2
)
pat
).
Tactic
Notation
"iAssert"
open_constr
(
Q
)
"as"
"("
simple_intropattern
(
x1
)
simple_intropattern
(
x2
)
simple_intropattern
(
x3
)
")"
constr
(
pat
)
:
=
iAssertCore
Q
as
pat
(
fun
H
=>
iDestructHyp
H
as
(
x1
x2
x3
)
pat
).
Tactic
Notation
"iAssert"
open_constr
(
Q
)
"as"
"("
simple_intropattern
(
x1
)
simple_intropattern
(
x2
)
simple_intropattern
(
x3
)
simple_intropattern
(
x4
)
")"
constr
(
pat
)
:
=
iAssertCore
Q
as
pat
(
fun
H
=>
iDestructHyp
H
as
(
x1
x2
x3
x4
)
pat
).
Tactic
Notation
"iAssert"
open_constr
(
Q
)
"with"
constr
(
Hs
)
"as"
"%"
simple_intropattern
(
pat
)
:
=
...
...
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