div notation and rfl

Stream: mathlib4

[Antoine Labelle]

Why doesn't the following work in Lean 4?

example (a b : ℤ) : a / b = Int.div a b := rfl

I'm trying to close a goal of this form, where b is replaced by some complicated expression, and I'm confused by why this isn't closed by rfl.

[Mario Carneiro]

example (a b : ℤ) : a / b = Int.ediv a b := rfl

[Mario Carneiro]

See https://leanprover.zulipchat.com/#narrow/stream/341532-lean4-dev/topic/.5BRFC.5D.20Int.2Ediv.20convention

[Mario Carneiro]

Hopefully this will be resolved soon, with Int.ediv getting renamed to Int.div and moved to core

[Antoine Labelle]

I see. I'm working on Data.Rat.Lemmas and several things that used to be rfl in mathlib3 break in mathlib4 because of that, since some definitions about rational numbers rely on Int.div rather than Int.ediv (Rat.normalize and Rat.mul specifically). Should I try to refactor these definitions to use Int.ediv instead?

[Scott Morrison]

Yes.

[Scott Morrison]

Rename the lemmas to mention ediv. The notation /. correctly points to ediv.

[Johan Commelin]

So these lemmas in Algebra.EuclideanDomain.Instances are no longer true:

theorem Int.negSucc_mod_ofNat (m n : Nat) :
  (Int.negSucc m % (ofNat n) : Int) = -ofNat (m.succ % n) := rfl
theorem Int.negSucc_mod_negSucc (m n : Nat) :
  (Int.negSucc m % (negSucc n) : Int) = -ofNat (m.succ % n.succ) := rfl

What is the expected path forward?

[Ruben Van de Velde]

Did we change % to emod or just / to ediv?

[Scott Morrison]

Both

[Mario Carneiro]

Antoine Labelle said:

I see. I'm working on Data.Rat.Lemmas and several things that used to be rfl in mathlib3 break in mathlib4 because of that, since some definitions about rational numbers rely on Int.div rather than Int.ediv (Rat.normalize and Rat.mul specifically). Should I try to refactor these definitions to use Int.ediv instead?

No, you should use the API lemmas that are stated in terms of Int.ediv

[Antoine Labelle]

Mario Carneiro said:

Antoine Labelle said:

I see. I'm working on Data.Rat.Lemmas and several things that used to be rfl in mathlib3 break in mathlib4 because of that, since some definitions about rational numbers rely on Int.div rather than Int.ediv (Rat.normalize and Rat.mul specifically). Should I try to refactor these definitions to use Int.ediv instead?

No, you should use the API lemmas that are stated in terms of Int.ediv

Hmm well the file I'm working on is the one with a lot of the API lemmas, and several mathlib3 proofs need to unfold the definitions.

[Mario Carneiro]

The lemmas I'm talking about already exist in Std