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
Jonas Kastberg
iris
Commits
f351a117
Commit
f351a117
authored
Jan 25, 2017
by
Ralf Jung
Browse files
Merge branch 'master' of
https://gitlab.mpisws.org/FP/iriscoq
parents
b4edc070
76fb6fa5
Changes
43
Hide whitespace changes
Inline
Sidebyside
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
...
...
Prev
1
2
3
Next
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