PNat が入っている式も示せる omega の派生タクティク

Zulip: > Omega with PNat

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

The issue's entry points are the PNat lemmas and the omega_preprocess_pnat and omega_pnat tactic definitions shown in the body. Read those definitions and the imported Mathlib.Data.PNat.Basic behavior first. Done means the example deriving 1 < b from a < b works with the demonstrated tactic.