API building

Stream: new members

[Michał Mrugała]

I wrote a proof of a simple fact about ideals in lean today:

import Mathlib

variable (R : Type*) [Semiring R]
variable (I₁ I₂ : Ideal R)
variable (α : R)
variable (h₁ : I₁ ≤ (Ideal.span {α})) (h₂ : I₂ ≤ (Ideal.span {α}))

example : I₁ + I₂ ≤ Ideal.span {α} := by
  intro x hx
  rw [show I₁ + I₂ = I₁ ⊔ I₂ from rfl] at hx
  rw [Submodule.mem_sup] at hx
  obtain ⟨m, hm, n, hn, hmnx⟩ := hx
  rw [← hmnx]
  have hmα := h₁ hm
  have hnα := h₂ hn
  exact Submodule.add_mem (Ideal.span {α}) (h₁ hm) (h₂ hn)

rw?? lead me to writing

rw [show I₁ + I₂ = I₁ ⊔ I₂ from rfl] at hx
rw [Submodule.mem_sup] at hx

but this felt "unoptimal". It felt that Ideal.mem_add and Submodule.mem_add should have existed in the library already. I was surprised both that these didn't exist and that rw?? didn't find a single step equivalent to them. Is there merit to adding these lemmas or would doing this just unnecessarily bloat the library?

[Aaron Liu]

docs#Submodule.add_eq_sup

[Aaron Liu]

I'm surprised that's the only lemma I could find

[Aaron Liu]

It's @[simp], so I guess that's something

[Aaron Liu]

import Mathlib

variable (R : Type*) [Semiring R]
variable (I₁ I₂ : Ideal R)
variable (α : R)
variable (h₁ : I₁ ≤ (Ideal.span {α})) (h₂ : I₂ ≤ (Ideal.span {α}))

example : I₁ + I₂ ≤ Ideal.span {α} :=
  (Submodule.add_eq_sup I₁ I₂).trans_le (sup_le h₁ h₂)

[Kenny Lau]

I guess this means + isn't really the canonical way to add ideals together then :slight_smile:

[Michał Mrugała]

I'm aware of this lemma, but its existence doesn't address the issue I'm raising. Additionally, if you use rw?? on hx you won't see it show up.

[Michał Mrugała]

Aaron Liu said:

import Mathlib

variable (R : Type*) [Semiring R]
variable (I₁ I₂ : Ideal R)
variable (α : R)
variable (h₁ : I₁ ≤ (Ideal.span {α})) (h₂ : I₂ ≤ (Ideal.span {α}))

example : I₁ + I₂ ≤ Ideal.span {α} :=
  (Submodule.add_eq_sup I₁ I₂).trans_le (sup_le h₁ h₂)

Yeah this is the proof I would ordinarily use but I wanted to formalize the one I did specifically.

[Kenny Lau]

My counter-point is that if you aren't using simp normal forms, you shouldn't expect any tactic to work. Doing simp before the intro, or simp at hx after the intro, both convert it into simp normal form.

[Kenny Lau]

import Mathlib

variable (R : Type*) [Semiring R]
variable (I₁ I₂ : Ideal R)
variable (α : R)
variable (h₁ : I₁ ≤ (Ideal.span {α})) (h₂ : I₂ ≤ (Ideal.span {α}))

example : I₁ + I₂ ≤ Ideal.span {α} := by simp [*]

[Michał Mrugała]

That's a good point, although I find it strange that I₁ + I₂ simplifies to I₁ ⊔ I₂. It's not entirely clear to me why docs#Submodule.add_eq_sup is a simp lemma in the first place.

I think if we want lean to become more accessible to the average mathematician we really ought to have lemmas like Ideal.mem_add.

[Aaron Liu]

So just docs#Submodule.mem_sup but change the sup to an add?

[Michał Mrugała]

For both Ideal and Submodule probably.

[Michał Mrugała]

I'm happy to make a PR adding this, just want to check with the community if this is desirable in the first place.

[Kenny Lau]

@Michał Mrugała the reason is that it is much more convenient (from the perspective of formalisation, sorry mathematicians) to build on existing structure. In particular, the ideals/submodules form a complete lattice, so it is very very very convenient to use that language.

[Kenny Lau]

I don't think the community will think this is desirable because we have many many many lemmas about submodules phrased in the language of complete lattice.

[Michał Mrugała]

I’m not entirely sure why adding more lemmas here would interfere with using the complete lattice API

[Aaron Liu]

It's just harder to maintain more theorems

[Kenny Lau]

your lemmas just won't be used because simp automatically turns + into sup

[Jireh Loreaux]

Arguably the only reason we have + for ideals at all is that it makes them into a semiring with the * operation.

[Kenny Lau]

omg we should have tsum defeq to iSup :upside_down:

[Aaron Liu]

That's probably impossible

[Yakov Pechersky]

Let's say you didn't even know add_eq_sup. This still works:

example : I₁ + I₂ ≤ Ideal.span {α} := by
  refine (add_le_add h₁ h₂).trans ?_
  simp

[Kenny Lau]

Yakov Pechersky said:

Let's say you didn't even know add_eq_sup.

(until you put a question mark after simp...)

[Yakov Pechersky]

Sure, but I think that (add_le_add h1 h2).trans <| by simp is golfed pretty well, and the term looks syntactically like the expression of goal.