Tej Chajed authored Dec 01, 2020 and Robbert Krebbers committed Dec 01, 2020

`iDestruct ("H" with "HP")` where "H" is persistent is supposed to
consume "H" if it isn't a forall. Due to a bug in the tactic, this
behavior was never triggered and "H" was always left alone.

This test is incompatible with Coq 8.8 and Coq 8.9, but Iris no longer
supports those versions.

put it into a type class `BiPureForall`.

This property does not hold for embeddings of classical logic into Coq.

A failing iIntros for implications should prettify the identifier before
printing, and iIntros on something that isn't a wand or implication
should say what couldn't be introduced (to clarify that `iIntros "HP
HQ"` failed because of the HQ in particular, for example).

`iDestruct H as "H1 H2"` produces an error that says the pattern should
contain exactly one proper introduction pattern. When multiple patterns
are provided, due to Ltac variable shadowing iDestructHypFindPat was
instead reporting only the first pattern in the error message (and even
that was printed as the parsed AST rather than the original string).

The error handling for `iIntro (?)` and similar tactics didn't correctly
report failures when the goal couldn't be turned into a universal
quantifier. This is something missing from !482 due to no test
triggering the error.

Tej Chajed authored Jul 22, 2020 and Robbert Krebbers committed Jul 22, 2020

Fixes #337.

Preserve identifiers in binders where possible, analogous to the support
for destructing existentials in !479.

Fixes #336.

Tej Chajed authored Jul 21, 2020 and Robbert Krebbers committed Jul 21, 2020

When running `iDestruct "H" as (?) "H"`, use the name of the binder in
"H". For example, if "H" has type `∃ y, Φ y`,  we now use `y` as the
name of the variable after freshening. Previously the name was always
the equivalent of running `fresh H`.

The implementation achieves this by forwarding the desired identifier
name through the `IntoExist` typeclass. Identifiers are serialized in
Gallina by using them as the name of a function of type `ident_name :=
unit -> unit`.

Fixes #325.

Also added a tests for the various `iSpecialize` error cases involving
the `[%]` and `[//]` specialization patterns.

Fixes #319

Fix #302, including their ASCII variants.
- Don't use quotes `'` that are not surrounded by spaces.
- However, notation `'(⊢@{' PROP } )` prevents parsing `(⊢@{PROP} Q)` using the
`⊢@{PROP} Q` notation.

To fix that, we force left-factorization: we add a notation for `'(⊢@{' PROP }
Q )`, defined to coincide with '⊢@{' PROP } Q but which can be left-factored
with `( '⊢@{' PROP } )`.

- Add left and right operator sections for (bi)entailment
- Add tests.

Also do all of the above also for ASCII notations, except for operator sections,
which seem to require more discussion.

Fixes #307.

Notably this support relies on string to identifier conversion, which
works natively using Ltac2 in Coq 8.11+ and with a plugin
(https://github.com/ppedrot/coq-string-ident) in Coq 8.10. To use it,
you must replace intro_patterns.string_to_ident_hook with a real
implementation; see https://gitlab.mpi-sws.org/iris/string-ident for a
working implementation that works with Coq 8.11 (using Ltac2).

The syntax is %H (within a string intro pattern). This is technically
backwards-incompatible, because this was previously supported and parsed
as % and H separately. To restore the old behavior, separate with a
space, eg [% H].

- The error messages were wrong: the goal needs to be absorbing, not the hypothesis.
- The wrong failure number was used in `iAssumption`, which caused the error not
  to be propagated properly.

Gregory Malecha authored Mar 16, 2020 and Robbert Krebbers committed Mar 16, 2020

- remove "odd" comment
- move atomic triples to bi_scope