obtain just doesn't care

Stream: general

[Scott Morrison]

If I run obtain ⟨l, w⟩ := e, where e is some existential, and the goal is not a prop, I (quite reasonably) get the error induction tactic failed, recursor 'Exists.dcases_on' can only eliminate into Prop.

However, as a mathematician, I really don't care, and would prefer that obtain could automatically use Exists.some and Exists.some_spec (or something functionally equivalent).

Could/should we do this? I'm worried that it would have to be an Exists specific hack.

[Scott Morrison]

I'd be happy with obtain! as syntax if people are scared of allowing this as default behaviour.

[Scott Morrison]

I have found myself sometimes writing apply nonempty.some _, before the obtain line, and then apply nonempty.intro, afterwards when I am in a hurry and just want my witness. :-)

[Mario Carneiro]

I think it would be good to have obtain!, since I can imagine this syntax unifying with let et al and it's not that unusual to use it for programs and other data, and using noncomputable stuff silently as a fallback will cause weird errors

[Eric Rodriguez]

In the same vein, I'd also still like by_contra!

[Gabriel Ebner]

I prefer by_cases, by_contra, and obtain because they're typically used in proofs and most lemmas already use choice. But I could put up with the apostrophe if the error message included a hint to add it.

[Kevin Buzzard]

You could perhaps mock this up from choose?

import tactic
example (h : ∃ a : ℕ, a = a + 1) : ℕ :=
begin
  choose a ha using h,
  /-
  a : ℕ
  ha : a = a + 1
  ⊢ ℕ
  -/
  exact 37
end