evalNatGCD — Mathlib

Lean4
/-- Extension for `Nat.gcd`.
Uses positivity of the left term, if available, then tries the right term.

The implementation relies on the fact that `Positivity.core` on `ℕ` never returns `nonzero`. -/
@[positivity Nat.gcd _ _]
def evalNatGCD : PositivityExt where
  eval {u α} z p
    e := do
    match u, α, e with
    | 0, ~q(ℕ), ~q(Nat.gcd $a $b) =>
      assertInstancesCommute
      match ← core z p a with
      | .positive pa =>
        return .positive q(Nat.gcd_pos_of_pos_left $b $pa)
      | _ =>
        match ← core z p b with
        | .positive pb =>
          return .positive q(Nat.gcd_pos_of_pos_right $a $pb)
        | _ =>
          failure
    | _, _, _ =>
      throwError"not Nat.gcd"
Похожие утверждения