3411935e53
This PR also pulls in some mathlib theorems on testBit and Nat and establishes facts about 2^w that are needed here and which are generally useful for bitvector reasoning. The following theorem is not generalized to arbitrary x instead of 2, as this would require a condition to be added for x > 1 which would have to be passed to simp each time this theorem should fire. chore: derive from testBit_two_pow chore: convert first to prop and then decide chore: move intMax down as well chore: add simp set Add simp-set into this PR chore: fix simp extension Move file to src/Lean to fix build Add prelude update date Add university of cambridge as copyright holder improve naming use whitespace uniformly use decide (n = m) Drop the 'Nat.' namespace Update src/Init/Data/BitVec/Lemmas.lean Co-authored-by: Siddharth <siddu.druid@gmail.com> Update src/Init/Data/BitVec/Lemmas.lean Co-authored-by: Siddharth <siddu.druid@gmail.com> Fix build add some theorems Revert "add some theorems" This reverts commit fb97bc2007e371854b40badb3d6014da034c1f5e. WIP Shorten proof Update src/Init/Data/Nat/Lemmas.lean finish proofs Update src/Init/Data/BitVec/Lemmas.lean Co-authored-by: Kim Morrison <scott@tqft.net> Update src/Init/Data/Nat/Lemmas.lean Co-authored-by: Kim Morrison <scott@tqft.net> chore: move BoolToPropSimps |
||
|---|---|---|
| .. | ||
| Bitwise | ||
| Basic.lean | ||
| Bitwise.lean | ||
| Compare.lean | ||
| Control.lean | ||
| Div.lean | ||
| Dvd.lean | ||
| Gcd.lean | ||
| Lcm.lean | ||
| Lemmas.lean | ||
| Linear.lean | ||
| Log2.lean | ||
| MinMax.lean | ||
| Mod.lean | ||
| Power2.lean | ||
| Simproc.lean | ||
| SOM.lean | ||