Real.isInteger

Stream: Is there code for X?

[Jakob von Raumer]

Is there a definition of what it means for a real number to be an integer (i.e. it's in the image of the cast)

[Eric Wieser]

Membership in Set.range Int.cast, or Int.castRingHom.range?

[Kevin Buzzard]

We also don't seem to have a bespoke definition of what it means for a real number to be rational, which surprised me recently.

[Jakob von Raumer]

Eric Wieser said:

Membership in Set.range Int.cast, or Int.castRingHom.range?

Yes, I just thought there would be enough need for an abbreviation (I was looking for a characterization of $\lfloor x \rfloor + \lceil x \rceil$ and was suprised that it didn't exist)

[Jireh Loreaux]

I wouldn't define it only for real numbers. Do it for any type with the cast.

[Jakob von Raumer]

With then giving the type explicitly?

[Aaron Liu]

Kevin Buzzard said:

We also don't seem to have a bespoke definition of what it means for a real number to be rational, which surprised me recently.

In Mathlib.Data.Real.Irrational, it's spelled as ¬Irrational :)

[Jakob von Raumer]

Jireh Loreaux said:

I wouldn't define it only for real numbers. Do it for any type with the cast.

What would you call it?

[Jakob von Raumer]

I think it would be really useful to have Real.IsInteger as a type class and equip it with all the closure properties... Does anyone know why Irrational hasn't been made a class (but instead simplifies composite terms)?

[Yaël Dillies]

What would you do with this typeclass?

[Riccardo Brasca]

A class is useful when there are instances for it. In this case it seems rather unlikely to have such instances. The same is true, for example, for Nat.Prime.

[Jakob von Raumer]

Have instances for all OfNats, for all casts from Int and Nat, and closure under addition, subtraction, multiplication, exponentiation

[Jakob von Raumer]

Guess the point against it would be that it's better style to norm_cast for those expressions

[Eric Wieser]

Jakob von Raumer said:

Have instances for all OfNats, for all casts from Int and Nat, and closure under addition, subtraction, multiplication, exponentiation

You get this closure for free with \mem Rat.castHom.range

[Jakob von Raumer]

What do you mean by "for free"? Composite expressions don't simplify

[Eric Wieser]

Jakob von Raumer said:

Have instances for all OfNats, for all casts from Int and Nat, and closure under addition, subtraction, multiplication, exponentiation

I think you're implying that "the property is structural" is a sufficient argument for using a typeclass, but I think the requirement is usually also that "the property is structural and about types"

[Eric Wieser]

(of course typeclasses do work in the former case, but I think it's controversial in the context of mathlib to use them in this way)

[Jakob von Raumer]

Yea I guess the point of reference is something like Subgroup.mul_mem or so

[Jakob von Raumer]

I just like the brevity of something like this

class Real.IsInteger (r : ℝ) : Prop := sorry

instance [OfNat ℝ n] : Real.IsInteger (OfNat.ofNat n : ℝ) := sorry

@[simp]
lemma floor_isInteger {r : ℝ} [Real.IsInteger r] : ⌊r⌋ = r := sorry

example {r : ℝ} [Real.IsInteger r] : ⌊5 + r⌋ = 5 + r := by simp

[Jakob von Raumer]

Ah, bad example, the OfNat is already pulled out by another simp lemma :sweat_smile:

[Jakob von Raumer]

NeZerowould be a similar thing

[Yakov Pechersky]

My thought is that in these "this prop is obvious for some subclass of terms of the type", this is the place for an autoparam with a possibly custom (simple) tactic.

[Yakov Pechersky]

In the case of this floor example, the stronger lemma is the iff. Which could then be used in the custom autoparam tactic to discharge the proof obligation.

[Violeta Hernández]

I think this might be somewhat of an XY. Given h : x \in range coe, you can use obtain <y, rfl> := h to rewrite any instance of x by ↑y, at which point you get all the structural lemmas you're talking about in the form of cast_add, cast_mul, etc.

[Violeta Hernández]

This approach works for casts from naturals, integers, and rationals, and requires none of the duplication.

[Jireh Loreaux]

Violeta, while I understand your point completely, I think it nevertheless makes sense to have the following (along with IsInteger and maybe IsRational versions, although I suspect IsRational will be much less useful than the others):

import Mathlib

variable {α : Type*}

def IsNatural [NatCast α]  (a : α) : Prop := a ∈ Set.range ((↑) : ℕ → α)

namespace IsNatural

@[simp]
protected lemma ofNat [NatCast α] (n : ℕ) [n.AtLeastTwo] : IsNatural (ofNat(n) : α) := ⟨OfNat.ofNat n, rfl⟩

section AddMonoidWithOne

variable [AddMonoidWithOne α]

@[simp]
protected lemma zero : IsNatural (0 : α) := ⟨0, Nat.cast_zero⟩

@[simp]
protected lemma one : IsNatural (1 : α) := ⟨1, Nat.cast_one⟩

@[aesop safe apply]
protected lemma add {n m : α} (hn : IsNatural n) (hm : IsNatural m) : IsNatural (n + m) := by
  obtain ⟨n, rfl⟩ := hn
  obtain ⟨m, rfl⟩ := hm
  exact ⟨n + m, Nat.cast_add _ _⟩

@[aesop safe apply]
protected lemma smul {n : ℕ} {m : α} (hm : IsNatural m) : IsNatural (n • m) := by
  induction n with
  | zero => simp
  | succ n ih =>
    rw [add_nsmul]
    aesop

end AddMonoidWithOne

section Semiring

variable [Semiring α]

@[aesop safe apply]
protected lemma mul {n m : α} (hn : IsNatural n) (hm : IsNatural m) : IsNatural (n * m) := by
  obtain ⟨n, rfl⟩ := hn
  obtain ⟨m, rfl⟩ := hm
  exact ⟨n * m, Nat.cast_mul _ _⟩

@[aesop safe apply]
protected lemma pow {n : ℕ} {m : α} (hm : IsNatural m) : IsNatural (m ^ n) := by
  obtain ⟨m, rfl⟩ := hm
  exact ⟨m ^ n, by simp⟩

example {n m k : α} (hn : IsNatural n) (hm : IsNatural m) (hk : IsNatural k) :
    IsNatural (k ^ 2 + 3 • n + k * m + 24 : α) := by
  aesop

end Semiring

end IsNatural

Others can feel free to disagree here. There are certainly other things that could be done. (e.g., you could show that k n m in the example are all in the range of cast interpreted as a ring hom, then you could probably prove also that the quantity contained therein is in that range using existing aesop lemmas.) But I still think this could be nice and perhaps worth having.

[Jireh Loreaux]

@Jakob von Raumer in the above, notice that there is no need for type classes or to provide the type explicitly.

[Eric Wieser]

I'll note we do have docs#Mathlib.Meta.NormNum.IsNat, though it's an implementation detail of norm_num

[Jakob von Raumer]

Thanks, it's a good alternative to (ab)using the type classes. Is there now a concerted effort to annotate more lemmas for aesop?

[Kevin Buzzard]

BTW one really silly thing in mathlib is docs#harmonic_not_int , which says that for $n\geq2$ we have $\sum_{i=1}^n\frac{1}{i}\not\in\Z$ but it's spelt using docs#Rat.isInt which is Bool-valued so the statement looks really odd in the docs.

My earlier comment about "we don't have the predicate that a real number is rational" was misremembered on my part -- what I meant was "we don't seem to have the predicate that a rational number is integral".

[Jireh Loreaux]

I think you should annotate lemmas with aesop whenever it makes sense. We should certainly use it.