Snippets Groups Projects

Forked from Iris / Iris

5667 commits behind the upstream repository.

Merge branch 'contractive' into 'master'

Robbert Krebbers authored 8 years ago

New definition of contractive.

The current notion of `Contractive` does not allow one to deal with functions with multiple arguments, for example, binary functions that are contractive in both arguments (like `lft_vs` in lambdarust), or binary functions that are contractive in one of their arguments.

To that end, I propose I reformulate the notion of `Contractive` so that we can express being contractive using a `Proper`. The new definition is:

Definition dist_later {A : ofeT} (n : nat) (x y : A) : Prop :=
match n with 0 => True | S n => x ≡{n}≡ y end.
Notation Contractive f := (∀ n, Proper (dist_later n ==> dist n) f).

Also, it turns out that using this definition we can implement a `solve_contractive` tactic in the same way as the `solve_proper` tactic.

Unfortunately, the new tactic does not quite work for the weakest precondition connective in Iris because the proof involves induction, and the induction hypothesis does not quite fit into the new `solve_contractive` tactic.

See merge request !32

5dab83f7

5dab83f7 8 years ago

Name	Last commit	Last update
algebra
base_logic
benchmark
docs
heap_lang
prelude
program_logic
proofmode
tests
.gitignore
.gitlab-ci.yml
CHANGELOG.md
LICENSE
LICENSE-CODE
LICENSE-DOCS
Makefile
ProofMode.md
README.md
_CoqProject
naming.txt
opam

IRIS COQ DEVELOPMENT

This is the Coq development of the Iris Project.

Prerequisites

This version is known to compile with:

Coq 8.5pl2
Ssreflect 1.6

For development, better make sure you have a version of Ssreflect that includes commit ad273277 (no such version has been released so far, you will have to fetch the development branch yourself). Iris compiles fine even without this patch, but proof bullets will only be in 'strict' (enforcing) mode with the fixed version of Ssreflect. If you are using opam, you can easily get a fixed version by running

opam pin add coq-mathcomp-ssreflect https://github.com/math-comp/math-comp.git#ad273277ab38bfe458e9332dea5f3a79e3885567

Building Instructions

Run the following command to build the full development:

make

The development can then be installed as the Coq user contribution iris by running:

make install

Structure

The folder prelude contains an extended "Standard Library" by Robbert Krebbers.
The folder algebra contains the COFE and CMRA constructions as well as the solver for recursive domain equations.
The folder base_logic defines the Iris base logic and the primitive connectives. It also contains derived constructions that are entirely independent of the choice of resources.
- The subfolder lib contains some generally useful derived constructions. Most importantly, it defines composeable dynamic resources and ownership of them; the other constructions depend on this setup.
The folder program_logic specializes the base logic to build Iris, the program logic. This includes weakest preconditions that are defined for any language satisfying some generic axioms, and some derived constructions that work for any such language.
The folder proofmode contains the Iris proof mode, which extends Coq with contexts for persistent and spatial Iris assertions. It also contains tactics for interactive proofs in Iris. Documentation can be found in ProofMode.md.
The folder heap_lang defines the ML-like concurrent heap language
- The subfolder lib contains a few derived constructions within this language, e.g., parallel composition. Most notable here is lib/barrier, the implementation and proof of a barrier as described in http://doi.acm.org/10.1145/2818638.
The folder tests contains modules we use to test our infrastructure. Users of the Iris Coq library should not depend on these modules; they may change or disappear without any notice.

Documentation

A LaTeX version of the core logic definitions and some derived forms is available in docs/iris.tex. A compiled PDF version of this document is available online.