chore: move String.utf8EncodeChar to the prelude (#10264)
This PR moves `String.utf8EncodeChar` to the prelude to prepare for the imminent redefinition of `String`. The definition in the prelude uses modulo and division operations on natural numbers. In `String.Extra`, a `csimp` lemma is provided, showing that the new definition is equal to the previous one (which is now called `utf8EncodeCharFast`) which uses bitwise operations on `UInt8`.
This commit is contained in:
Markus Himmel
GitHub
parent
0b3550f284
commit
19bd0254c3
14 changed files with 325 additions and 223 deletions
|
|
@ -21,13 +21,6 @@ namespace BitVec
|
|||
|
||||
section Nat
|
||||
|
||||
/--
|
||||
The bitvector with value `i mod 2^n`.
|
||||
-/
|
||||
@[expose, match_pattern]
|
||||
protected def ofNat (n : Nat) (i : Nat) : BitVec n where
|
||||
toFin := Fin.ofNat (2^n) i
|
||||
|
||||
instance instOfNat : OfNat (BitVec n) i where ofNat := .ofNat n i
|
||||
|
||||
/-- Return the bound in terms of toNat. -/
|
||||
|
|
|
|||
|
|
@ -122,7 +122,7 @@ theorem getElem_of_getLsbD_eq_true {x : BitVec w} {i : Nat} (h : x.getLsbD i = t
|
|||
This normalized a bitvec using `ofFin` to `ofNat`.
|
||||
-/
|
||||
theorem ofFin_eq_ofNat : @BitVec.ofFin w (Fin.mk x lt) = BitVec.ofNat w x := by
|
||||
simp only [BitVec.ofNat, Fin.ofNat, lt, Nat.mod_eq_of_lt]
|
||||
simp only [BitVec.ofNat, Fin.Internal.ofNat_eq_ofNat, Fin.ofNat, lt, Nat.mod_eq_of_lt]
|
||||
|
||||
/-- Prove nonequality of bitvectors in terms of nat operations. -/
|
||||
theorem toNat_ne_iff_ne {n} {x y : BitVec n} : x.toNat ≠ y.toNat ↔ x ≠ y := by
|
||||
|
|
@ -299,7 +299,7 @@ theorem length_pos_of_ne {x y : BitVec w} (h : x ≠ y) : 0 < w :=
|
|||
|
||||
theorem ofFin_ofNat (n : Nat) :
|
||||
ofFin (no_index (OfNat.ofNat n : Fin (2^w))) = OfNat.ofNat n := by
|
||||
simp only [OfNat.ofNat, Fin.ofNat, BitVec.ofNat]
|
||||
simp only [OfNat.ofNat, Fin.Internal.ofNat_eq_ofNat, Fin.ofNat, BitVec.ofNat]
|
||||
|
||||
-- We use a `grind_pattern` as `@[grind]` will not use the `no_index` term.
|
||||
grind_pattern ofFin_ofNat => ofFin (OfNat.ofNat n : Fin (2^w))
|
||||
|
|
|
|||
|
|
@ -51,6 +51,11 @@ The assumption `NeZero n` ensures that `Fin n` is nonempty.
|
|||
@[expose] protected def ofNat (n : Nat) [NeZero n] (a : Nat) : Fin n :=
|
||||
⟨a % n, Nat.mod_lt _ (pos_of_neZero n)⟩
|
||||
|
||||
@[simp]
|
||||
theorem Internal.ofNat_eq_ofNat {n : Nat} {hn} {a : Nat} :
|
||||
letI : NeZero n := ⟨Nat.pos_iff_ne_zero.1 hn⟩
|
||||
Fin.Internal.ofNat n hn a = Fin.ofNat n a := rfl
|
||||
|
||||
@[deprecated Fin.ofNat (since := "2025-05-28")]
|
||||
protected def ofNat' (n : Nat) [NeZero n] (a : Nat) : Fin n :=
|
||||
Fin.ofNat n a
|
||||
|
|
|
|||
|
|
@ -257,8 +257,6 @@ attribute [simp] Nat.le_refl
|
|||
|
||||
theorem succ_lt_succ {n m : Nat} : n < m → succ n < succ m := succ_le_succ
|
||||
|
||||
theorem lt_succ_of_le {n m : Nat} : n ≤ m → n < succ m := succ_le_succ
|
||||
|
||||
theorem le_of_lt_add_one {n m : Nat} : n < m + 1 → n ≤ m := le_of_succ_le_succ
|
||||
|
||||
theorem lt_add_one_of_le {n m : Nat} : n ≤ m → n < m + 1 := succ_le_succ
|
||||
|
|
@ -271,37 +269,15 @@ theorem not_add_one_le_self : (n : Nat) → ¬ n + 1 ≤ n := Nat.not_succ_le_se
|
|||
|
||||
theorem add_one_pos (n : Nat) : 0 < n + 1 := Nat.zero_lt_succ n
|
||||
|
||||
theorem succ_sub_succ_eq_sub (n m : Nat) : succ n - succ m = n - m := by
|
||||
induction m with
|
||||
| zero => exact rfl
|
||||
| succ m ih => apply congrArg pred ih
|
||||
|
||||
theorem pred_le : ∀ (n : Nat), pred n ≤ n
|
||||
| zero => Nat.le.refl
|
||||
| succ _ => le_succ _
|
||||
|
||||
theorem pred_lt : ∀ {n : Nat}, n ≠ 0 → pred n < n
|
||||
| zero, h => absurd rfl h
|
||||
| succ _, _ => lt_succ_of_le (Nat.le_refl _)
|
||||
|
||||
theorem sub_one_lt : ∀ {n : Nat}, n ≠ 0 → n - 1 < n := pred_lt
|
||||
|
||||
@[simp] theorem sub_le (n m : Nat) : n - m ≤ n := by
|
||||
induction m with
|
||||
| zero => exact Nat.le_refl (n - 0)
|
||||
| succ m ih => apply Nat.le_trans (pred_le (n - m)) ih
|
||||
|
||||
theorem sub_lt_of_lt {a b c : Nat} (h : a < c) : a - b < c :=
|
||||
Nat.lt_of_le_of_lt (Nat.sub_le _ _) h
|
||||
|
||||
theorem sub_lt : ∀ {n m : Nat}, 0 < n → 0 < m → n - m < n
|
||||
| 0, _, h1, _ => absurd h1 (Nat.lt_irrefl 0)
|
||||
| _+1, 0, _, h2 => absurd h2 (Nat.lt_irrefl 0)
|
||||
| n+1, m+1, _, _ =>
|
||||
Eq.symm (succ_sub_succ_eq_sub n m) ▸
|
||||
show n - m < succ n from
|
||||
lt_succ_of_le (sub_le n m)
|
||||
|
||||
theorem sub_succ (n m : Nat) : n - succ m = pred (n - m) := rfl
|
||||
|
||||
theorem succ_sub_succ (n m : Nat) : succ n - succ m = n - m :=
|
||||
|
|
@ -316,9 +292,6 @@ theorem sub_add_eq (a b c : Nat) : a - (b + c) = a - b - c := by
|
|||
| zero => simp
|
||||
| succ c ih => simp only [Nat.add_succ, Nat.sub_succ, ih]
|
||||
|
||||
protected theorem lt_of_lt_of_le {n m k : Nat} : n < m → m ≤ k → n < k :=
|
||||
Nat.le_trans
|
||||
|
||||
protected theorem lt_of_lt_of_eq {n m k : Nat} : n < m → m = k → n < k :=
|
||||
fun h₁ h₂ => h₂ ▸ h₁
|
||||
|
||||
|
|
@ -356,12 +329,10 @@ protected theorem pos_of_ne_zero {n : Nat} : n ≠ 0 → 0 < n := (eq_zero_or_po
|
|||
|
||||
theorem pos_of_neZero (n : Nat) [NeZero n] : 0 < n := Nat.pos_of_ne_zero (NeZero.ne _)
|
||||
|
||||
attribute [simp] Nat.lt_add_one
|
||||
|
||||
theorem lt.base (n : Nat) : n < succ n := Nat.le_refl (succ n)
|
||||
|
||||
theorem lt_succ_self (n : Nat) : n < succ n := lt.base n
|
||||
|
||||
@[simp] protected theorem lt_add_one (n : Nat) : n < n + 1 := lt.base n
|
||||
|
||||
protected theorem le_total (m n : Nat) : m ≤ n ∨ n ≤ m :=
|
||||
match Nat.lt_or_ge m n with
|
||||
| Or.inl h => Or.inl (Nat.le_of_lt h)
|
||||
|
|
@ -457,7 +428,6 @@ protected theorem le_lt_asymm : ∀{a b : Nat}, a ≤ b → ¬(b < a) := flip Na
|
|||
|
||||
theorem gt_of_not_le {n m : Nat} (h : ¬ n ≤ m) : n > m := (Nat.lt_or_ge m n).resolve_right h
|
||||
protected theorem lt_of_not_ge : ∀{a b : Nat}, ¬(b ≥ a) → b < a := Nat.gt_of_not_le
|
||||
protected theorem lt_of_not_le : ∀{a b : Nat}, ¬(a ≤ b) → b < a := Nat.gt_of_not_le
|
||||
|
||||
theorem ge_of_not_lt {n m : Nat} (h : ¬ n < m) : n ≥ m := (Nat.lt_or_ge n m).resolve_left h
|
||||
protected theorem le_of_not_gt : ∀{a b : Nat}, ¬(b > a) → b ≤ a := Nat.ge_of_not_lt
|
||||
|
|
@ -770,10 +740,6 @@ protected theorem mul_lt_mul_of_pos_left {n m k : Nat} (h : n < m) (hk : k > 0)
|
|||
protected theorem mul_lt_mul_of_pos_right {n m k : Nat} (h : n < m) (hk : k > 0) : n * k < m * k :=
|
||||
Nat.mul_comm k m ▸ Nat.mul_comm k n ▸ Nat.mul_lt_mul_of_pos_left h hk
|
||||
|
||||
protected theorem mul_pos {n m : Nat} (ha : n > 0) (hb : m > 0) : n * m > 0 :=
|
||||
have h : 0 * m < n * m := Nat.mul_lt_mul_of_pos_right ha hb
|
||||
Nat.zero_mul m ▸ h
|
||||
|
||||
protected theorem le_of_mul_le_mul_left {a b c : Nat} (h : c * a ≤ c * b) (hc : 0 < c) : a ≤ b :=
|
||||
Nat.ge_of_not_lt fun hlt : b < a =>
|
||||
have h' : c * b < c * a := Nat.mul_lt_mul_of_pos_left hlt hc
|
||||
|
|
@ -833,11 +799,6 @@ set_option linter.missingDocs false in
|
|||
@[deprecated Nat.pow_le_pow_right (since := "2025-02-17")]
|
||||
abbrev pow_le_pow_of_le_right := @Nat.pow_le_pow_right
|
||||
|
||||
protected theorem pow_pos (h : 0 < a) : 0 < a^n :=
|
||||
match n with
|
||||
| 0 => Nat.zero_lt_one
|
||||
| _ + 1 => Nat.mul_pos (Nat.pow_pos h) h
|
||||
|
||||
set_option linter.missingDocs false in
|
||||
@[deprecated Nat.pow_pos (since := "2025-02-17")]
|
||||
abbrev pos_pow_of_pos := @Nat.pow_pos
|
||||
|
|
@ -1199,6 +1160,8 @@ protected theorem sub_eq_iff_eq_add {c : Nat} (h : b ≤ a) : a - b = c ↔ a =
|
|||
protected theorem sub_eq_iff_eq_add' {c : Nat} (h : b ≤ a) : a - b = c ↔ a = b + c := by
|
||||
rw [Nat.add_comm, Nat.sub_eq_iff_eq_add h]
|
||||
|
||||
attribute [simp] sub_le
|
||||
|
||||
protected theorem sub_one_sub_lt_of_lt (h : a < b) : b - 1 - a < b := by
|
||||
rw [← Nat.sub_add_eq]
|
||||
exact sub_lt (zero_lt_of_lt h) (Nat.lt_add_right a Nat.one_pos)
|
||||
|
|
|
|||
|
|
@ -24,47 +24,6 @@ there is some `c` such that `b = a * c`.
|
|||
instance : Dvd Nat where
|
||||
dvd a b := Exists (fun c => b = a * c)
|
||||
|
||||
theorem div_rec_lemma {x y : Nat} : 0 < y ∧ y ≤ x → x - y < x :=
|
||||
fun ⟨ypos, ylex⟩ => sub_lt (Nat.lt_of_lt_of_le ypos ylex) ypos
|
||||
|
||||
theorem div_rec_fuel_lemma {x y fuel : Nat} (hy : 0 < y) (hle : y ≤ x) (hfuel : x < fuel + 1) :
|
||||
x - y < fuel :=
|
||||
Nat.lt_of_lt_of_le (div_rec_lemma ⟨hy, hle⟩) (Nat.le_of_lt_succ hfuel)
|
||||
|
||||
/--
|
||||
Division of natural numbers, discarding the remainder. Division by `0` returns `0`. Usually accessed
|
||||
via the `/` operator.
|
||||
|
||||
This operation is sometimes called “floor division.”
|
||||
|
||||
This function is overridden at runtime with an efficient implementation. This definition is
|
||||
the logical model.
|
||||
|
||||
Examples:
|
||||
* `21 / 3 = 7`
|
||||
* `21 / 5 = 4`
|
||||
* `0 / 22 = 0`
|
||||
* `5 / 0 = 0`
|
||||
-/
|
||||
@[extern "lean_nat_div", irreducible]
|
||||
protected def div (x y : @& Nat) : Nat :=
|
||||
if hy : 0 < y then
|
||||
let rec
|
||||
go (fuel : Nat) (x : Nat) (hfuel : x < fuel) : Nat :=
|
||||
match fuel with
|
||||
| 0 => by contradiction
|
||||
| succ fuel =>
|
||||
if h : y ≤ x then
|
||||
go fuel (x - y) (div_rec_fuel_lemma hy h hfuel) + 1
|
||||
else
|
||||
0
|
||||
termination_by structural fuel
|
||||
go (x + 1) x (Nat.lt_succ_self _)
|
||||
else
|
||||
0
|
||||
|
||||
instance instDiv : Div Nat := ⟨Nat.div⟩
|
||||
|
||||
private theorem div.go.fuel_congr (x y fuel1 fuel2 : Nat) (hy : 0 < y) (h1 : x < fuel1) (h2 : x < fuel2) :
|
||||
Nat.div.go y hy fuel1 x h1 = Nat.div.go y hy fuel2 x h2 := by
|
||||
match fuel1, fuel2 with
|
||||
|
|
@ -154,36 +113,6 @@ protected def divExact (x y : @& Nat) (h : y ∣ x) : Nat :=
|
|||
@[simp]
|
||||
theorem divExact_eq_div {x y : Nat} (h : y ∣ x) : x.divExact y h = x / y := rfl
|
||||
|
||||
/--
|
||||
The modulo operator, which computes the remainder when dividing one natural number by another.
|
||||
Usually accessed via the `%` operator. When the divisor is `0`, the result is the dividend rather
|
||||
than an error.
|
||||
|
||||
This is the core implementation of `Nat.mod`. It computes the correct result for any two closed
|
||||
natural numbers, but it does not have some convenient [definitional
|
||||
reductions](lean-manual://section/type-system) when the `Nat`s contain free variables. The wrapper
|
||||
`Nat.mod` handles those cases specially and then calls `Nat.modCore`.
|
||||
|
||||
This function is overridden at runtime with an efficient implementation. This definition is the
|
||||
logical model.
|
||||
-/
|
||||
@[extern "lean_nat_mod", irreducible]
|
||||
protected noncomputable def modCore (x y : Nat) : Nat :=
|
||||
if hy : 0 < y then
|
||||
let rec
|
||||
go (fuel : Nat) (x : Nat) (hfuel : x < fuel) : Nat :=
|
||||
match fuel with
|
||||
| 0 => by contradiction
|
||||
| succ fuel =>
|
||||
if h : y ≤ x then
|
||||
go fuel (x - y) (div_rec_fuel_lemma hy h hfuel)
|
||||
else
|
||||
x
|
||||
termination_by structural fuel
|
||||
go (x + 1) x (Nat.lt_succ_self _)
|
||||
else
|
||||
x
|
||||
|
||||
private theorem modCore.go.fuel_congr (x y fuel1 fuel2 : Nat) (hy : 0 < y) (h1 : x < fuel1) (h2 : x < fuel2) :
|
||||
Nat.modCore.go y hy fuel1 x h1 = Nat.modCore.go y hy fuel2 x h2 := by
|
||||
match fuel1, fuel2 with
|
||||
|
|
@ -214,51 +143,6 @@ protected theorem modCore_eq (x y : Nat) : Nat.modCore x y =
|
|||
next =>
|
||||
simp only [false_and, ↓reduceIte, *]
|
||||
|
||||
|
||||
/--
|
||||
The modulo operator, which computes the remainder when dividing one natural number by another.
|
||||
Usually accessed via the `%` operator. When the divisor is `0`, the result is the dividend rather
|
||||
than an error.
|
||||
|
||||
`Nat.mod` is a wrapper around `Nat.modCore` that special-cases two situations, giving better
|
||||
definitional reductions:
|
||||
* `Nat.mod 0 m` should reduce to `m`, for all terms `m : Nat`.
|
||||
* `Nat.mod n (m + n + 1)` should reduce to `n` for concrete `Nat` literals `n`.
|
||||
|
||||
These reductions help `Fin n` literals work well, because the `OfNat` instance for `Fin` uses
|
||||
`Nat.mod`. In particular, `(0 : Fin (n + 1)).val` should reduce definitionally to `0`. `Nat.modCore`
|
||||
can handle all numbers, but its definitional reductions are not as convenient.
|
||||
|
||||
This function is overridden at runtime with an efficient implementation. This definition is the
|
||||
logical model.
|
||||
|
||||
Examples:
|
||||
* `7 % 2 = 1`
|
||||
* `9 % 3 = 0`
|
||||
* `5 % 7 = 5`
|
||||
* `5 % 0 = 5`
|
||||
* `show ∀ (n : Nat), 0 % n = 0 from fun _ => rfl`
|
||||
* `show ∀ (m : Nat), 5 % (m + 6) = 5 from fun _ => rfl`
|
||||
-/
|
||||
@[extern "lean_nat_mod"]
|
||||
protected def mod : @& Nat → @& Nat → Nat
|
||||
/-
|
||||
Nat.modCore is defined with fuel and thus does not reduce with open terms very well.
|
||||
Nevertheless it is desirable for trivial `Nat.mod` calculations, namely
|
||||
* `Nat.mod 0 m` for all `m`
|
||||
* `Nat.mod n (m + n + 1)` for concrete literals `n`,
|
||||
to reduce definitionally.
|
||||
This property is desirable for `Fin n` literals, as it means `(ofNat 0 : Fin n).val = 0` by
|
||||
definition.
|
||||
-/
|
||||
| 0, _ => 0
|
||||
| n@(_ + 1), m =>
|
||||
if m ≤ n -- NB: if n < m does not reduce as well as `m ≤ n`!
|
||||
then Nat.modCore n m
|
||||
else n
|
||||
|
||||
instance instMod : Mod Nat := ⟨Nat.mod⟩
|
||||
|
||||
protected theorem modCore_eq_mod (n m : Nat) : Nat.modCore n m = n % m := by
|
||||
change Nat.modCore n m = Nat.mod n m
|
||||
match n, m with
|
||||
|
|
@ -315,24 +199,6 @@ theorem mod_eq_sub_mod {a b : Nat} (h : a ≥ b) : a % b = (a - b) % b :=
|
|||
| Or.inl h₁ => h₁.symm ▸ (Nat.sub_zero a).symm ▸ rfl
|
||||
| Or.inr h₁ => (mod_eq a b).symm ▸ if_pos ⟨h₁, h⟩
|
||||
|
||||
theorem mod_lt (x : Nat) {y : Nat} : y > 0 → x % y < y := by
|
||||
induction x, y using mod.inductionOn with
|
||||
| base x y h₁ =>
|
||||
intro h₂
|
||||
have h₁ : ¬ 0 < y ∨ ¬ y ≤ x := Decidable.not_and_iff_or_not.mp h₁
|
||||
match h₁ with
|
||||
| Or.inl h₁ => exact absurd h₂ h₁
|
||||
| Or.inr h₁ =>
|
||||
have hgt : y > x := gt_of_not_le h₁
|
||||
have heq : x % y = x := mod_eq_of_lt hgt
|
||||
rw [← heq] at hgt
|
||||
exact hgt
|
||||
| ind x y h h₂ =>
|
||||
intro h₃
|
||||
have ⟨_, h₁⟩ := h
|
||||
rw [mod_eq_sub_mod h₁]
|
||||
exact h₂ h₃
|
||||
|
||||
@[simp] protected theorem sub_mod_add_mod_cancel (a b : Nat) [NeZero a] : a - b % a + b % a = a := by
|
||||
rw [Nat.sub_add_cancel]
|
||||
cases a with
|
||||
|
|
|
|||
|
|
@ -264,9 +264,6 @@ protected theorem pos_of_lt_add_left : n < k + n → 0 < k := by
|
|||
protected theorem add_pos_left (h : 0 < m) (n) : 0 < m + n :=
|
||||
Nat.lt_of_lt_of_le h (Nat.le_add_right ..)
|
||||
|
||||
protected theorem add_pos_right (m) (h : 0 < n) : 0 < m + n :=
|
||||
Nat.lt_of_lt_of_le h (Nat.le_add_left ..)
|
||||
|
||||
protected theorem add_self_ne_one : ∀ n, n + n ≠ 1
|
||||
| n+1, h => by rw [Nat.succ_add, Nat.succ.injEq] at h; contradiction
|
||||
|
||||
|
|
|
|||
|
|
@ -11,6 +11,7 @@ import all Init.Data.ByteArray.Basic
|
|||
public import Init.Data.String.Basic
|
||||
import all Init.Data.String.Basic
|
||||
import Init.Data.UInt.Lemmas
|
||||
import Init.Data.UInt.Bitwise
|
||||
|
||||
public section
|
||||
|
||||
|
|
@ -135,7 +136,7 @@ the corresponding string, or panics if the array is not a valid UTF-8 encoding o
|
|||
/--
|
||||
Returns the sequence of bytes in a character's UTF-8 encoding.
|
||||
-/
|
||||
def utf8EncodeChar (c : Char) : List UInt8 :=
|
||||
def utf8EncodeCharFast (c : Char) : List UInt8 :=
|
||||
let v := c.val
|
||||
if v ≤ 0x7f then
|
||||
[v.toUInt8]
|
||||
|
|
@ -152,8 +153,58 @@ def utf8EncodeChar (c : Char) : List UInt8 :=
|
|||
(v >>> 6).toUInt8 &&& 0x3f ||| 0x80,
|
||||
v.toUInt8 &&& 0x3f ||| 0x80]
|
||||
|
||||
private theorem Nat.add_two_pow_eq_or_of_lt {b : Nat} (i : Nat) (b_lt : b < 2 ^ i) (a : Nat) :
|
||||
b + 2 ^ i * a = b ||| 2 ^ i * a := by
|
||||
rw [Nat.add_comm, Nat.or_comm, Nat.two_pow_add_eq_or_of_lt b_lt]
|
||||
|
||||
@[csimp]
|
||||
theorem utf8EncodeChar_eq_utf8EncodeCharFast : @utf8EncodeChar = @utf8EncodeCharFast := by
|
||||
funext c
|
||||
simp only [utf8EncodeChar, utf8EncodeCharFast, UInt8.ofNat_uInt32ToNat, UInt8.ofNat_add,
|
||||
UInt8.reduceOfNat, UInt32.le_iff_toNat_le, UInt32.reduceToNat]
|
||||
split
|
||||
· rfl
|
||||
· split
|
||||
· simp only [List.cons.injEq, ← UInt8.toNat_inj, UInt8.toNat_add, UInt8.toNat_ofNat',
|
||||
Nat.reducePow, UInt8.reduceToNat, Nat.mod_add_mod, UInt8.toNat_or, UInt8.toNat_and,
|
||||
UInt32.toNat_toUInt8, UInt32.toNat_shiftRight, UInt32.reduceToNat, Nat.reduceMod, and_true]
|
||||
refine ⟨?_, ?_⟩
|
||||
· rw [Nat.mod_eq_of_lt (by omega), Nat.add_two_pow_eq_or_of_lt 5 (by omega) 6,
|
||||
Nat.and_two_pow_sub_one_eq_mod _ 5, Nat.shiftRight_eq_div_pow,
|
||||
Nat.mod_eq_of_lt (b := 256) (by omega)]
|
||||
· rw [Nat.mod_eq_of_lt (by omega), Nat.add_two_pow_eq_or_of_lt 6 (by omega) 2,
|
||||
Nat.and_two_pow_sub_one_eq_mod _ 6, Nat.mod_mod_of_dvd _ (by decide)]
|
||||
· split
|
||||
· simp only [List.cons.injEq, ← UInt8.toNat_inj, UInt8.toNat_add, UInt8.toNat_ofNat',
|
||||
Nat.reducePow, UInt8.reduceToNat, Nat.mod_add_mod, UInt8.toNat_or, UInt8.toNat_and,
|
||||
UInt32.toNat_toUInt8, UInt32.toNat_shiftRight, UInt32.reduceToNat, Nat.reduceMod, and_true]
|
||||
refine ⟨?_, ?_, ?_⟩
|
||||
· rw [Nat.mod_eq_of_lt (by omega), Nat.add_two_pow_eq_or_of_lt 4 (by omega) 14,
|
||||
Nat.and_two_pow_sub_one_eq_mod _ 4, Nat.shiftRight_eq_div_pow,
|
||||
Nat.mod_eq_of_lt (b := 256) (by omega)]
|
||||
· rw [Nat.mod_eq_of_lt (by omega), Nat.add_two_pow_eq_or_of_lt 6 (by omega) 2,
|
||||
Nat.and_two_pow_sub_one_eq_mod _ 6, Nat.shiftRight_eq_div_pow,
|
||||
Nat.mod_mod_of_dvd (c.val.toNat / 2 ^ 6) (by decide)]
|
||||
· rw [Nat.mod_eq_of_lt (by omega), Nat.add_two_pow_eq_or_of_lt 6 (by omega) 2,
|
||||
Nat.and_two_pow_sub_one_eq_mod _ 6, Nat.mod_mod_of_dvd c.val.toNat (by decide)]
|
||||
· simp only [List.cons.injEq, ← UInt8.toNat_inj, UInt8.toNat_add, UInt8.toNat_ofNat',
|
||||
Nat.reducePow, UInt8.reduceToNat, Nat.mod_add_mod, UInt8.toNat_or, UInt8.toNat_and,
|
||||
UInt32.toNat_toUInt8, UInt32.toNat_shiftRight, UInt32.reduceToNat, Nat.reduceMod, and_true]
|
||||
refine ⟨?_, ?_, ?_, ?_⟩
|
||||
· rw [Nat.mod_eq_of_lt (by omega), Nat.add_two_pow_eq_or_of_lt 3 (by omega) 30,
|
||||
Nat.and_two_pow_sub_one_eq_mod _ 3, Nat.shiftRight_eq_div_pow,
|
||||
Nat.mod_mod_of_dvd _ (by decide)]
|
||||
· rw [Nat.mod_eq_of_lt (by omega), Nat.add_two_pow_eq_or_of_lt 6 (by omega) 2,
|
||||
Nat.and_two_pow_sub_one_eq_mod _ 6, Nat.shiftRight_eq_div_pow,
|
||||
Nat.mod_mod_of_dvd (c.val.toNat / 2 ^ 12) (by decide)]
|
||||
· rw [Nat.mod_eq_of_lt (by omega), Nat.add_two_pow_eq_or_of_lt 6 (by omega) 2,
|
||||
Nat.and_two_pow_sub_one_eq_mod _ 6, Nat.shiftRight_eq_div_pow,
|
||||
Nat.mod_mod_of_dvd (c.val.toNat / 2 ^ 6) (by decide)]
|
||||
· rw [Nat.mod_eq_of_lt (by omega), Nat.add_two_pow_eq_or_of_lt 6 (by omega) 2,
|
||||
Nat.and_two_pow_sub_one_eq_mod _ 6, Nat.mod_mod_of_dvd c.val.toNat (by decide)]
|
||||
|
||||
@[simp] theorem length_utf8EncodeChar (c : Char) : (utf8EncodeChar c).length = c.utf8Size := by
|
||||
simp [Char.utf8Size, utf8EncodeChar]
|
||||
simp [Char.utf8Size, utf8EncodeChar_eq_utf8EncodeCharFast, utf8EncodeCharFast]
|
||||
cases Decidable.em (c.val ≤ 0x7f) <;> simp [*]
|
||||
cases Decidable.em (c.val ≤ 0x7ff) <;> simp [*]
|
||||
cases Decidable.em (c.val ≤ 0xffff) <;> simp [*]
|
||||
|
|
|
|||
|
|
@ -29,21 +29,6 @@ def UInt8.toFin (x : UInt8) : Fin UInt8.size := x.toBitVec.toFin
|
|||
@[deprecated UInt8.toFin (since := "2025-02-12"), inherit_doc UInt8.toFin]
|
||||
def UInt8.val (x : UInt8) : Fin UInt8.size := x.toFin
|
||||
|
||||
/--
|
||||
Converts a natural number to an 8-bit unsigned integer, wrapping on overflow.
|
||||
|
||||
This function is overridden at runtime with an efficient implementation.
|
||||
|
||||
Examples:
|
||||
* `UInt8.ofNat 5 = 5`
|
||||
* `UInt8.ofNat 255 = 255`
|
||||
* `UInt8.ofNat 256 = 0`
|
||||
* `UInt8.ofNat 259 = 3`
|
||||
* `UInt8.ofNat 32770 = 2`
|
||||
-/
|
||||
@[extern "lean_uint8_of_nat"]
|
||||
def UInt8.ofNat (n : @& Nat) : UInt8 := ⟨BitVec.ofNat 8 n⟩
|
||||
|
||||
/--
|
||||
Converts a natural number to an 8-bit unsigned integer, returning the largest representable value if
|
||||
the number is too large.
|
||||
|
|
@ -222,8 +207,8 @@ instance UInt32.instOfNat : OfNat UInt32 n := ⟨UInt32.ofNat n⟩
|
|||
|
||||
theorem UInt32.ofNatLT_lt_of_lt {n m : Nat} (h1 : n < UInt32.size) (h2 : m < UInt32.size) :
|
||||
n < m → UInt32.ofNatLT n h1 < UInt32.ofNat m := by
|
||||
simp only [(· < ·), BitVec.toNat, ofNatLT, BitVec.ofNatLT, ofNat, BitVec.ofNat, Fin.ofNat,
|
||||
Nat.mod_eq_of_lt h2, imp_self]
|
||||
simp only [(· < ·), BitVec.toNat, ofNatLT, BitVec.ofNatLT, ofNat, BitVec.ofNat,
|
||||
Fin.Internal.ofNat_eq_ofNat, Fin.ofNat, Nat.mod_eq_of_lt h2, imp_self]
|
||||
|
||||
@[deprecated UInt32.ofNatLT_lt_of_lt (since := "2025-02-13")]
|
||||
theorem UInt32.ofNat'_lt_of_lt {n m : Nat} (h1 : n < UInt32.size) (h2 : m < UInt32.size) :
|
||||
|
|
@ -231,8 +216,8 @@ theorem UInt32.ofNat'_lt_of_lt {n m : Nat} (h1 : n < UInt32.size) (h2 : m < UInt
|
|||
|
||||
theorem UInt32.lt_ofNatLT_of_lt {n m : Nat} (h1 : n < UInt32.size) (h2 : m < UInt32.size) :
|
||||
m < n → UInt32.ofNat m < UInt32.ofNatLT n h1 := by
|
||||
simp only [(· < ·), BitVec.toNat, ofNatLT, BitVec.ofNatLT, ofNat, BitVec.ofNat, Fin.ofNat,
|
||||
Nat.mod_eq_of_lt h2, imp_self]
|
||||
simp only [(· < ·), BitVec.toNat, ofNatLT, BitVec.ofNatLT, ofNat, BitVec.ofNat, Fin.Internal.ofNat_eq_ofNat,
|
||||
Fin.ofNat, Nat.mod_eq_of_lt h2, imp_self]
|
||||
|
||||
@[deprecated UInt32.lt_ofNatLT_of_lt (since := "2025-02-13")]
|
||||
theorem UInt32.lt_ofNat'_of_lt {n m : Nat} (h1 : n < UInt32.size) (h2 : m < UInt32.size) :
|
||||
|
|
|
|||
|
|
@ -40,7 +40,7 @@ theorem intCast_ofNat (x : Nat) : (OfNat.ofNat (α := Int) x : UInt8) = OfNat.of
|
|||
rw [Int.toNat_emod (Int.zero_le_ofNat x) (by decide)]
|
||||
erw [Int.toNat_natCast]
|
||||
rw [Int.toNat_pow_of_nonneg (by decide)]
|
||||
simp only [ofNat, BitVec.ofNat, Fin.ofNat, Int.reduceToNat, Nat.dvd_refl,
|
||||
simp only [ofNat, BitVec.ofNat, Fin.Internal.ofNat_eq_ofNat, Fin.ofNat, Int.reduceToNat, Nat.dvd_refl,
|
||||
Nat.mod_mod_of_dvd, instOfNat]
|
||||
|
||||
end UInt8
|
||||
|
|
@ -70,7 +70,7 @@ theorem intCast_ofNat (x : Nat) : (OfNat.ofNat (α := Int) x : UInt16) = OfNat.o
|
|||
rw [Int.toNat_emod (Int.zero_le_ofNat x) (by decide)]
|
||||
erw [Int.toNat_natCast]
|
||||
rw [Int.toNat_pow_of_nonneg (by decide)]
|
||||
simp only [ofNat, BitVec.ofNat, Fin.ofNat, Int.reduceToNat, Nat.dvd_refl,
|
||||
simp only [ofNat, BitVec.ofNat, Fin.Internal.ofNat_eq_ofNat, Fin.ofNat, Int.reduceToNat, Nat.dvd_refl,
|
||||
Nat.mod_mod_of_dvd, instOfNat]
|
||||
|
||||
end UInt16
|
||||
|
|
@ -100,7 +100,7 @@ theorem intCast_ofNat (x : Nat) : (OfNat.ofNat (α := Int) x : UInt32) = OfNat.o
|
|||
rw [Int.toNat_emod (Int.zero_le_ofNat x) (by decide)]
|
||||
erw [Int.toNat_natCast]
|
||||
rw [Int.toNat_pow_of_nonneg (by decide)]
|
||||
simp only [ofNat, BitVec.ofNat, Fin.ofNat, Int.reduceToNat, Nat.dvd_refl,
|
||||
simp only [ofNat, BitVec.ofNat, Fin.Internal.ofNat_eq_ofNat, Fin.ofNat, Int.reduceToNat, Nat.dvd_refl,
|
||||
Nat.mod_mod_of_dvd, instOfNat]
|
||||
|
||||
end UInt32
|
||||
|
|
@ -130,7 +130,7 @@ theorem intCast_ofNat (x : Nat) : (OfNat.ofNat (α := Int) x : UInt64) = OfNat.o
|
|||
rw [Int.toNat_emod (Int.zero_le_ofNat x) (by decide)]
|
||||
erw [Int.toNat_natCast]
|
||||
rw [Int.toNat_pow_of_nonneg (by decide)]
|
||||
simp only [ofNat, BitVec.ofNat, Fin.ofNat, Int.reduceToNat, Nat.dvd_refl,
|
||||
simp only [ofNat, BitVec.ofNat, Fin.Internal.ofNat_eq_ofNat, Fin.ofNat, Int.reduceToNat, Nat.dvd_refl,
|
||||
Nat.mod_mod_of_dvd, instOfNat]
|
||||
|
||||
end UInt64
|
||||
|
|
@ -157,7 +157,7 @@ theorem intCast_ofNat (x : Nat) : (OfNat.ofNat (α := Int) x : USize) = OfNat.of
|
|||
rw [Int.toNat_emod (Int.zero_le_ofNat x)]
|
||||
· erw [Int.toNat_natCast]
|
||||
rw [Int.toNat_pow_of_nonneg (by decide)]
|
||||
simp only [ofNat, BitVec.ofNat, Fin.ofNat, Int.reduceToNat, Nat.dvd_refl,
|
||||
simp only [ofNat, BitVec.ofNat, Fin.Internal.ofNat_eq_ofNat, Fin.ofNat, Int.reduceToNat, Nat.dvd_refl,
|
||||
Nat.mod_mod_of_dvd, instOfNat]
|
||||
· obtain _ | _ := System.Platform.numBits_eq <;> simp_all
|
||||
|
||||
|
|
|
|||
|
|
@ -1865,6 +1865,9 @@ protected theorem Nat.le_trans {n m k : Nat} : LE.le n m → LE.le m k → LE.le
|
|||
| h, Nat.le.refl => h
|
||||
| h₁, Nat.le.step h₂ => Nat.le.step (Nat.le_trans h₁ h₂)
|
||||
|
||||
protected theorem Nat.lt_of_lt_of_le {n m k : Nat} : LT.lt n m → LE.le m k → LT.lt n k :=
|
||||
Nat.le_trans
|
||||
|
||||
protected theorem Nat.lt_trans {n m k : Nat} (h₁ : LT.lt n m) : LT.lt m k → LT.lt n k :=
|
||||
Nat.le_trans (le_step h₁)
|
||||
|
||||
|
|
@ -1968,6 +1971,27 @@ theorem Nat.ble_eq_true_of_le (h : LE.le n m) : Eq (Nat.ble n m) true :=
|
|||
theorem Nat.not_le_of_not_ble_eq_true (h : Not (Eq (Nat.ble n m) true)) : Not (LE.le n m) :=
|
||||
fun h' => absurd (Nat.ble_eq_true_of_le h') h
|
||||
|
||||
theorem Nat.lt_succ_of_le {n m : Nat} : LE.le n m → LT.lt n (succ m) := succ_le_succ
|
||||
|
||||
protected theorem Nat.lt_add_one (n : Nat) : LT.lt n (HAdd.hAdd n 1) := Nat.le_refl (succ n)
|
||||
|
||||
theorem Nat.lt_succ_self (n : Nat) : LT.lt n (succ n) := Nat.lt_add_one _
|
||||
|
||||
protected theorem Nat.lt_of_not_le {a b : Nat} (h : Not (LE.le a b)) : LT.lt b a :=
|
||||
(Nat.lt_or_ge b a).resolve_right h
|
||||
|
||||
protected theorem Nat.add_pos_right :
|
||||
{b : Nat} → (a : Nat) → (hb : LT.lt 0 b) → LT.lt 0 (HAdd.hAdd a b)
|
||||
| succ _, _, _ => Nat.zero_lt_succ _
|
||||
|
||||
protected theorem Nat.mul_pos :
|
||||
{n m : Nat} → (hn : LT.lt 0 n) → (hm : LT.lt 0 m) → LT.lt 0 (HMul.hMul n m)
|
||||
| _, succ _, ha, _ => Nat.add_pos_right _ ha
|
||||
|
||||
protected theorem Nat.pow_pos {a : Nat} : {n : Nat} → (h : LT.lt 0 a) → LT.lt 0 (HPow.hPow a n)
|
||||
| zero, _ => Nat.zero_lt_succ _
|
||||
| succ _, h => Nat.mul_pos (Nat.pow_pos h) h
|
||||
|
||||
/--
|
||||
A decision procedure for non-strict inequality of natural numbers, usually accessed via the
|
||||
`DecidableLE Nat` instance.
|
||||
|
|
@ -2021,6 +2045,160 @@ protected def Nat.sub : (@& Nat) → (@& Nat) → Nat
|
|||
instance instSubNat : Sub Nat where
|
||||
sub := Nat.sub
|
||||
|
||||
theorem Nat.succ_sub_succ_eq_sub (n m : Nat) : Eq (HSub.hSub (succ n) (succ m)) (HSub.hSub n m) :=
|
||||
m.rec rfl (fun _ ih => congrArg pred ih)
|
||||
|
||||
theorem Nat.pred_le : ∀ (n : Nat), LE.le (Nat.pred n) n
|
||||
| zero => Nat.le.refl
|
||||
| succ _ => le_succ _
|
||||
|
||||
theorem Nat.sub_le (n m : Nat) : LE.le (HSub.hSub n m) n :=
|
||||
m.rec (Nat.le_refl _) (fun _ ih => Nat.le_trans (pred_le _) ih)
|
||||
|
||||
theorem Nat.sub_lt : ∀ {n m : Nat}, LT.lt 0 n → LT.lt 0 m → LT.lt (HSub.hSub n m) n
|
||||
| 0, _, h1, _ => absurd h1 (Nat.lt_irrefl 0)
|
||||
| Nat.succ _, 0, _, h2 => absurd h2 (Nat.lt_irrefl 0)
|
||||
| Nat.succ n, Nat.succ m, _, _ =>
|
||||
Eq.symm (succ_sub_succ_eq_sub n m) ▸
|
||||
show LT.lt (HSub.hSub n m) (succ n) from
|
||||
lt_succ_of_le (sub_le n m)
|
||||
|
||||
theorem Nat.div_rec_lemma {x y : Nat} :
|
||||
(And (LT.lt 0 y) (LE.le y x)) → LT.lt (HSub.hSub x y) x :=
|
||||
fun ⟨ypos, ylex⟩ => sub_lt (Nat.lt_of_lt_of_le ypos ylex) ypos
|
||||
|
||||
theorem Nat.div_rec_fuel_lemma {x y fuel : Nat} (hy : LT.lt 0 y) (hle : LE.le y x)
|
||||
(hfuel : LT.lt x (HAdd.hAdd fuel 1)) : LT.lt (HSub.hSub x y) fuel :=
|
||||
Nat.lt_of_lt_of_le (div_rec_lemma ⟨hy, hle⟩) (Nat.le_of_lt_succ hfuel)
|
||||
|
||||
set_option bootstrap.genMatcherCode false in
|
||||
/--
|
||||
Division of natural numbers, discarding the remainder. Division by `0` returns `0`. Usually accessed
|
||||
via the `/` operator.
|
||||
|
||||
This operation is sometimes called “floor division.”
|
||||
|
||||
This function is overridden at runtime with an efficient implementation. This definition is
|
||||
the logical model.
|
||||
|
||||
Examples:
|
||||
* `21 / 3 = 7`
|
||||
* `21 / 5 = 4`
|
||||
* `0 / 22 = 0`
|
||||
* `5 / 0 = 0`
|
||||
-/
|
||||
@[extern "lean_nat_div", irreducible]
|
||||
protected def Nat.div (x y : @& Nat) : Nat :=
|
||||
dite (LT.lt 0 y) (fun hy =>
|
||||
let rec
|
||||
go (fuel : Nat) (x : Nat) (hfuel : LT.lt x fuel) : Nat :=
|
||||
match fuel with
|
||||
| succ fuel =>
|
||||
dite (LE.le y x)
|
||||
(fun h => HAdd.hAdd (go fuel (HSub.hSub x y) (div_rec_fuel_lemma hy h hfuel)) 1)
|
||||
(fun _ => 0)
|
||||
termination_by structural fuel
|
||||
go (succ x) x (Nat.lt_succ_self _))
|
||||
(fun _ => 0)
|
||||
|
||||
instance Nat.instDiv : Div Nat := ⟨Nat.div⟩
|
||||
|
||||
set_option bootstrap.genMatcherCode false in
|
||||
/--
|
||||
The modulo operator, which computes the remainder when dividing one natural number by another.
|
||||
Usually accessed via the `%` operator. When the divisor is `0`, the result is the dividend rather
|
||||
than an error.
|
||||
|
||||
This is the core implementation of `Nat.mod`. It computes the correct result for any two closed
|
||||
natural numbers, but it does not have some convenient [definitional
|
||||
reductions](lean-manual://section/type-system) when the `Nat`s contain free variables. The wrapper
|
||||
`Nat.mod` handles those cases specially and then calls `Nat.modCore`.
|
||||
|
||||
This function is overridden at runtime with an efficient implementation. This definition is the
|
||||
logical model.
|
||||
-/
|
||||
@[extern "lean_nat_mod"]
|
||||
protected noncomputable def Nat.modCore (x y : Nat) : Nat :=
|
||||
dite (LT.lt 0 y)
|
||||
(fun hy =>
|
||||
let rec
|
||||
go (fuel : Nat) (x : Nat) (hfuel : LT.lt x fuel) : Nat :=
|
||||
match fuel with
|
||||
| succ fuel =>
|
||||
dite (LE.le y x)
|
||||
(fun h => go fuel (HSub.hSub x y) (div_rec_fuel_lemma hy h hfuel))
|
||||
(fun _ => x)
|
||||
termination_by structural fuel
|
||||
go (succ x) x (Nat.lt_succ_self _))
|
||||
(fun _ => x)
|
||||
|
||||
theorem Nat.modCoreGo_lt {fuel y : Nat} (hy : LT.lt 0 y) : (x : Nat) → (hfuel : LT.lt x fuel) →
|
||||
LT.lt (Nat.modCore.go y hy fuel x hfuel) y :=
|
||||
fuel.rec (fun _ h => absurd h (Nat.not_lt_zero _))
|
||||
(fun _ ih x _ =>
|
||||
show LT.lt (dite _ _ _) _ from
|
||||
match Nat.decLe y x with
|
||||
| .isTrue _ => ih _ _
|
||||
| .isFalse h => Nat.lt_of_not_le h)
|
||||
|
||||
theorem Nat.modCore_lt {x y : Nat} (hy : LT.lt 0 y) : LT.lt (Nat.modCore x y) y :=
|
||||
show LT.lt (dite _ _ _) y from
|
||||
match Nat.decLt 0 y with
|
||||
| .isTrue _ => Nat.modCoreGo_lt hy x (Nat.lt_succ_self _)
|
||||
| .isFalse h => absurd hy h
|
||||
|
||||
attribute [irreducible] Nat.modCore
|
||||
|
||||
set_option bootstrap.genMatcherCode false in
|
||||
/--
|
||||
The modulo operator, which computes the remainder when dividing one natural number by another.
|
||||
Usually accessed via the `%` operator. When the divisor is `0`, the result is the dividend rather
|
||||
than an error.
|
||||
|
||||
`Nat.mod` is a wrapper around `Nat.modCore` that special-cases two situations, giving better
|
||||
definitional reductions:
|
||||
* `Nat.mod 0 m` should reduce to `m`, for all terms `m : Nat`.
|
||||
* `Nat.mod n (m + n + 1)` should reduce to `n` for concrete `Nat` literals `n`.
|
||||
|
||||
These reductions help `Fin n` literals work well, because the `OfNat` instance for `Fin` uses
|
||||
`Nat.mod`. In particular, `(0 : Fin (n + 1)).val` should reduce definitionally to `0`. `Nat.modCore`
|
||||
can handle all numbers, but its definitional reductions are not as convenient.
|
||||
|
||||
This function is overridden at runtime with an efficient implementation. This definition is the
|
||||
logical model.
|
||||
|
||||
Examples:
|
||||
* `7 % 2 = 1`
|
||||
* `9 % 3 = 0`
|
||||
* `5 % 7 = 5`
|
||||
* `5 % 0 = 5`
|
||||
* `show ∀ (n : Nat), 0 % n = 0 from fun _ => rfl`
|
||||
* `show ∀ (m : Nat), 5 % (m + 6) = 5 from fun _ => rfl`
|
||||
-/
|
||||
@[extern "lean_nat_mod"]
|
||||
protected def Nat.mod : @& Nat → @& Nat → Nat
|
||||
/-
|
||||
Nat.modCore is defined with fuel and thus does not reduce with open terms very well.
|
||||
Nevertheless it is desirable for trivial `Nat.mod` calculations, namely
|
||||
* `Nat.mod 0 m` for all `m`
|
||||
* `Nat.mod n (m + n + 1)` for concrete literals `n`,
|
||||
to reduce definitionally.
|
||||
This property is desirable for `Fin n` literals, as it means `(ofNat 0 : Fin n).val = 0` by
|
||||
definition.
|
||||
-/
|
||||
| 0, _ => 0
|
||||
| n@(succ _), m => ite (LE.le m n) (Nat.modCore n m) n
|
||||
|
||||
instance Nat.instMod : Mod Nat := ⟨Nat.mod⟩
|
||||
|
||||
theorem Nat.mod_lt : (x : Nat) → {y : Nat} → (hy : LT.lt 0 y) → LT.lt (HMod.hMod x y) y
|
||||
| 0, succ _, _ => Nat.zero_lt_succ _
|
||||
| succ n, m, hm =>
|
||||
show LT.lt (ite (LE.le m (succ n)) (Nat.modCore (succ n) m) (succ n)) _ from
|
||||
match Nat.decLe m (succ n) with
|
||||
| .isTrue _ => Nat.modCore_lt hm
|
||||
| .isFalse h => Nat.lt_of_not_le h
|
||||
|
||||
attribute [gen_constructor_elims] Nat
|
||||
|
||||
/--
|
||||
|
|
@ -2090,6 +2268,14 @@ instance {n} : LE (Fin n) where
|
|||
instance Fin.decLt {n} (a b : Fin n) : Decidable (LT.lt a b) := Nat.decLt ..
|
||||
instance Fin.decLe {n} (a b : Fin n) : Decidable (LE.le a b) := Nat.decLe ..
|
||||
|
||||
/--
|
||||
Returns `a` modulo `n` as a `Fin n`.
|
||||
|
||||
This function exists for bootstrapping purposes. Use `Fin.ofNat` instead.
|
||||
-/
|
||||
@[expose] protected def Fin.Internal.ofNat (n : Nat) (hn : LT.lt 0 n) (a : Nat) : Fin n :=
|
||||
⟨HMod.hMod a n, Nat.mod_lt _ hn⟩
|
||||
|
||||
/--
|
||||
A bitvector of the specified width.
|
||||
|
||||
|
|
@ -2126,6 +2312,13 @@ instance : DecidableEq (BitVec w) := BitVec.decEq
|
|||
protected def BitVec.ofNatLT {w : Nat} (i : Nat) (p : LT.lt i (hPow 2 w)) : BitVec w where
|
||||
toFin := ⟨i, p⟩
|
||||
|
||||
/--
|
||||
The bitvector with value `i mod 2^n`.
|
||||
-/
|
||||
@[expose, match_pattern]
|
||||
protected def BitVec.ofNat (n : Nat) (i : Nat) : BitVec n where
|
||||
toFin := Fin.Internal.ofNat (HPow.hPow 2 n) (Nat.pow_pos (Nat.zero_lt_succ _)) i
|
||||
|
||||
/--
|
||||
Return the underlying `Nat` that represents a bitvector.
|
||||
|
||||
|
|
@ -2174,6 +2367,21 @@ This function is overridden at runtime with an efficient implementation.
|
|||
def UInt8.ofNatLT (n : @& Nat) (h : LT.lt n UInt8.size) : UInt8 where
|
||||
toBitVec := BitVec.ofNatLT n h
|
||||
|
||||
/--
|
||||
Converts a natural number to an 8-bit unsigned integer, wrapping on overflow.
|
||||
|
||||
This function is overridden at runtime with an efficient implementation.
|
||||
|
||||
Examples:
|
||||
* `UInt8.ofNat 5 = 5`
|
||||
* `UInt8.ofNat 255 = 255`
|
||||
* `UInt8.ofNat 256 = 0`
|
||||
* `UInt8.ofNat 259 = 3`
|
||||
* `UInt8.ofNat 32770 = 2`
|
||||
-/
|
||||
@[extern "lean_uint8_of_nat"]
|
||||
def UInt8.ofNat (n : @& Nat) : UInt8 := ⟨BitVec.ofNat 8 n⟩
|
||||
|
||||
set_option bootstrap.genMatcherCode false in
|
||||
/--
|
||||
Decides whether two 8-bit unsigned integers are equal. Usually accessed via the `DecidableEq UInt8`
|
||||
|
|
@ -2784,6 +2992,37 @@ def List.concat {α : Type u} : List α → α → List α
|
|||
| nil, b => cons b nil
|
||||
| cons a as, b => cons a (concat as b)
|
||||
|
||||
/--
|
||||
Returns the sequence of bytes in a character's UTF-8 encoding.
|
||||
-/
|
||||
def String.utf8EncodeChar (c : Char) : List UInt8 :=
|
||||
let v := c.val.toNat
|
||||
ite (LE.le v 0x7f)
|
||||
(List.cons (UInt8.ofNat v) List.nil)
|
||||
(ite (LE.le v 0x7ff)
|
||||
(List.cons
|
||||
(UInt8.ofNat (HAdd.hAdd (HMod.hMod (HDiv.hDiv v 64) 0x20) 0xc0))
|
||||
(List.cons
|
||||
(UInt8.ofNat (HAdd.hAdd (HMod.hMod v 0x40) 0x80))
|
||||
List.nil))
|
||||
(ite (LE.le v 0xffff)
|
||||
(List.cons
|
||||
(UInt8.ofNat (HAdd.hAdd (HMod.hMod (HDiv.hDiv v 4096) 0x10) 0xe0))
|
||||
(List.cons
|
||||
(UInt8.ofNat (HAdd.hAdd (HMod.hMod (HDiv.hDiv v 64) 0x40) 0x80))
|
||||
(List.cons
|
||||
(UInt8.ofNat (HAdd.hAdd (HMod.hMod v 0x40) 0x80))
|
||||
List.nil)))
|
||||
(List.cons
|
||||
(UInt8.ofNat (HAdd.hAdd (HMod.hMod (HDiv.hDiv v 262144) 0x08) 0xf0))
|
||||
(List.cons
|
||||
(UInt8.ofNat (HAdd.hAdd (HMod.hMod (HDiv.hDiv v 4096) 0x40) 0x80))
|
||||
(List.cons
|
||||
(UInt8.ofNat (HAdd.hAdd (HMod.hMod (HDiv.hDiv v 64) 0x40) 0x80))
|
||||
(List.cons
|
||||
(UInt8.ofNat (HAdd.hAdd (HMod.hMod v 0x40) 0x80))
|
||||
List.nil))))))
|
||||
|
||||
/--
|
||||
A string is a sequence of Unicode code points.
|
||||
|
||||
|
|
|
|||
|
|
@ -151,7 +151,7 @@ public abbrev foldlUtf8 (c : Char) (f : σ → UInt8 → σ) (init : σ) : σ :=
|
|||
Id.run <| foldlUtf8M c (pure <| f · ·) init
|
||||
|
||||
example : foldlUtf8 c (fun l b => b::l) List.nil = (String.utf8EncodeChar c).reverse := by
|
||||
simp only [foldlUtf8, foldlUtf8M, String.utf8EncodeChar]
|
||||
simp only [foldlUtf8, foldlUtf8M, String.utf8EncodeChar_eq_utf8EncodeCharFast, String.utf8EncodeCharFast]
|
||||
if h1 : c.val ≤ 0x7f then simp [h1]
|
||||
else if h2 : c.val ≤ 0x7ff then simp [h1, h2]
|
||||
else if h3 : c.val ≤ 0xffff then simp [h1, h2, h3]
|
||||
|
|
|
|||
|
|
@ -134,28 +134,28 @@ example {α : Type} (x y : α) : x = y ↔ y = x := by apply?
|
|||
|
||||
/--
|
||||
info: Try this:
|
||||
exact Nat.add_pos_left ha b
|
||||
exact Nat.add_pos_right a hb
|
||||
-/
|
||||
#guard_msgs in
|
||||
example (a b : Nat) (ha : 0 < a) (_hb : 0 < b) : 0 < a + b := by apply?
|
||||
example (a b : Nat) (_ha : 0 < a) (hb : 0 < b) : 0 < a + b := by apply?
|
||||
|
||||
/--
|
||||
info: Try this:
|
||||
exact Nat.add_pos_left ha b
|
||||
exact Nat.add_pos_right a hb
|
||||
-/
|
||||
#guard_msgs in
|
||||
-- Verify that if maxHeartbeats is 0 we don't stop immediately.
|
||||
set_option maxHeartbeats 0 in
|
||||
example (a b : Nat) (ha : 0 < a) (_hb : 0 < b) : 0 < a + b := by apply?
|
||||
example (a b : Nat) (_ha : 0 < a) (hb : 0 < b) : 0 < a + b := by apply?
|
||||
|
||||
section synonym
|
||||
|
||||
/--
|
||||
info: Try this:
|
||||
exact Nat.add_pos_left ha b
|
||||
exact Nat.add_pos_right a hb
|
||||
-/
|
||||
#guard_msgs in
|
||||
example (a b : Nat) (ha : a > 0) (_hb : 0 < b) : 0 < a + b := by apply?
|
||||
example (a b : Nat) (_ha : a > 0) (hb : 0 < b) : 0 < a + b := by apply?
|
||||
|
||||
/--
|
||||
info: Try this:
|
||||
|
|
|
|||
|
|
@ -337,7 +337,7 @@ set_option pp.analyze.trustSubtypeMk true in
|
|||
|
||||
#testDelabN Nat.brecOn
|
||||
#testDelabN Nat.below
|
||||
#testDelabN Nat.mod_lt
|
||||
#testDelabN Nat.mod_eq_of_lt
|
||||
#testDelabN List.partition
|
||||
#testDelabN List.partition.loop
|
||||
#testDelabN StateT.modifyGet
|
||||
|
|
@ -360,6 +360,9 @@ set_option pp.analyze.trustSubtypeMk true in
|
|||
#testDelabN Lean.Server.FileWorker.handlePlainTermGoal
|
||||
#testDelabN Lean.Server.FileWorker.handlePlainGoal
|
||||
|
||||
-- TODO: this hangs
|
||||
-- #testDelabN Nat.mod_lt
|
||||
|
||||
-- TODO: this error occurs because we use a term's type to determine `blockImplicit` (@),
|
||||
-- whereas we should actually use the expected type based on the function being applied.
|
||||
-- #testDelabN HEq.subst
|
||||
|
|
|
|||
|
|
@ -79,7 +79,7 @@ theorem getElem_of_getLsbD_eq_true {x : BitVec w} {i : Nat} (h : x.getLsbD i = t
|
|||
This normalized a bitvec using `ofFin` to `ofNat`.
|
||||
-/
|
||||
theorem ofFin_eq_ofNat : @BitVec.ofFin w (Fin.mk x lt) = BitVec.ofNat w x := by
|
||||
simp only [BitVec.ofNat, Fin.ofNat, lt, Nat.mod_eq_of_lt]
|
||||
simp only [BitVec.ofNat, Fin.Internal.ofNat_eq_ofNat, Fin.ofNat, lt, Nat.mod_eq_of_lt]
|
||||
|
||||
/-- Prove nonequality of bitvectors in terms of nat operations. -/
|
||||
theorem toNat_ne_iff_ne {n} {x y : BitVec n} : x.toNat ≠ y.toNat ↔ x ≠ y := by
|
||||
|
|
@ -212,7 +212,7 @@ theorem length_pos_of_ne {x y : BitVec w} (h : x ≠ y) : 0 < w := by grind
|
|||
|
||||
theorem ofFin_ofNat (n : Nat) :
|
||||
ofFin (no_index (OfNat.ofNat n : Fin (2^w))) = OfNat.ofNat n := by
|
||||
simp only [OfNat.ofNat, Fin.ofNat, BitVec.ofNat]
|
||||
simp only [OfNat.ofNat, Fin.Internal.ofNat_eq_ofNat, Fin.ofNat, BitVec.ofNat]
|
||||
|
||||
-- We use a `grind_pattern` as `@[grind]` will not use the `no_index` term.
|
||||
grind_pattern ofFin_ofNat => ofFin (OfNat.ofNat n : Fin (2^w))
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue