PNat coercions

Stream: mathlib4

[Michael Stoll]

Can we have a simplemma that does ((37 : ℕ+) : ℕ) = 37 for all positive values of 37?
(For every concrete value, this is rfl, but I was not able to figure out how to write this for general n.)

[Eric Wieser]

This would be stated using OfNat.ofNat

[Michael Stoll]

But how, precisely?

[Eric Wieser]

You should be able to find lots of similar lemma statements by searching for that

[Eric Wieser]

Eg docs#zpow_ofNat, which is unreadable in the docs, but stated:

-- See note [no_index around OfNat.ofNat]
@[to_additive ofNat_zsmul]
lemma zpow_ofNat (a : G) (n : ℕ) : a ^ (no_index (OfNat.ofNat n) : ℤ) = a ^ OfNat.ofNat n :=
  zpow_coe_nat ..

[Michael Stoll]

I was wondering why such a simp lemma does not exist:

import Mathlib

example : ((37 : ℕ+) : ℕ) = 37 := by simp -- simp made no progress

[Michael Stoll]

So maybe the no_index is the secret sauce here.

[Eric Wieser]

Because no one wrote the lemma yet, I think

[Eric Wieser]

OfNat didn't exist in Lean3, so mathlib is full of holes around it

[Michael Stoll]

The next problem is that for general n, (OfNat.ofNat n) : ℕ+ does not type-check. But this works:

@[simp]
lemma PNat.val_ofNat (n : ℕ) : ((no_index (OfNat.ofNat n.succ) : ℕ+) : ℕ) = n.succ := rfl

example : ((37 : ℕ+) : ℕ) = 37 := by simp

@Riccardo Brasca : Can you add this simp lemma in #10683 and use it in the proofs?

[Eric Wieser]

You should use [n.AtLeastTwo] or perhaps [NeZero n], rather than n.succ

[Michael Stoll]

[n.AtLeastTwo] does not help against "failed to synthesize instance
OfNat ℕ+ n".

[Michael Stoll]

Same with [NeZero n].

[Michael Stoll]

I guess this is because there cannot be a NatCast instance for PNat.

[Timo Carlin-Burns]

Indeed, the OfNat instance for PNat doesn't use Nat.AtLeastTwo like most other ones:

#check instOfNatPNatHAddNatInstHAddInstAddNatOfNat
-- (n : ℕ) → OfNat ℕ+ (n + 1)

Maybe it should be split into an instance for n = 1 and an instance for n.AtLeastTwo for consistency

[Eric Wieser]

Ah, in that case the n.succ spelling is fine

[Riccardo Brasca]

Thanks for the suggestion! I will do it tomorrow