## Stream: new members

### Topic: working with sets

#### Brian Jiang (Mar 23 2020 at 20:14):

If I define a reduced residue class as follows:
 def reduced_residue_class (n: nat):={ k : nat | k < n \and k.coprime n }

#### Brian Jiang (Mar 23 2020 at 20:15):

is there a way to get the size of this set?

#### Brian Jiang (Mar 23 2020 at 20:15):

also I would like to get the product of all elements in the set

#### Johan Commelin (Mar 23 2020 at 20:15):

Well.... Lean doesn't know yet that the set is finite...

#### Johan Commelin (Mar 23 2020 at 20:16):

Even though it's obvious.

#### Johan Commelin (Mar 23 2020 at 20:17):

This might be one reason to choose

def rsc (n : nat) : finset nat := (finset.range n).filter \$ assume k, k.coprime n


#### Johan Commelin (Mar 23 2020 at 20:17):

Then you can talk about finset.card _ afterwards

#### Brian Jiang (Mar 23 2020 at 20:17):

is there any way around this? maybe by adding an assumption that says its finite?

#### Brian Jiang (Mar 23 2020 at 20:17):

is there any way around this? maybe by adding an assumption that says its finite?

ok thanks

#### Brian Jiang (Mar 23 2020 at 20:18):

can I get the product of all elements in this set somehow?

#### Johan Commelin (Mar 23 2020 at 20:19):

also

lemma mem_rsc (n k : nat) : k \in rsc n \iff (k < n \and k.coprime n) := sorry


#### Johan Commelin (Mar 23 2020 at 20:19):

With the finset definition, the product is also easier.

#### Johan Commelin (Mar 23 2020 at 20:20):

def prod_rsc (n) : nat := (rsc n).prod id


#### Brian Jiang (Mar 23 2020 at 20:22):

what do I have to import for finset and prod?

#### Kevin Buzzard (Mar 23 2020 at 20:23):

You can't take the product until you define the multiplication.

#### Johan Commelin (Mar 23 2020 at 20:25):

Brian Jiang said:

what do I have to import for finset and prod?

algebra.big_operators

#### Brian Jiang (Mar 23 2020 at 20:33):

@Kevin Buzzard : How may I define this multiplication?

#### Brian Jiang (Mar 23 2020 at 20:34):

also, would it be possible to define another set that has all the values of rsc n  scaled by a factor of a?

#### Kevin Buzzard (Mar 23 2020 at 20:51):

Well you can do regular multiplication and then reduce mod n -- but then you have to prove that the result is coprime to n. If you want to roll your own then you will have to do work before you can even start multiplying.

If you want to learn how to prove theorems in Lean than you could try working on the natural number game.

#### Matias Heikkilä (Apr 12 2022 at 06:58):

I'm trying to build a sort of "syntactic intuition" on lean. At this point I understand that implications (and the universal quantification) can be "peeled" with intro and the existential quantification can be "peeled" with use. Is there a similar pattern that could be used with something like this image.png ?

#### Matias Heikkilä (Apr 12 2022 at 06:59):

I guess I would like to have the right side of the set builder notation as the claim to work with this in the elementary way (?)

#### Yaël Dillies (Apr 12 2022 at 06:59):

Try dsimp and you will see that this really is an hidden existential.

#### Matias Heikkilä (Apr 12 2022 at 07:00):

thanks for the tip! would you say thatdsimp is often useful with set builder notation?

#### Yaël Dillies (Apr 12 2022 at 07:02):

At the level of things you are doing now, dsimp only does cosmetic changes. You can delete them from your proof, and most likely everything will still work fine (except maybe rw because it works up to syntactical equality).

#### Eric Wieser (Apr 12 2022 at 08:18):

Note that "set builder notation" is just the function docs#set_of

#### Eleanor McMurtry (Apr 13 2022 at 09:08):

so I'm working through this proof:

def conjugate (H : mysubgroup G) (g : G) : mysubgroup G :=
{ carrier := { a : G | ∃ h ∈ H, a = g * h * g⁻¹ },
one_mem' := ⟨1, by simp [H.one_mem]⟩,
mul_mem' := begin
dsimp,
rintros x y ⟨a, ha, rfl⟩ ⟨b, hb, rfl⟩,
exact ⟨a * b, H.mul_mem ha hb, by group⟩,
end,
inv_mem' := begin
rintros x ⟨a, ha, rfl⟩,
exact ⟨a⁻¹, H.inv_mem ha, by group⟩
end,
}


and I am a bit confused with how exactly rfl works in the rintros matching. my understanding is that ⟨a, ha⟩ binds to ∃ (h : G) (H : H ∈ H), and then I'm left with x = g * h * g⁻¹. what does putting rfl in for the last bit do exactly? does it just declare that x = g * h * g⁻¹ is defined to be reflexively true or something?

#### Eleanor McMurtry (Apr 13 2022 at 09:08):

like I get that rfl : ∀ a. a = a but I'm not sure what it does in this context

