 11 Nov, 2017 1 commit


Robbert Krebbers authored

 02 Nov, 2017 2 commits


Robbert Krebbers authored

Robbert Krebbers authored
Thanks to Amin Timany for an initial version of the proof.

 01 Nov, 2017 1 commit


Robbert Krebbers authored
This solves issue #100: the proof mode notation is sometimes not printed. As Ralf discovered, the problem is that there are two overlapping notations: ```coq Notation "P ⊢ Q" := (uPred_entails P Q). ``` And the "proof mode" notation: ``` Notation "Γ '' □ Δ '' ∗ Q" := (of_envs (Envs Γ Δ) ⊢ Q%I). ``` These two notations overlap, so, when having a "proof mode" goal of the shape `of_envs (Envs Γ Δ) ⊢ Q%I`, how do we know which notation is Coq going to pick for pretty printing this goal? As we have seen, this choice depends on the import order (since both notations appear in different files), and as such, Coq sometimes (unintendedly) uses the first notation instead of the latter. The idea of this commit is to wrap `of_envs (Envs Γ Δ) ⊢ Q%I` into a definition so that there is no ambiguity for the pretty printer anymore.

 29 Oct, 2017 1 commit


Robbert Krebbers authored
This commit is based on code by Amin Timany.

 28 Oct, 2017 2 commits


Robbert Krebbers authored
This way, it can be used with `iApply`.

JacquesHenri Jourdan authored
This is to be used on top of stdpp's 4b5d254e.

 27 Oct, 2017 1 commit


Ralf Jung authored

 26 Oct, 2017 8 commits


Robbert Krebbers authored

Ralf Jung authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored
Now that we have the plain modality, we can get rid of the basic updates in the soundness statement.

Robbert Krebbers authored

Amin Timany authored

Robbert Krebbers authored

 25 Oct, 2017 8 commits


Robbert Krebbers authored
Replace/remove some occurences of `persistently` into `persistent` where the property instead of the modality is used.

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored
Rename `UCMRA` → `Ucmra` Rename `CMRA` → `Cmra` Rename `OFE` → `Ofe` (`Ofe` was already used partially, but many occurences were missing) Rename `STS` → `Sts` Rename `DRA` → `Dra`

Robbert Krebbers authored

Robbert Krebbers authored
I have reimplemented the tactic for introduction of ∀s/pures using type classes, which directly made it much more modular.

Robbert Krebbers authored
The advantage is that we can directly use a Coq introduction pattern `cpat` to perform actions to the pure assertion. Before, this had to be done in several steps: iDestruct ... as "[Htmp ...]"; iDestruct "Htmp" as %cpat. That is, one had to introduce a temporary name. I expect this to be quite useful in various developments as many of e.g. our invariants are written as: ∃ x1 .. x2, ⌜ pure stuff ⌝ ∗ spacial stuff.

 27 Sep, 2017 1 commit


Robbert Krebbers authored
This causes a bit of backwards incompatibility: it may now succeed with later stripping below unlocked/TC transparent definitions. This problem actually occured for `wsat`.

 26 Sep, 2017 1 commit


Robbert Krebbers authored
We used to normalize the goal, and then checked whether it was of a certain shape. Since `uPred_valid P` normalized to `True ⊢ P`, there was no way of making a distinction between the two, hence `True ⊢ P` was treated as `uPred_valid P`. In this commit, I use type classes to check whether the goal is of a certain shape. Since we declared `uPred_valid` as `Typeclasses Opaque`, we can now make a distinction between `True ⊢ P` and `uPred_valid P`.

 21 Sep, 2017 1 commit


Robbert Krebbers authored

 20 Sep, 2017 2 commits


Robbert Krebbers authored

Robbert Krebbers authored
In order to do that, we need to quantify over nonexpansive predicates instead of arbitrary predicates.

 18 Sep, 2017 2 commits


Robbert Krebbers authored
That caused some problems, e.g.: From iris.base_logic Require Export fix. Gave: Syntax error: [constr:global] expected after [export_token] (in [vernac:gallina_ext]).

Robbert Krebbers authored

 17 Sep, 2017 4 commits


Robbert Krebbers authored

Robbert Krebbers authored
For obsolete reasons, that no longer seem to apply, we used ∅ as the unit.

Robbert Krebbers authored

Robbert Krebbers authored

 28 Aug, 2017 1 commit


Robbert Krebbers authored
 Use Φ and Ψ for predicates.  Use _1 and _2 suffixes for the different directions of a lemma.  Not all lemmas started with _uPred; we do not let the bigop lemmas (for instance) start with uPred_ either, so I just got rid of the prefix.

 24 Aug, 2017 3 commits
 23 Aug, 2017 1 commit


Ralf Jung authored
