 13 Feb, 2017 1 commit


Ralf Jung authored

 12 Feb, 2017 1 commit


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.

 11 Feb, 2017 7 commits


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 nonempty.  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

David Swasey authored

 10 Feb, 2017 6 commits


Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

 09 Feb, 2017 6 commits


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

 07 Feb, 2017 4 commits
 06 Feb, 2017 1 commit


Ralf Jung authored

 03 Feb, 2017 1 commit


Robbert Krebbers authored

 02 Feb, 2017 2 commits
 01 Feb, 2017 3 commits


Robbert Krebbers authored
It no longer requires the functions on both sides of the relation to be syntactically the same.

Robbert Krebbers authored

JacquesHenri 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. Identityfree 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.

 30 Jan, 2017 6 commits


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 /= H2H2]`  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

JacquesHenri Jourdan authored

 29 Jan, 2017 1 commit


Robbert Krebbers authored

 28 Jan, 2017 1 commit


Ralf Jung authored
notation for declaring a function nonexpansive See merge request !42
