Zulip Chat Archive

Stream: general

Topic: tactic.apply does follow spec / specified poorly


view this post on Zulip 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.

view this post on Zulip Scott Morrison (Mar 31 2020 at 01:30):

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

view this post on Zulip 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 ...

view this post on Zulip 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