is_[XX] deprecated

Stream: new members

[Amaury Hayat]

Hi! I just realized that there was many function deprecated like is_subring, is_subgroup, is_add_monoid, etc. What would be then the correct way to express a theorem like:

def Zd (d:ℕ) : set ℝ := {z |∃ a:ℤ,∃ b:ℤ, z=(real.sqrt d)*b+a}
theorem my_th (d:ℕ) : is_subring (Zd d ) :=
begin
sorry
end

[Eric Wieser]

def Zd (d:ℕ) : subring ℝ :=
{ carrier := {z | ∃ a b:ℤ, z = (real.sqrt d)*b + a}
  -- add fields to make the red squiggles go away
  }

[Eric Wieser]

You might be interested in docs#zsqrtd.to_real and docs#ring_hom.range if you were not already aware of them.

[Patrick Massot]

In VSCode, you can also write def Zd (d:ℕ) : subring ℝ := _, click the light bulb and select "Generate a skeleton..." in the menu.

[Amaury Hayat]

Thanks a lot, this is really helpful ! Independently of this particular example, I wanted to have a theorem that says
Theorem : " G is a subring of $\mathbb{R}$" what should I use instead of is_subring (since its apparently deprecated) ?

[Eric Wieser]

This might be an #xy problem. There are two ways to make the statement you are suggesting:

• G, a specific set ℝ defined elsewhere, is a subring
• Define G as a specific subring ℝ

Is the any particular reason you care about the difference?

[Kevin Buzzard]

In Lean, there is a type subring \R of subrings of the reals, and a subring of $\mathbb{R}$ is a term of that type. In particular, defining a subring is a definition. If you have already defined a subset of $\R$ then that's a term of type set \R which is a different type; you still have to make a definition. To make the definition you have to prove a theorem (G is closed under +,-,*,0,1 or whatever) but it's still a definition.

[Eric Wieser]

If for whatever reason you do have a definition of G : set ℝ that you can't change, a typical approach would be to define a new G_subring, and then prove the two are equal:

def G : set ℝ := sorry

def G_subring : subring ℝ :=
{ carrier := G,
  one_mem' := _,
  mul_mem' := _,
  zero_mem' := _,
  add_mem' := _,
  neg_mem' := _ }  -- generated using the approach Patrick describes

@[simp]
def G_subring_eq_G : ↑G_subring = G := rfl

[Amaury Hayat]

OK thanks ! Yes I agree with the fact that there are two ways to make the statement. I see how to do the second one and indeed I was trying to express the first one. And I agree of course that I still have to make a definition. Is that the reason why is_subring / is_group and so on were deprecated ?

[Amaury Hayat]

Then if I understood correctly the last answer of @Eric Wieser, if I wanted to write a simple undergrad exercice in lean on the form "Show that G (defined earlier) is a subring of $\mathbb{R}$" the proper way to express the exercise in Lean would say "Show that there exists G_ : subring \br such that ↑G_ = G".

[Kevin Buzzard]

is_subring can still be used, but it shouldn't be a class; this is a design decision and the reasons for it are complex, one of them being that subring allows you to use dot notation, e.g. like A.zero_mem is the proof that $0\in A$.

[Kevin Buzzard]

As for the proper way to express an exercise, you should write a #mwe. Yes, what you say works, but when I do this stuff with my undergraduates I just write stuff like

def G_subring : subring \R :=
{ carrier := G,
   mul_mem := sorry,
...
}

and get the students to fill in the sorrys. I don't feel bound to attempt to phrase the question in exactly the way it has been phrased in a book, I would rather write more idiomatic Lean code which has the same underlying meaning.

[Amaury Hayat]

Ok, thanks a lot for the helpful answers (as always) !