Zulip Chat Archive

Stream: new members

Topic: Unfolding set constructor notation


view this post on Zulip Keefer Rowan (May 16 2020 at 13:59):

I understand what set constructor notation is doing, but I can't figure out where it is defined so I can't figure out what definition to tell lean to unfold. I know how to find definitions of simple notation like #print notation * but I don't know how to do it for complicated notation like the set constructor notation. So where is set constructor notation defined/how can I unfold it?

view this post on Zulip Kevin Buzzard (May 16 2020 at 14:01):

I totally agree that this is annoying and frustrating. I went through a phase of trying to understand what Lean was by unfolding everything in sight and set notation, and stuff like there exists and inf stuff are very hard to see through: they are just some "scoped something". But in the set case you can just set_option pp.notation false and find out what's going on. It's something like set_of that you're looking for.

view this post on Zulip Keefer Rowan (May 16 2020 at 14:04):

Thanks! Your answer implies that I usually shouldn't have to unfold stuff to prove something, is there a better way to show something like:

{a : α | a  A  a  B} x = {a : α | a  B  a  A} x

without unfold set_of?

view this post on Zulip Kevin Buzzard (May 16 2020 at 14:21):

In some sense your goal should never be that, because it's not in canonical form

view this post on Zulip Kevin Buzzard (May 16 2020 at 14:24):

If I found myself in that state I would probably first do show x \in A \and x \in B = x \in B and x \in A to get things back into some kind of normality, and then use the ext tactic.

view this post on Zulip Johan Commelin (May 16 2020 at 14:24):

@Keefer Rowan How did you end up with that goal?

view this post on Zulip Johan Commelin (May 16 2020 at 14:24):

I think that 1 or 2 lines before it, you should have written ext x.

view this post on Zulip Reid Barton (May 16 2020 at 14:24):

Here again there are two kinds of approaches depending on whether or not you want to exploit your knowledge of the definition of { | }:

  1. Using that knowledge:
  • You could compute mentally that the goal is really just x ∈ A ∧ x ∈ B = x ∈ B ∧ x ∈ A. So use change x ∈ A ∧ x ∈ B = x ∈ B ∧ x ∈ A to make that the new goal.
  • Alternatively, you can see that the new goal is going to be closed by something like and.comm (this might be phrased in terms of iff, though, not sure) so just apply that directly.
  1. Not using that knowledge:
  • find some lemma that rewrites {a | p a} x to p x.

In this case (and also in the compl one earlier) it's better to just do 1, since the definition of this notation is so basic.

view this post on Zulip Kevin Buzzard (May 16 2020 at 14:25):

There are 100 ways to say everything in Lean, and a proper subset of them are "canonical". If you stick to the canonical ways then the simp tactic will be of much more help to you.

view this post on Zulip Kevin Buzzard (May 16 2020 at 14:26):

You learn the canonical ways by looking at statements of lemmas in the library

view this post on Zulip Kevin Buzzard (May 16 2020 at 14:26):

show and change do the same thing, by the way

view this post on Zulip Keefer Rowan (May 16 2020 at 15:34):

@Johan Commelin This is where I was:

theorem inter_comm {α : Type u} {A B : set α} : A  B = B  A :=
begin
    unfold has_inter.inter set.inter, sorry,
end

(BTW: I know this is almost certainly already in the library)

Also ext x gives an "unknown identifier". I'm working with very basic imports, so maybe isn't imported.

view this post on Zulip Keefer Rowan (May 16 2020 at 15:40):

I think I see what's going on though, you're saying that if I prove the theorem by set extensionality, I won't run into this state. What do I need to import to get ext? I was able to prove theorem setext {α : Type u} (A B : set α) : (∀ (x : α), x ∈ A ↔ x ∈ B) → A = B, which allows me to do this, but I should probably be using the proper tactic.

view this post on Zulip Bryan Gin-ge Chen (May 16 2020 at 15:41):

Yeah, ext is a mathlib tactic. You would have to use apply set.ext instead. Here's the proof in mathlib.

view this post on Zulip Bryan Gin-ge Chen (May 16 2020 at 16:02):

Oh hmm, set.ext is proved in mathlib too.

view this post on Zulip Kevin Buzzard (May 16 2020 at 16:28):

import tactic

theorem inter_comm {α : Type} {A B : set α} : A  B = B  A :=
begin
  ext x,
  rw [set.mem_inter_iff, set.mem_inter_iff],
  apply and_comm,
end

In this proof nothing ever leaves the canonical form.


Last updated: May 15 2021 at 22:14 UTC