mathlib4#856 refactor of solve_by_elim

Stream: PR reviews

[Scott Morrison]

I would like to get mathlib4#856 merged (both because it keeps rotting, and because I think we can build several other useful tactics on top of it).

However I'm encountering a weird problem, explained here.

In particular, the line

solve_by_elim [le_trans _ hy']

is showing the error unknown identifier 'hy''. However solve_by_elim is working perfectly, successfully closing the goal using hy'. (See the #print statement below.)

I can't work out who is generating this error, and why? Perhaps I'm just doing something dumb, or perhaps something relating to the user interface (showing tooltips, etc) is having trouble?

Note that solve_by_elim has to do some fancy delayed elaboration of its arguments (because it may need to apply them multiple times, so has to have fresh metavariables each time). I'm guessing that this is something to do with the problem, but given that solve_by_elim is correctly closing the goal, I'm not really sure what this could be about.

[Scott Morrison]

@Mario Carneiro, if you had a chance to look at this that would be wonderful. :-)

[Mario Carneiro]

I just debugged a very similar error in linarith reported by @Heather Macbeth , and the issue was a missing withMainContext / g.withContext

[Mario Carneiro]

@Scott Morrison I took a look, and there seems to be a call to elabTerm inside partitionLocalHyps which is not wrapped in any withContext even though the documentation says it expects to be called in the context of one

[Mario Carneiro]

The tactic seems to be working on multiple goals though so I'm not sure what the intended behavior is

[Scott Morrison]

Thanks, I'll investigate that, and document behavior for solve_by_elim*, that operates on multiple user facing goals.

[Scott Morrison]

Okay, I've simply removed partitionLocalHyps. It was an over-optimisation that wasn't necessary in the first place.

Now we only run elabTerm when we need to, rather than trying once at the beginning to partition arguments into expressions and local hypotheses. If you specify many -h arguments to solve_by_elim, these will now be elaborated more times as solve_by_elim runs, but it seems rather unlikely this could ever be a performance problem.

[Eric Wieser]

Does this mean that solve_by_elim will now not elaborate some terms at all?

[Eric Wieser]

I.e, does this introduce the norm_num [this is nonsense] bug that we have in lean 3, for solve_by_elim?

[Scott Morrison]

No, solve_by_elim will always elaborate the terms you pass it (in fact, it will re-elaborate them every time they could be used, to avoid stuck metavariables on seperate applications).

The fix described in this thread means that we don't elaborate terms one extra time, to see if we can avoid re-elaborating them repeatedly later (on the basis that if they are local hyps we can just store the FVarId)

[Scott Morrison]

I've just merged master again on this PR.