Improving recursive inspection of hypotheses for hint generation
Currently, to generate a good BiAbd/Abduct instance for application, we look beneath literal connectives until we can't.
Then, we start looking for AtomIntoExist
, AtomIntoWand
, etc instances.
We could improve this by having one class, AtomIntoConnective A C : atom_into_connective := A ⊢ C
where A
should be an atom, and C
an arbitrary connective. This would give us additional expressive power:
- For one, it allows the following instance:
AtomIntoConnective (if b then P else Q) ((P ∗ (b = true)) ∨ (Q ∗ (b = false))
. This may be very nice for closing atomic updates. - It also reduces the number of available classes.
- We need to think about how we could still support the extension of proving literal wands, if available.
- In the future, maybe we could write some smart Ltac to autogenerate such recursive inspections for arbitrary user-defined fixpoints.