The positive natural numbers

This file contains the definitions, and basic results. Most algebraic facts are deferred to Data.PNat.Basic, as they need more imports.

ink

def PNat : Type

ℕ+ is the type of positive natural numbers. It is defined as a subtype, and the VM representation of ℕ+ is the same as ℕ because the proof is not stored.

Equations

• ℕ+ = { n // 0 < n }

ink

def «termℕ+» : Lean.ParserDescr

ℕ+ is the type of positive natural numbers. It is defined as a subtype, and the VM representation of ℕ+ is the same as ℕ because the proof is not stored.

Equations

• «termℕ+» = Lean.ParserDescr.node `termℕ+ 1024 (Lean.ParserDescr.symbol "ℕ+")

ink

instance instOnePNat : One ℕ+

Equations

• instOnePNat = { one := { val := 1, property := Nat.zero_lt_one } }

ink

def PNat.val : ℕ+ → ℕ

The underlying natural number

Equations

• PNat.val = Subtype.val

ink

instance coePNatNat : Coe ℕ+ ℕ

Equations

• coePNatNat = { coe := PNat.val }

ink

instance instReprPNat : Repr ℕ+

Equations

• instReprPNat = { reprPrec := fun n n' => reprPrec (↑n) n' }

ink

instance instOfNatPNatHAddNatInstHAddInstAddNatOfNat (n : ℕ) : OfNat ℕ+ (n + 1)

Equations

• instOfNatPNatHAddNatInstHAddInstAddNatOfNat n = { ofNat := { val := n + 1, property := (_ : 0 < Nat.succ n) } }

ink

@[simp]

theorem PNat.mk_coe (n : ℕ) (h : 0 < n) : ↑{ val := n, property := h } = n

ink

def PNat.natPred (i : ℕ+) : ℕ

Predecessor of a ℕ+, as a ℕ.

Equations

• PNat.natPred i = ↑i - 1

ink

@[simp]

theorem PNat.natPred_eq_pred {n : ℕ} (h : 0 < n) : PNat.natPred { val := n, property := h } = Nat.pred n

ink

def Nat.toPNat (n : ℕ) (h : autoParam (0 < n) _auto✝) : ℕ+

Convert a natural number to a positive natural number. The positivity assumption is inferred by dec_trivial.

Equations

• Nat.toPNat n = { val := n, property := h }

ink

def Nat.succPNat (n : ℕ) : ℕ+

Write a successor as an element of ℕ+.

Equations

• Nat.succPNat n = { val := Nat.succ n, property := (_ : 0 < Nat.succ n) }

ink

@[simp]

theorem Nat.succPNat_coe (n : ℕ) : ↑(Nat.succPNat n) = Nat.succ n

ink

@[simp]

theorem Nat.natPred_succPNat (n : ℕ) : PNat.natPred (Nat.succPNat n) = n

ink

@[simp]

theorem PNat.succPNat_natPred (n : ℕ+) : Nat.succPNat (PNat.natPred n) = n

ink

def Nat.toPNat' (n : ℕ) : ℕ+

Convert a natural number to a PNat. n+1 is mapped to itself, and 0 becomes 1.

Equations

• Nat.toPNat' n = Nat.succPNat (Nat.pred n)

ink

@[simp]

theorem Nat.toPNat'_coe (n : ℕ) : ↑(Nat.toPNat' n) = if 0 < n then n else 1

ink

theorem PNat.mk_le_mk (n : ℕ) (k : ℕ) (hn : 0 < n) (hk : 0 < k) : { val := n, property := hn } ≤ { val := k, property := hk } ↔ n ≤ k

We now define a long list of structures on ℕ+ induced by similar structures on ℕ. Most of these behave in a completely obvious way, but there are a few things to be said about subtraction, division and powers.

ink

theorem PNat.mk_lt_mk (n : ℕ) (k : ℕ) (hn : 0 < n) (hk : 0 < k) : { val := n, property := hn } < { val := k, property := hk } ↔ n < k

ink

@[simp]

theorem PNat.coe_le_coe (n : ℕ+) (k : ℕ+) : ↑n ≤ ↑k ↔ n ≤ k

ink

@[simp]

theorem PNat.coe_lt_coe (n : ℕ+) (k : ℕ+) : ↑n < ↑k ↔ n < k

ink

@[simp]

theorem PNat.pos (n : ℕ+) : 0 < ↑n

ink

theorem PNat.eq {m : ℕ+} {n : ℕ+} : ↑m = ↑n → m = n

ink

theorem PNat.coe_injective : Function.Injective fun a => ↑a

ink

@[simp]

theorem PNat.ne_zero (n : ℕ+) : ↑n ≠ 0

ink

instance NeZero.pnat {a : ℕ+} : NeZero ↑a

Equations

• @NeZero.pnat = @NeZero.pnat.proof_1

ink

theorem PNat.toPNat'_coe {n : ℕ} : 0 < n → ↑(Nat.toPNat' n) = n

ink

@[simp]

theorem PNat.coe_toPNat' (n : ℕ+) : Nat.toPNat' ↑n = n

ink

@[simp]

theorem PNat.one_le (n : ℕ+) : 1 ≤ n

ink

@[simp]

theorem PNat.not_lt_one (n : ℕ+) : ¬n < 1

ink

instance PNat.instInhabitedPNat : Inhabited ℕ+

Equations

• PNat.instInhabitedPNat = { default := 1 }

ink

@[simp]

theorem PNat.mk_one {h : 0 < 1} : { val := 1, property := h } = 1

ink

@[simp]

theorem PNat.one_coe : ↑1 = 1

ink

@[simp]

theorem PNat.coe_eq_one_iff {m : ℕ+} : ↑m = 1 ↔ m = 1

ink

instance PNat.instWellFoundedRelationPNat : WellFoundedRelation ℕ+

Equations

• PNat.instWellFoundedRelationPNat = measure fun a => ↑a

ink

def PNat.strongInductionOn {p : ℕ+ → Sort u_1} (n : ℕ+) : ((k : ℕ+) → ((m : ℕ+) → m < k → p m) → p k) → p n

Strong induction on ℕ+.

Equations

• PNat.strongInductionOn n x = x n fun a x => PNat.strongInductionOn a x

ink

def PNat.modDivAux : ℕ+ → ℕ → ℕ → ℕ+ × ℕ

We define m % k and m / k in the same way as for ℕ except that when m = n * k we take m % k = k and m / k = n - 1. This ensures that m % k is always positive and m = (m % k) + k * (m / k) in all cases. Later we define a function div_exact which gives the usual m / k in the case where k divides m.

Equations

• PNat.modDivAux x x x = match x, x, x with | k, 0, q => (k, Nat.pred q) | x, Nat.succ r, q => ({ val := r + 1, property := (_ : 0 < Nat.succ r) }, q)

ink

def PNat.modDiv (m : ℕ+) (k : ℕ+) : ℕ+ × ℕ

mod_div m k = (m % k, m / k). We define m % k and m / k in the same way as for ℕ except that when m = n * k we take m % k = k and m / k = n - 1. This ensures that m % k is always positive and m = (m % k) + k * (m / k) in all cases. Later we define a function div_exact which gives the usual m / k in the case where k divides m.

Equations

• PNat.modDiv m k = PNat.modDivAux k (↑m % ↑k) (↑m / ↑k)

ink

def PNat.mod (m : ℕ+) (k : ℕ+) : ℕ+

We define m % k in the same way as for ℕ except that when m = n * k we take m % k = k This ensures that m % k is always positive.

Equations

• PNat.mod m k = (PNat.modDiv m k).fst

ink

def PNat.div (m : ℕ+) (k : ℕ+) : ℕ

We define m / k in the same way as for ℕ except that when m = n * k we take m / k = n - 1. This ensures that m = (m % k) + k * (m / k) in all cases. Later we define a function div_exact which gives the usual m / k in the case where k divides m.

Equations

• PNat.div m k = (PNat.modDiv m k).snd

ink

theorem PNat.mod_coe (m : ℕ+) (k : ℕ+) : ↑(PNat.mod m k) = if ↑m % ↑k = 0 then ↑k else ↑m % ↑k

ink

theorem PNat.div_coe (m : ℕ+) (k : ℕ+) : PNat.div m k = if ↑m % ↑k = 0 then Nat.pred (↑m / ↑k) else ↑m / ↑k

ink

def PNat.divExact (m : ℕ+) (k : ℕ+) : ℕ+

If h : k | m, then k * (div_exact m k) = m. Note that this is not equal to m / k.

Equations

• PNat.divExact m k = { val := Nat.succ (PNat.div m k), property := (_ : 0 < Nat.succ (PNat.div m k)) }

ink

instance Nat.canLiftPNat : CanLift ℕ ℕ+ PNat.val fun n => 0 < n

Equations

• Nat.canLiftPNat = { prf := Nat.canLiftPNat.proof_1 }

ink

instance Int.canLiftPNat : CanLift ℤ ℕ+ (fun x => ↑↑x) fun x => 0 < x

Equations

• Int.canLiftPNat = { prf := Int.canLiftPNat.proof_1 }