• Robbert Krebbers's avatar
    Support for specialization of P₁ -★ .. -★ Pₙ -★ Q where Q is persistent. · 090aaea3
    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.
    090aaea3
ProofMode.md 9.54 KB