 16 Oct, 2016 1 commit


JacquesHenri Jourdan authored
This fact is deduced from reducibility. Unfortunately, this sometimes depends on the type of states being inhabited, so that this additional hypothesis sometimes appear.

 13 Oct, 2016 2 commits
 12 Oct, 2016 3 commits


Ralf Jung authored
rename program_logic.{ownership > wsat}. It really is about world satisfaction and invariants more than about ownership.

Robbert Krebbers authored

Ralf Jung authored

 10 Oct, 2016 3 commits
 07 Oct, 2016 1 commit


Ralf Jung authored

 06 Oct, 2016 1 commit


Robbert Krebbers authored

 05 Oct, 2016 1 commit


Robbert Krebbers authored

 28 Sep, 2016 2 commits


Robbert Krebbers authored
This allows us to factor out properties about connectives that commute with the big operators.

Robbert Krebbers authored

 27 Sep, 2016 2 commits


Robbert Krebbers authored
Used in iRevert, iClear, iFrame, and for generalizing the IH in iInduction and iLöb.

Robbert Krebbers authored
As proposed by JH Jourdan in issue 34.

 20 Sep, 2016 4 commits


Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

 09 Sep, 2016 3 commits


Robbert Krebbers authored

Robbert Krebbers authored
Before this commit, given "HP" : P and "H" : P ★ Q with Q persistent, one could write: iSpecialize ("H" with "#HP") to eliminate the wand in "H" while keeping the resource "HP". The lemma: own_valid : own γ x ⊢ ✓ x was the prototypical example where this pattern (using the #) was used. However, the pattern was too limited. For example, given "H" : P₁ ★ P₂ ★ Q", one could not write iSpecialize ("H" with "#HP₁") because P₂ ★ Q is not persistent, even when Q is. So, instead, this commit introduces the following tactic: iSpecialize pm_trm as # which allows one to eliminate implications and wands while being able to use all hypotheses to prove the premises, as well as being able to use all hypotheses to prove the resulting goal. In the case of iDestruct, we now check whether all branches of the introduction pattern start with an `#` (moving the hypothesis to the persistent context) or `%` (moving the hypothesis to the pure Coq context). If this is the case, we allow one to use all hypotheses for proving the premises, as well as for proving the resulting goal.

JacquesHenri Jourdan authored

 07 Sep, 2016 2 commits


JacquesHenri Jourdan authored
Define disjointness of namespaces in terms of masks.\n\nThe proofs are made simpler and some lemmas get more general.

JacquesHenri Jourdan authored

 06 Sep, 2016 1 commit


Robbert Krebbers authored
I had to perform some renaming to avoid name clashes.

 05 Sep, 2016 1 commit


JacquesHenri Jourdan authored

 04 Sep, 2016 1 commit


Robbert Krebbers authored

 29 Aug, 2016 3 commits


Robbert Krebbers authored
This way we ensure that Coq gives an error message when one accidentially writes "N ⊆ E" instead of "nclose N ⊆ E". Before, it used the ⊆ instance of lists.

Robbert Krebbers authored
This avoids Coq distinguishing iProp and uPred (iResUR _) when it should not.

Robbert Krebbers authored
(which are useful in Amin's logical relations development).

 28 Aug, 2016 1 commit


Robbert Krebbers authored
This also removes the double use of the name 'wp_fork' in both program_logic/weakestpre and heap_lang/lifting.

 25 Aug, 2016 5 commits


Robbert Krebbers authored

Janno authored

Robbert Krebbers authored
Following the time anology of later, the stepindex 0 corresponds does not correspond to 'now', but rather to the end of time (i.e. 'last').

Robbert Krebbers authored

Robbert Krebbers authored
Make names more consistent with the rest of the development, make definitions type classes opaque so that the proofmode does not unfold then, declare timeless, persistent and proper instances.

 23 Aug, 2016 1 commit


Robbert Krebbers authored

 22 Aug, 2016 2 commits


Robbert Krebbers authored

Robbert Krebbers authored
This implements issue #3.
