Created
March 22, 2024 03:43
-
-
Save semorrison/e70fd3b5c572d3787963c8bf58b2eeb8 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| theorem _root_.Nat.mod_eq_sub_div_mul {a b : Nat} : a % b = a - (a / b) * b := by | |
| rw [eq_comm, Nat.sub_eq_iff_eq_add (Nat.div_mul_le_self _ _), Nat.mul_comm, Nat.mod_add_div] | |
| theorem _root_.Nat.mod_eq_sub_mul_div {a b : Nat} : a % b = a - b * (a / b) := by | |
| rw [Nat.mod_eq_sub_div_mul, Nat.mul_comm] | |
| theorem _root_.BitVec.extractLsb_flatten (hi lo : Nat) {w : Nat} (vs : List (BitVec w)) | |
| (w₁ : lo ≤ hi) (w₂ : hi < w * vs.length) (h : hi / w = lo / w) : | |
| extractLsb hi lo (BitVec.flatten vs) = | |
| BitVec.cast (by simp [Nat.mod_eq_sub_mul_div, h]; have := Nat.mul_div_le lo w; omega) | |
| (extractLsb (hi % w) (lo % w) (vs[vs.length - 1 - hi / w]?.getD 0#w)) := sorry -- In Lean soon | |
| protected def _root_.BitVec.consCasesOn {w : Nat} {motive : BitVec (w+1) → Sort u} (x : BitVec (w+1)) | |
| (cons : (b : Bool) → (x : BitVec w) → motive (cons b x)) : motive x := by | |
| rw [eq_msb_cons_truncate x] | |
| apply cons | |
| protected def _root_.BitVec.appendCasesOn {a b w : Nat} (h : a + b = w) {motive : BitVec w → Sort u} (x : BitVec w) | |
| (cons : (y : BitVec a) → (z : BitVec b) → motive (BitVec.cast h (y ++ z))) : motive x := by | |
| have : x = BitVec.cast h ((x >>> b).truncate a ++ x.truncate b) := sorry | |
| rw [this] | |
| apply cons | |
| @[simp] theorem _root_.BitVec.toNat_append' {w v : Nat} {x : BitVec w} {y : BitVec v} : (x ++ y).toNat = 2^v * x.toNat + y.toNat := sorry | |
| theorem _root_.BitVec.extractLsb_congr (h_hi : hi = hi') (h_lo : lo = lo') : extractLsb hi lo v = BitVec.cast (by omega) (extractLsb hi' lo' v) := sorry | |
| -- set_option maxHeartbeats 5000000 | |
| theorem foo : XTimes = DPSFP.FFmul02 := by | |
| funext x | |
| apply BitVec.appendCasesOn (by rfl : 4 + 4 = 8) x; intro x₁ x₂ | |
| simp only [XTimes] | |
| rw [DPSFP.FFmul02] | |
| simp only | |
| rw [BitVec.extractLsb_flatten _ _ _ (by omega) (by simp; omega) (by omega)] | |
| have t₁ : 15 - ((x₁ ++ x₂).toNat * 8 + 7) / 128 = 15 - x₁.toNat := by | |
| rw [BitVec.toNat_append'] | |
| rw [Nat.mul_comm _ 8, Nat.mul_add, ← Nat.mul_assoc, Nat.add_assoc] | |
| simp only [Nat.reduceAdd, BitVec.cast_eq, Nat.reducePow, Nat.reduceMul] | |
| rw [Nat.mul_add_div (by decide)] | |
| rw [Nat.div_eq_of_lt (by omega)] | |
| simp | |
| have t₂ : ((x₁ ++ x₂).toNat * 8 + 7) % 128 = x₂.toNat * 8 + 7 := sorry | |
| have t₃ : ((x₁ ++ x₂).toNat * 8) % 128 = x₂.toNat * 8 := sorry | |
| simp | |
| conv => | |
| congr | |
| · skip | |
| · congr | |
| rw [BitVec.extractLsb_congr t₂ t₃] | |
| congr | |
| rw [t₁] | |
| simp | |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
I tried to do a case generation. I only added the last tactic. This tactic fails with
tactic apply failed, failed to unify ?m.101825 x₁