More issues with OfNat

Stream: mathlib4

[Chris B]

In working on Fin and unsigned intengers, I ran across two issues with OfNat; the first is that as it stands, the instance of OfNat that's defined by the ofNat_class macro doesn't seem to take priority over the instance of OfNat for a type in the prelude, so by default, even if a type has an element of something like AddMonoid, (0 : A) + x will still select the OfNat instance from the prelude.

SinceZero is used as the base for e.g.MonoidWithZero, and Zero isn't tied to OfNat, but the lemmas are written with 0 literals, sometimes the goal state will show (0 : A) * x = 0 or something that's definitionally equal to that, but MonoidWithZero.zero_mul won't actually work, and I'm not even sure the reason why it doesn't work is consistent. This part in particular seems really unintuitive.

For two examples, the nat lit 0 here resolves as the OfNat from the prelude instead of the one from the ofNat_class macro, and while have h1 : (0 : USize).val = (0 : Fin USize.size) :=.. is a definitional equality, simplification with MonoidWithZero.zero_mul only works for the other integer types.

[Mac]

Personally, I think it would be nice if OfNat.ofNat was like coe and was magically reduced immediately. I think that would help in a lot of these cases?

[Chris B]

I'm not sure whether that would solve the issue of Zero and OfNat 0 not actually being related either in their definition or by a given structure. The pp.all output for these is a headache; I feel like some interaction that's supposed to happen with these instances:

  instance {α} [$Class α] : OfNat α (nat_lit $n) where
    ofNat := ‹$Class α›.1

  instance {α} [OfNat α (nat_lit $n)] : $Class α where
    $field:ident := $n

is not actually happening.

[Mario Carneiro]

Mac said:

Personally, I think it would be nice if OfNat.ofNat was like coe and was magically reduced immediately. I think that would help in a lot of these cases?

This would make the job of normNum very difficult, because it has to recognize numerals somehow and this is much harder if a numeral can be eagerly expanded to almost anything

[Mario Carneiro]

That doesn't necessarily mean it's not a good idea to unfold numerals eagerly, but they would have to unfold to something predictable by normNum

[Chris B]

speaking of normNum, can this be solved with like a LawfulZero that includes the OfNat instance and a proof that OfNat 0 = Zero.zero?

[Mario Carneiro]

Don't the algebraic classes already have that axiom?

[Chris B]

I don't think so. I assumed that's what the OfNat instance in the ofNat_class macro was for, but it doesnt seem to work in that role.

[Gabriel Ebner]

Good morning!

Personally, I think it would be nice if OfNat.ofNat was like coe and was magically reduced immediately. I think that would help in a lot of these cases?

The problem with this suggestion is that we have lemmas and definitions which are generic over OfNat, e.g. ∀ [LinearOrderedField α], 42 < (69 : α) (to what should ofNat expand here? and it should be the same as 42 < (69 : ℝ)). By contrast, we are never generic in coercions, we don't[1] have lemmas with a [Coe α] assumption.
[1] There are two such lemmas in mathlib, and they are only used to unfold coercions and will become obsolete in Lean 4.

[Gabriel Ebner]

but MonoidWithZero.zero_mul won't actually work

I can't reproduce this, the mul_zero lemma applies in both cases here (in your PR, revision adaf6348b7bf). Do you have an example where it breaks?

example (x : USize) : OfNat.ofNat (nat_lit 0) (self := instOfNatUSize) * x = 0 := by
  simp only [zero_mul]

example (x : USize) : OfNat.ofNat (nat_lit 0) (self := instOfNat) * x = 0 := by
  simp only [zero_mul]

[Gabriel Ebner]

speaking of normNum, can this be solved with like a LawfulZero that includes the OfNat instance and a proof that OfNat 0 = Zero.zero?

