better tactics for real analysis?

Stream: Is there code for X?

[Alex Kontorovich]

Here's a typical argument one encounters when teaching real analysis (so not using filters):

import Mathlib

def SeqLim (a : ℕ → ℝ) (L : ℝ) := ∀ ε > 0, ∃ N, ∀ n ≥ N, |a n - L| < ε

example : SeqLim (fun n ↦ (-1) ^ n / n) 0 := by
  intro ε hε
  let N := ⌈ε⁻¹⌉₊+1
  have hN : (N : ℝ) = ⌈ε⁻¹⌉₊+1 := by exact_mod_cast (by rfl)
  have hεinv : ε⁻¹ ≤ ⌈ε⁻¹⌉₊ := by bound
  have hN' : ε⁻¹ < N := by bound
  have hNpos : (0 : ℝ) < N := by linarith
  use N
  intro n hn
  have hn' : (N : ℝ) ≤ n := by exact_mod_cast hn
  calc
    _ = |(-1: ℝ) ^ n / n| := by ring_nf
    _ = |(-1: ℝ) ^ n| / |(n : ℝ)| := by apply abs_div
    _ = (n : ℝ)⁻¹ := by bound
    _ ≤ (N : ℝ)⁻¹ := by field_simp [show (0 : ℝ) < n by linarith]; exact hn'
    _ < ε := by field_simp at hN' ⊢; exact hN'

There are so many papercuts:

