resolve some sorry

opencompl · Dec 23, 2024 · 46a9269 · 46a9269
1 parent 59851d4
commit 46a9269
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 10 deletions.
diff --git a/SSA/Experimental/Bits/AutoStructs/FiniteStateMachine.lean b/SSA/Experimental/Bits/AutoStructs/FiniteStateMachine.lean
@@ -397,9 +397,7 @@ def one : FSM (Fin 0) :=
   ext n
   cases n
   · rfl
-  · simp [eval, carry_one, nextBit]
-    sorry -- TODO: fix this proof
-
+  · simp! [eval, carry_one, nextBit, one, mk]
 
 def negOne : FSM (Fin 0) :=
   { α := Empty,
@@ -410,7 +408,7 @@ def negOne : FSM (Fin 0) :=
 @[simp] lemma eval_negOne (x : Fin 0 → BitStream) : negOne.eval x = BitStream.negOne := by
   ext; simp [negOne, eval, nextBit]
 
-def ls (b : Bool) : FSM Unit :=
+@[simp] def ls (b : Bool) : FSM Unit :=
   { α := Unit,
     initCarry := fun _ => b,
     nextBitCirc := fun x =>
@@ -431,8 +429,7 @@ theorem carry_ls (b : Bool) (x : Unit → BitStream) : ∀ (n : ℕ),
   ext n
   cases n
   · rfl
-  · simp [ls, carry_ls, eval, nextBit, BitStream.concat]
-    sorry -- TODO: fix this proof
+  · simp [ls, carry, carry_ls, eval, nextBit, BitStream.concat]
 
 def var (n : ℕ) : FSM (Fin (n+1)) :=
   { α := Empty,

diff --git a/SSA/Experimental/Bits/Fast/FiniteStateMachine.lean b/SSA/Experimental/Bits/Fast/FiniteStateMachine.lean
@@ -559,8 +559,7 @@ def one : FSM (Fin 0) :=
   ext n
   cases n
   · rfl
-  · simp [eval, carry_one, nextBit]
-    sorry
+  · simp! [eval, carry_one, nextBit, one]
 
 def negOne : FSM (Fin 0) :=
   { α := Empty,
@@ -595,8 +594,7 @@ theorem carry_ls (b : Bool) (x : Unit → BitStream) : ∀ (n : ℕ),
   ext n
   cases n
   · rfl
-  · simp [carry_ls, eval, nextBit, BitStream.concat]
-    sorry
+  · simp [ls, carry_ls, eval, nextBit, BitStream.concat, carry]
 
 def var (n : ℕ) : FSM (Fin (n+1)) :=
   { α := Empty,