Mathlib.Tactic.NormNum.Result

Mathlib.Meta.NormNum.instAddMonoidWithOneNat definition

: AddMonoidWithOne ℕ

Full source

/-- A shortcut (non)instance for `AddMonoidWithOne ℕ` to shrink generated proofs. -/
def instAddMonoidWithOneNat : AddMonoidWithOne ℕ := inferInstance

Natural numbers as an additive monoid with one

Informal description

The natural numbers `ℕ` form an additive monoid with one, where the additive structure includes a zero element and a successor operation, and the multiplicative structure includes a multiplicative identity. This instance is used to simplify generated proofs in the `norm_num` tactic.

Mathlib.Meta.NormNum.instAddMonoidWithOne definition

{α : Type u} [Ring α] : AddMonoidWithOne α

Full source

/-- A shortcut (non)instance for `AddMonoidWithOne α` from `Ring α` to shrink generated proofs. -/
def instAddMonoidWithOne {α : Type u} [Ring α] : AddMonoidWithOne α := inferInstance

Additive monoid with one structure for a ring

Informal description

Given a ring $\alpha$, the structure `AddMonoidWithOne` is automatically inferred for $\alpha$, providing the additive monoid structure with a one element.

Mathlib.Meta.NormNum.inferAddMonoidWithOne definition

(α : Q(Type u)) : MetaM Q(AddMonoidWithOne $α)

Full source

/-- Helper function to synthesize a typed `AddMonoidWithOne α` expression. -/
def inferAddMonoidWithOne (α : Q(Type u)) : MetaM Q(AddMonoidWithOne $α) :=
  return ← synthInstanceQ q(AddMonoidWithOne $α) <|>
    throwError "not an AddMonoidWithOne"

Synthesis of additive monoid with one structure

Informal description

The function `inferAddMonoidWithOne` takes a type `α` and attempts to synthesize an instance of `AddMonoidWithOne α`. If it fails to find such an instance, it throws an error indicating that `α` is not an additive monoid with one.

Mathlib.Meta.NormNum.inferSemiring definition

(α : Q(Type u)) : MetaM Q(Semiring $α)

Full source

/-- Helper function to synthesize a typed `Semiring α` expression. -/
def inferSemiring (α : Q(Type u)) : MetaM Q(Semiring $α) :=
  return ← synthInstanceQ q(Semiring $α) <|> throwError "not a semiring"

Semiring instance synthesis for `norm_num`

Informal description

Given a type `α`, the function attempts to synthesize a proof that `α` is a semiring. If successful, it returns the proof; otherwise, it throws an error indicating that `α` is not a semiring.

Mathlib.Meta.NormNum.inferRing definition

(α : Q(Type u)) : MetaM Q(Ring $α)

Full source

/-- Helper function to synthesize a typed `Ring α` expression. -/
def inferRing (α : Q(Type u)) : MetaM Q(Ring $α) :=
  return ← synthInstanceQ q(Ring $α) <|> throwError "not a ring"

Ring instance synthesizer

Informal description

The function `inferRing` takes a type `α` and attempts to synthesize a proof that `α` is a ring, or throws an error if it fails to do so.

Mathlib.Meta.NormNum.mkRawIntLit definition

(n : ℤ) : Q(ℤ)

Full source

/--
Represent an integer as a "raw" typed expression.

This uses `.lit (.natVal n)` internally to represent a natural number,
rather than the preferred `OfNat.ofNat` form.
We use this internally to avoid unnecessary typeclass searches.

This function is the inverse of `Expr.intLit!`.
-/
def mkRawIntLit (n : ℤ) : Q(ℤ) :=
  let lit : Q(ℕ) := mkRawNatLit n.natAbs
  if 0 ≤ n then q(.ofNat $lit) else q(.negOfNat $lit)

Raw integer literal construction

Informal description

The function constructs a typed expression representing an integer `n` in its "raw" form, using `.lit (.natVal n)` internally to represent natural numbers. For non-negative integers, it uses `OfNat.ofNat`, and for negative integers, it uses `.negOfNat`. This avoids unnecessary typeclass searches and is the inverse operation of `Expr.intLit!`.

Mathlib.Meta.NormNum.mkRawRatLit definition

(q : ℚ) : Q(ℚ)

Full source

/--
Represent an integer as a "raw" typed expression.

This `.lit (.natVal n)` internally to represent a natural number,
rather than the preferred `OfNat.ofNat` form.
We use this internally to avoid unnecessary typeclass searches.
-/
def mkRawRatLit (q : ℚ) : Q(ℚ) :=
  let nlit : Q(ℤ) := mkRawIntLit q.num
  let dlit : Q(ℕ) := mkRawNatLit q.den
  q(mkRat $nlit $dlit)

Raw rational literal construction

Informal description

The function constructs a typed expression representing a rational number `q` in its "raw" form, using `mkRawIntLit` for the numerator and `mkRawNatLit` for the denominator, and then combines them with `mkRat`.

Mathlib.Meta.NormNum.rawIntLitNatAbs definition

(n : Q(ℤ)) : (m : Q(ℕ)) × Q(Int.natAbs $n = $m)

Full source

/-- Extract the raw natlit representing the absolute value of a raw integer literal
(of the type produced by `Mathlib.Meta.NormNum.mkRawIntLit`) along with an equality proof. -/
def rawIntLitNatAbs (n : Q(ℤ)) : (m : Q(ℕ)) × Q(Int.natAbs $n = $m) :=
  if n.isAppOfArity ``Int.ofNat 1 then
    have m : Q(ℕ) := n.appArg!
    ⟨m, show Q(Int.natAbs (Int.ofNat $m) = $m) from q(Int.natAbs_natCast $m)⟩
  else if n.isAppOfArity ``Int.negOfNat 1 then
    have m : Q(ℕ) := n.appArg!
    ⟨m, show Q(Int.natAbs (Int.negOfNat $m) = $m) from q(Int.natAbs_neg $m)⟩
  else
    panic! "not a raw integer literal"

Extraction of natural absolute value from raw integer literal with proof

Informal description

Given a raw integer literal expression `n` of type `ℤ`, this function extracts the natural number literal `m` representing the absolute value of `n`, along with a proof that the absolute value of `n` is equal to `m`. The function handles both positive integers (constructed with `Int.ofNat`) and negative integers (constructed with `Int.negOfNat`), and panics if the input is not a raw integer literal.

