data.pnat.basic - mathlib docs

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}

source

@[protected, instance]

def coe_pnat_nat :

has_coe ℕ+ ℕ

Equations

coe_pnat_nat = {coe := subtype.val (λ (n : ℕ), 0 < n)}

source

@[protected, instance]

def pnat.has_repr :

has_repr ℕ+

Equations

pnat.has_repr = {repr := λ (n : ℕ+), repr n.val}

source

def pnat.nat_pred (i : ℕ+) :

ℕ

Predecessor of a ℕ+, as a ℕ.

Equations

i.nat_pred = ↑i - 1

source

@[simp]

theorem pnat.one_add_nat_pred (n : ℕ+) :

1 + n.nat_pred = ↑n

source

@[simp]

theorem pnat.nat_pred_add_one (n : ℕ+) :

n.nat_pred + 1 = ↑n

source

@[simp]

theorem pnat.nat_pred_eq_pred {n : ℕ} (h : 0 < n) :

pnat.nat_pred ⟨n, h⟩ = n.pred

source

def nat.to_pnat (n : ℕ) (h : 0 < n . "exact_dec_trivial") :

ℕ+

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

Equations

n.to_pnat h = ⟨n, h⟩

source

def nat.succ_pnat (n : ℕ) :

ℕ+

Write a successor as an element of ℕ+.

Equations

n.succ_pnat = ⟨n.succ, _⟩

source

@[simp]

theorem nat.succ_pnat_coe (n : ℕ) :

↑(n.succ_pnat) = n.succ

source

theorem nat.succ_pnat_inj {n m : ℕ} :

n.succ_pnat = m.succ_pnat → n = m

source

def nat.to_pnat' (n : ℕ) :

ℕ+

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

Equations

n.to_pnat' = n.pred.succ_pnat

source

@[simp]

theorem nat.to_pnat'_coe (n : ℕ) :

