Finite nimber arithmetic #

This file defines the type alias NatNimber of the natural numbers, endowed with nimber arithmetic. The goal is to define the field structure computably, and prove that it matches that on Nimber.

source

@[simp]

theorem NatNimber.val_one :

val 1 = 1

source

@[simp]

theorem NatNimber.not_neg (a✝ : NatNimber) :

¬a✝ < 0

source

@[simp]

theorem NatNimber.val_symm :

val.symm = of

source

theorem NatNimber.pos_iff_ne_zero {a✝ : NatNimber} :

0 < a✝ ↔ a✝ ≠ 0

source

@[simp]

theorem NatNimber.of_eq_zero {a✝ : ℕ} :

of a✝ = 0 ↔ a✝ = 0

source

instance NatNimber.instOrderBot :

OrderBot NatNimber

Equations

NatNimber.instOrderBot = inferInstanceAs (OrderBot ℕ)

source

theorem NatNimber.induction {p✝ : NatNimber → Prop} (i✝ : NatNimber) :

(∀ (j : NatNimber), (∀ k < j, p✝ k) → p✝ j) → p✝ i✝

Well-founded induction for NatNimber.

source

@[simp]

theorem NatNimber.of_eq_one {a✝ : ℕ} :

of a✝ = 1 ↔ a✝ = 1

source

noncomputable instance NatNimber.instConditionallyCompleteLinearOrderBot :

ConditionallyCompleteLinearOrderBot NatNimber

Equations

NatNimber.instConditionallyCompleteLinearOrderBot = inferInstanceAs (ConditionallyCompleteLinearOrderBot ℕ)

source

@[simp]

theorem NatNimber.val_eq_zero {a✝ : NatNimber} :

val a✝ = 0 ↔ a✝ = 0

source

theorem NatNimber.eq_zero_or_pos (a✝ : NatNimber) :

a✝ = 0 ∨ 0 < a✝

source

theorem NatNimber.val_eq_iff {a✝ : NatNimber} {b✝ : ℕ} :

val a✝ = b✝ ↔ a✝ = of b✝

source

@[simp]

theorem NatNimber.of_symm :

of.symm = val

source

@[simp]

theorem NatNimber.succ_of (a✝ : ℕ) :

Order.succ (of a✝) = of (a✝ + 1)

source

@[match_pattern]

def NatNimber.val :

NatNimber ≃o ℕ

The identity function between NatNimber and Nat.

Equations

NatNimber.val = OrderIso.refl NatNimber

Instances For

source

instance instInhabitedNatNimber :

Inhabited NatNimber

Equations

instInhabitedNatNimber = instInhabitedNat

source

instance NatNimber.instSuccOrder :

SuccOrder NatNimber

Equations

NatNimber.instSuccOrder = inferInstanceAs (SuccOrder ℕ)

source

instance NatNimber.instPartialOrder :

PartialOrder NatNimber

Equations

NatNimber.instPartialOrder = inferInstanceAs (PartialOrder ℕ)

source

theorem NatNimber.val_lt_iff {a✝ : NatNimber} {b✝ : ℕ} :

val a✝ < b✝ ↔ a✝ < of b✝

source

@[simp]

theorem NatNimber.le_zero {a✝ : NatNimber} :

a✝ ≤ 0 ↔ a✝ = 0

source

@[match_pattern]

def NatNimber.of :

ℕ ≃o NatNimber

The identity function between Nat and NatNimber.

Equations

NatNimber.of = OrderIso.refl ℕ

Instances For

source

@[simp]

theorem NatNimber.succ_ne_zero (a✝ : NatNimber) :

Order.succ a✝ ≠ 0

source

instance NatNimber.instZeroLEOneClass :

ZeroLEOneClass NatNimber

source

@[simp]

theorem NatNimber.val_image_Iio (a✝ : NatNimber) :

⇑val '' Set.Iio a✝ = Set.Iio (val a✝)

source

@[simp]

theorem NatNimber.of_val (a✝ : NatNimber) :

of (val a✝) = a✝

source

@[simp]

theorem NatNimber.zero_le (a✝ : NatNimber) :

0 ≤ a✝

source

@[simp]

theorem NatNimber.val_eq_one {a✝ : NatNimber} :

val a✝ = 1 ↔ a✝ = 1

source

@[simp]

theorem NatNimber.bot_eq_zero :

⊥ = 0

source

theorem NatNimber.of_lt_iff {a✝ : ℕ} {b✝ : NatNimber} :

of a✝ < b✝ ↔ a✝ < val b✝

source

theorem NatNimber.val_le_iff {a✝ : NatNimber} {b✝ : ℕ} :

val a✝ ≤ b✝ ↔ a✝ ≤ of b✝

source

@[simp]

theorem NatNimber.succ_zero :

Order.succ 0 = 1

source

@[simp]

theorem NatNimber.of_zero :

of 0 = 0

source

instance NatNimber.instNoMaxOrder :

NoMaxOrder NatNimber

source

instance instZeroNatNimber :

Zero NatNimber

Equations

instZeroNatNimber = Nat.instMulZeroClass.toZero

source

