`interval_cases` for `pnat`s does not work, because `norm_num` does not support `pnat` (except sometimes)

[TwoFX]

The following fails (Lean 3.17.1):

import tactic.interval_cases

example (n : ℕ+) (h0 : 4 ≤ n) (h1 : 3 ≤ n) (h2 : n < 5) : n = 4 :=
by interval_cases n

/-
tactic failed, there are unsolved goals
state:
h0 : 4 ≤ ite (2 ≤ 1) 3 4,
h1 : 3 ≤ ite (2 ≤ 1) 3 4,
h2 : ite (2 ≤ 1) 3 4 < 5
⊢ ite (2 ≤ 1) 3 4 = 4
-/

The problem is that interval_cases combines lower bounds using max and then uses norm_num to simplify the resulting term. However, norm_num does not support pnats, as exemplified by the fact that in the following snippet two out of three uses of norm_num fail:

import tactic.norm_num

example (a : ℕ+) : ite ((1 : ℕ+) ≤ 2) 1 2 = a :=
by { norm_num, sorry } -- works, goal becomes 1 = a

example (a : ℕ+) : ite ((2 : ℕ+) ≤ 1) 1 2 = a :=
by { norm_num, sorry } -- norm_num failed to simplify

example (a : ℕ+) : ite ((1 : ℕ+) < 2) 1 2 = a :=
by { norm_num, sorry } -- norm_num failed to simplify

Simple uses of interval_cases with pnat will only invoke norm_num in the first situation, which is why interval_cases sometimes works with pnat.

[digama0]

Could you clarify this issue so it actually says what fails?

[TwoFX]

Could you clarify this issue so it actually says what fails?

I have updated the issue text with the error messages. I haven't tracked down why norm_num fails to simplify in the last two examples.

[digama0]

The problem is that norm_num needs linear_ordered_semiring ℕ+ for the theorems it applies, but this is false. Either we need a better typeclass, or norm_num needs to special case pnat.

[digama0]

We can't even use prove_nat_uncast in order to reflect it to a nat equality because this requires semiring pnat.