How much choice is too much choice?

Stream: general

[Eric Wieser]

In a few reviews, I've suggested changing code within theorems along the lines of

example {α : Type*} (p : α → Prop) (h : ∃ x, p x) : true := begin
  have := foo h.some h.some_spec, -- edit, thanks Johan: no need to use long `classical` names
  trivial,
end

to

example {α : Type*} (p : α → Prop) (h : ∃ x, p x) : true := begin
  obtain ⟨x, px⟩ := h,
  have := foo x px,
  trivial,
end

with my argument being "there's no need to use choice here". Of course, the counterargument is "but it saves me a line if I do it with .some and .some_spec". Where does mathlib draw the line for using choice vs not?

[Eric Wieser]

I've seen a clear argument that there are many cases that it's "mathematically" convenient, but is "syntactically" convenient a good enough reason too?

[Kevin Buzzard]

Presumably have := foo h.1 h.2 doesn't work?

[Eric Wieser]

Right, projections only work on structures, because to work on props they'd have to be non-computable

[Eric Rodriguez]

This is the same question I ask when I get takeaways :b
I feel like it's nice to not use choice, it's nice to not have to mark things noncomputable that are in principle computable

[Kevin Buzzard]

But if you're proving a theorem I suspect you won't have to mark it noncomputable.

[Eric Rodriguez]

For example the structure I'm currently working on has a computable solution (the problem is in general in NEXP tho, so not realistic...) but I have to mark a fair few defs noncomputable cos of it

[Eric Wieser]

Right, I'm specifically talking about theorems here

[Eric Wieser]

Kevin Buzzard said:

Presumably have := foo h.1 h.2 doesn't work?

If we wanted to encourage this type of use, we could add:

alias classical.some ← Exists.witness
alias classical.some_spec ← Exists.spec

and then use foo h.witness h.spec (edit: we already have these)

[Kevin Buzzard]

I personally think there's a lot going for that proposal.

[Eric Wieser]

Doing so feels tantamount to saying "Exists.rec is constructivist nonsense". But maybe that is the stance of many mathlib users.

[Bryan Gin-ge Chen]

Maybe there's a tactic that could be written for this case which gives us the best of both worlds: something short which doesn't introduce choice if it doesn't have to?

[Johan Commelin]

Don't we have docs#Exists.some already?

[Eric Wieser]

I guess that was one of those things which is hard to find because the docs for core lean don't reference things in mathlib, thanks Johan Commelin!

[Yury G. Kudryashov]

I think that we should have parts of the library that clearly declare "we avoid classical.choice here", and for the rest of the library h.some is OK.

[Mario Carneiro]

I think using cases/obtain here is stylistically better, and gives you the ability to name the parts of the expression. It's "fine" to use h.some but I would prefer to avoid it in these trivial cases. Ideally, eventually, the "second wave" of AC-free formalization will wash over this statement and eliminate the unnecessary use of AC, but that's only worthwhile if all dependencies of the theorem are already AC-free, which is not the case for the vast majority of mathlib theorems, so this isn't actually a matter of avoiding choice for the most part.

[Mario Carneiro]

Plus, I can't think of many examples where you can't refactor the obtain version to actually be shorter. For the given example:

example {α : Type*} (p : α → Prop) : ∃ x, p x -> true | ⟨x, px⟩ := begin
  have := foo x px,
  trivial,
end

[Mario Carneiro]

If h.some and h.some_spec isn't duplicating a big expression in place of h, then that means it's a local hypothesis, so you can probably do some variation at the point where h is introduced to pattern match on it instead