Verify big-endian and little-endian radix/bits/bytes #237
Conversation
|
also I think I named lemmas vs theorems pretty arbitrarily, it appears the codebase convention is to just use theorem? |
stdlib/lampe/Stdlib/Field/Mod.lean
Outdated
| conv_rhs => rw [RadixVec.msd_lsds_decomposition (v:=n)] | ||
| have := Fin.val_eq_of_eq $ ih (n := n.lsds) | ||
| simpa [RadixVec.ofDigitsBE, RadixVec.toDigitsBE, RadixVec.ofLimbsBE] | ||
| theorem RadixVec.toDigitsBE'_bytes_eq_map_toFin_map_ofNatLT (hr : 1 < 256) (m : ℕ) : |
There was a problem hiding this comment.
so I didn't know if I should move this one to Helpers cuz it depends on a specific base? maybe I should abstract it right?
There was a problem hiding this comment.
I would dispute this being a theorem worth stating at all, why do we need it? It's only used once
stdlib/lampe/Stdlib/Field/Mod.lean
Outdated
| simp_all | ||
| · simp_all | ||
|
|
||
| theorem List.take_succ_lt_of_take_lt [DecidableEq α] [LT α] [DecidableLT α] {l₁ l₂ : List α} |
There was a problem hiding this comment.
I didn't know where to put all these list/bitvec lemmas
There was a problem hiding this comment.
Eh, some new file I guess, in a subtree that suggests "mathlib extensions go here"
stdlib/lampe/Stdlib/Field/Mod.lean
Outdated
| theorem ofDigitsBE'_toList {r : Radix} {l : List.Vector (Digit r) d}: RadixVec.ofDigitsBE' l.toList = (RadixVec.ofDigitsBE l).val := by | ||
| simp only [RadixVec.ofDigitsBE'] | ||
| congr <;> simp | ||
| theorem ofDigitsBE'_lt_of_shorter_than_modulus {r : Radix} {data : List (Digit r)} {P : Prime} |
There was a problem hiding this comment.
also wasn't sure if I should move this to RadixVec cuz it depends on Prime and stuff...
kustosz
left a comment
kustosz
left a comment
There was a problem hiding this comment.
Good stuff! Please try to bring formatting closer to https://leanprover-community.github.io/contribute/style.html
stdlib/lampe/Stdlib/Field/Mod.lean
Outdated
| simp_all | ||
| · simp_all | ||
|
|
||
| theorem List.take_succ_lt_of_take_lt [DecidableEq α] [LT α] [DecidableLT α] {l₁ l₂ : List α} |
There was a problem hiding this comment.
Eh, some new file I guess, in a subtree that suggests "mathlib extensions go here"
stdlib/lampe/Stdlib/Field/Mod.lean
Outdated
| _ < (r - 1) * r.val ^ d + r.val ^ d := by simp [*] | ||
| _ = (↑r - 1) * ↑r ^ d + 1 * ↑r ^ d := by simp | ||
| _ = _ := by rw [←Nat.add_mul, this, mul_comm] | ||
| theorem List.Vector.map_toFin_map_ofFin {n d : ℕ} (v : List.Vector (Fin (2^n)) d) : |
There was a problem hiding this comment.
Not a fan of this theorem existing at all. It's a combination of just List.Vector.map_map and List.Vector.map_id, no need to be so specific about the functions involved. I'd buy just toFin_ofFin : _ = id used in conjunction with the above, but this level of specialization here feels excessive
stdlib/lampe/Stdlib/Field/Mod.lean
Outdated
| apply List.Vector.eq | ||
| simp only [List.Vector.toList_map, List.map_map, BitVec.toFin_ofFin_comp, List.map_id] | ||
|
|
||
| theorem List.Vector.map_ofFin_map_toFin {n d : ℕ} (v : List.Vector (BitVec n) d) : |
stdlib/lampe/Stdlib/Field/Mod.lean
Outdated
| theorem List.Vector.reverse_map {α β : Type} {d : ℕ} (v : List.Vector α d) (f : α → β) : | ||
| (v.map f).reverse = v.reverse.map f := by | ||
| apply List.Vector.eq | ||
| simp only [List.Vector.toList_reverse, List.Vector.toList_map, List.map_reverse] |
stdlib/lampe/Stdlib/Field/Mod.lean
Outdated
| conv_rhs => rw [RadixVec.msd_lsds_decomposition (v:=n)] | ||
| have := Fin.val_eq_of_eq $ ih (n := n.lsds) | ||
| simpa [RadixVec.ofDigitsBE, RadixVec.toDigitsBE, RadixVec.ofLimbsBE] | ||
| theorem RadixVec.toDigitsBE'_bytes_eq_map_toFin_map_ofNatLT (hr : 1 < 256) (m : ℕ) : |
There was a problem hiding this comment.
I would dispute this being a theorem worth stating at all, why do we need it? It's only used once
Eduardogbg
force-pushed
the
edu/endianess
branch
from
c9d1137 to
35ad916
Compare
iamrecursion
changed the title
trivial/exact ()being redundant due to a tactics change that I had in a different commit but now I squashed oops