Nat.mod 0 n = 0 no longer true by rfl

Stream: mathlib4

[Gabriel Ebner]

Lean 4 has special kernel support for computation with Nat.mod (as well as special extern functions for VM computation), so it shouldn't make a big difference if we change the Nat.mod definition.

[Gabriel Ebner]

That said, it's a huge coincidence that nat.mod 0 n reduces in Lean 3. If I had picked a different value for the initial fuel, then we wouldn't have that defeq (because 0 < n ∧ n ≤ 0 doesn't reduce).

[Eric Wieser]

Given a fair bit of mathlib builds upon that coincidence, it seems a shame to throw away the coincidence without a compelling reason

[Notification Bot]

20 messages were moved from this topic to #mathlib4 > Porting Nat.mod_def by Eric Wieser.

[Notification Bot]

24 messages were moved here from #mathlib4 > Data.Fin.Basic (mathlib4#1084) by Eric Wieser.

[Eric Wieser]

I've created https://github.com/leanprover/lean4/pull/2014 as a draft, mainly to see if CI is happy. What are your thoughts on this, @Gabriel Ebner?

[Eric Wieser]

Gabriel Ebner said:

Lean 4 has special kernel support for computation with Nat.mod (as well as special extern functions for VM computation), so it shouldn't make a big difference if we change the Nat.mod definition.

Oh, so I guess that means that the kernel would have to change to match the new implementation?

[Mario Carneiro]

the kernel implementation is only for literals

[Eric Wieser]

I get a pretty weird error in CI from my change above

[Eric Wieser]

A downstream simp call produces an invalid term

[Mario Carneiro]

so as long as you haven't actually changed the value of the definition (and since you proved the same defining equation I think it's safe to say this is not the case) the kernel doesn't have to change

[Eric Wieser]

This proof:

@[simp] theorem gcd_zero_right (n : Nat) : gcd n 0 = n := by
  cases n <;> simp [gcd_succ]

fails with

application type mismatch
  @Eq.ndrec Nat (succ n✝) (fun n => gcd n 0 = n)
    (of_eq_true
      (Eq.trans (congrFun (congrArg Eq (congrFun (congrArg gcd (zero_mod (succ n✝))) (succ n✝))) (succ n✝))
        (eq_self (succ n✝))))
argument has type
  gcd (0 % succ n✝) (succ n✝) = succ n✝
but function has type
  (fun n => gcd n 0 = n) (succ n✝) → ∀ {b : Nat}, succ n✝ = b → (fun n => gcd n 0 = n) b

[Eric Wieser]

Which is scary because the term which has a type mismatch is being produced by simp

[Eric Wieser]

it works fine as

@[simp] theorem gcd_zero_right (n : Nat) : gcd n 0 = n := by
  cases n with
  | zero => simp [gcd_succ]
  | succ n =>
    rw [gcd_succ]
    exact gcd_zero_left _

[Eric Wieser]

But I feel like the failure might be a warning sign

[Mario Carneiro]

does simp only [gcd_succ]; sorry work in the second branch?

[Eric Wieser]

No, with

application type mismatch
  id (sorryAx (gcd (0 % succ n) (succ n) = succ n))
argument has type
  gcd (0 % succ n) (succ n) = succ n
but function has type
  gcd (succ n) 0 = succ n → gcd (succ n) 0 = succ n

[Mario Carneiro]

Can you replicate this outside core?

[Eric Wieser]

If I stupidly edited things in .elean/toolchains/..., how do I wipe them and start afresh?

[Mario Carneiro]

I think you can use elan toolchain uninstall bla

[Eric Wieser]

I think this image is toast, I'll spin up a new one

[Eric Wieser]

Yes, it reproduces outside core

import Init.WF
import Init.WFTactics
import Init.Data.Nat.Basic
namespace Nat

protected def modCore (y : Nat) : Nat → Nat → Nat
  | Nat.zero, x => x
  | Nat.succ fuel, x => if 0 < y ∧ y ≤ x then Nat.modCore y fuel (x - y) else x

protected def mod' (x y : @& Nat) : Nat :=
Nat.modCore y x x

@[simp] theorem zero_mod' (b : Nat) : Nat.mod' 0 b = 0 := rfl

end Nat

namespace Nat

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

noncomputable def gcd' (a b : Nat) : Nat :=
  WellFounded.fix (measure id).wf gcdF' a b

@[simp] theorem gcd'_zero_left (y : Nat) : gcd' 0 y = y :=
  rfl

theorem gcd'_succ (x y : Nat) : gcd' (succ x) y = gcd' (Nat.mod' y (succ x)) (succ x) :=
  rfl
--              VVVVVVVVVVVVVVV error here
@[simp] theorem gcd'_zero_right (n : Nat) : gcd' n 0 = n := by
  cases n <;> simp [gcd'_succ]

end Nat

[Eric Wieser]

(deleted)

[Mario Carneiro]

Oh I meant using mod', no prelude

[Eric Wieser]

Edited above

[Eric Wieser]

Shall I make a lean4 bug report?

[Mario Carneiro]

great, now I can use show_term on the simp call:

import Std.Tactic.Basic
...
@[simp] theorem gcd'_zero_right (n : Nat) : gcd' n 0 = n := by
  cases n with
  | zero => simp [gcd'_succ]
  | succ n => show_term simp only [gcd'_succ]; sorry
-- @id (gcd' (succ n) 0 = succ n) (sorryAx (gcd' (Nat.mod' 0 (succ n)) (succ n) = succ n))

[Mario Carneiro]

it seems that something was marked as a dsimp lemma that isn't rfl

[Eric Wieser]

Changing gcd'_succ to be proved by id rfl makes the error go away

[Mario Carneiro]

this could be one of those rare instances of non-transitivity of defeq

[Mario Carneiro]

It is surprising that gcd'_succ is provable by rfl in the first place, so using id rfl seems reasonable

[Eric Wieser]

Filed as leanprover/lean4#2021