- Feb 13, 2017
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Jacques-Henri Jourdan authored
When using [iAssert ... with ">[]"], we should not use [tac_assert_persistent], and eliminate the modality instead. This patch is still not ideal, because some modalities (e.g., later) preserve persistence.
-
- Feb 12, 2017
-
-
Robbert Krebbers authored
For example, when having `"H" : ∀ x : Z, P x`, using `iSpecialize ("H" $! (0:nat))` now works. We do this by first resolving the `IntoForall` type class, and then instantiating the quantifier.
-
- Feb 11, 2017
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
Instead of doing all the instantiations by invoking a single type class search, it now performs the instantiations by invoking individual type class searches. This a.) gives better error messages and b.) works when `xj` depends on `xi`.
-
Robbert Krebbers authored
In the following ways: - When having `P → Q` it will now also work when the spatial context is non-empty. - When having `∀ x : A, Q` it will now do an `iIntros (_)`.
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Ralf Jung authored
Make it possible to apply the observational view shift lemmas. See merge request !40
-
-
- Feb 10, 2017
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
- Feb 09, 2017
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
In this case, we cannot use all the hypotheses for proving the premises as well as for the remaining goal.
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
- Feb 07, 2017
- Feb 06, 2017
-
-
Ralf Jung authored
-
- Feb 03, 2017
-
-
Robbert Krebbers authored
-
- Feb 02, 2017
- Feb 01, 2017
-
-
Robbert Krebbers authored
It no longer requires the functions on both sides of the relation to be syntactically the same.
-
Robbert Krebbers authored
-
Jacques-Henri Jourdan authored
Cancelable elements are a new way of proving local updates, by removing some cancellable element of the global state, provided that we own it and we are willing to lose this ownership. Identity-free elements are an auxiliary that is necessary to prove that [Some x] is cancelable. For technical reasons, these two notions are not defined exactly like what one might expect, but also take into account validity. Otherwise, an exclusive element would not be cancelable or idfree, which is rather confusing.
-
- Jan 30, 2017
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
This fixes issue #57. I considered supporting these introduction patterns also in a nested fashion -- for example allowing `iDestruct foo as [H1 [{H1} H1 /= H2|H2]` -- but that turned out to be quite difficult. Where should we allow `/=`, `{H}` and `{$H}` exactly. Clearly something like `>/=` makes no sense, unless we adopt to some kind of 'stack like' semantics for introduction patterns as in ssreflect. Alternatively, we could only allow these patterns in the branches of the destructing introduction pattern `[... | ... | ...]` but that brings other complications, e.g.: - What to do with `(H1 & /= & H3)`? - How to distinguish the introduction patterns `[H _]` and `[_ H]` for destructing a spatial conjunction? We cannot simply match on the shape of the introduction pattern anymore, because one could also write `[_ H /=]`.
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Jacques-Henri Jourdan authored
-