interval_cases for `PNat`

Stream: mathlib4

[Moritz Firsching]

While working on !4#2155, I noticed that the ported interval_cases tactic currently doesn't work on PNat. The corresponding line is commented out https://github.com/leanprover-community/mathlib4/blob/c16c0c414d4ea87bd10716ffd38b93d9d66aa215/Mathlib/Tactic/IntervalCases.lean#L287
Is this a TODO that should be fixed? Does this depend on something that is still missing, like some features of norm_num or can the tactic in principle be adapted to work for PNat now?

[Jireh Loreaux]

Is it just that PNat wasn't ported when interval_cases was? Probably we just need to port the relevant pnatMethods code.

[Jireh Loreaux]

Let me look into this briefly.

[Jireh Loreaux]

Sorry, I think you are right that we're missing a PNat plugin for norm_num. I think once we have it this should be all that's needed for interval_cases:

lemma _root_.PNat.add_one_le_of_not_le {a b : ℕ+} (h : ¬b ≤ a) : a + 1 ≤ b := by
  exact (PNat.coe_lt_coe a b).mpr <| Nat.gt_of_not_le h
lemma _root_.PNat.le_sub_one_of_not_le {a b : ℕ+} (h : ¬b ≤ a) : a ≤ b - 1 := by
  rw [←PNat.coe_le_coe, PNat.sub_coe, if_pos ((PNat.one_le a).trans_lt (not_le.mp h))]
  refine (Nat.le_sub_iff_add_le b.prop).mpr <| (PNat.coe_lt_coe a b).mpr (not_le.mp h)

/-- A `Methods` implementation for `ℕ+`.
This tells `interval_cases` how to work on positive natural numbers. -/
def pnatMethods : Methods where
  initLB (e : Q(ℕ+)) :=
    pure (.le 1, q(1), q(PNat.one_le $e))
  eval e := do
    let ⟨z, e, p⟩ := (← NormNum.derive (α := (q(ℕ+) : Q(Type))) e).toRawIntEq.get!
    pure (z, e, p)
  proveLE (lhs rhs : Q(ℕ+)) := mkDecideProof q($lhs ≤ $rhs)
  proveLT (lhs rhs : Q(ℕ+)) := mkDecideProof q(¬$rhs ≤ $lhs)
  roundUp (lhs rhs _ : Q(ℕ+)) (p : Q(¬$rhs ≤ $lhs)) := pure q(PNat.add_one_le_of_not_le $p)
  roundDown (lhs rhs _ : Q(ℕ+)) (p : Q(¬$rhs ≤ $lhs)) := pure q(PNat.le_sub_one_of_not_le $p)
  mkNumeral
    | Nat.succ i => pure q(OfNat.ofNat (Nat.succ $i) : ℕ+)
    | _ => failure

[Jireh Loreaux]

@Mario Carneiro if you give me a hint about how to include PNat handling in norm_num I would be happy to give it a shot.

[Mario Carneiro]

it can't be done, at least not until pnat has numerals

[Jireh Loreaux]

Sorry, what do you mean by "numerals"? We have docs4#instOfNatPNatHAddNatInstHAddInstAddNatOfNat

[Mario Carneiro]

I see. Even then it is quite hard because pnat doesn't have an AddMonoidWithOne instance, which is required for norm_num

[Mario Carneiro]

the best alternative I can think of is to have norm_num extensions for things like PNat.val (a + b)

[Jireh Loreaux]

So for interval_cases we'll need to do something more like mathlib 3 then? I didn't see any special handling of nat, int or pnat there.

[Mario Carneiro]

interval_cases was completely rewritten for lean 4

[Mario Carneiro]

The old implementation is not good at all, it used #reduce instead of norm_num

[Kevin Buzzard]

The lean 3 version was super slow (and presumably this is why)

[Gareth Ma]

Hey, so is interval_cases way faster on lean 4?

[Mario Carneiro]

yes