Mathlib.Meta.NormNum.mkOfNat definition

(α : Q(Type u)) (_sα : Q(AddMonoidWithOne $α)) (lit : Q(ℕ)) :
    MetaM ((a' : Q($α)) × Q($lit = $a'))

Full source

/--
Constructs an `ofNat` application `a'` with the canonical instance, together with a proof that
the instance is equal to the result of `Nat.cast` on the given `AddMonoidWithOne` instance.

This function is performance-critical, as many higher level tactics have to construct numerals.
So rather than using typeclass search we hardcode the (relatively small) set of solutions
to the typeclass problem.
-/
def mkOfNat (α : Q(Type u)) (_sα : Q(AddMonoidWithOne $α)) (lit : Q(ℕ)) :
    MetaM ((a' : Q($α)) × Q($lit = $a')) := do
  if α.isConstOf ``Nat then
    let a' : Q(ℕ) := q(OfNat.ofNat $lit : ℕ)
    pure ⟨a', (q(Eq.refl $a') : Expr)⟩
  else if α.isConstOf ``Int then
    let a' : Q(ℤ) := q(OfNat.ofNat $lit : ℤ)
    pure ⟨a', (q(Eq.refl $a') : Expr)⟩
  else if α.isConstOf ``Rat then
    let a' : Q(ℚ) := q(OfNat.ofNat $lit : ℚ)
    pure ⟨a', (q(Eq.refl $a') : Expr)⟩
  else
    let some n := lit.rawNatLit? | failure
    match n with
    | 0 => pure ⟨q(0 : $α), (q(Nat.cast_zero (R := $α)) : Expr)⟩
    | 1 => pure ⟨q(1 : $α), (q(Nat.cast_one (R := $α)) : Expr)⟩
    | k+2 =>
      let k : Q(ℕ) := mkRawNatLit k
      let _x : Q(Nat.AtLeastTwo $lit) :=
        (q(instNatAtLeastTwo (n := $k)) : Expr)
      let a' : Q($α) := q(OfNat.ofNat $lit)
      pure ⟨a', (q(Eq.refl $a') : Expr)⟩

Construction of `ofNat` with equality proof

Informal description

Given a type `α` with an `AddMonoidWithOne` instance and a natural number literal `lit`, this function constructs an `ofNat` application `a'` of type `α` along with a proof that `lit` is equal to `a'`. The function handles special cases for `Nat`, `Int`, and `Rat` directly for performance reasons, and falls back to general `Nat.cast` for other types.

Mathlib.Meta.NormNum.IsNat structure

{α : Type u} [AddMonoidWithOne α] (a : α) (n : ℕ)

Full source

/-- Assert that an element of a semiring is equal to the coercion of some natural number. -/
structure IsNat {α : Type u} [AddMonoidWithOne α] (a : α) (n : ℕ) : Prop where
  /-- The element is equal to the coercion of the natural number. -/
  out : a = n

Natural number coercion equality in a semiring

Informal description

The structure `IsNat` asserts that an element `a` of a semiring `α` (with an additive monoid structure and a one) is equal to the canonical image of a natural number `n` in `α`. In other words, it provides a proof that `a = n` where `n` is considered as an element of `α` via the natural coercion.

Mathlib.Meta.NormNum.IsNat.raw_refl theorem

(n : ℕ) : IsNat n n

Full source

theorem IsNat.raw_refl (n : ℕ) : IsNat n n := ⟨rfl⟩

Reflexivity of Natural Number Coercion: $\text{IsNat}(n, n)$

Informal description

For any natural number $n$, the `IsNat` predicate holds for $n$ itself, i.e., $n$ is equal to its own canonical image in any semiring $\alpha$ with an additive monoid structure and a one element.

Nat.rawCast definition

{α : Type u} [AddMonoidWithOne α] (n : ℕ) : α

Full source

/--
A "raw nat cast" is an expression of the form `(Nat.rawCast lit : α)` where `lit` is a raw
natural number literal. These expressions are used by tactics like `ring` to decrease the number
of typeclass arguments required in each use of a number literal at type `α`.
-/
@[simp] def _root_.Nat.rawCast {α : Type u} [AddMonoidWithOne α] (n : ℕ) : α := n

Raw natural number cast

Informal description

Given a type $\alpha$ with an additive monoid structure that includes a one element, the function `Nat.rawCast` maps a natural number $n$ to its representation in $\alpha$ as `(Nat.rawCast n : α)`. This is used to reduce the number of typeclass arguments needed when working with number literals in $\alpha$.

Mathlib.Meta.NormNum.IsNat.to_eq theorem

