Basic lemmas about natural numbers #
The primary purpose of the lemmas in this file is to assist with reasoning about sizes of objects, array indices and such.
This file was upstreamed from Std, and later these lemmas should be organised into other files more systematically.
@[reducible, inline, deprecated Nat.and_forall_add_one (since := "2024-07-30")]
Equations
@[reducible, inline, deprecated Nat.or_exists_add_one (since := "2024-07-30")]
Equations
add #
sub #
@[reducible, inline]
Equations
min/max #
mul #
div/mod #
pow #
@[reducible, inline]
@[reducible, inline]
log2 #
dvd #
shiftLeft and shiftRight #
Decidability of predicates #
Equations
- Nat.decidableForallFin P = decidable_of_iff (∀ (k : Nat) (h : k < n), P ⟨k, h⟩) ⋯
instance
Nat.decidableExistsLT
{p : Nat → Prop}
[h : DecidablePred p]
:
DecidablePred fun (n : Nat) => ∃ (m : Nat), m < n ∧ p m
Equations
- Nat.decidableExistsLT 0 = isFalse ⋯
- n.succ.decidableExistsLT = decidable_of_decidable_of_iff ⋯
instance
Nat.decidableExistsLE
{p : Nat → Prop}
[DecidablePred p]
:
DecidablePred fun (n : Nat) => ∃ (m : Nat), m ≤ n ∧ p m
instance
Nat.decidableExistsLT'
{k : Nat}
{p : (m : Nat) → m < k → Prop}
[I : (m : Nat) → (h : m < k) → Decidable (p m h)]
:
Dependent version of decidableExistsLT
.
Equations
- Nat.decidableExistsLT' = isFalse ⋯
- Nat.decidableExistsLT' = decidable_of_iff ((∃ (m : Nat), ∃ (h : m < n), P m ⋯) ∨ P n ⋯) ⋯
instance
Nat.decidableExistsLE'
{k : Nat}
{p : (m : Nat) → m ≤ k → Prop}
[I : (m : Nat) → (h : m ≤ k) → Decidable (p m h)]
:
Dependent version of decidableExistsLE
.
Equations
- Nat.decidableExistsLE' = decidable_of_iff (∃ (m : Nat), ∃ (h : m < k + 1), p m ⋯) ⋯