 20 Feb, 2018 3 commits


Robbert Krebbers authored
This regression was caused by a bug in handling spec patterns.

Robbert Krebbers authored
We now use the `Maybe` prefix as also used for `Frame`: it indicates whether progress has been made by stripping of a later or not.

Robbert Krebbers authored
In the same way that `iFrame` would succeed on said goals.

 19 Feb, 2018 4 commits


Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored
This made the definition much simpler, and provides support for all specialization patterns (although most are not very useful in combination with `iAssert`).

Robbert Krebbers authored

 15 Feb, 2018 2 commits


JacquesHenri Jourdan authored

JacquesHenri Jourdan authored

 13 Feb, 2018 3 commits


JacquesHenri Jourdan authored

JacquesHenri Jourdan authored

JacquesHenri Jourdan authored

 12 Feb, 2018 4 commits


JacquesHenri Jourdan authored

JacquesHenri Jourdan authored
This reverts commit 78ba9509.

JacquesHenri Jourdan authored

Robbert Krebbers authored
This supports Iris 2 like update modalities, as used in e.g. by @jtassaro. This commit fixes issue #154.

 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

 23 Jan, 2018 3 commits


Robbert Krebbers authored
This is to make sure that e.g. `//` in `iEval (rewrite .. // ..)` does not immediately close the goal by reflexivity.

Robbert Krebbers authored

Robbert Krebbers 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 5 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