{α : Type u} [AddMonoidWithOne α] {n} : {a a' : α} → IsNat a n → n = a' → a = a'

Full source

theorem IsNat.to_eq {α : Type u} [AddMonoidWithOne α] {n} : {a a' : α} → IsNat a n → n = a' → a = a'
  | _, _, ⟨rfl⟩, rfl => rfl

Equality Transfer via Natural Number Coercion

Informal description

Let $\alpha$ be a type with an additive monoid structure and a one element. For any elements $a, a' \in \alpha$ and natural number $n$, if $a$ is equal to the canonical image of $n$ in $\alpha$ (i.e., $\text{IsNat}(a, n)$ holds) and $n = a'$, then $a = a'$.

Mathlib.Meta.NormNum.IsNat.to_raw_eq theorem

{a : α} {n : ℕ} [AddMonoidWithOne α] : IsNat (a : α) n → a = n.rawCast

Full source

theorem IsNat.to_raw_eq {a : α} {n : ℕ} [AddMonoidWithOne α] : IsNat (a : α) n → a = n.rawCast
  | ⟨e⟩ => e

Equality of Natural Number Coercion to Raw Cast

Informal description

For any element $a$ in an additive monoid with one $\alpha$ and any natural number $n$, if $a$ is equal to the canonical image of $n$ in $\alpha$ (i.e., `IsNat a n` holds), then $a$ is equal to the raw cast of $n$ in $\alpha$ (i.e., $a = \text{Nat.rawCast}\,n$).

Mathlib.Meta.NormNum.IsNat.of_raw theorem

(α) [AddMonoidWithOne α] (n : ℕ) : IsNat (n.rawCast : α) n

Full source

theorem IsNat.of_raw (α) [AddMonoidWithOne α] (n : ℕ) : IsNat (n.rawCast : α) n := ⟨rfl⟩

Raw Cast Satisfies Natural Number Coercion

Informal description

For any type $\alpha$ with an additive monoid structure that includes a one element, and for any natural number $n$, the raw cast of $n$ in $\alpha$ satisfies the `IsNat` predicate, i.e., $\text{IsNat}(n.\text{rawCast}, n)$ holds.

Mathlib.Meta.NormNum.isNat.natElim theorem

{p : ℕ → Prop} : {n : ℕ} → {n' : ℕ} → IsNat n n' → p n' → p n

Full source

@[elab_as_elim]
theorem isNat.natElim {p : ℕ → Prop} : {n : ℕ} → {n' : ℕ} → IsNat n n' → p n' → p n
  | _, _, ⟨rfl⟩, h => h

Natural Number Coercion Predicate Elimination

Informal description

For any predicate $p$ on natural numbers and any natural numbers $n$ and $n'$, if `IsNat n n'` holds (meaning $n$ is equal to the canonical image of $n'$ in some semiring), then $p(n')$ implies $p(n)$.

Mathlib.Meta.NormNum.IsInt structure

[Ring α] (a : α) (n : ℤ)

Full source

/-- Assert that an element of a ring is equal to the coercion of some integer. -/
structure IsInt [Ring α] (a : α) (n : ℤ) : Prop where
  /-- The element is equal to the coercion of the integer. -/
  out : a = n

Integer coercion equality in a ring

Informal description

The structure `IsInt a n` asserts that an element `a` of a ring `α` is equal to the image of an integer `n` under the canonical map from the integers to `α`.

Int.rawCast definition

[Ring α] (n : ℤ) : α

Full source

/--
A "raw int cast" is an expression of the form:

* `(Nat.rawCast lit : α)` where `lit` is a raw natural number literal
* `(Int.rawCast (Int.negOfNat lit) : α)` where `lit` is a nonzero raw natural number literal

(That is, we only actually use this function for negative integers.) This representation is used by
tactics like `ring` to decrease the number of typeclass arguments required in each use of a number
literal at type `α`.
-/
@[simp] def _root_.Int.rawCast [Ring α] (n : ℤ) : α := n

Raw integer cast in a ring

Informal description

The function `Int.rawCast` takes an integer `n` and returns its representation in a ring `α`. Specifically: - If `n` is a natural number literal, it returns `(Nat.rawCast lit : α)` - If `n` is a negative integer (represented as `Int.negOfNat lit` where `lit` is a nonzero natural number literal), it returns `(Int.rawCast (Int.negOfNat lit) : α)` This representation is primarily used for negative integers to reduce the number of required typeclass arguments when working with number literals in ring `α`.

Mathlib.Meta.NormNum.IsInt.to_isNat theorem

{α} [Ring α] : ∀ {a : α} {n}, IsInt a (.ofNat n) → IsNat a n

Full source

theorem IsInt.to_isNat {α} [Ring α] : ∀ {a : α} {n}, IsInt a (.ofNat n) → IsNat a n
  | _, _, ⟨rfl⟩ => ⟨by simp⟩

Non-negative integer image implies natural number image in a ring

Informal description

Let $\alpha$ be a ring and let $a \in \alpha$. If $a$ is equal to the canonical image of the non-negative integer $\text{ofNat}\, n$ in $\alpha$ (i.e., $\text{IsInt}\, a\, (\text{ofNat}\, n)$ holds), then $a$ is also equal to the canonical image of the natural number $n$ in $\alpha$ (i.e., $\text{IsNat}\, a\, n$ holds).

Mathlib.Meta.NormNum.IsNat.to_isInt theorem

{α} [Ring α] : ∀ {a : α} {n}, IsNat a n → IsInt a (.ofNat n)

Full source

theorem IsNat.to_isInt {α} [Ring α] : ∀ {a : α} {n}, IsNat a n → IsInt a (.ofNat n)
  | _, _, ⟨rfl⟩ => ⟨by simp⟩

Natural Number Image Implies Integer Image in a Ring

Informal description

Let $\alpha$ be a ring and let $a \in \alpha$. If $a$ is equal to the canonical image of a natural number $n$ in $\alpha$ (i.e., $\text{IsNat}\, a\, n$ holds), then $a$ is also equal to the canonical image of the integer $\text{ofNat}\, n$ in $\alpha$ (i.e., $\text{IsInt}\, a\, (\text{ofNat}\, n)$ holds).

Mathlib.Meta.NormNum.IsInt.to_raw_eq theorem

{a : α} {n : ℤ} [Ring α] : IsInt (a : α) n → a = n.rawCast

Full source

theorem IsInt.to_raw_eq {a : α} {n : ℤ} [Ring α] : IsInt (a : α) n → a = n.rawCast
  | ⟨e⟩ => e

Equality of Integer Image and Raw Cast in a Ring

Informal description

Let $\alpha$ be a ring and let $a \in \alpha$. If $a$ is equal to the image of an integer $n$ under the canonical map from $\mathbb{Z}$ to $\alpha$ (i.e., $\text{IsInt}\, a\, n$ holds), then $a$ is equal to the raw cast of $n$ in $\alpha$ (i.e., $a = n.\text{rawCast}$).

Mathlib.Meta.NormNum.IsInt.of_raw theorem

(α) [Ring α] (n : ℤ) : IsInt (n.rawCast : α) n

Full source

theorem IsInt.of_raw (α) [Ring α] (n : ℤ) : IsInt (n.rawCast : α) n := ⟨rfl⟩

Raw Cast Yields Canonical Integer Image in a Ring

Informal description

For any ring $\alpha$ and any integer $n$, the raw cast of $n$ in $\alpha$ is equal to the canonical image of $n$ in $\alpha$, i.e., $\text{IsInt}\, (n.\text{rawCast})\, n$ holds.

Mathlib.Meta.NormNum.IsInt.neg_to_eq theorem

{α} [Ring α] {n} : {a a' : α} → IsInt a (.negOfNat n) → n = a' → a = -a'

Full source

theorem IsInt.neg_to_eq {α} [Ring α] {n} :
    {a a' : α} → IsInt a (.negOfNat n) → n = a' → a = -a'
  | _, _, ⟨rfl⟩, rfl => by simp [Int.negOfNat_eq, Int.cast_neg]

Negation of Integer Coercion in a Ring

Informal description

Let $\alpha$ be a ring, and let $a, a' \in \alpha$. If there exists an integer $n$ such that $a$ is equal to the image of $-n$ under the canonical map from the integers to $\alpha$, and $n = a'$, then $a = -a'$.

Mathlib.Meta.NormNum.IsInt.nonneg_to_eq theorem

{α} [Ring α] {n} {a a' : α} (h : IsInt a (.ofNat n)) (e : n = a') : a = a'

Full source

theorem IsInt.nonneg_to_eq {α} [Ring α] {n}
    {a a' : α} (h : IsInt a (.ofNat n)) (e : n = a') : a = a' := h.to_isNat.to_eq e

Equality of Ring Element and Non-Negative Integer Image

Informal description

Let $\alpha$ be a ring, and let $a, a' \in \alpha$. If $a$ is equal to the canonical image of the non-negative integer $n$ in $\alpha$ (i.e., $\text{IsInt}\, a\, (\text{ofNat}\, n)$ holds) and $n = a'$, then $a = a'$.

Mathlib.Meta.NormNum.IsRat inductive

[Ring α] (a : α) (num : ℤ) (denom : ℕ) : Prop

Full source

/--
Assert that an element of a ring is equal to `num / denom`
(and `denom` is invertible so that this makes sense).
We will usually also have `num` and `denom` coprime,
although this is not part of the definition.
-/
inductive IsRat [Ring α] (a : α) (num : ℤ) (denom : ℕ) : Prop
  | mk (inv : Invertible (denom : α)) (eq : a = num * ⅟(denom : α))

Rational number representation in a ring

Informal description

The predicate `IsRat a num denom` asserts that an element `a` of a ring `α` is equal to the fraction `num / denom`, where `num` is an integer and `denom` is a natural number. This makes sense because `denom` is assumed to be invertible in the ring. Typically, `num` and `denom` are also coprime, although this condition is not part of the formal definition.

Rat.rawCast definition

[DivisionRing α] (n : ℤ) (d : ℕ) : α

Full source

/--
A "raw rat cast" is an expression of the form:

* `(Nat.rawCast lit : α)` where `lit` is a raw natural number literal
* `(Int.rawCast (Int.negOfNat lit) : α)` where `lit` is a nonzero raw natural number literal
* `(Rat.rawCast n d : α)` where `n` is a raw int literal, `d` is a raw nat literal, and `d` is not
  `1` or `0`.

(where a raw int literal is of the form `Int.ofNat lit` or `Int.negOfNat nzlit` where `lit` is a raw
nat literal)

This representation is used by tactics like `ring` to decrease the number of typeclass arguments
required in each use of a number literal at type `α`.
-/
@[simp]
def _root_.Rat.rawCast [DivisionRing α] (n : ℤ) (d : ℕ) : α := n / d

Raw rational number cast

Informal description

The function `Rat.rawCast` takes an integer `n` and a natural number `d`, and returns the element `n / d` in a division ring `α`. This represents a raw rational number cast into the division ring `α`.

Mathlib.Meta.NormNum.IsRat.to_isNat theorem

{α} [Ring α] : ∀ {a : α} {n}, IsRat a (.ofNat n) (nat_lit 1) → IsNat a n

Full source

theorem IsRat.to_isNat {α} [Ring α] : ∀ {a : α} {n}, IsRat a (.ofNat n) (nat_lit 1) → IsNat a n
  | _, _, ⟨inv, rfl⟩ => have := @invertibleOne α _; ⟨by simp⟩

Conversion from rational to natural number equality in a ring

Informal description

Let $\alpha$ be a ring. For any element $a \in \alpha$ and natural number $n$, if $a$ is equal to the rational number $\text{ofNat}(n)/1$ (i.e., $a = n$ as a rational number), then $a$ is equal to the natural number $n$ in $\alpha$.

Mathlib.Meta.NormNum.IsNat.to_isRat theorem

{α} [Ring α] : ∀ {a : α} {n}, IsNat a n → IsRat a (.ofNat n) (nat_lit 1)

Full source

theorem IsNat.to_isRat {α} [Ring α] : ∀ {a : α} {n}, IsNat a n → IsRat a (.ofNat n) (nat_lit 1)
  | _, _, ⟨rfl⟩ => ⟨⟨1, by simp, by simp⟩, by simp⟩

Natural number equality implies rational equality with denominator one in a ring

Informal description

Let $\alpha$ be a ring. For any element $a \in \alpha$ and natural number $n$, if $a$ is equal to the natural number $n$ in $\alpha$ (i.e., $\text{IsNat}(a, n)$ holds), then $a$ is also equal to the rational number $\frac{n}{1}$ in $\alpha$ (i.e., $\text{IsRat}(a, n, 1)$ holds).

Mathlib.Meta.NormNum.IsRat.to_isInt theorem

{α} [Ring α] : ∀ {a : α} {n}, IsRat a n (nat_lit 1) → IsInt a n

Full source

theorem IsRat.to_isInt {α} [Ring α] : ∀ {a : α} {n}, IsRat a n (nat_lit 1) → IsInt a n
  | _, _, ⟨inv, rfl⟩ => have := @invertibleOne α _; ⟨by simp⟩

Rational with Denominator One Implies Integer Representation in a Ring

Informal description

For any ring $\alpha$, if an element $a \in \alpha$ is equal to the rational number $\frac{n}{1}$ (where $n$ is an integer), then $a$ is equal to the image of $n$ under the canonical map from $\mathbb{Z}$ to $\alpha$.

Mathlib.Meta.NormNum.IsInt.to_isRat theorem

{α} [Ring α] : ∀ {a : α} {n}, IsInt a n → IsRat a n (nat_lit 1)

Full source

theorem IsInt.to_isRat {α} [Ring α] : ∀ {a : α} {n}, IsInt a n → IsRat a n (nat_lit 1)
  | _, _, ⟨rfl⟩ => ⟨⟨1, by simp, by simp⟩, by simp⟩

Integer Representation Implies Rational Representation with Denominator One

Informal description

For any ring $\alpha$, if an element $a \in \alpha$ is equal to the image of an integer $n$ under the canonical map from $\mathbb{Z}$ to $\alpha$ (i.e., $\text{IsInt}(a, n)$ holds), then $a$ is also equal to the rational number $\frac{n}{1}$ in $\alpha$ (i.e., $\text{IsRat}(a, n, 1)$ holds).

Mathlib.Meta.NormNum.IsRat.to_raw_eq theorem

{n : ℤ} {d : ℕ} [DivisionRing α] : ∀ {a}, IsRat (a : α) n d → a = Rat.rawCast n d

Full source

theorem IsRat.to_raw_eq {n : ℤ} {d : ℕ} [DivisionRing α] :
    ∀ {a}, IsRat (a : α) n d → a = Rat.rawCast n d
  | _, ⟨inv, rfl⟩ => by simp [div_eq_mul_inv]

Equality of Rational Representation to Raw Cast: $\text{IsRat}(a, n, d) \Rightarrow a = n/d$

Informal description

For any division ring $\alpha$, integer $n$, and natural number $d$, if an element $a \in \alpha$ satisfies the predicate $\text{IsRat}(a, n, d)$, then $a$ is equal to the raw rational cast $\text{Rat.rawCast}(n, d) = n / d$.

Mathlib.Meta.NormNum.IsRat.neg_to_eq theorem

{α} [DivisionRing α] {n d} : {a n' d' : α} → IsRat a (.negOfNat n) d → n = n' → d = d' → a = -(n' / d')

Full source

theorem IsRat.neg_to_eq {α} [DivisionRing α] {n d} :
    {a n' d' : α} → IsRat a (.negOfNat n) d → n = n' → d = d' → a = -(n' / d')
  | _, _, _, ⟨_, rfl⟩, rfl, rfl => by simp [div_eq_mul_inv]

Negation of Rational Representation in Division Ring

Informal description

Let $\alpha$ be a division ring. For any elements $a, n', d' \in \alpha$ and integers $n, d$, if $a$ is equal to the rational number $-\frac{n}{d}$ (represented as `IsRat a (.negOfNat n) d`), and if $n = n'$ and $d = d'$, then $a = -\left(\frac{n'}{d'}\right)$.

Mathlib.Meta.NormNum.IsRat.nonneg_to_eq theorem

{α} [DivisionRing α] {n d} : {a n' d' : α} → IsRat a (.ofNat n) d → n = n' → d = d' → a = n' / d'

Full source

theorem IsRat.nonneg_to_eq {α} [DivisionRing α] {n d} :
    {a n' d' : α} → IsRat a (.ofNat n) d → n = n' → d = d' → a = n' / d'
  | _, _, _, ⟨_, rfl⟩, rfl, rfl => by simp [div_eq_mul_inv]

Equality of Non-negative Rational Representation in Division Ring

Informal description

Let $\alpha$ be a division ring. For any elements $a, n', d' \in \alpha$ and natural number $n$ and $d$, if `IsRat a (.ofNat n) d` holds (meaning $a$ is equal to the rational number formed by $n/d$), and if $n = n'$ and $d = d'$, then $a = n'/d'$.

Mathlib.Meta.NormNum.IsRat.of_raw theorem

(α) [DivisionRing α] (n : ℤ) (d : ℕ) (h : (d : α) ≠ 0) : IsRat (Rat.rawCast n d : α) n d

Full source

theorem IsRat.of_raw (α) [DivisionRing α] (n : ℤ) (d : ℕ)
    (h : (d : α) ≠ 0) : IsRat (Rat.rawCast n d : α) n d :=
  have := invertibleOfNonzero h
  ⟨this, by simp [div_eq_mul_inv]⟩

Rational Representation of Raw Cast in Division Ring

Informal description

Let $\alpha$ be a division ring. For any integer $n$ and natural number $d$ such that the image of $d$ in $\alpha$ is nonzero (i.e., $(d : \alpha) \neq 0$), the element $\text{Rat.rawCast}(n, d) \in \alpha$ satisfies the predicate $\text{IsRat}(\text{Rat.rawCast}(n, d), n, d)$, meaning it is equal to the fraction $n/d$ in $\alpha$.

Mathlib.Meta.NormNum.IsRat.den_nz theorem

{α} [DivisionRing α] {a n d} : IsRat (a : α) n d → (d : α) ≠ 0

Full source

theorem IsRat.den_nz {α} [DivisionRing α] {a n d} : IsRat (a : α) n d → (d : α) ≠ 0
  | ⟨_, _⟩ => Invertible.ne_zero (d : α)

Nonzero Denominator in Rational Representation over Division Ring

Informal description

For any division ring $\alpha$, if an element $a \in \alpha$ satisfies the predicate $\text{IsRat}(a, n, d)$ (i.e., $a = n / d$ where $n \in \mathbb{Z}$ and $d \in \mathbb{N}$), then the denominator $d$ is nonzero in $\alpha$, i.e., $d \neq 0$.

Mathlib.Meta.NormNum.Result' inductive

Full source

/-- The result of `norm_num` running on an expression `x` of type `α`.
Untyped version of `Result`. -/
inductive Result' where
  /-- Untyped version of `Result.isBool`. -/
  | isBool (val : Bool) (proof : Expr)
  /-- Untyped version of `Result.isNat`. -/
  | isNat (inst lit proof : Expr)
  /-- Untyped version of `Result.isNegNat`. -/
  | isNegNat (inst lit proof : Expr)
  /-- Untyped version of `Result.isRat`. -/
  | isRat (inst : Expr) (q : Rat) (n d proof : Expr)
  deriving Inhabited

Untyped normalization result for `norm_num`

Informal description

The `Result'` type represents the possible outcomes of the `norm_num` procedure when applied to an expression of type `α`. It can be one of the following: - A proof that the expression is equal to the coercion of a natural number, integer, or rational number into `α`. - A proof that the expression is equal to the boolean values `true` or `false`. This is an untyped version of the `Result` type used in the `norm_num` procedure.

Mathlib.Meta.NormNum.instInhabitedResult' instance

: Inhabited✝ (@Mathlib.Meta.NormNum.Result')

Full source

Inhabited

Inhabited Type for Untyped Normalization Results

Informal description

The type `Result'` used in the `norm_num` procedure is inhabited, meaning there always exists a default value of this type.

Mathlib.Meta.NormNum.Result definition

{α : Q(Type u)} (x : Q($α))

Full source

/-- The result of `norm_num` running on an expression `x` of type `α`. -/
@[nolint unusedArguments] def Result {α : Q(Type u)} (x : Q($α)) := Result'

Normalization result for `norm_num`

Informal description

The `Result` type represents the possible outcomes of the `norm_num` procedure when applied to an expression `x` of type `α`. It contains a proof that `x` is equal to one of the following: - The canonical embedding of a natural number, integer, or rational number into `α$ - The boolean values `true` or `false$

Mathlib.Meta.NormNum.instInhabitedResult instance

{α : Q(Type u)} {x : Q($α)} : Inhabited (Result x)

Full source

instance {α : Q(Type u)} {x : Q($α)} : Inhabited (Result x) := inferInstanceAs (Inhabited Result')

Inhabited Type for Normalization Results

Informal description

For any type $\alpha$ and expression $x$ of type $\alpha$, the type `Result x` representing normalization results in the `norm_num` procedure is inhabited, meaning it always has a default value.

Mathlib.Meta.NormNum.Result.isTrue definition

{x : Q(Prop)} : ∀ (proof : Q($x)), Result q($x)

Full source

/-- The result is `proof : x`, where `x` is a (true) proposition. -/
@[match_pattern, inline] def Result.isTrue {x : Q(Prop)} :
    ∀ (proof : Q($x)), Result q($x) := Result'.isBool true

True proposition result for `norm_num`

Informal description

The constructor `Result.isTrue` takes a proof that a proposition `x$ is true and produces a `Result` object representing this fact.

Mathlib.Meta.NormNum.Result.isFalse definition

{x : Q(Prop)} : ∀ (proof : Q(¬$x)), Result q($x)

Full source

/-- The result is `proof : ¬x`, where `x` is a (false) proposition. -/
@[match_pattern, inline] def Result.isFalse {x : Q(Prop)} :
    ∀ (proof : Q(¬$x)), Result q($x) := Result'.isBool false

False proposition result for `norm_num`

Informal description

The constructor `Result.isFalse` takes a proof that a proposition `x` is false and produces a `Result` object representing this fact.

Mathlib.Meta.NormNum.Result.isNat definition

 {α : Q(Type u)} {x : Q($α)} :
  ∀ (inst : Q(AddMonoidWithOne $α) := by assumption) (lit : Q(ℕ)) (proof : Q(IsNat $x $lit)), Result x

Full source

/-- The result is `lit : ℕ` (a raw nat literal) and `proof : isNat x lit`. -/
@[match_pattern, inline] def Result.isNat {α : Q(Type u)} {x : Q($α)} :
    ∀ (inst : Q(AddMonoidWithOne $α) := by assumption) (lit : Q(ℕ)) (proof : Q(IsNat $x $lit)),
      Result x := Result'.isNat

Natural number normalization result for `norm_num`

Informal description

The constructor `Result.isNat` produces a normalization result stating that a typed expression `x` of type `α` (where `α` is an additive monoid with one) is equal to the canonical embedding of a natural number `lit` into `α`, with a proof that this equality holds.

Mathlib.Meta.NormNum.Result.isNegNat definition

 {α : Q(Type u)} {x : Q($α)} :
  ∀ (inst : Q(Ring $α) := by assumption) (lit : Q(ℕ)) (proof : Q(IsInt $x (.negOfNat $lit))), Result x

Full source

/-- The result is `-lit` where `lit` is a raw nat literal
and `proof : isInt x (.negOfNat lit)`. -/
@[match_pattern, inline] def Result.isNegNat {α : Q(Type u)} {x : Q($α)} :
    ∀ (inst : Q(Ring $α) := by assumption) (lit : Q(ℕ)) (proof : Q(IsInt $x (.negOfNat $lit))),
      Result x := Result'.isNegNat

Negative natural number normalization result for `norm_num`

Informal description

Given a typed expression `x` of type `α` in a ring, the constructor `Result.isNegNat` produces a normalization result stating that `x` is equal to the negation of a natural number `lit`, with a proof that this equality holds.

Mathlib.Meta.NormNum.Result.isRat definition

 {α : Q(Type u)} {x : Q($α)} :
  ∀ (inst : Q(DivisionRing $α) := by assumption) (q : Rat) (n : Q(ℤ)) (d : Q(ℕ)) (proof : Q(IsRat $x $n $d)), Result x

Full source

/-- The result is `proof : isRat x n d`,
where `n` is either `.ofNat lit` or `.negOfNat lit` with `lit` a raw nat literal,
`d` is a raw nat literal (not 0 or 1),
`n` and `d` are coprime, and `q` is the value of `n / d`. -/
@[match_pattern, inline] def Result.isRat {α : Q(Type u)} {x : Q($α)} :
    ∀ (inst : Q(DivisionRing $α) := by assumption) (q : Rat) (n : Q(ℤ)) (d : Q(ℕ))
      (proof : Q(IsRat $x $n $d)), Result x := Result'.isRat

Normalization result for rational numbers in `norm_num`

Informal description

Given a typed expression `x` of type `α` in a division ring, the `Result.isRat` constructor produces a normalization result stating that `x` is equal to the rational number `n/d` (where `n` is an integer and `d` is a natural number), with a proof that this equality holds.

Mathlib.Meta.NormNum.instToMessageDataResult instance

{α : Q(Type u)} {x : Q($α)} : ToMessageData (Result x)

Full source

instance {α : Q(Type u)} {x : Q($α)} : ToMessageData (Result x) where
  toMessageData
  | .isBool true proof => m!"isTrue ({proof})"
  | .isBool false proof => m!"isFalse ({proof})"
  | .isNat _ lit proof => m!"isNat {lit} ({proof})"
  | .isNegNat _ lit proof => m!"isNegNat {lit} ({proof})"
  | .isRat _ q _ _ proof => m!"isRat {q} ({proof})"

Message Data Conversion for `norm_num` Results

Informal description

For any typed expression `x` of type `α`, the `Result x` type can be converted to a message data format for display purposes.

Mathlib.Meta.NormNum.Result.toRat definition

{α : Q(Type u)} {e : Q($α)} : Result e → Option Rat

Full source

/-- Returns the rational number that is the result of `norm_num` evaluation. -/
def Result.toRat {α : Q(Type u)} {e : Q($α)} : Result e → Option Rat
  | .isBool .. => none
  | .isNat _ lit _ => some lit.natLit!
  | .isNegNat _ lit _ => some (-lit.natLit!)
  | .isRat _ q .. => some q

Conversion of normalization result to rational number

Informal description

Given a normalization result for an expression `e` of type `α`, this function returns the corresponding rational number if `e` is equal to a natural number, integer, or rational number (represented as `n/d` where `n` is an integer and `d` is a natural number). If `e` is a boolean value (`true` or `false`), the function returns `none`.

Mathlib.Meta.NormNum.Result.toRatNZ definition

{α : Q(Type u)} {e : Q($α)} : Result e → Option (Rat × Option Expr)

Full source

/-- Returns the rational number that is the result of `norm_num` evaluation, along with a proof
that the denominator is nonzero in the `isRat` case. -/
def Result.toRatNZ {α : Q(Type u)} {e : Q($α)} : Result e → Option (RatRat × Option Expr)
  | .isBool .. => none
  | .isNat _ lit _ => some (lit.natLit!, none)
  | .isNegNat _ lit _ => some (-lit.natLit!, none)
  | .isRat _ q _ _ p => some (q, q(IsRat.den_nz $p))

Normalization result to rational number with denominator proof

Informal description

Given a normalization result for an expression `e` of type `α`, this function returns: - If `e` is equal to a natural number `n`, returns `(n, none)` - If `e` is equal to a negative integer `-n`, returns `(-n, none)` - If `e` is equal to a rational number `q = n/d`, returns `(q, p)` where `p` is a proof that the denominator `d` is nonzero - If `e` is a boolean value (`true` or `false`), returns `none`

Mathlib.Meta.NormNum.Result.toRawEq definition

{α : Q(Type u)} {e : Q($α)} : Result e → (e' : Q($α)) × Q($e = $e')

Full source

/--
Given a `NormNum.Result e` (which uses `IsNat`, `IsInt`, `IsRat` to express equality to a rational
numeral), converts it to an equality `e = Nat.rawCast n`, `e = Int.rawCast n`, or
`e = Rat.rawCast n d` to a raw cast expression, so it can be used for rewriting.
-/
def Result.toRawEq {α : Q(Type u)} {e : Q($α)} : Result e → (e' : Q($α)) × Q($e = $e')
  | .isBool false p =>
    have e : Q(Prop) := e; have p : Q(¬$e) := p
    ⟨(q(False) : Expr), (q(eq_false $p) : Expr)⟩
  | .isBool true p =>
    have e : Q(Prop) := e; have p : Q($e) := p
    ⟨(q(True) : Expr), (q(eq_true $p) : Expr)⟩
  | .isNat _ lit p => ⟨q(Nat.rawCast $lit), q(IsNat.to_raw_eq $p)⟩
  | .isNegNat _ lit p => ⟨q(Int.rawCast (.negOfNat $lit)), q(IsInt.to_raw_eq $p)⟩
  | .isRat _ _ n d p => ⟨q(Rat.rawCast $n $d), q(IsRat.to_raw_eq $p)⟩

Conversion of normalization result to raw cast equality

Informal description

Given a `NormNum.Result e` which proves that an expression `e` of type `α` is equal to a natural number, integer, or rational number (or is `true` or `false`), this function converts it to an equality `e = Nat.rawCast n`, `e = Int.rawCast n`, or `e = Rat.rawCast n d` where the right-hand side is a raw cast expression. This equality can then be used for rewriting purposes.

Mathlib.Meta.NormNum.Result.toRawIntEq definition

{α : Q(Type u)} {e : Q($α)} : Result e →
    Option (ℤ × (e' : Q($α)) × Q($e = $e'))

Full source

/--
`Result.toRawEq` but providing an integer. Given a `NormNum.Result e` for something known to be an
integer (which uses `IsNat` or `IsInt` to express equality to an integer numeral), converts it to
an equality `e = Nat.rawCast n` or `e = Int.rawCast n` to a raw cast expression, so it can be used
for rewriting. Gives `none` if not an integer.
-/
def Result.toRawIntEq {α : Q(Type u)} {e : Q($α)} : Result e →
    Option (ℤℤ × (e' : Q($α)) × Q($e = $e'))
  | .isNat _ lit p => some ⟨lit.natLit!, q(Nat.rawCast $lit), q(IsNat.to_raw_eq $p)⟩
  | .isNegNat _ lit p => some ⟨-lit.natLit!, q(Int.rawCast (.negOfNat $lit)), q(IsInt.to_raw_eq $p)⟩
  | .isRat _ .. | .isBool .. => none

Conversion of normalization result to integer raw cast equality

Informal description

Given a normalization result `Result e` for an expression `e` of type `α` that is known to be equal to an integer numeral (via `IsNat` or `IsInt`), this function produces an integer `n` and a proof that `e` is equal to either `Nat.rawCast n` or `Int.rawCast n`, depending on whether the integer is positive or negative. The output is `none` if the result does not correspond to an integer.

Mathlib.Meta.NormNum.Result.ofRawNat definition

{α : Q(Type u)} (e : Q($α)) : Result e

Full source

/-- Constructs a `Result` out of a raw nat cast. Assumes `e` is a raw nat cast expression. -/
def Result.ofRawNat {α : Q(Type u)} (e : Q($α)) : Result e := Id.run do
  let .app (.app _ (sα : Q(AddMonoidWithOne $α))) (lit : Q(ℕ)) := e | panic! "not a raw nat cast"
  .isNat sα lit (q(IsNat.of_raw $α $lit) : Expr)

Normalization result from raw natural number cast

Informal description

Given a typed expression `e` of type `α` that represents a raw natural number cast, the function constructs a `Result` object containing a proof that `e` is equal to the canonical embedding of the natural number into `α`. This assumes `α` has an `AddMonoidWithOne` instance.

Mathlib.Meta.NormNum.Result.ofRawInt definition

{α : Q(Type u)} (n : ℤ) (e : Q($α)) : Result e

Full source

/-- Constructs a `Result` out of a raw int cast.
Assumes `e` is a raw int cast expression denoting `n`. -/
def Result.ofRawInt {α : Q(Type u)} (n : ℤ) (e : Q($α)) : Result e :=
  if 0 ≤ n then
    Result.ofRawNat e
  else Id.run do
    let .app (.app _ (rα : Q(Ring $α))) (.app _ (lit : Q(ℕ))) := e | panic! "not a raw int cast"
    .isNegNat rα lit (q(IsInt.of_raw $α (.negOfNat $lit)) : Expr)

Normalization result from raw integer cast

Informal description

Given an integer `n` and a typed expression `e` of type `α`, the function constructs a `Result` object containing a proof that `e` is equal to the canonical embedding of `n` into `α`. If `n` is non-negative, it uses the natural number embedding; if `n` is negative, it constructs a proof that `e` is equal to the negation of the corresponding natural number.

Mathlib.Meta.NormNum.Result.toSimpResult definition

{α : Q(Type u)} {e : Q($α)} : Result e → MetaM Simp.Result

Full source

/-- Convert a `Result` to a `Simp.Result`. -/
def Result.toSimpResult {α : Q(Type u)} {e : Q($α)} : Result e → MetaM Simp.Result
  | r@(.isBool ..) => let ⟨expr, proof?⟩ := r.toRawEq; pure { expr, proof? }
  | .isNat sα lit p => do
    let ⟨a', pa'⟩ ← mkOfNat α sα lit
    return { expr := a', proof? := q(IsNat.to_eq $p $pa') }
  | .isNegNat _rα lit p => do
    let ⟨a', pa'⟩ ← mkOfNat α q(AddCommMonoidWithOne.toAddMonoidWithOne) lit
    return { expr := q(-$a'), proof? := q(IsInt.neg_to_eq $p $pa') }
  | .isRat _ q n d p => do
    have lit : Q(ℕ) := n.appArg!
    if q < 0 then
      let p : Q(IsRat $e (.negOfNat $lit) $d) := p
      let ⟨n', pn'⟩ ← mkOfNat α q(AddCommMonoidWithOne.toAddMonoidWithOne) lit
      let ⟨d', pd'⟩ ← mkOfNat α q(AddCommMonoidWithOne.toAddMonoidWithOne) d
      return { expr := q(-($n' / $d')), proof? := q(IsRat.neg_to_eq $p $pn' $pd') }
    else
      let p : Q(IsRat $e (.ofNat $lit) $d) := p
      let ⟨n', pn'⟩ ← mkOfNat α q(AddCommMonoidWithOne.toAddMonoidWithOne) lit
      let ⟨d', pd'⟩ ← mkOfNat α q(AddCommMonoidWithOne.toAddMonoidWithOne) d
      return { expr := q($n' / $d'), proof? := q(IsRat.nonneg_to_eq $p $pn' $pd') }

Conversion from normalization result to simplification result

Informal description

The function converts a `Result` object, which represents the normalization of an expression `e` of type `α` to a natural number, integer, or rational number (or a boolean value), into a `Simp.Result` object. The conversion process involves: - For boolean results, directly extracting the expression and proof - For natural numbers, constructing the corresponding `ofNat` term and equality proof - For negative integers, constructing the negation of the corresponding `ofNat` term and equality proof - For rational numbers, handling both positive and negative cases by constructing the appropriate division expression and equality proof

Mathlib.Meta.NormNum.BoolResult abbrev

(p : Q(Prop)) (b : Bool) : Type

Full source

/-- Given `Mathlib.Meta.NormNum.Result.isBool p b`, this is the type of `p`.
  Note that `BoolResult p b` is definitionally equal to `Expr`, and if you write `match b with ...`,
  then in the `true` branch `BoolResult p true` is reducibly equal to `Q($p)` and
  in the `false` branch it is reducibly equal to `Q(¬ $p)`. -/
abbrev BoolResult (p : Q(Prop)) (b : Bool) : Type :=
  Q(Bool.rec (¬ $p) ($p) $b)

Boolean Result Type for Proposition Normalization

Informal description

Given a proposition `p` in Lean's expression language and a boolean value `b`, `BoolResult p b` is the type representing the proof that `p` is equal to `b`. Specifically: - If `b` is `true`, then `BoolResult p true` is reducibly equal to the type of proofs of `p` (`Q($p)`). - If `b` is `false`, then `BoolResult p false` is reducibly equal to the type of proofs of `¬ p` (`Q(¬ $p)`).

Mathlib.Meta.NormNum.Result.ofBoolResult definition

{p : Q(Prop)} {b : Bool} (prf : BoolResult p b) : Result q(Prop)

Full source

/-- Obtain a `Result` from a `BoolResult`. -/
def Result.ofBoolResult {p : Q(Prop)} {b : Bool} (prf : BoolResult p b) : Result q(Prop) :=
  Result'.isBool b prf

Conversion from Boolean Result to Normalization Result

Informal description

Given a proposition `p` and a boolean value `b`, along with a proof `prf` that `p` is equal to `b` (represented by `BoolResult p b`), this function constructs a `Result` object showing that the expression `p` normalizes to the boolean value `b`.

Mathlib.Meta.NormNum.Result.eqTrans definition

{α : Q(Type u)} {a b : Q($α)} (eq : Q($a = $b)) : Result b → Result a

Full source

/-- If `a = b` and we can evaluate `b`, then we can evaluate `a`. -/
def Result.eqTrans {α : Q(Type u)} {a b : Q($α)} (eq : Q($a = $b)) : Result b → Result a
  | .isBool true proof =>
    have a : Q(Prop) := a
    have b : Q(Prop) := b
    have eq : Q($a = $b) := eq
    have proof : Q($b) := proof
    Result.isTrue (x := a) q($eq ▸ $proof)
  | .isBool false proof =>
    have a : Q(Prop) := a
    have b : Q(Prop) := b
    have eq : Q($a = $b) := eq
    have proof : Q(¬ $b) := proof
    Result.isFalse (x := a) q($eq ▸ $proof)
  | .isNat inst lit proof => Result.isNat inst lit q($eq ▸ $proof)
  | .isNegNat inst lit proof => Result.isNegNat inst lit q($eq ▸ $proof)
  | .isRat inst q n d proof => Result.isRat inst q n d q($eq ▸ $proof)

Transitivity of normalization results via equality

Informal description

Given a proof that two expressions $a$ and $b$ of type $\alpha$ are equal ($a = b$) and a normalization result for $b$, this function produces a normalization result for $a$ by transferring the proof of equality.