simp normal form: ofNat or Nat.cast?

Stream: mathlib4

[Yury G. Kudryashov]

Do we simplify either of OfNat.ofNat n and Nat.cast n to another?

[Gabriel Ebner]

OfNat.ofNat should not be simplified to Nat.cast because this loops. We'd get 42 = OfNat.ofNat R (nat_lit 42) --> Nat.cast (OfNat.ofNat Nat (nat_lit 42)) --> ...

[Yury G. Kudryashov]

Do we simplify it in the other direction?

[Gabriel Ebner]

The other way around would make sense, but only for numeric literals. That is, Nat.cast (OfNat.ofNat Nat n) = OfNat.ofNat R n would be a reasonable simp lemma.

[Yury G. Kudryashov]

Also, what is the right way to write simp lemmas about natural literals?

[Gabriel Ebner]

That is a sore point.

[Gabriel Ebner]

We have three different "kinds" of numeric literals.

[Gabriel Ebner]

There's 0.

[Gabriel Ebner]

There's 1.

[Yury G. Kudryashov]

I'm trying to port docs#algebra.bit0_smul_bit0

[Gabriel Ebner]

And there's n but only for [n.AtLeastTwo].

[Gabriel Ebner]

Right, instead of 0/1/bit0/bit1 we now need 0/1/AtLeastTwo

[Yury G. Kudryashov]

@[simp] theorem ofNat_smul_ofNat (m n : ℕ) [m.AtLeastTwo] [n.AtLeastTwo] :
    (OfNat.ofNat m : R) • (OfNat.ofNat n : A) = OfNat.ofNat (m * n) := _

doesn't work because we don't have AtLeastTwo for m * n.

[Yury G. Kudryashov]

Should I use m * n in the RHS?

[Gabriel Ebner]

Mmh, you could add (m * n).AtLeastTwo here.

[Gabriel Ebner]

I'm thinking about adding a LawfulOfNat class, then that lemma would require [LawfulOfNat R m] [LawfulOfNat A n] [LawfulOfNat A (m * n)].

[Gabriel Ebner]

And would also work for n ∈ {0, 1}.

[Yury G. Kudryashov]

Is it a Prop class?

[Gabriel Ebner]

If it's in Prop, you need to write [OfNat R n] [LawfulOfNat R n]. Otherwise [LawfulOfNat R n] would be enough. Not sure whats better.

[Johan Commelin]

I propose going for a mixin.

[Johan Commelin]

But that is predicated on the following orthogonal proposal: extend auto-implicit syntax so that if you write [LawfulOfNat R n] and there is no OfNat R n in scope, then automatically add [OfNat R n] as variable or assumption.

[Yury G. Kudryashov]

Coq has special syntax for this kind of arguments (I don't remember the details). What about [[LawfulOfNat R n]]?

[Notification Bot]

61 messages were moved from this topic to #mathlib4 > mixin algebraic typeclasses by Eric Wieser.

[Eric Wieser]

What about Int.ofNat vs Nat.cast? I don't understand what's going on here:

import Mathlib.Data.Nat.Cast.Defs
import Mathlib.Data.Int.Basic

#synth Coe ℕ ℤ  -- instCoeNatInt aka `Int.ofNat`
#check ((↑) : ℕ → ℤ) -- `Nat.cast`
#check ((↑) : Fin 2 → ℤ) -- `fun x => Int.ofNat ↑x`; why isn't this `fun x => Nat.cast ↑x`?

Why does Coe find the "wrong" instance?

[Gabriel Ebner]

YSK that Coe is only one way to declare a coercion. What (↑) searches for is CoeT (amongst other things; there are special cases hardcoded for sorts, functions, monads, etc.).

[Gabriel Ebner]

As for the coercion Fin 2 → ℤ. I think we need to add a [NatCast R] : Coe ℕ R instance as well (in addition to the already existing CoeTail ℕ R and CoeHTCT ℕ R instances). :exhausted:

[Eric Wieser]

Ah, right; we need the instance to be exactly the same type as docs4#instCoeNatInt ?

[Gabriel Ebner]

It also needs to be Coe, so that it applies instead of the Coe Nat Int instance.

[Eric Wieser]

https://leanprover-community.github.io/mathlib_docs/notes.html#coercion%20into%20rings says it can't be Coe

[Eric Wieser]

Should I just add the special case of Coe Nat Int?

[Eric Wieser]

!4#2878 does that. @Mario Carneiro, should this instance be in Std?

[Mario Carneiro]

Just FYI, I'm delegating those kinds of questions (re: instance design) to @Gabriel Ebner . I'll merge it if he approves (and in this case it seems like he does)