 23 Dec, 2017 1 commit


JacquesHenri Jourdan authored

 21 Dec, 2017 1 commit


JacquesHenri Jourdan authored

 20 Dec, 2017 1 commit


Robbert Krebbers authored

 14 Dec, 2017 1 commit


Ralf Jung authored

 22 Nov, 2017 1 commit


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

 14 Nov, 2017 1 commit


Robbert Krebbers authored

 13 Nov, 2017 4 commits


Robbert Krebbers authored

Robbert Krebbers authored

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.

Robbert Krebbers authored

 06 Nov, 2017 1 commit


Robbert Krebbers authored

 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.

 28 Oct, 2017 1 commit


Robbert Krebbers authored

 27 Oct, 2017 2 commits


Robbert Krebbers authored

Robbert Krebbers authored
This closes issue #64.

 26 Oct, 2017 1 commit


Robbert Krebbers authored

 25 Oct, 2017 3 commits


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

 28 Sep, 2017 1 commit


Robbert Krebbers authored

 27 Sep, 2017 1 commit


Robbert Krebbers authored

 26 Sep, 2017 2 commits


Robbert Krebbers authored

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

 28 Aug, 2017 4 commits


Robbert Krebbers authored
persistent context. Given the source does not contain a box:  Before: noop if there is a Persistent instance.  Now: noop in all cases.

Robbert Krebbers authored
We now first iPoseProof the lemma and instantiate its premises before trying to search for the subterm where to apply. As a result, instantiation of the premises of the applied lemmas happens only once, instead of it being done for each subterm as obtained by reshape_expr.

Robbert Krebbers authored

Robbert Krebbers authored

 24 Aug, 2017 1 commit


Robbert Krebbers authored

 20 Aug, 2017 1 commit


Robbert Krebbers authored
This makes it easier to frame or introduce some modalities before introducing universal quantifiers.

 04 Aug, 2017 1 commit


Robbert Krebbers authored

 12 May, 2017 3 commits


Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored
Otherwise, the tactic will fail subsequently. Besides, it was inconsistent w.r.t. the iLöb tactic, which was already doing this.

 09 May, 2017 1 commit


Robbert Krebbers authored

 13 Apr, 2017 1 commit


Robbert Krebbers authored

 28 Mar, 2017 1 commit


Robbert Krebbers authored

 23 Mar, 2017 1 commit


Robbert Krebbers authored
This fixes issue #84.

 21 Mar, 2017 1 commit


Robbert Krebbers authored
