- Nov 01, 2019
-
-
Ralf Jung authored
-
-
- Sep 19, 2019
-
-
Robbert Krebbers authored
-
- Sep 13, 2019
-
-
Jacques-Henri Jourdan authored
The general idea is to first import/export modules which are further than the current one, and then import/export modules which are close dependencies. This commit tries to use the same order of imports for every file, and describes the convention in ProofGuide.md. There is one exception, where we do not follow said convention: in program_logic/weakestpre.v, using that order would break printing of texan triples (??).
-
- Mar 05, 2019
-
-
Ralf Jung authored
-
- Feb 20, 2019
-
-
Robbert Krebbers authored
-
- Jan 24, 2019
-
-
Maxime Dénès authored
This is in preparation for coq/coq#9274.
-
- Jan 11, 2019
-
-
Robbert Krebbers authored
-
- May 03, 2018
-
-
Ralf Jung authored
-
- May 02, 2018
-
-
Ralf Jung authored
If the accessor introduces a binder, the first Coq-level intro pattern of `iInv` is used for that binder unless the type of the binder is unit, in which case `iInv` removes it completely. Binders on the closing view shift are not (yet) supported as they are harder to smoothly eliminate in the unit case.
-
- Apr 26, 2018
-
-
Ralf Jung authored
New IntoAcc typeclass to decouple creating and elliminating accessors; ElimInv supports both with and without Hclose
-
- Apr 25, 2018
- Apr 04, 2018
-
-
Robbert Krebbers authored
Extend ElimModal with Boolean flags to specify whether it operates on the persistent/spatial context.
-
- Apr 03, 2018
-
-
Robbert Krebbers authored
The closing view shift's LHS mask is now universally quantified, which makes it easier to execute the closing view shift.
-
Robbert Krebbers authored
-
- Mar 05, 2018
-
-
Ralf Jung authored
This is backwards-compatible; it desugars to a normal application on previous versions
-
- Mar 01, 2018
-
-
Jacques-Henri Jourdan authored
This requires changing the Hint Mode of the [Frame] type class because it should not fail if its parameter is an evar, but instantiate it instead. In order to prevent all the other instances of [Frame] to intantiate this evar themselves, we create a new type class [KnwonFrame], which corresponds to the old behavior.
-
Jacques-Henri Jourdan authored
-
Jacques-Henri Jourdan authored
-
- Feb 23, 2018
-
-
Robbert Krebbers authored
-
Joseph Tassarotti authored
-
Robbert Krebbers authored
-
Joseph Tassarotti authored
-
- Feb 21, 2018
-
-
Robbert Krebbers authored
-
- Jan 24, 2018
-
-
Robbert Krebbers authored
This partially solves #112.
-
- Dec 11, 2017
-
-
Jacques-Henri Jourdan authored
-
- Nov 13, 2017
-
-
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.
-
- Oct 30, 2017
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
- Oct 25, 2017
-
-
Robbert Krebbers authored
-
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.
-
- Sep 26, 2017
-
-
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`.
-
- Sep 17, 2017
-
-
Robbert Krebbers authored
-
- Mar 22, 2017
-
-
Ralf Jung authored
-
- Jan 11, 2017
-
-
Ralf Jung authored
This approach is originally by Robbert
-
- Jan 05, 2017
-
-
Ralf Jung authored
-
Robbert Krebbers authored
-
- Jan 04, 2017
-
- Jan 03, 2017
-
-
Ralf Jung authored
This patch was created using find -name *.v | xargs -L 1 awk -i inplace '{from = 0} /^From/{ from = 1; ever_from = 1} { if (from == 0 && seen == 0 && ever_from == 1) { print "Set Default Proof Using \"Type*\"."; seen = 1 } }1 ' and some minor manual editing
-