working with sets

Stream: new members

[Brian Jiang]

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]

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

[Brian Jiang]

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

[Johan Commelin]

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

[Johan Commelin]

Even though it's obvious.

[Johan Commelin]

This might be one reason to choose

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

[Johan Commelin]

Then you can talk about finset.card _ afterwards

[Brian Jiang]

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

[Brian Jiang]

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

[Brian Jiang]

ok thanks

[Brian Jiang]

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

[Johan Commelin]

also

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

[Johan Commelin]

With the finset definition, the product is also easier.

[Johan Commelin]

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

[Brian Jiang]

what do I have to import for finset and prod?

[Kevin Buzzard]

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

[Johan Commelin]

Brian Jiang said:

what do I have to import for finset and prod?

algebra.big_operators

[Brian Jiang]

@Kevin Buzzard : How may I define this multiplication?

[Brian Jiang]

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]

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ä]

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ä]

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]

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

[Matias Heikkilä]

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

[Yaël Dillies]

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]

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

[Eleanor McMurtry]

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]

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

[Yaël Dillies]

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]

It is equivalent to

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

[Eleanor McMurtry]

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

[Eleanor McMurtry]

wait that doesn't work Ruben

[Eleanor McMurtry]

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

[Eleanor McMurtry]

very good thanks!

[Mauricio Collares]

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]

oh! that makes more sense, and is pretty wild

[Yaël Dillies]

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]

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]

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

[Mauricio Collares]

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]

No, rintro is much more powerful.

[Mauricio Collares]

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]

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

[Mauricio Collares]

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]

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

[Eric Wieser]

rfl isn't a keyword in lean 3

[Mauricio Collares]

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]

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]

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]

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