Nat.sqrt no longer reduces definitionally

Stream: mathlib4

[David Renshaw]

This proof was broken by batteries#1395:

import Batteries

example : Nat.sqrt 3 = 1 := by rfl

Nat.sqrt now uses Nat.log2, which uses decreasing_by and therefore does not reduce.

An improvement to Nat.log2 landed in lean4#10046, but that's not yet available on leanprover/lean4:v4.23.0-rc2.

Is there an easy workaround for proofs like the above? Should I just wait until the Lean version gets bumped?

[Aaron Liu]

I guess norm_num if you have mathlib

[Damiano Testa]

Amusingly, group also works.

[Aaron Liu]

if you don't have mathlib you can unfold Nat.sqrt to get Nat.sqrt.iter and use the characterizing lemmas for log2 (docs#Nat.le_log2) to show what the log2 is and then maybe rfl will work

[Kevin Buzzard]

Damiano Testa said:

Amusingly, group also works.

Why?

[Aaron Liu]

Kevin Buzzard said:

Damiano Testa said:

Amusingly, group also works.

Why?

I'm guessing it calls norm_num

[Aaron Liu]

it calls ring_nf which calls norm_num

[Aaron Liu]

https://github.com/leanprover-community/mathlib4/blob/b498015292d2010eb7b6caca844fe9e6bd5b36b1/Mathlib/Tactic/Group.lean#L65-L67

[David Renshaw]

Stepping up one level to what actually broke in my proof:

import Mathlib

example : ¬ IsSquare 2 := by decide

This worked before mathlib4#29142 and does not work now. Is there a workaround?

[Aaron Liu]

import Mathlib

example : ¬ IsSquare 2
  | ⟨_ + 3, hn⟩ => nomatch hn

[David Renshaw]

Thanks. I got it working, but it's not pretty. https://github.com/dwrensha/compfiles/commit/1f13be8b301843fee3231e6077df7f39d48a6ba5

[Aaron Liu]

should we have a norm_num extension to reduce IsSquare on Nat and Int and Rat

[Damiano Testa]

Kevin Buzzard said:

Damiano Testa said:

Amusingly, group also works.

Why?

I had no idea, until Aaron mentioned the fact that internally there is a norm_num. I found out using hint.

[Kim Morrison]

Apologies about this, I didn't entirely overlook this issue but managed to forget that log2 has only been fixed in the future...

Is it less work to undo these changes and redo them in two weeks, or to leave adaptation notes in place where the breakages occur now, removing them in two weeks?

[Eric Wieser]

Should nontrivial Decidable instance be written with a by decide example after them to catch this type of issue in future?

[Eric Wieser]

(where "trivial" means inferInstanceAs <| ...)

[David Renshaw]

Just noting for completeness: the definitional reduction started working again in leanprover/lean4:v4.24.0-rc1, but recently stopped working once more, due to https://github.com/leanprover-community/batteries/pull/1447 I guess.

(I can work around this, and I think that a norm_num extension sounds like a decent longer term solution.)

[Yury G. Kudryashov]

I have a norm_num extension for IsSquare somewhere in the code approved for opensourcing. I'll open a PR this weekend. OTOH, I would prefer to have by decide work on IsSquare 3. As for batteries#1447, we can switch to a fuel-based definition of iter, see #28768 for an example.

[Markus Himmel]

You can also do this, which is probably more or less what the norm_num extension does, just by hand:

import Mathlib

theorem Nat.sqrt_eq_iff {m n : Nat} :
    Nat.sqrt m = n ↔ n * n ≤ m ∧ m < (n + 1) * (n + 1) := by
  refine ⟨?_, fun ⟨h₁, h₂⟩ => le_antisymm ?_ ?_⟩
  · rintro rfl
    exact ⟨sqrt_le _, lt_succ_sqrt _⟩
  · rwa [le_iff_lt_add_one, sqrt_lt]
  · rwa [le_sqrt]

theorem Nat.isSquare_iff {m : Nat} :
    IsSquare m ↔ Nat.sqrt m * Nat.sqrt m = m := by
  simp_rw [← Nat.exists_mul_self m, IsSquare, eq_comm]

example : ¬ IsSquare 2 := by
  simp [Nat.isSquare_iff]

example : ¬ IsSquare 5 := by
  simp [Nat.isSquare_iff, show Nat.sqrt 5 = 2 by simp [Nat.sqrt_eq_iff]]

example : ¬ IsSquare 234123412314123 := by
  simp [Nat.isSquare_iff, show Nat.sqrt 234123412314123 = 15301091 by simp [Nat.sqrt_eq_iff]]

[Aaron Liu]

Yury G. Kudryashov said:

I have a norm_num extension for IsSquare somewhere in the code approved for opensourcing. I'll open a PR this weekend. OTOH, I would prefer to have by decide work on IsSquare 3. As for batteries#1447, we can switch to a fuel-based definition of iter, see #28768 for an example.

I was gonna open a PR now

[Aaron Liu]

well, in a few minutes

[Yury G. Kudryashov]

I can review it after breakfast.

[Aaron Liu]

this has been taking more than a few minutes

[Aaron Liu]

#30439 (I still need to write tests) (I wrote tests)

[Yury G. Kudryashov]

Does Mathlib need adaptations?

[Yury G. Kudryashov]

I thought you were going to write a PR to make Nat.sqrt computable again.

[Yury G. Kudryashov]

I already have a norm_num extension for IsSquare.

[Yury G. Kudryashov]

Now I'll need to compare your code to mine. I'll do it tonight.

[Aaron Liu]

Yury G. Kudryashov said:

I thought you were going to write a PR to make Nat.sqrt computable again.

oh yeah I can do that too if you want

[Yury G. Kudryashov]

You may want to reuse some material for #28768 (though the proofs will be shorter for n = 2).

[David Renshaw]

Once https://github.com/leanprover/lean4/pull/7965 gets included in a release, I think it should be possible to revert https://github.com/leanprover-community/batteries/pull/1447 and have Nat.sqrt reduce definitionally in an efficient way.

[David Renshaw]

If that comes to pass, is an IsSquareextension for norm_num still desirable?

[Yury G. Kudryashov]

There are a few open PRs with this extension.

[Yury G. Kudryashov]

#30439

[Yury G. Kudryashov]

#31671

[Yury G. Kudryashov]

#32365

[Yury G. Kudryashov]

I would prefer to have one of them merged, but I would prefer if another maintainer makes a choice.