## Stream: general

### Topic: tactic.apply does follow spec / specified poorly

#### Scott Morrison (Mar 31 2020 at 01:25):

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 (Mar 31 2020 at 01:30):

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

#### Scott Morrison (Mar 31 2020 at 01:31):

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 (Mar 31 2020 at 01:32):

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...

Last updated: May 11 2021 at 23:11 UTC