 12 Feb, 2018 2 commits


JacquesHenri Jourdan authored
This reverts commit 78ba9509.

JacquesHenri Jourdan authored

 07 Feb, 2018 1 commit


Robbert Krebbers authored
This commit implements a generic `iAlways` tactic that is not tied to `persistently`, `affinely` and `plainly` but can be instantiated with a variety of alwaysstyle modalities. In order to plug in an alwaysstyle modality, one has to decide for both the persistent and spatial what action should be performed upon introducing the modality:  Introduction is only allowed when the context is empty.  Introduction is only allowed when all hypotheses satisfy some predicate `C : PROP → Prop` (where `C` should be a type class).  Introduction will only keep the hypotheses that satisfy some predicate `C : PROP → Prop` (where `C` should be a type class).  Introduction will clear the context.  Introduction will keep the context asif. Formally, these actions correspond to the following inductive type: ```coq Inductive always_intro_spec (PROP : bi) :=  AIEnvIsEmpty  AIEnvForall (C : PROP → Prop)  AIEnvFilter (C : PROP → Prop)  AIEnvClear  AIEnvId. ``` An alwaysstyle modality is then a record `always_modality` packing together the modality with the laws it should satisfy to justify the given actions for both contexts.

 02 Feb, 2018 1 commit


JacquesHenri Jourdan authored

 25 Jan, 2018 1 commit


JacquesHenri Jourdan authored

 16 Jan, 2018 1 commit


Robbert Krebbers authored
This used to be done by using `ElimModal` in backwards direction. Having a separate type class for this gets rid of some hacks:  Both `Hint Mode`s in forward and backwards direction for `ElimModal`.  Weird type class precedence hacks to make sure the right instance is picked. These were needed because using `ElimModal` in backwards direction caused ambiguity.

 31 Dec, 2017 1 commit


Robbert Krebbers authored

 04 Dec, 2017 1 commit


JacquesHenri Jourdan authored

 03 Dec, 2017 1 commit


Robbert Krebbers authored
We do not have a notation for `bi_affinely` either, so this is at least consistent.

 27 Nov, 2017 1 commit


Robbert Krebbers authored

 22 Nov, 2017 2 commits


Robbert Krebbers authored
It used to be an inline pattern match. This also restores compatibility with Coq 8.6.1.

Robbert Krebbers authored

 13 Nov, 2017 1 commit


Robbert Krebbers authored
The proof mode now explicitly keeps track of anonymous hypotheses (i.e. hypotheses that are introduced by the introduction pattern `?`). Consider: Lemma foo {M} (P Q R : uPred M) : P ∗ (Q ∗ R) ∗ Q ∗ P. Proof. iIntros "? [H ?]". iFrame "H". iFrame. Qed. After the `iIntros`, the goal will be: _ : P "H" : Q _ : R ∗ Q ∗ P Anonymous hypotheses are displayed in a special way (`_ : P`). An important property of the new anonymous hypotheses is that it is no longer possible to refer to them by name, whereas before, anonymous hypotheses were given some arbitrary fresh name (typically prefixed by `~`). Note tactics can still operate on these anonymous hypotheses. For example, both `iFrame` and `iAssumption`, as well as the symbolic execution tactics, will use them. The only thing that is not possible is to refer to them yourself, for example, in an introduction, specialization or selection pattern. Advantages of the new approach:  Proofs become more robust as one cannot accidentally refer to anonymous hypotheses by their fresh name.  Fresh name generation becomes considerably easier. Since anonymous hypotheses are internally represented by natural numbers (of type `N`), we can just fold over the hypotheses and take the max plus one. This thus solve issue #101.

 03 Nov, 2017 1 commit


JacquesHenri Jourdan authored

 01 Nov, 2017 3 commits


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.

JacquesHenri Jourdan authored

JacquesHenri Jourdan authored
(□ P) now means (bi_bare (bi_persistently P)). This is motivated by the fact that these two modalities are rarely used separately. In the case of an affine BI, we keep the □ notation. This means that a bi_bare is inserted each time we use □. Hence, a few adaptations need to be done in the proof mode class instances.

 31 Oct, 2017 1 commit


Robbert Krebbers authored

 30 Oct, 2017 11 commits


Robbert Krebbers authored
Whenever we iSpecialize something whose conclusion is persistent, we now have to prove all the premises under the sink modality. This is strictly more powerful, as we now have to use just some of the hypotheses to prove the premises, instead of all.

Robbert Krebbers authored

Robbert Krebbers authored
This also applies to the introduction pattern `!#`. Both will now introduce as many ■ or □ as possible. This behavior is consistent with the dual, `#`, which also gets rid of as many ■ and □ modalities as possible.

Robbert Krebbers authored
(All the later lemmas are now prefixed by later_, and dito for laterN, and except_0).

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored
The absence of this axiom has two consequences:  We no longer have `■ (P ∗ Q) ⊢ ■ P ∗ ■ Q` and `□ (P ∗ Q) ⊢ □ P ∗ □ Q`, and as a result, separating conjunctions in the unrestricted/persistent context cannot be eliminated.  When having `(P ∗ ⬕ Q) ∗ P`, we do not get `⬕ Q ∗ P`. In the proof mode this means when having: H1 : P ∗ ⬕ Q H2 : P We cannot say `iDestruct ("H1" with "H2") as "#H1"` and keep `H2`. However, there is now a type class `PositiveBI PROP`, and when there is an instance of this type class, one gets the above reasoning principle back. TODO: Can we describe positivity of individual propositions instead of the whole BI? That way, we would get the above reasoning principles even when the BI is not positive, but the propositions involved are.

Robbert Krebbers authored
Otherwise, ownership of cores in our ordered RA model will not be persistent.

Robbert Krebbers authored

Robbert Krebbers authored

 28 Oct, 2017 2 commits


Robbert Krebbers authored

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

 27 Oct, 2017 1 commit


Robbert Krebbers authored

 26 Oct, 2017 2 commits


Robbert Krebbers authored

Robbert Krebbers authored

 25 Oct, 2017 4 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
I have reimplemented the tactic for introduction of ∀s/pures using type classes, which directly made it much more modular.

 05 Oct, 2017 1 commit


Robbert Krebbers authored

 06 Sep, 2017 1 commit


Robbert Krebbers authored
