 14 Nov, 2017 7 commits


Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored
This gives a 25% speedup on some files (e.g. boxes). This commit contains some hacks to work arround Coq issue #5699. This commit requires Coq v8.7 together with https://github.com/coq/coq/pull/1006

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored
This is an old flag set by the ssr plugin, and recently unset in coqstdpp, see https://gitlab.mpisws.org/robbertkrebbers/coqstdpp/issues/5.

Robbert Krebbers authored

 13 Nov, 2017 10 commits


Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert authored
Improved treatment of anonymous hypotheses in the proof mode See merge request FP/iriscoq!83

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

Robbert Krebbers authored

 12 Nov, 2017 1 commit


Robbert Krebbers authored

 11 Nov, 2017 7 commits


Robbert authored
Get rid of `later_proper'` See merge request FP/iriscoq!82

Robbert Krebbers authored

Robbert Krebbers authored

Ralf Jung authored
add later_ne; make later_proper match the other _proper lemmas See merge request FP/iriscoq!81

Ralf Jung authored

Robbert Krebbers authored

Robbert Krebbers authored

 09 Nov, 2017 8 commits


David Swasey authored
Add progress bit to WP. See merge request FP/iriscoq!37

David Swasey authored

David Swasey authored

David Swasey authored
This is derived from `wp_forget_not_stuck` and a trivial preorder on stuckness bits. (The two lemmas are redundant, but I have examples where each seems more natural than the other.) I did *not* bake `wp_stuckness_mono` into `strong_mono` for two reasons. Mainly, I didn't see a nice way to combine the two proofs (beyond `cut`). Less important, changing the type of `wp_strong_mono` will break code.

David Swasey authored
I saw no need for `stuckness_flip`: strong atomicity always works, while weak atomicity works only for expressions that are not stuck. Since this seemed unclear, I split lemma `wp_atomic'` up into `wp_strong_atomic` (parametric in the WP's `s`) and `wp_weak_atomic` (not). The proof mode instance is stated in terms of the derived rule `wp_atomic` (parametric in `s`).

David Swasey authored

David Swasey authored
 08 Nov, 2017 7 commits


David Swasey authored

David Swasey authored

David Swasey authored

David Swasey authored

David Swasey authored

David Swasey authored
Pull progress bit out of the WP fixpoint, make (most) wp adequacy notation only parsing, and generalize forget_progress.

David Swasey authored
