WIP: FSM abstractions

opencompl · Sep 30, 2024 · 24b76a6 · 24b76a6
1 parent 2b5ff4e
commit 24b76a6
Show file tree

Hide file tree

Showing 3 changed files with 434 additions and 289 deletions.
diff --git a/SSA/Experimental/Bits/Fast/BitStream.lean b/SSA/Experimental/Bits/Fast/BitStream.lean
@@ -85,8 +85,10 @@ abbrev map₂ (f : Bool → Bool → Bool) : BitStream → BitStream → BitStre
 def corec {β} (f : β → β × Bool) (b : β) : BitStream :=
   fun i => f ((Prod.fst ∘ f)^[i] b) |>.snd
 
+@[simp] theorem corec_zero {β} (f : β → β × Bool) (b : β) :
+    corec f b 0 = (f b).2 := rfl
 
-theorem corec_succ {β} (f : β → β × Bool) (b : β) (i : Nat) :
+@[simp] theorem corec_succ {β} (f : β → β × Bool) (b : β) (i : Nat) :
     corec f b (i + 1) = (corec f (f b).1) i := by
   induction' i with i ih
   · simp [corec]

diff --git a/SSA/Experimental/Bits/Fast/Circuit.lean b/SSA/Experimental/Bits/Fast/Circuit.lean
@@ -221,7 +221,7 @@ def map : ∀ (_c : Circuit α) (_f : α → β), Circuit β
   | or c₁ c₂, f => (map c₁ f) ||| (map c₂ f)
   | xor c₁ c₂, f => (map c₁ f) ^^^ (map c₂ f)
 
-lemma eval_map {c : Circuit α} {f : α → β} {g : β → Bool} :
+@[simp] lemma eval_map {c : Circuit α} {f : α → β} {g : β → Bool} :
     eval (map c f) g = eval c (λ x => g (f x)) := by
   induction c <;> simp [*, Circuit.map, eval] at *