evalIntGCD — Mathlib

Lean4
/-- Extension for `Int.gcd`.
Uses positivity of the left term, if available, then tries the right term. -/
@[positivity Int.gcd _ _]
def evalIntGCD : PositivityExt where
  eval {u α} _ _
    e := do
    match u, α, e with
    | 0, ~q(ℕ), ~q(Int.gcd $a $b) =>
      let z ← synthInstanceQ (q(Zero ℤ) : Q(Type))
      let p ← synthInstanceQ (q(PartialOrder ℤ) : Q(Type))
      assertInstancesCommute
      match (← catchNone (core z p a)).toNonzero with
      | some na =>
        return .positive q(Int.gcd_pos_of_ne_zero_left $b $na)
      | none =>
        match (← core z p b).toNonzero with
        | some nb =>
          return .positive q(Int.gcd_pos_of_ne_zero_right $a $nb)
        | none =>
          failure
    | _, _, _ =>
      throwError"not Int.gcd"
Похожие утверждения