 09 Sep, 2016 6 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.

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 3 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

Joseph Tassarotti authored

 06 Sep, 2016 6 commits


Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

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

 05 Sep, 2016 3 commits


Robbert Krebbers authored

JacquesHenri Jourdan authored

Robbert Krebbers authored

 04 Sep, 2016 1 commit


Robbert Krebbers authored

 02 Sep, 2016 1 commit


Robbert Krebbers authored

 01 Sep, 2016 5 commits


Joseph Tassarotti authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

 31 Aug, 2016 6 commits


Robbert Krebbers authored

Robbert Krebbers authored
Annoyingly, this requires one to prove the following in the model: (∀ x : A, ■ φ x) ⊢ ■ (∀ x : A, φ x)

Joseph Tassarotti authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

 30 Aug, 2016 6 commits


Robbert Krebbers authored
Thanks to Ranald Clouston for suggesting the axiom: ▷ P ⊢ ▷ False ∨ (▷ False → P) This axiom is used to prove timeless of implication, wand and forall. Timelessness of the pure and ownM connectives is still proven in the model, but we first state the property in a way that it does not involved derived notions (like the except_last modality).

Robbert Krebbers authored
It is unused, and ownM_empty is stronger.

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored
For that we need a slightly stronger property for distributing a later over an existential quantifier.

Robbert Krebbers authored

 29 Aug, 2016 2 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
