Integers and Gaussian integers as pairs of naturals

Mathlib's Primrec has no arithmetic on ℤ (and no Primcodable ℤ), so the enumeration behind lem:value-lower-approx carries its integers as pairs of naturals: PInt := ℕ × ℕ denotes a - b, and GInt := PInt × PInt denotes the Gaussian integer m + n i. Equality and order are the semantic ones (PInt.Eq', PInt.Lt', GInt.Eq'), decidable and primitive recursive; PInt.toInt and GInt.toC read the values off and commute with the operations provided. Every function here is primitive recursive, with the proof next to the definition.

Integers

@[reducible, inline]

abbrev MIPRE.ValueApprox.PInt : Type

An integer a - b, as the pair (a, b) of naturals.

Equations

• MIPRE.ValueApprox.PInt = (ℕ × ℕ)

def MIPRE.ValueApprox.PInt.toInt (x : PInt) : ℤ

The integer denoted.

Equations

• x.toInt = ↑x.1 - ↑x.2

def MIPRE.ValueApprox.PInt.zero : PInt

Equations

• MIPRE.ValueApprox.PInt.zero = (0, 0)

def MIPRE.ValueApprox.PInt.ofNat (n : ℕ) : PInt

Equations

• MIPRE.ValueApprox.PInt.ofNat n = (n, 0)

def MIPRE.ValueApprox.PInt.ofInt (m : ℤ) : PInt

Equations

• MIPRE.ValueApprox.PInt.ofInt m = (m.toNat, (-m).toNat)

def MIPRE.ValueApprox.PInt.add (x y : PInt) : PInt

Equations

• x.add y = (x.1 + y.1, x.2 + y.2)

def MIPRE.ValueApprox.PInt.neg (x : PInt) : PInt

Equations

• x.neg = (x.2, x.1)

def MIPRE.ValueApprox.PInt.mul (x y : PInt) : PInt

Equations

• x.mul y = (x.1 * y.1 + x.2 * y.2, x.1 * y.2 + x.2 * y.1)

def MIPRE.ValueApprox.PInt.sum (l : List PInt) : PInt

Equations

• MIPRE.ValueApprox.PInt.sum l = List.foldr MIPRE.ValueApprox.PInt.add MIPRE.ValueApprox.PInt.zero l

def MIPRE.ValueApprox.PInt.Eq' (x y : PInt) : Prop

Semantic equality of the denoted integers.

Equations

• x.Eq' y = (x.1 + y.2 = y.1 + x.2)

def MIPRE.ValueApprox.PInt.Lt' (x y : PInt) : Prop

Semantic strict order of the denoted integers.

Equations

• x.Lt' y = (x.1 + y.2 < y.1 + x.2)

@[instance_reducible]

instance MIPRE.ValueApprox.PInt.instDecidableRelEq' : DecidableRel Eq'

Equations

• x.instDecidableRelEq' y = { decide := (x.1 + y.2).beq (y.1 + x.2), reflects_decide := ⋯ }

@[instance_reducible]

instance MIPRE.ValueApprox.PInt.instDecidableRelLt' : DecidableRel Lt'

Equations

• x.instDecidableRelLt' y = { decide := (x.1 + y.2).succ.ble (y.1 + x.2), reflects_decide := ⋯ }

@[simp]

theorem MIPRE.ValueApprox.PInt.toInt_zero : zero.toInt = 0

@[simp]

theorem MIPRE.ValueApprox.PInt.toInt_ofNat (n : ℕ) : (ofNat n).toInt = ↑n

@[simp]

theorem MIPRE.ValueApprox.PInt.toInt_ofInt (m : ℤ) : (ofInt m).toInt = m

@[simp]

theorem MIPRE.ValueApprox.PInt.toInt_add (x y : PInt) : (x.add y).toInt = x.toInt + y.toInt

@[simp]

theorem MIPRE.ValueApprox.PInt.toInt_neg (x : PInt) : x.neg.toInt = -x.toInt

@[simp]

theorem MIPRE.ValueApprox.PInt.toInt_mul (x y : PInt) : (x.mul y).toInt = x.toInt * y.toInt

@[simp]

theorem MIPRE.ValueApprox.PInt.toInt_sum (l : List PInt) : (sum l).toInt = (List.map toInt l).sum

theorem MIPRE.ValueApprox.PInt.eq'_iff {x y : PInt} : x.Eq' y ↔ x.toInt = y.toInt

theorem MIPRE.ValueApprox.PInt.lt'_iff {x y : PInt} : x.Lt' y ↔ x.toInt < y.toInt

theorem MIPRE.ValueApprox.PInt.primrec_ofNat : Primrec ofNat

theorem MIPRE.ValueApprox.PInt.primrec_add : Primrec₂ add

theorem MIPRE.ValueApprox.PInt.primrec_neg : Primrec neg

theorem MIPRE.ValueApprox.PInt.primrec_mul : Primrec₂ mul

