 20 Sep, 2016 10 commits


Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored
This also solves a name clash with the extension order of CMRAs.

Robbert Krebbers authored
Before, it failed when these tactics were invoked with persistent hypotheses. The new behavior is more convenient when using these tactics to build other tactics.

Robbert Krebbers authored

Robbert Krebbers authored

 19 Sep, 2016 8 commits


Robbert Krebbers authored
This comment mostly addresses issue #34. There are still some issues:  For iLöb we can write `iLöb (x1 .. xn) as "IH"` to revert x1 .. xn before performing Löb induction. An analogue notation for iInduction results in parsing conflicts.  The names of the induction hypotheses in the Coq intro pattern are ignored. Instead, when using `iInduction x as pat "IH"` the induction hypotheses are given fresh names starting with "IH". The problem here is that the names in the introduction pattern are idents, whereas the induction hypotheses are inserted into the proof mode context, and thus need to have strings as names.

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored
This closes issue 32.

Robbert Krebbers authored

Robbert Krebbers authored
This solves issue 33.

Robbert Krebbers authored

 15 Sep, 2016 3 commits


JacquesHenri Jourdan authored

JacquesHenri Jourdan authored

JacquesHenri Jourdan authored

 14 Sep, 2016 5 commits


JacquesHenri Jourdan authored
This makes the typeclass mechanism able to use instances like [Is_true X > Blah], where X reduces to X.

Amin Timany authored

Amin Timany authored

Amin Timany authored
We need to change the core of X from ∅ to X to make elements of gset persistent.


 13 Sep, 2016 1 commit


JacquesHenri Jourdan authored

 12 Sep, 2016 1 commit


 09 Sep, 2016 9 commits


Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

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.

Robbert Krebbers authored

Robbert Krebbers authored

JacquesHenri Jourdan authored

JacquesHenri Jourdan authored

 08 Sep, 2016 1 commit


Ralf Jung authored
rvs is (classically) equivalent to a kind of double negation Proofs showing that rvs is equivalent to a kind of stepindexed double negation modality under classical axioms. For now, placed in algebra/double_negation.v until the new directory structure is finalized. cc: @jung @robbertkrebbers See merge request !8

 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