• all the casting, and needing to prove things by exact_mod_cast
• having to call an actual theorem (abs_div) because none of the tactics I tried did it
• things that bound can do in serial but not without the intermediate step (e.g. hN' fails without hεinv, though both are proved by bound)
• that field_simp didn't figure out $0<n$ by itself (though it's solved by linarith) -- and then it needed an exact. Is there a field_simpa or something, that then checks the assumptions?
• there should be a better way to go from ε⁻¹ < N to N⁻¹ < ε (and by the way, N⁻¹ doesn't work without explicit casting (N : ℝ)⁻¹, even if the context is ℝ...)

Any help on smoothing out any of these steps would be much appreciated!! Thank you!

[Alex Meiburg]

For a while I've thought there should be an extension to rify that changes variable types. (It's supposed to be the "opposite of lift", but it isn't really, because lift changes variables, rify only changes hypotheses.) I tried to see if I could get lift to do something better behavior here but it became a mess. Here's a bad attempt:

Header

import Mathlib

def SeqLim (a : ℕ → ℝ) (L : ℝ) := ∀ ε > 0, ∃ N, ∀ n ≥ N, |a n - L| < ε

instance : CanLift ℕ ℝ Nat.floor (fun _ ↦ True) where
  prf x _ := ⟨x, by simp⟩

example : SeqLim (fun n ↦ (-1) ^ n / n) 0 := by
  intro ε hε
  have hεinv : ε⁻¹ ≤ ⌈ε⁻¹⌉₊ := by bound
  set N := ⌈ε⁻¹⌉₊+1 with hN; clear_value N --can't `lift N` if it's a let-expr
  use N
  intro n hn
  lift n to ℝ using trivial
  lift N to ℝ using trivial
  rify at hn hN --and `lift` doesn't appropriately change the inequalities' types, so we have to `rify` those
  --And then the other tactics still do a bad job of handling the `floor` expressions everywhere.
  have hN' : ε⁻¹ < N := by bound
  have hNpos : (0 : ℝ) < N := by linarith
  have hn' : 0 < n := by bound
  rify at hn
  calc
    _ = |(-1: ℝ) ^ n / n| := by ring_nf
    _ = |(-1: ℝ) ^ n| / |(n : ℝ)| := by apply abs_div
    _ = 1 / n := by bound
    _ ≤ 1 / N := by field_simp [show (0 : ℝ) < n by linarith]; exact hn
    _ < ε := by field_simp at hN' ⊢; exact hN'

This afternoon I think I could make what I'm picturing though. If you don't mind one more 'nonstandard' tactic, I think it might improve several of these pain points for you!

[Michael Rothgang]

You can pass a custom discharger to field_simp, as in field_simp (discharger := linarith).

[Alex Meiburg]

Is this helpful?

import Mathlib

open Lean.Parser.Tactic in
open Lean in
/--
Given a variable `n` that's a ℕ, change that variable to a ℝ - while simultaneously trying
to transfer related hypotheses to the reals, and keeping a record that it's nonnegative.
-/
syntax (name := transfer_to_real) "transfer_to_real" ident : tactic

macro_rules
  | `(tactic| transfer_to_real $var) => do
    `(tactic| (
      --Every natural number is nonnegative, at least keep this fact
      have h_nonneg := Nat.cast_nonneg' (α := ℝ) $var
      rify at *
      --Try to take a stronger assumption if we can though, in particular that any positive natural number is at least one
      try (
        clear h_nonneg
        have h_pos : (1 : ℝ) ≤ $var := Nat.one_le_cast.mpr (show 0 < $var by rify at *; first | linarith | omega)
      )
      set tmp := ($var : ℝ) --`set` will clear out most instances of the variable now
      --In case there's any more pesky instances of the variable not caught by the rify
      try repeat rw [show $var = ⌊($var : ℝ)⌋₊ from (Nat.floor_natCast $var).symm, show ⌊($var : ℝ)⌋₊ = ⌊tmp⌋₊ from rfl] at *
      --Clear out the relationship between the new and old variable, and then the old variable itself. But if we can't clear the
      --old variable, it means it's still appearing somewhere, in which case it's probably safer to keep them both around.
      try (clear_value tmp; clear $var)
      rename ℝ => $var
      ))

--`abs_div` would be a good `grind =` lemma. Maybe for instructional purposes we can assume this is already the case?
attribute [grind =] abs_div

---------

def SeqLim (a : ℕ → ℝ) (L : ℝ) := ∀ ε > 0, ∃ N, ∀ n ≥ N, |a n - L| < ε

example : SeqLim (fun n ↦ (-1) ^ n / n) 0 := by
  intro ε hε
  have hεinv : ε⁻¹ ≤ ⌈ε⁻¹⌉₊ := by bound
  set N := ⌈ε⁻¹⌉₊+1 with hN
  use N
  transfer_to_real N
  intro n hn
  transfer_to_real n
  have hN' : ε⁻¹ < N := by bound
  calc
    _ = |(-1: ℝ) ^ ⌊n⌋₊ / n| := by ring_nf
    _ = |(-1: ℝ) ^ ⌊n⌋₊| / |n| := by grind
    _ = 1 / n := by simp; linarith
    _ ≤ 1 / N := by simpa [field]
    _ < ε := by field_simp at hN' ⊢; exact hN'

Most of the simplification comes from the transfer_to_real macro, that I hope generalizes to other problems of your ok.

Although field_simpa doesn't quite exist, simpa [field] comes pretty close. That works for your first one, but sadly simpa [field] using hN' doesn't quite work - it ends with 1 < ε * N vs 1 < N * ε.

I swapped out the apply abs_div for a grind where I gave it that attribute, which admittedly is just a layer of indirection. But if you can prepare an environment for your students with some of these grind lemmas, this might be a good way to clean things up. It's one more tactic to explain, but you can sort of explain grind as "try to follow obvious any equalities around and see if you can match things up", and explain that abs_div is one of the "obvious equalities" to try that grind knows about. I think abs_div actually should be marked grind in Mathlib.

[Michael Rothgang]

I sort of could get the original field_simp call to work: you need one more positivity hypothesis: the relevant branch is

    _ ≤ (N : ℝ)⁻¹ := by
      have : 0 < (n : ℝ) := sorry
      field_simp (discharger := linarith); field_simp [this]; assumption

[Chris Henson]

The first exact_mod_cast (rfl) can be grind.

[Alex Kontorovich]

Thanks all, this is really useful, and could certainly point in the direction of improvements. But my dream would be to have tactics to replace the sorrys below, without needing any "helper" lines at all:

import Mathlib

def SeqLim (a : ℕ → ℝ) (L : ℝ) := ∀ ε > 0, ∃ N, ∀ n ≥ N, |a n - L| < ε

example : SeqLim (fun n ↦ (-1) ^ n / n) 0 := by
  intro ε hε
  let N := ⌈1 / ε⌉₊+1
  use N
  intro n hn
  calc
    _ = 1 / n := by sorry
    _ ≤ 1 / N := by sorry
    _ < ε := by sorry

At present, even the calc block doesn't compile without changing 1 / n to (1 : ℝ) / n, even though Lean should "know" that the first _ is a real number... How far are we from being able to do something like this? Thanks!

[Alex Meiburg]

I can get this:

attribute [simp] abs_div
attribute [grind! .] Nat.le_ceil
attribute [grind =] inv_lt_iff_one_lt_mul₀ inv_eq_one_div

def SeqLim (a : ℕ → ℝ) (L : ℝ) := ∀ ε > 0, ∃ N, ∀ n ≥ N, |a n - L| < ε

example : SeqLim (fun n ↦ (-1) ^ n / n) 0 := by
  intro ε hε
  set N := ⌈ε⁻¹⌉₊ + 1 with hN
  use N
  transfer_to_real N
  intro n hn
  transfer_to_real N
  calc
    _ = 1 / n := by simp; positivity
    _ ≤ 1 / N := by simpa [field]
    _ < ε := by
      have hN' : ε⁻¹ < N := by grind
      grind

I think the grinds are realistic, I don't think abs_div should be marked simp realistically though, so that simp; positivity really "ought" to be simp [abs_div]; positivity. I think that the by simp; positivityand have hN' : ε⁻¹ < N := by grind; grind could both become a single grind with a bit more work.

If you want the 1 / n to parse, I guess that's an issue with how calc blocks elaborate? If the first element in the chain is a _, then the current goal should be used to elaborate that to infer the type of its right hand side. Likewise for the last one. If it's not an underscore, it elaborates correctly:

example : SeqLim (fun n ↦ (-1) ^ n / n) 0 := by
  intro ε hε
  let N := ⌈1 / ε⌉₊+1
  use N
  intro n hn
  calc
    |(-1 : ℝ) ^ n / ↑n - 0| = 1 / n := by sorry
    _ ≤ 1 / N := by sorry
    _ < ε := by sorry

so that seems fixable. (Beyond my ken though)

[Kevin Buzzard]

The typical mathematics undergraduate has no feeling for the "difference" between the three goals; even though from a formal perspective they all need different tools, all of them are true by "it's obvious" and even if we can find one tactic which does each of them, it's still somehow not the dream situation where at each step you just go "please kill this obvious goal". Would sledgehammer kill all of these goals in Isabelle, for example?

[Frédéric Dupuis]

For the casting issue, I wish there were a way to specify the default type for numeric literals, i.e. something like set_option defaultNumeralType ℝ in or something like that.

[Alex Kontorovich]

This is really great! I can hide the attributes and set_option defaultNumeralType inside code the students never see. Then maybe I can make a special obvious tactic, which is a wrapper for things like try transfer_to_real, try simp; positivity, try simpa [field], try grind etc? Even if it's "cheating", in that the obvious tactic isn't robust at all, but only does what I need it to in each level (and I add more to it as the levels progress), I would love to be able to see:

example : SeqLim (fun n ↦ (-1) ^ n / n) 0 := by
  intro ε hε
  set N := ⌈ε⁻¹⌉₊ + 1 with hN
  use N
  intro n hn
  calc
    _ = 1 / n := by obvious
    _ ≤ 1 / N := by obvious
    _ < ε := by obvious

[Kim Morrison]

Alex Meiburg said:

If you want the 1 / n to parse, I guess that's an issue with how calc blocks elaborate? If the first element in the chain is a _, then the current goal should be used to elaborate that to infer the type of its right hand side.

This seems a really useful feature. Would someone be interested in writing standalone description of this, as an feature request for lean4?

[Kim Morrison]

Frédéric Dupuis said:

For the casting issue, I wish there were a way to specify the default type for numeric literals, i.e. something like set_option defaultNumeralType ℝ in or something like that.

@Frédéric Dupuis, @Alex Kontorovich this is available as:

attribute [default_instance] Rat.instOfNat

/-- info: 1 : Rat -/
#guard_msgs in
#check 1

It would be nice to have a front-end for this so you don't need to know the instance name, e.g. set_default_numeral_type α could try to find an instance of type ∀ n, OfNat α n, and then add the default_instance attribute to it. Would anyone be interested in implementing that?

[Kim Morrison]

@Frédéric Dupuis, this is the sort of thing that Claude Code can do pretty much unattended this days. Would you be interested in reviewing/merging #30769?

[Alex Meiburg]

Oh, that version doesn't work for Reals though (or other rings that get their instance that way), that's kind of a big limitation right?

[Alex Meiburg]

Hmm, also

attribute [default_instance] instOfNatPNatOfNeZeroNat

works but

set_default_numeral_type PNat

doesn't, for instance. (Sorry, I'm just offering criticisms, I don't know how to fix this.)

Can the command create a new, reducible instance that appropriately bundles everything together - and then use that? So e.g. for Reals it creates an alias for @instNatOfAtLeastTwo Real, and similarly for 0 and 1, and then smacks them all together as default?

[Kim Morrison]

Haha, Nat.AtLeastTwo strikes again. My vote is that we kill that, and restore sanity in Mathlib's instances, even if technically this risks creating some diamonds (afaict they don't matter in practice...?)