↑(n.to_pnat') = ite (0 < n) n 1

source

@[protected, instance]

def pnat.decidable_eq :

decidable_eq ℕ+

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.

Equations

pnat.decidable_eq = λ (a b : ℕ+), subtype.decidable_eq a b

source

@[protected, instance]

def pnat.linear_order :

linear_order ℕ+

Equations

pnat.linear_order = subtype.linear_order (λ (n : ℕ), 0 < n)

source

@[simp]

theorem pnat.mk_le_mk (n k : ℕ) (hn : 0 < n) (hk : 0 < k) :

⟨n, hn⟩ ≤ ⟨k, hk⟩ ↔ n ≤ k

source

@[simp]

theorem pnat.mk_lt_mk (n k : ℕ) (hn : 0 < n) (hk : 0 < k) :

⟨n, hn⟩ < ⟨k, hk⟩ ↔ n < k

source

@[simp, norm_cast]

theorem pnat.coe_le_coe (n k : ℕ+) :

↑n ≤ ↑k ↔ n ≤ k

source

@[simp, norm_cast]

theorem pnat.coe_lt_coe (n k : ℕ+) :

↑n < ↑k ↔ n < k

source

@[simp]

theorem pnat.pos (n : ℕ+) :

0 < ↑n

source

theorem pnat.fact_pos (n : ℕ+) :

fact (0 < ↑n)

source

theorem pnat.eq {m n : ℕ+} :

↑m = ↑n → m = n

source

@[simp]

theorem pnat.coe_inj {m n : ℕ+} :

↑m = ↑n ↔ m = n

source

theorem pnat.coe_injective :

function.injective coe

source

@[simp]

theorem pnat.mk_coe (n : ℕ) (h : 0 < n) :

↑⟨n, h⟩ = n

source

@[protected, instance]

def pnat.has_add :

has_add ℕ+

Equations

pnat.has_add = {add := λ (a b : ℕ+), ⟨↑a + ↑b, _⟩}

source

@[protected, instance]

def pnat.add_comm_semigroup :

add_comm_semigroup ℕ+

Equations

pnat.add_comm_semigroup = function.injective.add_comm_semigroup coe pnat.coe_injective pnat.add_comm_semigroup._proof_1

source

@[simp]

theorem pnat.add_coe (m n : ℕ+) :

↑(m + n) = ↑m + ↑n

source

def pnat.coe_add_hom :

add_hom ℕ+ ℕ

pnat.coe promoted to an add_hom, that is, a morphism which preserves addition.

Equations

pnat.coe_add_hom = {to_fun := coe coe_to_lift, map_add' := pnat.add_coe}

source

@[protected, instance]

def pnat.add_left_cancel_semigroup :

add_left_cancel_semigroup ℕ+

Equations

pnat.add_left_cancel_semigroup = function.injective.add_left_cancel_semigroup coe pnat.coe_injective pnat.add_left_cancel_semigroup._proof_1

source

@[protected, instance]

def pnat.add_right_cancel_semigroup :

add_right_cancel_semigroup ℕ+

Equations

pnat.add_right_cancel_semigroup = function.injective.add_right_cancel_semigroup coe pnat.coe_injective pnat.add_right_cancel_semigroup._proof_1

source

@[protected, instance]

def pnat.has_le.le.covariant_class :

covariant_class ℕ+ ℕ+ has_add.add has_le.le

source

@[simp]

theorem pnat.ne_zero (n : ℕ+) :

↑n ≠ 0

source

theorem pnat.to_pnat'_coe {n : ℕ} :

0 < n → ↑(n.to_pnat') = n

source

@[simp]

theorem pnat.coe_to_pnat' (n : ℕ+) :

↑n.to_pnat' = n

source

@[protected, instance]

def pnat.has_mul :

has_mul ℕ+

Equations

pnat.has_mul = {mul := λ (m n : ℕ+), ⟨(m.val) * n.val, _⟩}

source

@[protected, instance]

def pnat.has_one :

has_one ℕ+

Equations

pnat.has_one = {one := 0.succ_pnat}

source

@[protected, instance]

def pnat.nat.has_pow :

has_pow ℕ+ ℕ

Equations

pnat.nat.has_pow = {pow := λ (x : ℕ+) (n : ℕ), ⟨↑x ^ n, _⟩}

source

@[protected, instance]

def pnat.comm_monoid :

comm_monoid ℕ+

Equations

pnat.comm_monoid = function.injective.comm_monoid coe pnat.coe_injective pnat.comm_monoid._proof_1 pnat.comm_monoid._proof_2 pnat.comm_monoid._proof_3

source

theorem pnat.lt_add_one_iff {a b : ℕ+} :

a < b + 1 ↔ a ≤ b

source

theorem pnat.add_one_le_iff {a b : ℕ+} :

a + 1 ≤ b ↔ a < b

source

@[simp]

theorem pnat.one_le (n : ℕ+) :

1 ≤ n

source

@[simp]

theorem pnat.not_lt_one (n : ℕ+) :

¬n < 1

source

@[protected, instance]

def pnat.order_bot :

order_bot ℕ+

Equations

pnat.order_bot = {bot := 1, bot_le := pnat.order_bot._proof_1}

source

@[simp]

theorem pnat.bot_eq_one :

⊥ = 1

source

@[protected, instance]

def pnat.inhabited :

inhabited ℕ+

Equations

pnat.inhabited = {default := 1}

source

@[simp]

theorem pnat.mk_one {h : 0 < 1} :

⟨1, h⟩ = 1

source

@[simp]

theorem pnat.mk_bit0 (n : ℕ) {h : 0 < bit0 n} :

⟨bit0 n, h⟩ = bit0 ⟨n, _⟩

source

@[simp]

theorem pnat.mk_bit1 (n : ℕ) {h : 0 < bit1 n} {k : 0 < n} :

⟨bit1 n, h⟩ = bit1 ⟨n, k⟩

source

@[simp]

theorem pnat.bit0_le_bit0 (n m : ℕ+) :

bit0 n ≤ bit0 m ↔ bit0 ↑n ≤ bit0 ↑m

source

@[simp]

theorem pnat.bit0_le_bit1 (n m : ℕ+) :

bit0 n ≤ bit1 m ↔ bit0 ↑n ≤ bit1 ↑m

source

@[simp]

theorem pnat.bit1_le_bit0 (n m : ℕ+) :

bit1 n ≤ bit0 m ↔ bit1 ↑n ≤ bit0 ↑m

source

@[simp]

theorem pnat.bit1_le_bit1 (n m : ℕ+) :

bit1 n ≤ bit1 m ↔ bit1 ↑n ≤ bit1 ↑m

source

@[simp]

theorem pnat.one_coe :

↑1 = 1

source

@[simp]

theorem pnat.mul_coe (m n : ℕ+) :

↑m * n = (↑m) * ↑n

source

def pnat.coe_monoid_hom :

ℕ+ →* ℕ

pnat.coe promoted to a monoid_hom.

Equations

pnat.coe_monoid_hom = {to_fun := coe coe_to_lift, map_one' := pnat.one_coe, map_mul' := pnat.mul_coe}

source

@[simp]

theorem pnat.coe_coe_monoid_hom :

⇑pnat.coe_monoid_hom = coe

source

@[simp]

theorem pnat.coe_eq_one_iff {m : ℕ+} :

↑m = 1 ↔ m = 1

source

@[simp]

theorem pnat.le_one_iff {n : ℕ+} :

n ≤ 1 ↔ n = 1

source

theorem pnat.lt_add_left (n m : ℕ+) :

n < m + n

source

theorem pnat.lt_add_right (n m : ℕ+) :

n < n + m

source

@[simp]

theorem pnat.coe_bit0 (a : ℕ+) :

↑(bit0 a) = bit0 ↑a

source

@[simp]

theorem pnat.coe_bit1 (a : ℕ+) :

↑(bit1 a) = bit1 ↑a

source

@[simp]

theorem pnat.pow_coe (m : ℕ+) (n : ℕ) :

↑(m ^ n) = ↑m ^ n

source

@[protected, instance]

def pnat.ordered_cancel_comm_monoid :

ordered_cancel_comm_monoid ℕ+

Equations

pnat.ordered_cancel_comm_monoid = {mul := comm_monoid.mul pnat.comm_monoid, mul_assoc := _, mul_left_cancel := pnat.ordered_cancel_comm_monoid._proof_1, one := comm_monoid.one pnat.comm_monoid, one_mul := _, mul_one := _, npow := comm_monoid.npow pnat.comm_monoid, npow_zero' := _, npow_succ' := _, mul_comm := _, le := linear_order.le pnat.linear_order, lt := linear_order.lt pnat.linear_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, mul_le_mul_left := pnat.ordered_cancel_comm_monoid._proof_2, le_of_mul_le_mul_left := pnat.ordered_cancel_comm_monoid._proof_3}

source

@[protected, instance]

def pnat.distrib :

distrib ℕ+

Equations

pnat.distrib = function.injective.distrib coe pnat.coe_injective pnat.distrib._proof_1 pnat.distrib._proof_2

source

@[protected, instance]

def pnat.has_sub :

has_sub ℕ+

Subtraction a - b is defined in the obvious way when a > b, and by a - b = 1 if a ≤ b.

Equations

pnat.has_sub = {sub := λ (a b : ℕ+), (↑a - ↑b).to_pnat'}

source

theorem pnat.sub_coe (a b : ℕ+) :

↑(a - b) = ite (b < a) (↑a - ↑b) 1

source

theorem pnat.add_sub_of_lt {a b : ℕ+} :

a < b → a + (b - a) = b

source

@[protected, instance]

def pnat.has_well_founded :

has_well_founded ℕ+

Equations

pnat.has_well_founded = {r := has_lt.lt (preorder.to_has_lt ℕ+), wf := pnat.has_well_founded._proof_1}

source

def pnat.strong_induction_on {p : ℕ+ → Sort u_1} (n : ℕ+) (h : Π (k : ℕ+), (Π (m : ℕ+), m < k → p m) → p k) :

p n

Strong induction on ℕ+.

Equations

n.strong_induction_on = λ (IH : Π (k : ℕ+), (Π (m : ℕ+), m < k → p m) → p k), IH n (λ (a : ℕ+) (h : a < n), a.strong_induction_on IH)

source

theorem pnat.exists_eq_succ_of_ne_one {n : ℕ+} (h1 : n ≠ 1) :

∃ (k : ℕ+), n = k + 1

If n : ℕ+ is different from 1, then it is the successor of some k : ℕ+.

source

def pnat.case_strong_induction_on {p : ℕ+ → Sort u_1} (a : ℕ+) (hz : p 1) (hi : Π (n : ℕ+), (Π (m : ℕ+), m ≤ n → p m) → p (n + 1)) :

p a

Strong induction on ℕ+, with n = 1 treated separately.

Equations

a.case_strong_induction_on hz hi = a.strong_induction_on (λ (k : ℕ+) (hk : Π (m : ℕ+), m < k → p m), subtype.cases_on k (λ (k : ℕ) (kprop : 0 < k) (hk : Π (m : ℕ+), m < ⟨k, kprop⟩ → p m), k.cases_on (λ (kprop : 0 < 0) (hk : Π (m : ℕ+), m < ⟨0, kprop⟩ → p m), _.elim) (λ (k : ℕ) (kprop : 0 < k.succ) (hk : Π (m : ℕ+), m < ⟨k.succ, kprop⟩ → p m), k.cases_on (λ (kprop : 0 < 1) (hk : Π (m : ℕ+), m < ⟨1, kprop⟩ → p m), hz) (λ (k : ℕ) (kprop : 0 < k.succ.succ) (hk : Π (m : ℕ+), m < ⟨k.succ.succ, kprop⟩ → p m), hi ⟨k.succ, _⟩ (λ (m : ℕ+) (hm : m ≤ ⟨k.succ, _⟩), hk m _)) kprop hk) kprop hk) hk)

source

def pnat.rec_on (n : ℕ+) {p : ℕ+ → Sort u_1} (p1 : p 1) (hp : Π (n : ℕ+), p n → p (n + 1)) :

p n

An induction principle for ℕ+: it takes values in Sort*, so it applies also to Types, not only to Prop.

Equations

n.rec_on p1 hp = subtype.cases_on n (λ (n : ℕ) (h : 0 < n), nat.rec (λ (h : 0 < 0), absurd h pnat.rec_on._proof_1) (λ (n : ℕ) (IH : Π (h : 0 < n), p ⟨n, h⟩) (h : 0 < n.succ), n.cases_on (λ (IH : Π (h : 0 < 0), p ⟨0, h⟩) (h : 0 < 1), p1) (λ (n : ℕ) (IH : Π (h : 0 < n.succ), p ⟨n.succ, h⟩) (h : 0 < n.succ.succ), hp ⟨n.succ, _⟩ (IH _)) IH h) n h)

source

@[simp]

theorem pnat.rec_on_one {p : ℕ+ → Sort u_1} (p1 : p 1) (hp : Π (n : ℕ+), p n → p (n + 1)) :

1.rec_on p1 hp = p1

source

@[simp]

theorem pnat.rec_on_succ (n : ℕ+) {p : ℕ+ → Sort u_1} (p1 : p 1) (hp : Π (n : ℕ+), p n → p (n + 1)) :

(n + 1).rec_on p1 hp = hp n (n.rec_on p1 hp)

source

def pnat.mod_div_aux :

ℕ+ → ℕ → ℕ → ℕ+ × ℕ

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

k.mod_div_aux (r + 1) q = (⟨r + 1, _⟩, q)
k.mod_div_aux 0 q = (k, q.pred)

source

theorem pnat.mod_div_aux_spec (k : ℕ+) (r q : ℕ) (h : ¬(r = 0 ∧ q = 0)) :

↑((k.mod_div_aux r q).fst) + (↑k) * (k.mod_div_aux r q).snd = r + (↑k) * q

source

def pnat.mod_div (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

m.mod_div k = k.mod_div_aux (↑m % ↑k) (↑m / ↑k)

source

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

m.mod k = (m.mod_div k).fst

source

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