Zulip Chat Archive

Stream: general

Topic: obtain just doesn't care

Scott Morrison (May 28 2021 at 09:37):

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 (May 28 2021 at 09:37):

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

Scott Morrison (May 28 2021 at 09:39):

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 (May 28 2021 at 10:01):

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 (May 28 2021 at 10:56):

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

Gabriel Ebner (May 28 2021 at 11:24):

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 (May 28 2021 at 13:00):

You could perhaps mock this up from choose?

import tactic
example (h :  a : , a = a + 1) :  :=
  choose a ha using h,
  a : ℕ
  ha : a = a + 1
  ⊢ ℕ
  exact 37

Last updated: Dec 20 2023 at 11:08 UTC