Zulip Chat Archive

Stream: new members

Topic: How does Lean handle the equal operator on sets?


Andrew Lubrino (Jan 25 2022 at 01:08):

I've been working through Velleman's suggested set theory proof problems in Proof Designer (except I'm doing the proofs in Lean and not Proof Designer). I'm stuck on #8. I'm not sure I understand how Lean handles the equality operator on sets. Can Lean solve the below problem with how it is currently stated? I've tried using eq.subst and iff.elim_leftand neither worked. I'm mainly looking for help where the sorry is placed now.

variable {U : Type}
variables A B C : set U


  example (h : A  (B \ C) = ): A  B  C :=
  assume x,
  assume h₁ : x  A  B,
  show x  C, from
  by_contradiction
    (assume h₂ : x  C,
    have h₃ : x  B \ C, from and.intro h₁.right h₂,
    have h₄ : x  A  (B \ C), from and.intro h₁.left h₃,
    show x  , from sorry)

Alex J. Best (Jan 25 2022 at 01:20):

you can use docs#eq.subst directly here

variable {U : Type}
variables A B C : set U


  example (h : A  (B \ C) = ): A  B  C :=
  assume x,
  assume h₁ : x  A  B,
  show x  C, from
  by_contradiction
    (assume h₂ : x  C,
    have h₃ : x  B \ C, from and.intro h₁.right h₂,
    have h₄ : x  A  (B \ C), from and.intro h₁.left h₃,
    show x  , from h.subst h₄)

Andrew Lubrino (Jan 25 2022 at 01:31):

That works. Thank you. I originally tried (and then tested it again after your response) the below and that doesn't work. What's the difference between the below and what you have above?

variable {U : Type}
variables A B C : set U


  example (h : A  (B \ C) = ): A  B  C :=
  assume x,
  assume h₁ : x  A  B,
  show x  C, from
  by_contradiction
    (assume h₂ : x  C,
    have h₃ : x  B \ C, from and.intro h₁.right h₂,
    have h₄ : x  A  (B \ C), from and.intro h₁.left h₃,
    show x  , from eq.subst h h₄)

Alex J. Best (Jan 25 2022 at 01:51):

Huh, I'm actually not sure, I would have thought they would both work. It could be some elaboration order quirk, hopefully someone else can answer!

Reid Barton (Jan 25 2022 at 02:00):

https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Natural.20Numbers.20Game/near/199965854

Reid Barton (Jan 25 2022 at 02:01):

... seems related, except the conclusion here is the opposite?

Reid Barton (Jan 25 2022 at 02:03):

Maybe eq.subst should not have elab_as_eliminator, and could this be related to why the "stupid triangle" is so stupid?

Andrew Lubrino (Jan 25 2022 at 02:42):

Hmm. Weird. I'll just try both whenever I get an error like this in the future I guess.

Thanks!

Reid Barton (Jan 25 2022 at 02:49):

FWIW, pretty much everyone uses the rw tactic instead of using eq.subst directly.

Andrew Lubrino (Jan 25 2022 at 03:14):

Oh really? I'm still very much a beginner in Lean, so I'm not really too familiar with rw. I'm going to look into that and start using it more.


Last updated: Dec 20 2023 at 11:08 UTC