[Kim Morrison]

Maybe it's better here to include some hard-coded instances to use for specific types...

[Aaron Liu]

which diamonds

[Aaron Liu]

there are two different implementations which give two different diamonds

[Aaron Liu]

and a third one which is kind of redundant but has no diamonds (bundle another data field)

[Kim Morrison]

#23866 and #23867 were my last attempt at this, but there was insufficient enthusiasm and I gave up.

[Aaron Liu]

oh that's the way that creates lots and lots of diamonds

[Aaron Liu]

I guess you can see it as lots of instances of the same diamond

[Aaron Liu]

since Zero.zero + One.one is not in general defeq to One.one

[Chris Henson]

@Kim Morrison Is something like this what you had in mind? (Not a metaprogramming expert, advice is welcome!)

import Lean

open Lean Elab Command Term Meta

syntax (name := SetDefaultNumeralTypeCmd) "set_default_numeral_type" term : command

@[command_elab SetDefaultNumeralTypeCmd]
def elabSetDefaultNumeralType : CommandElab := fun stx => do
  match stx with
  | `(set_default_numeral_type $α) =>
    let ty ← (liftTermElabM) <| elabType α
    let dl ← liftTermElabM <| getDecLevel ty

    let natTy := Expr.const ``Nat []
    let ofNat := Expr.const ``OfNat [dl]
    let body := mkApp (mkApp ofNat ty) (Expr.bvar 0)
    let all := .forallE `n natTy body .default

    let inst ← liftTermElabM <| synthInstance all

    match inst with
    | .const name _ =>
        let attrStx ← `(attr| default_instance)
        liftCoreM <| Attribute.add name `default_instance attrStx
    | _ => throwError m!"the synthesized `{inst}` is not a constant"
  | _ => throwUnsupportedSyntax

