finishing up ofScientific in norm_num

Stream: mathlib4

[Thomas Murrills]

@Mario Carneiro , I'm finally finishing this up now that Rat.cast is reducible and I can get rid of LawfulOfScientific.

1. I noticed that we're using assumeInstancesCommute instead of assertInstancesCommute and I'm assuming the same philosophy applies here: that is, the lemmas are going to have an argument saying that the given DivisionRing OfScientific instance is equal to Rat.ofScientific followed by Rat.cast, and we just supply this as Eq.refl and let it fail in the kernel if it must (which it almost surely won't). Just wanted to run it by you in case we actually wanted a defeq check here for some reason.

2. Is it better performance-wise for those lemmas to have a hypothesis stating that the instance per se is equal to a canonical version, or one saying that for all arguments, its field applied to arguments is equal to the canonical one applied to arguments? (Or, that the single field of the instance is equal to the canonical function as a function?) Not sure if this difference matters or not.

3. Likewise, does it matter (performance-wise) whether the argument to Eq.refl is the canonical ofScientific or the division-ring one? Does it affect what we unfold and how?

[Mario Carneiro]

Yes to (1). What is "those lemmas" in (2)?

[Mario Carneiro]

the lemmas should not have any arguments asserting equality of instances

[Mario Carneiro]

Qq has the =Q type to represent definitional equalities that should hold. There is no equivalent expression in object-level lean

[Thomas Murrills]

Mario Carneiro said:

... What is "those lemmas" in (2)?

the lemmas should not have any arguments asserting equality of instances

These are the IsRat_ofScientific_of_true and isNat_ofScientific_of_false lemmas, which need one of the following as a hypothesis

1. σα = ⟨fun m s e ↦ (Rat.ofScientific m s e : α)⟩ (assert equality of instances)
2. OfScientific.ofScientific (α := α) = fun m s e ↦ (Rat.ofScientific m s e : α)
3. ∀ m s e, OfScientific.ofScientific (α := α) m s e = (Rat.ofScientific m s e : α)

[Thomas Murrills]

(Ignore the current commits, I pushed right before I saw your message, lol)

[Mario Carneiro]

link?

[Thomas Murrills]

!4#1707

[Mario Carneiro]

theorem isRat_ofScientific_of_true [DivisionRing α] [σα : OfScientific α] :
    {m e : ℕ} → {n : ℤ} → {d : ℕ} →
    σα = ⟨fun m s e ↦ (Rat.ofScientific m s e : α)⟩ →
    IsRat (mkRat m (10 ^ e) : α) n d → IsRat (OfScientific.ofScientific (α := α) m true e) n d
  | _, _, _, _, lh, ⟨_, eq⟩ => ⟨_, by
    simp only [lh, if_true, Rat.ofScientific, Rat.normalize_eq_mkRat]
    exact eq⟩

You should not be taking a OfScientific α hypothesis in this theorem, it should be the one derived from the division ring

[Thomas Murrills]

Right, true

[Thomas Murrills]

Hmm, using option 2, it doesn't like it when I infer an OfScientific instance anymore. Is this...an ok type for the hypothesis in the evaluator? Looks atypical. A little unsure of using explicit projections here. Q((($dα).toOfScientific).ofScientific = fun m s e ↦ (Rat.ofScientific m s e : $α))

[Thomas Murrills]

Alright, should be fixed, using option 2. (Can switch to 3 easily, I think)

[Thomas Murrills]

...Nevermind, the tests don't work anymore. :sweat_smile:

[Thomas Murrills]

(Oh! because Qq was "turned off" for the Eq.refl's. Just forgot to fix those.)

[Thomas Murrills]

Hmm, it doesn't like that. "(kernel) deep recursion detected"

[Mario Carneiro]

that Q(...) does indeed look atypical

[Mario Carneiro]

you should not need anything like that

[Mario Carneiro]

I don't really understand what you are trying though

[Thomas Murrills]

is an inferScientificOf dα def the way to go?

[Thomas Murrills]

What do you mean?

[Mario Carneiro]

I mean you are speaking without context

[Mario Carneiro]

you say "it doesn't work" before saying what "it" is

[Thomas Murrills]

Right, fair. This test gives the deep recursion error

example : (3.14159 : ℚ) = 314159/100000 := by norm_num1

[Mario Carneiro]

that could mean that the term doesn't typecheck

[Thomas Murrills]

I think it does? The other tests work

[Mario Carneiro]

what did you try? The test itself doesn't tell me much

[Mario Carneiro]

Thomas Murrills said:

I think it does? The other tests work

Also, if it's a good test it won't be testing exactly the same code paths as previous tests, so it is possible that norm_num only generates a bad term in this case

[Thomas Murrills]

When I was first implementing OfScientific, there were problems similar to this—I forget what exactly was different with the code to cause them, though. Terms with only a couple digits would work, but terms with more digits would cause a stack overflow. So, there are some tests that just have more digits, and it seems that was illuminating...

[Mario Carneiro]

remember that in norm_num type errors don't always manifest as a failure, they can also manifest as unfolding hell. Especially since the theorems being asserted are usually true, if you just normalize everything you often get a proof anyway, but with unacceptable performance and possibly a stack overflow or timeout

[Mario Carneiro]

you should check the defeq trace to see if anything surprising is being unfolded

[Thomas Murrills]

It's weird. having the extra instances around (as arguments to the lemmas used) seemed to work just fine, even though I'm sure this was abusing something somehow. I'll check that trace...

[Thomas Murrills]

Unrelated, but I noticed evalSub used some of the nice new Qq machinery for its initial checks. Not doing it in this PR, but should the others follow suit? Is that better, performance-wise?

[Thomas Murrills]

Interesting. Here's what I've found:

As long as the following two things are the case, the tests work fine. (Fast, even with an absurd number of digits.)

1. The lemmas take an explicit OfScientific α argument. This means that the type signature looks like this:

theorem isRat_ofScientific_of_true [DivisionRing α] (σα : OfScientific α) :
    {m e : ℕ} → {n : ℤ} → {d : ℕ} →
    @OfScientific.ofScientific α σα = (fun m s e ↦ (Rat.ofScientific m s e : α)) →
    IsRat (mkRat m (10 ^ e) : α) n d → IsRat (@OfScientific.ofScientific α σα m true e) n d

2. We use let σα ← inferOfScientificOfDivisionRing dα instead of something like (($dα).toOfScientific).ofScientific or have σα : Q(OfScientific α) := q(($dα).ofScientific.

If we use the obvious alternative to either of those—namely just a DivisionRing argument in the lemmas or a projection to obtain the instance (in any spot, such as the have)—we end up with (kernel) deep recursion detected for sufficiently long digit strings.

[Thomas Murrills]

I don't know why any of this happens, and I couldn't read a broader message from the defeq traces. For now, though, the version that works is up.

[Mario Carneiro]

Here's a minimized version:

theorem isRat_ofScientific_of_true' [DivisionRing α] :
    {m e : ℕ} → {n : ℤ} → {d : ℕ} →
    IsRat (mkRat m (10 ^ e) : α) n d → IsRat (OfScientific.ofScientific (α := α) m true e) n d
  | _, _, _, _, ⟨_, eq⟩ => ⟨_, by
    simp only [OfScientific.ofScientific, if_true, Rat.ofScientific, Rat.normalize_eq_mkRat]
    exact eq⟩

example : @IsRat ℚ (@DivisionRing.toRing ℚ Rat.divisionRing) 3.14159 (Int.ofNat 314159) 100000 :=
@isRat_ofScientific_of_true' ℚ Rat.divisionRing 314159 5 (Int.ofNat 314159) 100000 sorry
-- (kernel) deep recursion detected

[Thomas Murrills]

Minimized (depending on your metrics) further: it's (also?) a mkRat issue.

theorem foo [DivisionRing α] :
    {m e : ℕ} → {n : ℤ} → {d : ℕ} →
    IsRat (mkRat m (10 ^ e) : α) n d → IsRat (mkRat m (10 ^ e) : α) n d
  | _, _, _, _, h => h

example : @IsRat ℚ (@DivisionRing.toRing ℚ Rat.divisionRing) (mkRat 314159 (10 ^ 5)) (Int.ofNat 314159) 100000 :=
@foo ℚ Rat.divisionRing 314159 5 (Int.ofNat 314159) 100000 sorry
-- (kernel) deep recursion detected

[Mario Carneiro]

Minimized some more:

import Mathlib.Data.Rat.Basic
set_option trace.Meta.isDefEq true
example :
    @OfScientific.ofScientific Rat Rat.instOfScientificRat 314159 true 5 =
    @OfScientific.ofScientific Rat (@DivisionRing.toOfScientific Rat Rat.divisionRing) 314159 true 5 :=
  rfl

[Meta.isDefEq] ✅ OfScientific.ofScientific 314159 true 5 =
      OfScientific.ofScientific 314159 true
        5 =?= OfScientific.ofScientific 314159 true 5 = OfScientific.ofScientific 314159 true 5 ▼
  [] ✅ OfScientific.ofScientific 314159 true 5 =?= OfScientific.ofScientific 314159 true 5
  [] ✅ OfScientific.ofScientific 314159 true 5 =?= OfScientific.ofScientific 314159 true 5 ▼
    [] ✅ Rat.instOfScientificRat.1 314159 true 5 =?= DivisionRing.toOfScientific.1 314159 true 5 ▼
      [] ✅ Rat.ofScientific 314159 true 5 =?= ↑(Rat.ofScientific 314159 true 5) ▼
        [] ✅ Rat.ofScientific 314159 true 5 =?= RatCast.ratCast (Rat.ofScientific 314159 true 5) ▼
          [] ✅ if true = true then Rat.normalize (↑314159) (10 ^ 5)
              else ↑(Int.ofNat (314159 * 10 ^ 5)) =?= RatCast.ratCast (Rat.ofScientific 314159 true 5) ▼
            [] ✅ Decidable.casesOn (instDecidableEqBool true true) (fun x => ↑(Int.ofNat (314159 * 10 ^ 5))) fun x =>
                  Rat.normalize (↑314159) (10 ^ 5) =?= RatCast.ratCast (Rat.ofScientific 314159 true 5) ▶

cc: @Gabriel Ebner

[Mario Carneiro]

It appears that ratCast is less unfold-worthy than Rat.ofScientific

[Mario Carneiro]

this seems to make the work on making OfScientific diamonds commute worthless

[Thomas Murrills]

Is something similar true for mkRat vs. ratCast, then, given the above example which doesn't involve any sort of OfScientific?

[Thomas Murrills]

Mario Carneiro said:

this seems to make the work on making OfScientific diamonds commute worthless

well, at least the Eq.refl proof still succeeds now thanks to Rat.cast reducibility

[Mario Carneiro]

yes, I mean it's the same issue, <big term> = RatCast.ratCast <big term> should try to unfold ratCast, not <big term>

[Mario Carneiro]

that will only happen if <big term> can be normalized (e.g. it is a variable). If not lean will go crazy unfolding it

[Mario Carneiro]

making Rat.ofScientific opaque here will probably also work

[Thomas Murrills]

does it...make any sense to make RatCast.ratCast reducible? if it's something we want to unfold in most places? (can you even make structure fields reducible in this specific sense of the word?)

[Thomas Murrills]

(also, how would you unfold Rat.ofScientific to prove anything about it if it were opaque?)

[Mario Carneiro]

If it is @[irreducible] then you can still prove things about it

[Mario Carneiro]

and if it is irreducible_def then it is literally an opaque but there is an equality to the definition that you can use to prove things

[Thomas Murrills]

ah, ok

[Mario Carneiro]

more precisely it's not ratCast itself we want to unfold (it is a projection so this doesn't make sense) but rather @RatCast.ratCast.{0} Rat (@DivisionRing.toRatCast.{0} Rat Rat.divisionRing)

[Thomas Murrills]

Yeah, hmmm. It would be neat if we could somehow use the head of an expression to give lean a hint that it ought to readily unfold a specified application.

Or, honestly, just the ability to give structure projections in particular an attribute that makes complete applications of the projections readily unfold. Maybe that's what being a reducible structure projection should mean.

[Thomas Murrills]

(But I can also imagine that having complicated ways to mess with that kind of thing could cause some really unexpected behavior down the line...)

[Thomas Murrills]

Anyway, should I really go ahead and make Rat.ofScientific irreducible? It seems like a strange reason to adjust that definition—it seems like it's "not Rat.ofScientific's responsibility", so to speak—but I guess this definition is highly specific in its usage, so adjusting it so it can be used this way might make sense.

Though, is it better or worse than the current "non-instance OfScientific α argument" setup which seems to circumvent this unfolding problem anyway? (Esp. given that the theorems isRat_ofScientific_of_true, isNat_ofScientific_of_false are even more niche than Rat.ofScientific?)

[Heather Macbeth]

Looks like !4#1707 finally passes CI after two months of work from @Thomas Murrills. Could I ping this for review from someone who is confident with meta code? I'm looking forward to having this in mathlib!

[Thomas Murrills]

Let me give it just ooone more once-over today and then I’ll put it out for review! 😁

[Thomas Murrills]

Depending, of course, on what we want to do about this unfolding business.

@Mario Carneiro, should we make the round trip to std4 first and make Rat.ofScientific irreducible, or is letting these niche lemmas have a slightly weird type signature ok? (Or is there a better solution?)

[Thomas Murrills]

I've put it out for review because this is technically a review question, and we can always refactor if needed—this certainly won't be the last time NormNum.Basic is touched. :) And/or it can be addressed during review.

[Gabriel Ebner]

Anyway, should I really go ahead and make Rat.ofScientific irreducible?

Yes, it won't reduce anyhow since it uses gcd.

[Gabriel Ebner]

See also https://github.com/leanprover/lean4/commit/4167b2466a7dbad3cf489100d7d26559c3be7e21

[Thomas Murrills]

Alright, here's a PR making Rat.ofScientific irreducible :) std4#109

[Thomas Murrills]

So, I've been fixing !4#1707 to incorporate the std bump (thanks @Heather Macbeth !) and...I've hit (kernel) deep recursion again. That's on me—I shouldn't have assumed that the proposed solution of making Rat.ofScientific irreducible would work. I apologize for the wasted time. (Hopefully it wasn't completely wasted, I guess: defeq checks involving Rat.ofScientific are probably now less costly.) Lesson learned: always test a potential solution before using it.

The error

tl;dr it seems to be linked to the well-foundedness-based definition of gcd somehow.

The error is actually pretty generic. I've minimized it a lot, and I don't know if it's to do with defeq checks after all: the Meta.isDefEq trace is very short.. (I mean, this is a (kernel) error, so maybe that makes sense.)

Here's a version of it:

example (h : 10000 ≠ 0) : id (Rat.normalize 314159 10000 h) = Rat.normalize 314159 10000 h :=
  rfl -- (kernel) deep recursion detected

Note that the id (or some other expression equivalent to id) is required. Using a reducible version like @[reducible] def idR (a : α) := a doesn't change the error; but using fun x => x instead does eliminate the error. (I'm guessing because of how lambdas are handled, somehow?)

Perhaps we can blame the gcd in Rat.normalize:

example : id (Nat.gcd 314159 10000) = Nat.gcd 314159 10000 :=
  rfl -- (kernel) deep recursion detected

In turn, this seems to be due to the well-foundedness implementation, not the external code. Here's gcd copied over but without the extern:

private def gcdF (x : Nat) : (∀ x₁, x₁ < x → Nat → Nat) → Nat → Nat :=
  match x with
  | 0      => fun _ y => y
  | Nat.succ x => fun f y => f (y % Nat.succ x) (Nat.mod_lt _ (Nat.zero_lt_succ  _)) (Nat.succ x)

noncomputable def gcd2 (a b : @& Nat) : Nat :=
  WellFounded.fix (measure id).wf gcdF a b

example : id (gcd2 314159 10000) = gcd2 314159 10000 :=
  rfl -- (kernel) deep recursion detected

(Note, in case it's informative: in the course of teasing this out, Lean soaked up a lot of memory. Quitting VS code freed up 23 GB. And according to my iStatMenus R/W widget, it continues writing to disk for minutes after any errors have been cleared from the file, and only stops when I quit VS code or killall lean! Weird.)

(Note: making gcd2 irreducible doesn't help.)

Wrapping tricks

Oddly, the following prevents the error:

example : id (Int.ofNat (Nat.gcd 314159 10000)) = Int.ofNat (Nat.gcd 314159 10000) :=
  rfl -- ok

Int.ofNat is not special here—other expressions like e.g. casts produce the same behavior—but notably, it can't be replaced with simply id.

I'm guessing that something equivalent to whatever's going on here might be why I can play "tricks" to make the norm_num extension work (like passing in the instance as an argument to the lemmas).

In case it helps, note that switching the id and the Int.ofNat brings back the error—this makes a sort of sense, as now we're back to comparing the two expressions that caused us an issue before once we peel off Int.ofNat.

example : Int.ofNat (id (Nat.gcd 314159 10000)) = Int.ofNat (Nat.gcd 314159 10000) :=
  rfl -- (kernel) deep recursion detected

[Heather Macbeth]

I wonder if this could be related to the problems with the @[irreducible] attribute (reported in lean4#2161)?

[Thomas Murrills]

I tried to make gcd2 monadic to test that. Interestingly, before I even got to play around with irreducibility, when trace[debug] was present, the error vanished:

private def gcdF (x : Nat) : (∀ x₁, x₁ < x → Nat → CoreM Nat) → Nat → CoreM Nat :=
  match x with
  | 0      => fun _ y => pure y
  | Nat.succ x => (fun f y => do trace[debug] "{x}"; f (y % Nat.succ x) (Nat.mod_lt _ (Nat.zero_lt_succ  _)) (Nat.succ x))

noncomputable def gcd2 (a b : Nat) : CoreM Nat := do
  WellFounded.fix (measure id).wf gcdF a b

theorem x : id (gcd2 314159 10000) = gcd2 314159 10000 := rfl -- ok

But remove trace[debug] "{x}"; (and keep the do/monadicity), and suddenly it causes a (kernel) deep recursion detected error! :upside_down:

[Thomas Murrills]

(Though, are noncomputable defs irreducible by default? That would make sense...)

[Thomas Murrills]

Is there a way to download the lean4 build from lean4#2162 without building it myself? I'd like to test if that solves the issue, but it takes quite a long time for my computer to compile lean from scratch :sweat_smile:

[Thomas Murrills]

Ah, noncomputable defs are not automatically irreducible, i see. So I don't think lean4#2162 will make a difference...

[Gabriel Ebner]

Filed as lean4#2171

[Thomas Murrills]

Alright, !4#1707 is finally green and out for review (again)! :) It was reviewed by @Floris van Doorn at an earlier stage, so I suppose all that needs review are the commits afterward.

(Note: it was agreed in the meeting to go ahead with the lemmas which take an explicit OfScientific instance argument. When the (kernel) deep recursion detected error is addressed, I'll fix the lemmas.)