Maybe I should explain the design here. In Lean 4, numerals are implemented using the OfNat type class. An additive monoid needs to provide a zero numeral (so that we can use generic lemmas like mul_zero). Many types also provide numerals for all natural numbers themselves. So there are two ways you can get a zero in such a type: the zero from the additive monoid, or the zero from the type.

For obvious reasons, these two zeros must be definitionally equal (otherwise we'd run into the problems that you're describing).

The solution is to require---by convention---that the zero field of the Zero class is always defeq to ofNat 0. The default value of the zero field is 0, so if you never manually construct an instance of the Zero class then you shouldn't run into any issues. This also means that classes like CommRing do not extend both Zero and One, they extend OfNat instead.

Adding a LawfulZero class (with a zero = ofNat 0 proof) only makes the problem worse, because now you always have two non-defeq versions of zero (in a generic context).

[Mac]

@Gabriel Ebner Since we are on the topic, I'm curious, why is Zero not defined as a class abbrev? For example:

class abbrev Zero a := OfNat a (nat_lit 0)

[Mac]

or, more important, why does it not extend OfNat?

[Sebastian Ullrich]

(aside: I wonder if class abbrev should complain that you should use abbrev when given a single parent)

[Mario Carneiro]

Well, this is basically saying "why not use OfNat a (nat_lit 0) directly", and the answer is that you currently can't have OfNat a (nat_lit 0) and OfNat a (nat_lit 1) both as parents

[Mario Carneiro]

even if you could, it sounds very difficult to resolve that in the context of something that has OfNat a n for all n, while still having reasonable field projections and structure constructors

[Gabriel Ebner]

The previous discussion in this stream could also be interesting to you: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/0.F0.9F.94.B6.20.28.22zero.20diamond.22.29

[Gabriel Ebner]

I'm curious, why is Zero not defined as a class abbrev?

The problem is that class abbrev extends OfNat, which means there is a toOfNat field in both Zero and One. And that produces a clash if you extend both (as is the case in MonoidWithZero).

[Chris B]

Gabriel Ebner said:

speaking of normNum, can this be solved with like a LawfulZero that includes the OfNat instance and a proof that OfNat 0 = Zero.zero?

The solution is to require---by convention---that the zero field of the Zero class is always defeq to ofNat 0.