/-- info: 1 : Nat -/
#guard_msgs in
#check 1

set_default_numeral_type Rat

/-- info: 1 : Rat -/
#guard_msgs in
#check 1

[Chris Henson]

Oh, I see you already made a PR, oops. Good practice for me haha.

[Frédéric Dupuis]

Kim Morrison said:

Frédéric Dupuis, this is the sort of thing that Claude Code can do pretty much unattended this days. Would you be interested in reviewing/merging #30769?

Very nice! Although I feel someone better versed in metaprogramming should merge this...

[Kim Morrison]

Yeah, it shouldn't be merged as is, because of this Nat.AtLeastTwo nonsense.

[Kim Morrison]

A much more fundamental problem with using default_instance is that it can not be made local, so once you use this command it is set forever (including in downstream files).

[Kim Morrison]

So to even get off the ground here someone would need to write an RFC requesting local default_instance is allowed.

[Kim Morrison]

If that's done, then set_default_numeral_type α could probably just be implemented as a macro for

@[default_instance, reducible] instance : ∀ n, OfNat α n
| 0 => inferInstance
| 1 => inferInstance
| _ + 2 => inferInstance

[Michael Stoll]

Regarding the automatic casting to reals, note that in the example you probably want the exponent n still to be a natural number...

[Frédéric Dupuis]

Yeah, we definitely want this to be used locally, and ideally support set_default_numeral_type α in to use it on a single declaration.

[Alex Meiburg]

Would it be crazy to hope for that to land as a feature in core? It feels like if it could be done at a 'lower level' than messing with instances, it could be made a lot more sane

[Alex Meiburg]

I mean, obviously it's code someone would have to write first, but is a feature that would be hard to get into core on the basis of it being an undesirable feature/maintenance cost/complexity/whatever

[Kim Morrison]

I think asking for default_instance to be allowed to be local is a sensible and plausible request for core.

With that change, it's then straightforward to implement downstream (modulo having to deal with the Nat.AtLeastTwo mess, but that is a downstream problem).

[Kim Morrison]

default_instance is the mechanism by which Nat numerals work in the first place.