theorem NatNimber.of_eq_iff {a✝ : ℕ} {b✝ : NatNimber} :

of a✝ = b✝ ↔ a✝ = val b✝

source

instance NatNimber.instWellFoundedLT :

WellFoundedLT NatNimber

source

@[simp]

theorem NatNimber.of_one :

of 1 = 1

source

instance instWellFoundedRelationNatNimber :

WellFoundedRelation NatNimber

Equations

instWellFoundedRelationNatNimber = sizeOfWFRel

source

instance NatNimber.instNeZeroOfNat :

NeZero 1

source

theorem NatNimber.lt_wf :

WellFounded fun (x1 x2 : NatNimber) => x1 < x2

source

@[simp]

theorem NatNimber.val_zero :

val 0 = 0

source

@[simp]

theorem NatNimber.of_image_Iio (a✝ : ℕ) :

⇑of '' Set.Iio a✝ = Set.Iio (of a✝)

source

instance instNontrivialNatNimber :

Nontrivial NatNimber

Equations

instNontrivialNatNimber = Nat.instNontrivial

source

theorem NatNimber.of_le_iff {a✝ : ℕ} {b✝ : NatNimber} :

of a✝ ≤ b✝ ↔ a✝ ≤ val b✝

source

def NatNimber.ind {motive✝ : NatNimber → Sort u_1} (mk : (a : ℕ) → motive✝ (of a)) (a✝ : NatNimber) :

motive✝ a✝

A recursor for NatNimber. Use as induction x.

Equations

NatNimber.ind mk a✝ = mk (NatNimber.val a✝)

Instances For

source

@[simp]

theorem NatNimber.val_of (a✝ : ℕ) :

val (of a✝) = a✝

source

theorem NatNimber.succ_def (a✝ : NatNimber) :

Order.succ a✝ = of (val a✝ + 1)

source

def NatNimber :

Type

The natural numbers, endowed with nim operations.

Equations

NatNimber = ℕ

Instances For

source

instance instOneNatNimber :

One NatNimber

Equations

instOneNatNimber = Nat.instOne

source

instance NatNimber.instLinearOrder :

LinearOrder NatNimber

Equations

NatNimber.instLinearOrder = Nat.instLinearOrder

source

instance NatNimber.instToExpr :

Lean.ToExpr NatNimber

Equations

NatNimber.instToExpr = { toExpr := fun (x : NatNimber) => (Lean.Expr.const `NatNimber.of []).app (Lean.toExpr (NatNimber.val x)), toTypeExpr := Lean.Expr.const `NatNimber [] }

source

instance NatNimber.instToString :

ToString NatNimber

Equations

NatNimber.instToString = { toString := fun (x : NatNimber) => "∗" ++ (NatNimber.val x).repr }

source

@[simp]

theorem NatNimber.lt_one_iff_zero {a : NatNimber} :

a < 1 ↔ a = 0

source

@[simp]

theorem NatNimber.one_le_iff_ne_zero {a : NatNimber} :

1 ≤ a ↔ a ≠ 0

source

theorem NatNimber.le_one_iff {a : NatNimber} :

a ≤ 1 ↔ a = 0 ∨ a = 1

source

def NatNimber.toNimber :

NatNimber ↪o Nimber

The embedding NatNimber ↪o Nimber.

Equations

NatNimber.toNimber = { toFun := fun (x : NatNimber) => Nimber.of ↑(NatNimber.val x), inj' := NatNimber.toNimber._proof_1, map_rel_iff' := NatNimber.toNimber._proof_2 }

Instances For

source

@[simp]

theorem NatNimber.toNimber_zero :

toNimber 0 = 0

source

@[simp]

theorem NatNimber.toNimber_one :

toNimber 1 = 1

source

@[simp]

theorem NatNimber.toNimber_of (n : ℕ) :

toNimber (of n) = Nimber.of ↑n

source

instance NatNimber.instNeg :

Neg NatNimber

Equations

NatNimber.instNeg = { neg := fun (n : NatNimber) => n }

source

instance NatNimber.instAdd :

Add NatNimber

Equations

NatNimber.instAdd = { add := fun (m n : NatNimber) => NatNimber.of (NatNimber.val m ^^^ NatNimber.val n) }

source

instance NatNimber.instSub :

Sub NatNimber

Equations

NatNimber.instSub = { sub := fun (m n : NatNimber) => m + n }

source

@[simp]

theorem NatNimber.toNimber_add (x y : NatNimber) :

toNimber (x + y) = Nimber.of ↑(val x) + Nimber.of ↑(val y)

source

@[simp]

theorem NatNimber.sub_eq (x y : NatNimber) :

x - y = x + y

source

@[simp]

theorem NatNimber.neg_eq (x : NatNimber) :

-x = x

source

instance NatNimber.instMul :

Mul NatNimber

Equations

NatNimber.instMul = { mul := fun (x y : NatNimber) => NatNimber.mul✝ (max (NatNimber.val x).log2.log2 (NatNimber.val y).log2.log2 + 1) x y }

Documentation

CombinatorialGames.Nimber.Nat

Finite nimber arithmetic #