Proofs that end with Exists.choose_spec

Stream: mathlib4

[Robert Maxton]

I seem to keep writing proofs relying on Exists.choose, whose final line turn out to be essentially Exists.choose_spec, except that the existential hypothesis has either been transformed into something ugly, or I've simply lost the original name. Currently, I handle this with

...
simp
generalize_proofs h
exact h.choose_spec

or the like; but this is of course a non-terminal simp. Is there a systematically better way to handle this I don't know about?

[Robert Maxton]

(The main issue here, I believe, is that there's no nice way to address the existential hypothesis; I've tried simpa using Exists.choose_spec _, for example, but unless it's simple enough that I can just fill in the name myself that doesn't seem to work.)

[Robert Maxton]

I could use generalize_proofs before the simp, but then I end up with many proofs I would have to separately combine, probably with another simp anyway.

[Ruben Van de Velde]

It surprises me that you end up in this situation. Would it not be easier to do obtain \<x, hx\> := h_exists rather than let x := Exists.choose h_exists?

[Sébastien Gouëzel]

Instead of using Exists.choose, can you use the choose tactic, which is much more user-friendly?

[Robert Maxton]

Ruben Van de Velde said:

It surprises me that you end up in this situation. Would it not be easier to do obtain \<x, hx\> := h_exists rather than let x := Exists.choose h_exists?

I usually don't do either, actually; I just have e.g. hom | ⟨x, hx⟩ => (hx (𝟙 _)).choose

[Robert Maxton]

Sébastien Gouëzel said:

Instead of using Exists.choose, can you use the choose tactic, which is much more user-friendly?

Hm. Let's find out.

[Robert Maxton]

Nope; or, well, certainly I can write hom | ⟨x, hx⟩ => by choose y hy using hx (𝟙 _); exact y instead, but when I then have to interact with that definition later simpa using (Classical.choose_spec _) doesn't work

[Ruben Van de Velde]

I see

[Robert Maxton]

... I suppose I should probably have been more specific: the issue is with defining data at one point in a definition with Exists.choose, where later I need to access that data with Exists.choose_spec

[Robert Maxton]

... I could use Classical.indefiniteDescription everywhere instead; that would be ugly but might be more compatible with automation...

[Ruben Van de Velde]

In that case it might be easier to create an auxiliary def with the result of Exists.choose and add a specialized lemma about that def with Exists.choose_spec

[Ruben Van de Velde]

I'm reasonably sure Classical.indefiniteDescription would be more painful

[Robert Maxton]

Well, it'd mean that the last line of my data generation is Subtype.val _, which sometimes simp seems to be able to exploit automatically via Subtype.coe_prop.

[Robert Maxton]

Ruben Van de Velde said:

In that case it might be easier to create an auxiliary def with the result of Exists.choose and add a specialized lemma about that def with Exists.choose_spec

Mm. That would be somewhat unpleasant as this is occurring in a rather deeply nested series of definitions, but that itself probably isn't great practice... I'll think about it.

[Sébastien Gouëzel]

Do you have a #mwe?

[Yury G. Kudryashov]

BTW, I think that we should have an attribute version of the choose tactic. It should take a lemma claiming \forall a b, \ex x, p x \and q x and output def with lemmas.

[Yury G. Kudryashov]

(both choose and choose! versions can be useful)

[Kyle Miller]

Maybe @[split] could in general destruct the target type and make new declarations, using some list of types that we'd normally split (curry) if they were arguments to a function or lemma. What come to mind: and, exists, sigma, subtype, maybe prod.

Ah, maybe the syntax is @[split ⟨thm1, ⟨thm2, thm3⟩, thm4⟩] and there does not need to be a list of "blessed" types. There would be an implicit intro for this destruct syntax, so for example the ⟨thm2, thm3⟩ could be parameterized by more arguments if it's a forall there.

[Kyle Miller]

(Somewhat related: the discussion about mutual induction. This link is to joint theorem definitions.)

[Yury G. Kudryashov]

Should it be a superset of alias?