The positive natural numbers #
This file defines the type ℕ+
or pnat
, the subtype of natural numbers that are positive.
ℕ+
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.
Instances for pnat
- pnat.add_left_cancel_semigroup
- pnat.add_right_cancel_semigroup
- pnat.add_comm_semigroup
- pnat.linear_ordered_cancel_comm_monoid
- pnat.linear_order
- pnat.has_add
- pnat.has_mul
- pnat.has_one
- pnat.distrib
- coe_pnat_nat
- pnat.has_repr
- pnat.has_le.le.covariant_class
- pnat.has_lt.lt.covariant_class
- pnat.has_le.le.contravariant_class
- pnat.has_lt.lt.contravariant_class
- pnat.order_bot
- pnat.inhabited
- pnat.has_sub
- pnat.has_well_founded
- nat.can_lift_pnat
- int.can_lift_pnat
- pnat.encodable
- pnat.countable
- denumerable.pnat
- pnat.locally_finite_order
- nat.primes.coe_pnat
- slim_check.pnat.sampleable
Equations
- coe_pnat_nat = {coe := subtype.val (λ (n : ℕ), 0 < n)}
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.
pnat.coe
promoted to an add_hom
, that is, a morphism which preserves addition.
Equations
An equivalence between ℕ+
and ℕ
given by pnat.nat_pred
and nat.succ_pnat
.
Equations
The order isomorphism between ℕ and ℕ+ given by succ
.
Equations
- order_iso.pnat_iso_nat = {to_equiv := equiv.pnat_equiv_nat, map_rel_iff' := order_iso.pnat_iso_nat._proof_1}
Equations
- pnat.order_bot = {bot := 1, bot_le := pnat.order_bot._proof_1}
Equations
- pnat.inhabited = {default := 1}
pnat.coe
promoted to a monoid_hom
.
Equations
Equations
- pnat.has_well_founded = {r := has_lt.lt (preorder.to_has_lt ℕ+), wf := pnat.has_well_founded._proof_1}
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)
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)
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)
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)
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
.
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
- nat.can_lift_pnat = {coe := coe coe_to_lift, cond := λ (n : ℕ), 0 < n, prf := nat.can_lift_pnat._proof_1}
Equations
- int.can_lift_pnat = {coe := coe coe_to_lift, cond := λ (n : ℤ), 0 < n, prf := int.can_lift_pnat._proof_1}