Remove SolveSep normalization, replace with empty_hyp_first
SolveSep
currently has a boolean argument, specifying whether the first premise has been normalized. If not, the first thing the current automation does, is normalize it. Only then are other rules applied.
This normalization is probably only strictly necessary for supporting some disjunctions. It also clutters the SolveSep
definition.
Another problem is that there is not yet a good way to for using WP
/other specs in the proof automation. Currently there is a specific IntoSolveGoal
instance that takes a ReductionStep
as a source. It would be nice if we can unhook this from the proof automation, and instead use a BiAbd
, which are meant to be extended.
The proposal is to add a new vacuous hypothesis empty_hyp_first
, so that for goals of the form Δ ⊢ SolveSep M Q T
, we first look for a empty_hyp_first ∗ [R] ⊲ [M] Q ∗ [S]
. Instances of this should be simplifications that should always be applied. If one cannot be found, we continue as usual by looking. Examples of new instances will precisely be the disjunction simplification (which will require progress), and application of a WP spec.