Lean4
/-- The `norm_num` extension which identifies expressions of the form `(a : ℕ) | b`,
such that `norm_num` successfully recognises both `a` and `b`. -/
@[norm_num (_ : ℕ) ∣ _]
def evalNatDvd : NormNumExt where
eval {u α}
e := do
let .app (.app f (a : Q(ℕ))) (b : Q(ℕ)) ← whnfR e |
failure
guard <| ← withNewMCtxDepth <| isDefEq f q(Dvd.dvd (α := ℕ))
let sℕ : Q(AddMonoidWithOne ℕ) := q(instAddMonoidWithOneNat)
let ⟨na, pa⟩ ← deriveNat a sℕ;
let ⟨nb, pb⟩ ← deriveNat b sℕ
match nb.natLit! % na.natLit! with
| 0 =>
have : Q(Nat.mod $nb $na = nat_lit 0) := (q(Eq.refl (nat_lit 0)) : Expr)
return .isTrue q(isNat_dvd_true $pa $pb $this)
| c + 1 =>
have nc : Q(ℕ) := mkRawNatLit c
have : Q(Nat.mod $nb $na = Nat.succ $nc) := (q(Eq.refl (Nat.succ $nc)) : Expr)
return .isFalse q(isNat_dvd_false $pa $pb $this)
