Zulip Chat Archive

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 :=
  have : ( a : α, P a)  _,
  { apply equiv.forall_congr, },

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: Dec 20 2023 at 11:08 UTC