There's an MWE of what I'm talking about in this branch, specifically the stuff introduce in this commit. If you change the priority of the OfNat instance from ofNat_class to be (priority := high), it DOES seem to take the intance of OfNat from the underlying structure, but it still doesn't seem to work in the cases that are sorry'd, even though the manually defined Zero for Fin defines zero the same for any inhabited Fin n. Prelude defines OfNat differently for USize (even though I think they could all be the same if the other int types were defined in terms of OfNat').

[Gabriel Ebner]

(deleted)

[Gabriel Ebner]

This interesting. Here is where it goes wrong:

      [Meta.isDefEq.step] instOfNat =?= instOfNatUInt8
      [Meta.isDefEq.delta.unfoldLeft] instOfNat
        [Meta.isDefEq.step] { ofNat := Zero.zero } =?= instOfNatUInt8
        [Meta.isDefEq.delta.unfoldRight] instOfNatUInt8
          [Meta.isDefEq.step] { ofNat := Zero.zero } =?= { ofNat := UInt8.ofNat 0 }
          [Meta.isDefEq.step] Zero.zero =?= UInt8.ofNat 0
            [Meta.isDefEq.delta.unfoldRight] UInt8.ofNat
              [Meta.isDefEq.step] Zero.zero =?= { val := Fin.ofNat 0 }
              [Meta.isDefEq.delta.unfoldLeft] Zero.zero
                [Meta.isDefEq.step] MonoidWithZero.toZero.1 =?= { val := Fin.ofNat 0 }
                [Meta.isDefEq.step] MonoidWithZero.toZero =?= { zero := { val := Fin.ofNat 0 } }
                  [Meta.isDefEq.delta.unfoldLeft] MonoidWithZero.toZero
                    [Meta.isDefEq.step] ?self.2 =?= { zero := { val := Fin.ofNat 0 } }
                    [Meta.isDefEq.onFailure] ?self.2 =?= { zero := { val := Fin.ofNat 0 } }
                      [Meta.isDefEq.stuckMVar] found stuck MVar ?self : MonoidWithZero UInt8
                      [Meta.isDefEq.hint] ?self.2 =?= { zero := { val := Fin.ofNat 0 } }
                      [Meta.isDefEq.hint] { zero := { val := Fin.ofNat 0 } } =?= ?self.2

I would have expected this to cause a type-class search for MonoidWithZero UInt8 to unstuck ?self (and iirc that's what happens in Lean 3).

[Gabriel Ebner]

@Chris B Please just provide a MonoidWithZero instance. (Which is implied by the CommRing instance that I keep telling you to implement).

[Gabriel Ebner]

instance : MonoidWithZero UInt8 where
  zero_mul := sorry
  mul_zero := sorry

lemma UInt8.zero_mul' (a : UInt8) : 0 * a = 0 := by
  simp [zero_mul] -- works (and the zero comes from instOfNatUInt8)

[Chris B]

The issue arises in the implementation of MonoidWIthZero UInt8; if there was already an implementation I would obviously just use that, I only extracted the lemmas to make the mwe more clear. There is an implementation of MonoidWithZero in the PR, but making it work for USize requires extracting h0 and adding the mk_zero_eq_zero lemma, which is what's in the commit I linked. The other UInt sizes also don't work without extracting h0 as a separate have statement.

[Chris B]

The behavior seems roughly the same after moving to CommSemiring, despite the extra ofNat and Numeric stuff being in the mix: commit.

[Gabriel Ebner]

First of all, you're still missing the ofNat field (and proving that a + sorry = a is of course not possible). But then we might be hitting an actual issue:

                          [Meta.isDefEq.step] Semiring.toNumeric.1
                            0 =?= { val := 0 % UInt8.size, isLt := (_ : 0 % UInt8.size < UInt8.size) }
                          [Meta.isDefEq.step] Semiring.toNumeric.1 =?= Fin.mk
                            [Meta.isDefEq.step] Semiring.toNumeric =?= { ofNat := Fin.mk }

Lean never goes back and tries to reduce Semiring.toNumeric.1 (after unstucking it).

[Gabriel Ebner]

This is an almost worked out example for Semiring UInt8, everything seems to go smoothly:

lemma neg_def (a : UInt8) : -a = ⟨-a.val⟩ := rfl
lemma zero_def : (0 : UInt8) = ⟨0⟩ := rfl
lemma one_def : (1 : UInt8) = ⟨1⟩ := rfl

instance : Semiring UInt8 where
  add_zero := by simp [add_def, zero_def]
  mul_one := by simp [mul_def, one_def]
  one_mul := by simp [mul_def, one_def]
  zero_add := by simp [add_def, zero_def]

  ofNat := ofNat
  ofNat_succ a := sorry

  nsmul n a := ofNat (a.val * n)
  nsmul_zero' := by simp
  nsmul_succ' := sorry

  zero_mul := by simp [mul_def, zero_def]
  mul_zero := by simp [mul_def, zero_def]

  npow n a := ofNat (a.val.val ^ n)
  npow_zero' := by simp
  npow_succ' := sorry

  mul_add := by simp [mul_def, add_def, mul_add]
  add_mul := by simp [mul_def, add_def, add_mul]

[Gabriel Ebner]

I don't know yet what goes wrong when you use Semiring.add_zero instead of AddMonoid.add_zero.

[Chris B]

Thanks, I appreciate the guidance so far. I don't think I understand the interaction of typeclass inference and the OfNat instance defined after Numeric instance Numeric.OfNat [Numeric α] : OfNat α n := ⟨Numeric.ofNat n⟩; I would have expected zero_def in this example to use Numeric.OfNat, but it uses the default instance provided by the prelude:

instance : Numeric UInt8 where
  ofNat a := UInt8.mk (Numeric.ofNat a)

-- lhs is (@OfNat.ofNat UInt8 0 (@instOfNatUInt8 0))
lemma zero_def : (0 : UInt8) = ⟨0⟩ := rfl

I understand that these are all supposed to be defEq anyway.

[Chris B]

Actually I guess in this case it would be preferable for the derived instances to take priority since it's more convenient for all integers to use Fin.ofNat', but UInt* and USize are not defined the same in the prelude.

[Gabriel Ebner]

I think you're too hung up on the precise instance Lean puts there. Type-class synthesis makes no guarantees about what instance it will find. Anything that typechecks is fair game. Priorities are only a hint for performance optimizations. (Unless you really really know what you're doing.)

[Gabriel Ebner]

In the end it doesn't matter, since instOfNatUInt8 and the ofNat instance from Numeric are defeq. (And if they aren't, then that's a bug that absolutely needs to be fixed.)

[Gabriel Ebner]

instance : Numeric UInt8 where
  ofNat a := UInt8.mk (Numeric.ofNat a)

I think in this case it would be better to use ofNat := ofNat (i.e. define Numeric in terms of OfNat). Having two different definitions is a bit dangerous since they can get out of sync (even if they are defeq now).

[Chris B]

Ok, I'll just ditch the idea of papering over the differences in the OfNat definitions in the prelude for integers in light of the precedence stuff. While Mathlib4 is still in the "just trying things out" phase, I'd like to (respectfully) voice the opinion that having OfNat, Numeric, Zero, and One, some of which derive each other but not in a way that guarantees that the derived instance will be used and are required by convention to respect certain definitional equalities doesn't seem great.

[Mario Carneiro]

Note that part of the reason for Numeric is to avoid having to deal with the complication of dependent numerals, which is hell for normNum and pretty much anything that wants to actually reason about numbers

[Mario Carneiro]

It's an interesting design, but I don't think mathlib should have any support for types that only have some numerals. The most obvious candidates are things like Fin n or UInt8 and these will definitely not be able to reject out of bounds values anyway because we also want them to be rings

[Gabriel Ebner]

For clarification: all the UInt* types support all numerals. (300 : UInt8) elaborates just fine (and is equal to 44 as expected).

[Gabriel Ebner]

All the complications we have here are (simplifying a bit) because we now have a function Nat -> A instead of 0,1,+. Dependent numerals don't make any additional problems (except that we have to wrap OfNat in Numeric).

[Gabriel Ebner]

@Chris B I'm sorry if this came across as too much pressure. The PR now has working CommRing instances for UInt* so I've merged it. Dealing with definitional equalities is unfortunately a part of Lean, this here isn't even the worst example. In #general there's been a week-long discussion over how to do (e.g. matrix) inverses while avoiding non-defeq diamonds. However definitional equality is critically important, once you have two different versions of 0 = 0 you get into a special level of hell where rfl doesn't prove 0 = 0, simp doesn't simplify if 0 = 0 then 0 else 1, etc.

[Chris B]

@Gabriel Ebner Not at all, thank you for taking the time to help. I respect what you're saying about confronting definitional equalities being a necessary evil, my issue is with a) the complexity of the interaction between OfNat, Numeric, Zero, One, and the basic algebraic structures, and b) that this level of complexity is implicated by the act of writing 0 or 1.

[Joe Hendrix]

This might be outside the scope of normNat, but I wonder if it's feasible for tactics to cache known equivalences between constants and have normNat and other procedures reason modulo those equalities.

[Mario Carneiro]

@Joe Hendrix (I assume you mean normNum.) This is out of scope for normNum, which is explicitly for closed terms, the sort of thing for which #eval works. For reasoning modulo constants the normal forms get a lot more complicated, and you need something more like ring_nf (which is limited to only a specific kind of dependence on the uninterpreted constants, namely ring expressions).