From 76fb13202c7dc3c4aaa95383e3f536e5a274ac05 Mon Sep 17 00:00:00 2001 From: Siddharth Date: Sat, 28 Sep 2024 19:54:28 -0500 Subject: [PATCH] chore: delete dead code (#666) We delete dead code that has `sorry` in it, so that we can more easily grep for `sorry`s to solve in the code. --- SSA/Experimental/Bits/Fast/BitStream.lean | 9 ++------- SSA/Experimental/Bits/Fast/FiniteStateMachine.lean | 2 -- 2 files changed, 2 insertions(+), 9 deletions(-) diff --git a/SSA/Experimental/Bits/Fast/BitStream.lean b/SSA/Experimental/Bits/Fast/BitStream.lean index 4e7d5c11c..4984253b9 100644 --- a/SSA/Experimental/Bits/Fast/BitStream.lean +++ b/SSA/Experimental/Bits/Fast/BitStream.lean @@ -102,8 +102,8 @@ theorem ext {x y : BitStream} (h : ∀ i, x i = y i) : x = y := by The field projection `.1` distributes over function composition, so we can compute the first field of the result of the composition by repeatedly composing the first projection. -/ -theorem compose_first {α: Type u₁} (i : Nat) (a : α) - (f : α → α × Bool) : +theorem compose_first {α: Type u₁} (i : Nat) (a : α) + (f : α → α × Bool) : (f ((Prod.fst ∘ f)^[i] a)).1 = (Prod.fst ∘ f)^[i] (f a).1 := match i with | 0 => by simp @@ -354,11 +354,6 @@ thus could have a bit set in the `w+1`th position. Crucially, our decision procedure works by considering which equalities hold for *all* widths, -/ --- theorem ofBitVec_add {w} (x y z : ∀ w, BitVec w) : --- (∀ w, (x w + y w) = z w) ↔ (∀ w, (ofBitVec (x w)) + (ofBitVec (y w)) ) := by --- have ⟨h₁, h₂⟩ : True ∧ True := sorry --- sorry - variable {w : Nat} {x y : BitVec w} {a b a' b' : BitStream} local infix:20 " ≈ʷ " => EqualUpTo w diff --git a/SSA/Experimental/Bits/Fast/FiniteStateMachine.lean b/SSA/Experimental/Bits/Fast/FiniteStateMachine.lean index 7dcd1d97c..e7651c097 100644 --- a/SSA/Experimental/Bits/Fast/FiniteStateMachine.lean +++ b/SSA/Experimental/Bits/Fast/FiniteStateMachine.lean @@ -690,8 +690,6 @@ what we should do :) - Alternatively, we need to be able to decide `eventually always zero`. - Alternatively, we push negations inside, and decide `⬝ ≠ ⬝` and `⬝ ≰ ⬝`. -/ --- def lnot : FSM Unit := sorry - inductive Result : Type | falseAfter (n : ℕ) : Result