Omega with PNat

Stream: mathlib4

[Vasilii Nesterov]

Hi! I've written a simple wrapper around omega that can solve goals involving PNats:

import Mathlib.Data.PNat.Basic

lemma PNat.sub_coe' (a b : PNat) : ((a - b : PNat) : Nat) = a.val - 1 - b.val + 1 := by
  cases a
  cases b
  simp only [PNat.mk_coe, PNat.sub_coe, ← PNat.coe_lt_coe]
  split_ifs <;> omega

open Qq in
elab "omega_preprocess_pnat" : tactic =>
  Lean.Elab.Tactic.withMainContext do
    let goal ← Lean.Elab.Tactic.getMainGoal
    let ctx ← Lean.MonadLCtx.getLCtx
    let result : Lean.MVarId ← ctx.foldlM (init := goal) fun g decl => do
      let declExpr := decl.toExpr
      let declType ← Lean.Meta.inferType declExpr
      let isPNat ← Lean.Meta.isExprDefEq declType q(PNat)
      if isPNat then
        let p : Lean.Expr := Lean.Expr.app q(PNat.pos) declExpr
        let mvarIdNew ← g.define .anonymous (← Lean.Meta.inferType p) p
        let (_, mvarIdNew) ← mvarIdNew.intro1P
        return mvarIdNew
      else
        return g
    Lean.Elab.Tactic.setGoals [result]

syntax "omega_pnat" : tactic

macro_rules
| `(tactic| omega_pnat) => `(tactic|
  omega_preprocess_pnat;
  simp only [← PNat.coe_inj, ← PNat.coe_le_coe, ← PNat.coe_lt_coe, PNat.sub_coe', PNat.add_coe, PNat.mul_coe, PNat.val_ofNat] at *;
  omega
)

example (a b : PNat) (h : a < b) : 1 < b := by
  omega_pnat

Would it be worth PRing it in some form?

[Vasilii Nesterov]

It just translates PNat arithmetic (+, -, *) into Nat.

[Kevin Buzzard]

Definitely! I don't see any harm in a tactic with a niche but genuine use case.

Is another perhaps more useful approch to write a nify tactic, which takes goals or hypotheses involving pnats and changes them into equivalent goals involving nats? We have zify, qify etc, so that would fit into the general mathlib pattern. And then maybe nify; omega would be the way to solve many pnat goals.

[Kim Morrison]

Yes, both routes are great.

[Junyan Xu]

Maybe something similar can be done for docs#ENat, WithBot Nat (docs#Polynomial.degree), WithBot ENat (docs#Order.krullDim) ...

[Vasilii Nesterov]

Yes, I am working on this.

[Vasilii Nesterov]

The PR for ENat and PNat is ready: #21602

[Kim Morrison]

@Vasily Nesterov, would it be possible to refactor this to provide a enat_to_nat tactic (cases, simplify inequalities, translate), and then enat_omega is just enat_to_nat; omega? I think there would also be independent uses for enat_to_nat.

[Kim Morrison]

(Similarly for pnat.)

[Vasilii Nesterov]

How about pnat_to_nat x y z syntax for a tactic that translates variables x, y, z from the context from PNat to Nat and pushes the translation as far as possible?

[Vasilii Nesterov]

And similar tactic for ENat (in which case multiple goals might be created).

[Kevin Buzzard]

zify, qify and rify don't use this approach and people don't seem to be complaining that they want this fine-grained control.

[Kim Morrison]

I'd be content with one that just aggressively translates all relevant hypotheses. I think an optional at x y z syntax can't hurt if you want to implement it.