Classical.choose problem

Stream: lean4

[Martin Dvořák]

I would like to resolve the last sorry here:

import Mathlib.Tactic.LibrarySearch

def Foo {α : Type} : α → Prop := sorry

theorem exFoo (α : Type) : ∃ a : α, Foo a := sorry

noncomputable example {α : Type} : Foo (Classical.choose (exFoo α)) :=
  sorry

[Dagur Asgeirsson]

(exFoo α).choose_spec?

[Martin Dvořák]

Is it a bug that neither exact? nor apply? gave me a suggestion?

[Dagur Asgeirsson]

I don't know, probably :open_mouth:

[Martin Dvořák]

Also simp [Foo, exFoo] failed to close the goal (no matter whether classical was called beforehand).

[Eric Rodriguez]

Martin Dvořák said:

Is it a bug that neither exact? nor apply? gave me a suggestion?

Does it happen after you rewrite exFoo?

[Eric Rodriguez]

Wait, never mind. I'd say this is a bug, but maybe this is on the list of 'common' things that is excluded for performance

[Eric Rodriguez]

I think it's hard to match on patterns of the style ?f x

[Martin Dvořák]

I need to say that exact? failed me again today (and so did my memory, but that's besides the point here):
https://leanprover.zulipchat.com/#narrow/stream/348111-std4/topic/.E2.9C.94.20.60Exists.2Echoose.60.20has.20the.20property

[Martin Dvořák]

For future reference:

import Mathlib.Tactic.LibrarySearch

def Foo {α : Type} : α → Prop := sorry

theorem exFoo (α : Type) : ∃ a : α, Foo a := sorry

example {α : Type} : Foo (exFoo α).choose :=
  (exFoo α).choose_spec -- no result from `by exact?`

[Patrick Massot]

I think exact? looks for theorem whose conclusion starts with Foo, and doesn't find any.

[Patrick Massot]

It is frustrating, but also means exact? can scale to the current size of Mathlib. The Lean 3 version tried to apply every lemma, and I think it would have succeeded here. But it became unusable when Mathlib grew to 1 million lines.

[Martin Dvořák]

Well, I don't import Mathlib so the old version was normally fine for me.

[Martin Dvořák]

(deleted)

[Martin Dvořák]

What would I have to do for aesop to find the proof here? It doesn't succeed "out of the box".

aesop: failed to prove the goal after exhaustive search.

[Eric Wieser]

Can we just put this in the docstring of docs#Exist.choose ?

[Jannis Limperg]

Martin Dvořák said:

What would I have to do for aesop to find the proof here? It doesn't succeed "out of the box".

aesop: failed to prove the goal after exhaustive search.

attribute [aesop safe] Exists.choose_spec

[Scott Morrison]

Jannis' suggestion here initially sounds like an unhelpful answer, but if you read it that way you are missing the point.

Mostly aesop more powerful is like making simp more powerful: it requires PRs.

• Look at a goal and think "aesop should prove this"
• Be sad when it doesn't
• Think about the step it failed at, and come up with an aesop attribute that would help.
• Test locally
• DON'T STOP HERE
• Add that attribute in Mathlib at the earliest relevant point
• Fire off a PR to see if Mathlib builds, and run !bench to make sure it doesn't cause a bad regression
• Now everyone for ever after gets their problems solved by aesop.

[Jannis Limperg]

Yes! Sorry if my answer was unclear; Scott's process is what I had in mind.

[Eric Wieser]

Scott Morrison said:

Mostly aesop more powerful is like making simp more powerful: it requires PRs.

In this case, presumably choose_spec would be a bad simp lemma for performance reasons, as it has nothing to index the head symbol on. Is the same not true of aesop?

[Martin Dvořák]

How can I find the "earliest relevant point" please?

[Ruben Van de Velde]

You can try #find_home nameOfLemma

[Martin Dvořák]

I didn't know this command, thanks, but I want to find home for the aesop attribute.

[Damiano Testa]

I am not sure about the specific issue with the aesop attribute, but #find_home tends to work best with import Mathlib: it looks for the earliest file among the ones that are currently imported.

[Scott Morrison]

Usually aesop attributes should go with the definition. Currently we can't put aesop attributes in Std, but we're thinking about this.

[Mario Carneiro]

aesop depends on std, so in principle it could have a file for this

[Mario Carneiro]

I am a bit dubious about the merit of this particular attribute as mentioned above though

[Mario Carneiro]

I think the right way to handle choose_spec is to detect that h.choose is in the goal or hypotheses and add have := h.choose_spec in that case

[Mario Carneiro]

unifying it against random goals is horribly inefficient

[Martin Dvořák]

Mario Carneiro said:

I think the right way to handle choose_spec is to detect that h.choose is in the goal or hypotheses and add have := h.choose_spec in that case

You mean manually, or by a tactic?

[Mario Carneiro]

we're talking about aesop handling here

[Mario Carneiro]

of course you can do that by hand too

[Mario Carneiro]

but throwing it into a big soup of "things aesop knows about" is likely to end badly unless it either learns specifically how this kind of lemma is supposed to be used or it learns specifically about Exists.choose through some hard coded rules

[Scott Morrison]

This would be a fun tactic. It could even be generalized in useful ways, e.g. something that could either:

• look through the context for h.choose, and add h.choose_spec if it didn't already exist
• look through the context for ((n : Nat) : Int), and add h : 0 \le (n : Int) if it didn't already exist
  etc.

You would specify what patterns to look for, and the statements to construct from them, by some convenient user command.

[Patrick Massot]

The last example should be part of zify, together with trying to create inequalities for every Nat subtraction appearing.

[Jannis Limperg]

Indeed the rule I suggested would not be very efficient. @Xavier Généreux and I are currently working on making Aesop's forward reasoning suck less, and part of this will hopefully be efficient support for forward rules that look for a pattern in the goal, such as a choose_spec rule that looks for occurrences of Exists.choose. It'll probably be a while before this is available though.

[Scott Morrison]

Patrick Massot said:

The last example should be part of zify, together with trying to create inequalities for every Nat subtraction appearing.

Yes, I have something like this in omega now, which is why I suggested it here. It could be more efficient... I'll work out how to make it available separately as well.

[Scott Morrison]

Ideally this sort of pattern-matching-forward reasoning could be made available separately from aesop, even if aesop then uses it.

[James Gallicchio]

saturate | <pat> => <new-hypothesis>? it'd be really nice in termination-tactics as well, since forward reasoning for termination is a bit awkward atm

[James Gallicchio]

saturate is the wrong word for it, saturation should berepeated application of the forward reasoning tactic

[Jannis Limperg]

Scott Morrison said:

Ideally this sort of pattern-matching-forward reasoning could be made available separately from aesop, even if aesop then uses it.

That's a good idea; I'll try to keep the implementation self-contained.