Zulip Chat Archive

Stream: new members

Topic: Starting with Lean: exists.elim complication


Lucas Polymeris (Aug 19 2021 at 04:37):

Hello everyone, I recently started working with Lean and I wanted to formalize some notions I've been working on
for the past Month. But I'm stuck with a step, which should be solved with exists.elim I think, but doesn't seem to work:
a MWE I can come up with would be something like this:

lemma xd {C : Type} {h:  x : C, x = x}:  (X : set C), X   :=
begin
exists.elim h,
end

where the intention would be to prove it by constructing the a singleton set.
Shouldn't that tactic give x : C, and h: x = x ? Or what am I missing? Instead, when
I hover, I ger "don't know how yo synthesize placeholder".

Thanks and sorry for the noobie question.

Johan Commelin (Aug 19 2021 at 04:40):

@Lucas Polymeris Welcome. One way to deal with existentials is using the cases tactic. So you can write cases h with x hx, and this will decompose h into a witness x : C with property hx : x = x.

Scott Morrison (Aug 19 2021 at 04:41):

If you're using mathlib, you can also write obtain ⟨x, hx⟩ := h which is sometimes more readable than cases.

Lucas Polymeris (Aug 19 2021 at 05:07):

@Johan Commelin Oh, thanks. I think I didn't see that when reading about existential quantifier. Any hint on why doesn't
exists.elim work?

Kyle Miller (Aug 19 2021 at 05:16):

One thing is that exists.elim is not a tactic. Each statement in a begin ... end block needs to be a tactic -- Lean will be looking for tactic.interactive.exists.elim, which isn't what you want.

Kyle Miller (Aug 19 2021 at 05:17):

If you want to use exists.elim, this is one way to proceed:

lemma xd {C : Type} {h:  x : C, x = x}:  (X : set C), X   :=
begin
  apply exists.elim h,
  intros x hx,

end

Lucas Polymeris (Aug 19 2021 at 05:24):

@Kyle Miller Oh I see, thanks. I wasn't aware of that.

Mario Carneiro (Aug 19 2021 at 05:28):

You can also write terms directly if you don't use a begin ... end block, i.e.:

lemma xd {C : Type} {h:  x : C, x = x}:  (X : set C), X   :=
exists.elim h $ λ x hx, _

Mario Carneiro (Aug 19 2021 at 05:28):

which is what the tactics mentioned so far are doing under the hood


Last updated: Dec 20 2023 at 11:08 UTC