[Merged by Bors] - feat(tactic/interactive/choose): nondependent choose

[digama0]

Now you can write choose! to eliminate propositional arguments from the chosen functions.

example (h : ∀n m : ℕ, n < m → ∃i j, m = n + i ∨ m + j = n) : true :=
begin
  choose! i j h using h,
  guard_hyp i := ℕ → ℕ → ℕ,
  guard_hyp j := ℕ → ℕ → ℕ,
  guard_hyp h := ∀ (n m : ℕ), n < m → m = n + i n m ∨ m + j n m = n,
  trivial
end

[sgouezel]

I see you are using inhabited, but nonempty would be more general, and I don't think the junk value used matters much.

Also, what about using just choose for the new version, instead of choose!?

[digama0]

The reason for not making it default is to avoid the hit for typeclass search. But I can switch it to use nonempty instead (dunno how that affects the idea that was floated to maybe choose what the default value / function is).

[sgouezel]

I would'nt be too much worried about performance issues, as it's an interactive tactic and it's not used that frequently, so one additional typeclass search from time to time shouldn't be that bad. But I get your point, so let's keep the ! unless other people say that they'd also like it as the default.

And thanks for switching to nonempty!

[PatrickMassot]

I just checked that it works great on two real life examples I'm interested in (including #3740). My only little complain is that when choose! cannot find the relevant nonempty instance, it silently falls back to the choose behavior without error message.

[robertylewis]

Looks good, just a couple doc comments. Maybe it would be better to move this out of tactic.core/tactic.interactive into its own file.

[robertylewis]

bors merge

[bors]

👎 Rejected by label

[robertylewis]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Run tests