#### Yaël Dillies (Apr 13 2022 at 09:10):

This is not the same rfl as in rfl : ∀ a, a = a. This is part of the rintro syntax which automatically substitutes the LHS or RHS of an equality you introduce everywhere in the context, provided it is a single variable (so that substitution can work). So in that case it replaces x with g * h * g⁻¹.

#### Ruben Van de Velde (Apr 13 2022 at 09:10):

It is equivalent to

rintros x y ⟨a, ha, ha'⟩ ⟨b, hb, hb'⟩,
subst ha' hb',


#### Eleanor McMurtry (Apr 13 2022 at 09:12):

aha so rfl is just special syntax that is a shortcut for this?

#### Eleanor McMurtry (Apr 13 2022 at 09:13):

wait that doesn't work Ruben

#### Eleanor McMurtry (Apr 13 2022 at 09:14):

ah, subst ha', subst hb', does though

#### Eleanor McMurtry (Apr 13 2022 at 09:14):

very good thanks!

#### Mauricio Collares (Apr 13 2022 at 09:20):

Yaël Dillies said:

This is not the same rfl as in rfl : ∀ a, a = a. This is part of the rintro syntax which automatically substitutes the LHS or RHS of an equality you introduce everywhere in the context, provided it is a single variable (so that substitution can work). So in that case it replaces x with g * h * g⁻¹.

It is the same rfl, I think (at least modulo internal rintro implementation details)! rintro allows you to pattern match on stuff, and using rfl as a pattern "forces" unification.

#### Eleanor McMurtry (Apr 13 2022 at 09:26):

oh! that makes more sense, and is pretty wild

#### Yaël Dillies (Apr 13 2022 at 09:27):

I believe not, because the following fails:

example {α : Type*} {a b : α} : a = b → b = a :=
begin
rintro rfl, -- does what's expected
end

example {α : Type*} {a b : α} : a = b → b = a :=
begin
rintro (eq.refl _), -- intro tactic failed, Pi/let expression expected
end


#### Yaël Dillies (Apr 13 2022 at 09:29):

On top, rintro rfl works even if the relevant variables are already in context, which means it does not just do pattern-matching (pattern-matching only restricts variables that it introduces, it does not substitute the ones already in context).

#### Yaël Dillies (Apr 13 2022 at 09:33):

Of course, the two rfl are related, but they are not literally the same.

#### Mauricio Collares (Apr 13 2022 at 09:41):

Makes sense, thanks for the clarification! I think another point of view is that rintro simulates "in tactic-land" what pattern matching + unification would do "in term-land", and this simulation is not 100% accurate in the sense that it expects a particular keyword (which is not a bad thing, given how it is meant to be used).

#### Patrick Massot (Apr 13 2022 at 09:45):

No, rintro is much more powerful.

#### Mauricio Collares (Apr 13 2022 at 09:48):

I meant for the particular case of using rfl. Well, I think I might be just too used to unification in Agda, so I'll just read up more on how Lean does this.

#### Eric Wieser (Apr 13 2022 at 10:44):

Patrick, my understanding was that rintro was a weaker version of the equation compiler; is that not a good mental model?

#### Mauricio Collares (Apr 13 2022 at 10:52):

Perhaps related: In Lean 4, this works:

example {a b : Nat} : a = b → b = a
| rfl => rfl


After the =>, unification works as I expected (that is, the variable b disappears from context and is replaced by a everywhere). In Lean 3, though, I tried pattern matching on rfl the naïve way and it just gave me a variable named "rfl" without unifying. This might be related to the fact that rfl is just a value and no longer a keyword in Lean 4. Does this mean that rcases could be implemented in Mathlib4 in such a way that rfl is a special case of pattern matching?

#### Eric Wieser (Apr 13 2022 at 10:53):

In lean 3 you have to match on a and b too

#### Eric Wieser (Apr 13 2022 at 10:53):

rfl isn't a keyword in lean 3

#### Mauricio Collares (Apr 13 2022 at 10:55):

Ah, good to know it isn't! That makes a lot more sense. I was confused by the tactic#rcases documentation because I didn't click the rfl link there.

#### Mario Carneiro (Apr 13 2022 at 16:00):

Eric Wieser said:

Patrick, my understanding was that rintro was a weaker version of the equation compiler; is that not a good mental model?

It is similar in general design to the equation compiler, but it is not strictly dominated in either direction. rintro does not allow using term syntax like eq.refl _ for pattern matching; you have to use the anonymous constructor syntax ⟨⟩ instead of constructor names

#### Mario Carneiro (Apr 13 2022 at 16:02):

Unlike the equation compiler you can't do recursive definitions using rcases, but the equation compiler doesn't allow patterns like ⟨a | b, c | d⟩, and there is no equivalent of the - pattern either

#### Mario Carneiro (Apr 13 2022 at 16:04):

Strictly speaking, rfl is a rintro keyword, which means "use subst". You can't use any other term there

Last updated: Dec 20 2023 at 11:08 UTC