tactic.apply does follow spec / specified poorly

Stream: general

[Scott Morrison]

The apply tactic has an option new_goals, which should be one of

/-- How to order the new goals made from an `apply` tactic.
Supposing we were applying `e : ∀ (a:α) (p : P(a)), Q`
- `non_dep_first` would produce goals `⊢ P(?m)`, `⊢ α`. It puts the P goal at the front because none of the arguments after `p` in `e` depend on `p`. It doesn't matter what the result `Q` depends on.
- `non_dep_only` would produce goal `⊢ P(?m)`.
- `all` would produce goals `⊢ α`, `⊢ P(?m)`.
-/
inductive new_goals
| non_dep_first | non_dep_only | all

(non_dep_first is the default behaviour).

However I've just noticed that this only applies the one of the goals --- apply will put the _most_ dependent argument first, but then not worry about furthering ordering of goals.

Here's an example:

import data.equiv.basic

example {α : Type} (P : α → Prop) : true :=
begin
  have : (∀ a : α, P a) ↔ _,
  { apply equiv.forall_congr, },
end

After the apply statement we get the goals:

4 goals
α : Type,
P : α → Prop
⊢ ∀ {x : α}, P x ↔ ?m_1 (⇑?m_3 x)

α : Type,
P : α → Prop
⊢ Sort ?

α : Type,
P : α → Prop
⊢ ?m_1 → Prop

α : Type,
P : α → Prop
⊢ α ≃ ?m_1

Here I'd argue that what has been presented as the second goal should actually come last, as both the third and fourth goals depend on it.

[Scott Morrison]

It's not a bug per se, perhaps just unspecified.

[Scott Morrison]

I thought a little about patching this (in Lean, not C++), but it seemed painful. The partial ordering on expressions by "depending on" is pretty easy to implement, but it seems we don't have an insertion sort algorithm for "ordering" a list under a partial ordering ...

[Scott Morrison]

Having this fixed wouldn't actually solve my underlying problem, because what I really care about is that the 4th goal in the example above comes before either the 2nd or 3rd, and there's I think no principled way to argue this should be the output of apply...