Support destructing exists with intro patterns

Closes #310

See merge request !658

This note is obsolete due to iris/iris!640

generalize into_and_sep_affine so that generalizing just the conjunction instance for IntoExist is sufficient

Tej Chajed authored 4 years ago and Ralf Jung committed 3 years ago

The syntax re-uses the existing support for pure names, namely the % and
%H patterns. Using "[% H]" is like `iDestruct ... as (?) "H"` and using
"[%x H]" (with the string-ident plugin) is like `iDestruct ... as (x)
"H"`.

This changes how these patterns are parsed. Previously, both would have
been handled as conjunctions (using IntoAnd or IntoSep, depending on
whether the hypothesis is persistent or not). This means it was possible
for the user to use "[% H]" to destruct a pure hypothesis ⌜φ ∧ ψ⌝ and
put only the first conjunct in the Gallina context, leaving the other
one in the IPM; such patterns will now break, since iExistDestruct
does not handle this use case.

Provide functionality from string_ident natively

Closes #404

See merge request iris/iris!640

Tej Chajed authored 3 years ago and Ralf Jung committed 3 years ago

Fixes #404

Add big-op lemmas to ghost map

See merge request iris/iris!649

Add a verified interpreter for HeapLang

See merge request iris/iris!564

add more lemmas to list RA and move it to iris-staging

See merge request iris/iris!654