theorem MIPRE.ValueApprox.PInt.primrec_sum : Primrec sum

theorem MIPRE.ValueApprox.PInt.primrecRel_eq' : PrimrecRel Eq'

theorem MIPRE.ValueApprox.PInt.primrecRel_lt' : PrimrecRel Lt'

Gaussian integers

@[reducible, inline]

abbrev MIPRE.ValueApprox.GInt : Type

A Gaussian integer m + n i, as a pair of PInts.

Equations

• MIPRE.ValueApprox.GInt = (MIPRE.ValueApprox.PInt × MIPRE.ValueApprox.PInt)

def MIPRE.ValueApprox.GInt.toC (z : GInt) : ℂ

The complex number denoted.

Equations

• z.toC = ↑z.1.toInt + ↑z.2.toInt * Complex.I

def MIPRE.ValueApprox.GInt.zero : GInt

Equations

• MIPRE.ValueApprox.GInt.zero = (MIPRE.ValueApprox.PInt.zero, MIPRE.ValueApprox.PInt.zero)

def MIPRE.ValueApprox.GInt.ofNat (n : ℕ) : GInt

Equations

• MIPRE.ValueApprox.GInt.ofNat n = (MIPRE.ValueApprox.PInt.ofNat n, MIPRE.ValueApprox.PInt.zero)

def MIPRE.ValueApprox.GInt.ofInt (m n : ℤ) : GInt

Equations

• MIPRE.ValueApprox.GInt.ofInt m n = (MIPRE.ValueApprox.PInt.ofInt m, MIPRE.ValueApprox.PInt.ofInt n)

def MIPRE.ValueApprox.GInt.add (x y : GInt) : GInt

Equations

• x.add y = (x.1.add y.1, x.2.add y.2)

def MIPRE.ValueApprox.GInt.mul (x y : GInt) : GInt

Equations

• x.mul y = ((x.1.mul y.1).add (x.2.mul y.2).neg, (x.1.mul y.2).add (x.2.mul y.1))

def MIPRE.ValueApprox.GInt.conj (x : GInt) : GInt

Equations

• x.conj = (x.1, x.2.neg)

def MIPRE.ValueApprox.GInt.sum (l : List GInt) : GInt

Equations

• MIPRE.ValueApprox.GInt.sum l = List.foldr MIPRE.ValueApprox.GInt.add MIPRE.ValueApprox.GInt.zero l

def MIPRE.ValueApprox.GInt.Eq' (x y : GInt) : Prop

Semantic equality of the denoted Gaussian integers.

Equations

• x.Eq' y = (x.1.Eq' y.1 ∧ x.2.Eq' y.2)

@[instance_reducible]

instance MIPRE.ValueApprox.GInt.instDecidableRelEq' : DecidableRel Eq'

Equations

• x.instDecidableRelEq' y = { decide := decide (x.1.Eq' y.1) && decide (x.2.Eq' y.2), reflects_decide := ⋯ }

@[simp]

theorem MIPRE.ValueApprox.GInt.re_toC (z : GInt) : z.toC.re = ↑z.1.toInt

@[simp]

theorem MIPRE.ValueApprox.GInt.im_toC (z : GInt) : z.toC.im = ↑z.2.toInt

@[simp]

theorem MIPRE.ValueApprox.GInt.toC_zero : zero.toC = 0

@[simp]

theorem MIPRE.ValueApprox.GInt.toC_ofNat (n : ℕ) : (ofNat n).toC = ↑n

@[simp]

theorem MIPRE.ValueApprox.GInt.toC_ofInt (m n : ℤ) : (ofInt m n).toC = ↑m + ↑n * Complex.I

@[simp]

theorem MIPRE.ValueApprox.GInt.toC_add (x y : GInt) : (x.add y).toC = x.toC + y.toC

@[simp]

theorem MIPRE.ValueApprox.GInt.toC_mul (x y : GInt) : (x.mul y).toC = x.toC * y.toC

@[simp]

theorem MIPRE.ValueApprox.GInt.toC_conj (x : GInt) : x.conj.toC = star x.toC

@[simp]

theorem MIPRE.ValueApprox.GInt.toC_sum (l : List GInt) : (sum l).toC = (List.map toC l).sum

theorem MIPRE.ValueApprox.GInt.eq'_iff {x y : GInt} : x.Eq' y ↔ x.toC = y.toC

theorem MIPRE.ValueApprox.GInt.primrec_ofNat : Primrec ofNat

theorem MIPRE.ValueApprox.GInt.primrec_add : Primrec₂ add

theorem MIPRE.ValueApprox.GInt.primrec_mul : Primrec₂ mul

theorem MIPRE.ValueApprox.GInt.primrec_conj : Primrec conj

theorem MIPRE.ValueApprox.GInt.primrec_sum : Primrec sum

theorem MIPRE.ValueApprox.GInt.primrecRel_eq' : PrimrecRel Eq'