refactor: final refactor of the stream operators

leanprover · Aug 7, 2024 · ec671de · ec671de
1 parent 14b396a
commit ec671de
Show file tree

Hide file tree

Showing 3 changed files with 118 additions and 121 deletions.
diff --git a/LeanSAT/AIG/RefStreamOperator/Fold.lean b/LeanSAT/AIG/RefStreamOperator/Fold.lean
@@ -37,8 +37,8 @@ def fold (aig : AIG α) (target : FoldTarget aig) : Entrypoint α :=
 where
   @[specialize]
   go (aig : AIG α) (acc : Ref aig) (idx : Nat) (len : Nat) (input : RefStream aig len)
-     (f : (aig : AIG α) → BinaryInput aig → Entrypoint α) [LawfulOperator α BinaryInput f]
-  : Entrypoint α :=
+     (f : (aig : AIG α) → BinaryInput aig → Entrypoint α) [LawfulOperator α BinaryInput f] :
+     Entrypoint α :=
     if hidx:idx < len then
       let res := f aig ⟨acc, input.get idx hidx⟩
       let aig := res.aig
@@ -53,8 +53,8 @@ where
   termination_by len - idx
 
 theorem fold.go_le_size {aig : AIG α} (acc : Ref aig) (idx : Nat) (s : RefStream aig len)
-    (f : (aig : AIG α) → BinaryInput aig → Entrypoint α) [LawfulOperator α BinaryInput f]
-    : aig.decls.size ≤ (go aig acc idx len s f).1.decls.size := by
+    (f : (aig : AIG α) → BinaryInput aig → Entrypoint α) [LawfulOperator α BinaryInput f] :
+    aig.decls.size ≤ (go aig acc idx len s f).1.decls.size := by
   unfold go
   split
   . next h =>
@@ -64,17 +64,17 @@ theorem fold.go_le_size {aig : AIG α} (acc : Ref aig) (idx : Nat) (s : RefStrea
   . simp
   termination_by len - idx
 
-theorem fold_le_size {aig : AIG α} (target : FoldTarget aig)
-    : aig.decls.size ≤ (fold aig target).1.decls.size := by
+theorem fold_le_size {aig : AIG α} (target : FoldTarget aig) :
+    aig.decls.size ≤ (fold aig target).1.decls.size := by
   unfold fold
   dsimp
   refine Nat.le_trans ?_ (by apply fold.go_le_size)
   apply LawfulOperator.le_size (f := mkConstCached)
 
 theorem fold.go_decl_eq {aig : AIG α} (acc : Ref aig) (i : Nat) (s : RefStream aig len)
-    (f : (aig : AIG α) → BinaryInput aig → Entrypoint α) [LawfulOperator α BinaryInput f]
-    : ∀ (idx : Nat) (h1) (h2),
-        (go aig acc i len s f).1.decls[idx]'h2 = aig.decls[idx]'h1 := by
+    (f : (aig : AIG α) → BinaryInput aig → Entrypoint α) [LawfulOperator α BinaryInput f] :
+    ∀ (idx : Nat) (h1) (h2),
+      (go aig acc i len s f).1.decls[idx]'h2 = aig.decls[idx]'h1 := by
   generalize hgo : go aig acc i len s f = res
   unfold go at hgo
   split at hgo
@@ -90,11 +90,11 @@ theorem fold.go_decl_eq {aig : AIG α} (acc : Ref aig) (i : Nat) (s : RefStream
     simp
 termination_by len - i
 
-theorem fold_decl_eq {aig : AIG α} (target : FoldTarget aig)
-    : ∀ idx (h1 : idx < aig.decls.size) (h2),
-        (fold aig target).1.decls[idx]'h2
-          =
-        aig.decls[idx]'h1 := by
+theorem fold_decl_eq {aig : AIG α} (target : FoldTarget aig) :
+    ∀ idx (h1 : idx < aig.decls.size) (h2),
+      (fold aig target).1.decls[idx]'h2
+        =
+      aig.decls[idx]'h1 := by
   intros
   unfold fold
   dsimp
@@ -110,18 +110,18 @@ instance : LawfulOperator α FoldTarget fold where
 namespace fold
 
 theorem denote_go_and {aig : AIG α} (acc : AIG.Ref aig) (curr : Nat) (hcurr : curr ≤ len)
-      (input : RefStream aig len)
-    : ⟦
-        (go aig acc curr len input mkAndCached).aig,
-        (go aig acc curr len input mkAndCached).ref,
-        assign
-      ⟧
-        =
-      (
-        ⟦aig, acc, assign⟧
-          ∧
-        (∀ (idx : Nat) (hidx1 : idx < len), curr ≤ idx → ⟦aig, input.get idx hidx1, assign⟧)
-      ):= by
+    (input : RefStream aig len) :
+    ⟦
+      (go aig acc curr len input mkAndCached).aig,
+      (go aig acc curr len input mkAndCached).ref,
+      assign
+    ⟧
+      =
+    (
+      ⟦aig, acc, assign⟧
+        ∧
+      (∀ (idx : Nat) (hidx1 : idx < len), curr ≤ idx → ⟦aig, input.get idx hidx1, assign⟧)
+    ) := by
   generalize hgo : go aig acc curr len input mkAndCached = res
   unfold go at hgo
   split at hgo
@@ -163,11 +163,10 @@ termination_by len - curr
 end fold
 
 @[simp]
-theorem denote_fold_and {aig : AIG α} (s : RefStream aig len)
-    : ⟦(fold aig (FoldTarget.mkAnd s)), assign⟧
-        ↔
-      (∀ (idx : Nat) (hidx : idx < len), ⟦aig, s.get idx hidx, assign⟧)
-     := by
+theorem denote_fold_and {aig : AIG α} (s : RefStream aig len) :
+    ⟦(fold aig (FoldTarget.mkAnd s)), assign⟧
+      ↔
+    (∀ (idx : Nat) (hidx : idx < len), ⟦aig, s.get idx hidx, assign⟧) := by
   unfold fold
   simp only [FoldTarget.mkAnd]
   rw [fold.denote_go_and]

diff --git a/LeanSAT/AIG/RefStreamOperator/Map.lean b/LeanSAT/AIG/RefStreamOperator/Map.lean
@@ -23,9 +23,8 @@ namespace LawfulMapOperator
 
 @[simp]
 theorem denote_prefix_cast_ref {aig : AIG α} {input1 input2 : Ref aig}
-    {f : (aig : AIG α) → Ref aig → Entrypoint α}
-    [LawfulOperator α Ref f] [LawfulMapOperator α f] {h}
-      :
+    {f : (aig : AIG α) → Ref aig → Entrypoint α} [LawfulOperator α Ref f] [LawfulMapOperator α f]
+    {h} :
     ⟦f (f aig input1).aig (input2.cast h), assign⟧
       =
     ⟦f aig input2, assign⟧ := by
@@ -55,8 +54,8 @@ where
   @[specialize]
   go {len : Nat} (aig : AIG α) (idx : Nat) (hidx : idx ≤ len) (s : RefStream aig idx)
       (input : RefStream aig len) (f : (aig : AIG α) → Ref aig → Entrypoint α)
-      [LawfulOperator α Ref f] [LawfulMapOperator α f]
-      : RefStreamEntry α len :=
+      [LawfulOperator α Ref f] [LawfulMapOperator α f] :
+      RefStreamEntry α len :=
     if hidx:idx < len then
       let res := f aig (input.get idx hidx)
       let aig := res.aig
@@ -76,8 +75,8 @@ where
 
 theorem map.go_le_size {aig : AIG α} (idx : Nat) (hidx) (s : RefStream aig idx)
     (input : RefStream aig len) (f : (aig : AIG α) → Ref aig → Entrypoint α)
-    [LawfulOperator α Ref f] [LawfulMapOperator α f]
-    : aig.decls.size ≤ (go aig idx hidx s input f).aig.decls.size := by
+    [LawfulOperator α Ref f] [LawfulMapOperator α f] :
+    aig.decls.size ≤ (go aig idx hidx s input f).aig.decls.size := by
   unfold go
   split
   . next h =>
@@ -87,15 +86,15 @@ theorem map.go_le_size {aig : AIG α} (idx : Nat) (hidx) (s : RefStream aig idx)
   . simp
   termination_by len - idx
 
-theorem map_le_size {aig : AIG α} (target : MapTarget aig len)
-    : aig.decls.size ≤ (map aig target).aig.decls.size := by
+theorem map_le_size {aig : AIG α} (target : MapTarget aig len) :
+    aig.decls.size ≤ (map aig target).aig.decls.size := by
   unfold map
   apply map.go_le_size
 
 theorem map.go_decl_eq {aig : AIG α} (i) (hi)
     (s : RefStream aig i) (input : RefStream aig len) (f : (aig : AIG α) → Ref aig → Entrypoint α)
-    [LawfulOperator α Ref f] [LawfulMapOperator α f]
-    : ∀ (idx : Nat) (h1) (h2), (go aig i hi s input f).1.decls[idx]'h2 = aig.decls[idx]'h1 := by
+    [LawfulOperator α Ref f] [LawfulMapOperator α f] :
+    ∀ (idx : Nat) (h1) (h2), (go aig i hi s input f).1.decls[idx]'h2 = aig.decls[idx]'h1 := by
   generalize hgo : go aig i hi s input f = res
   unfold go at hgo
   split at hgo
@@ -112,11 +111,11 @@ theorem map.go_decl_eq {aig : AIG α} (i) (hi)
     simp
 termination_by len - i
 
-theorem map_decl_eq {aig : AIG α} (target : MapTarget aig len)
-    : ∀ idx (h1 : idx < aig.decls.size) (h2),
-        (map aig target).1.decls[idx]'h2
-          =
-        aig.decls[idx]'h1 := by
+theorem map_decl_eq {aig : AIG α} (target : MapTarget aig len) :
+    ∀ idx (h1 : idx < aig.decls.size) (h2),
+      (map aig target).1.decls[idx]'h2
+        =
+      aig.decls[idx]'h1 := by
   intros
   unfold map
   apply map.go_decl_eq
@@ -129,12 +128,12 @@ namespace map
 
 theorem go_get_aux {aig : AIG α} (curr : Nat) (hcurr : curr ≤ len) (s : RefStream aig curr)
     (input : RefStream aig len) (f : (aig : AIG α) → Ref aig → Entrypoint α)
-    [LawfulOperator α Ref f] [LawfulMapOperator α f]
+    [LawfulOperator α Ref f] [LawfulMapOperator α f] :
     -- The hfoo here is a trick to make the dependent type gods happy
-    : ∀ (idx : Nat) (hidx : idx < curr) (hfoo),
-        (go aig curr hcurr s input f).stream.get idx (by omega)
-          =
-        (s.get idx hidx).cast hfoo := by
+    ∀ (idx : Nat) (hidx : idx < curr) (hfoo),
+      (go aig curr hcurr s input f).stream.get idx (by omega)
+        =
+      (s.get idx hidx).cast hfoo := by
   intro idx hidx
   generalize hgo : go aig curr hcurr s input f = res
   unfold go at hgo
@@ -158,20 +157,20 @@ theorem go_get_aux {aig : AIG α} (curr : Nat) (hcurr : curr ≤ len) (s : RefSt
 termination_by len - curr
 
 theorem go_get {aig : AIG α} (curr : Nat) (hcurr : curr ≤ len) (s : RefStream aig curr)
-      (input : RefStream aig len) (f : (aig : AIG α) → Ref aig → Entrypoint α)
-      [LawfulOperator α Ref f] [LawfulMapOperator α f]
-    : ∀ (idx : Nat) (hidx : idx < curr),
-        (go aig curr hcurr s input f).stream.get idx (by omega)
-          =
-        (s.get idx hidx).cast (by apply go_le_size) := by
+    (input : RefStream aig len) (f : (aig : AIG α) → Ref aig → Entrypoint α)
+    [LawfulOperator α Ref f] [LawfulMapOperator α f] :
+    ∀ (idx : Nat) (hidx : idx < curr),
+      (go aig curr hcurr s input f).stream.get idx (by omega)
+        =
+      (s.get idx hidx).cast (by apply go_le_size) := by
   intros
   apply go_get_aux
 
 theorem go_denote_mem_prefix {aig : AIG α} (curr : Nat) (hcurr : curr ≤ len)
-      (s : RefStream aig curr) (input : RefStream aig len)
-      (f : (aig : AIG α) → Ref aig → Entrypoint α) [LawfulOperator α Ref f] [LawfulMapOperator α f]
-      (start : Nat) (hstart)
-  : ⟦
+    (s : RefStream aig curr) (input : RefStream aig len)
+    (f : (aig : AIG α) → Ref aig → Entrypoint α) [LawfulOperator α Ref f] [LawfulMapOperator α f]
+    (start : Nat) (hstart) :
+    ⟦
       (go aig curr hcurr s input f).aig,
       ⟨start, by apply Nat.lt_of_lt_of_le; exact hstart; apply go_le_size⟩,
       assign
@@ -186,14 +185,14 @@ theorem go_denote_mem_prefix {aig : AIG α} (curr : Nat) (hcurr : curr ≤ len)
     apply go_le_size
 
 theorem denote_go {aig : AIG α} (curr : Nat) (hcurr : curr ≤ len) (s : RefStream aig curr)
-      (input : RefStream aig len) (f : (aig : AIG α) → Ref aig → Entrypoint α)
-      [LawfulOperator α Ref f] [LawfulMapOperator α f]
-    : ∀ (idx : Nat) (hidx1 : idx < len),
-        curr ≤ idx
-          →
-        ⟦(go aig curr hcurr s input f).aig, (go aig curr hcurr s input f).stream.get idx hidx1, assign⟧
-          =
-        ⟦f aig (input.get idx hidx1), assign⟧ := by
+    (input : RefStream aig len) (f : (aig : AIG α) → Ref aig → Entrypoint α)
+    [LawfulOperator α Ref f] [LawfulMapOperator α f] :
+    ∀ (idx : Nat) (hidx1 : idx < len),
+      curr ≤ idx
+        →
+      ⟦(go aig curr hcurr s input f).aig, (go aig curr hcurr s input f).stream.get idx hidx1, assign⟧
+        =
+      ⟦f aig (input.get idx hidx1), assign⟧ := by
   intro idx hidx1 hidx2
   generalize hgo : go aig curr hcurr s input f = res
   unfold go at hgo
@@ -220,11 +219,11 @@ termination_by len - curr
 end map
 
 @[simp]
-theorem denote_map {aig : AIG α} (target : MapTarget aig len)
-    : ∀ (idx : Nat) (hidx : idx < len),
-        ⟦(map aig target).aig, (map aig target).stream.get idx hidx, assign⟧
-          =
-        ⟦target.func aig (target.stream.get idx hidx), assign⟧ := by
+theorem denote_map {aig : AIG α} (target : MapTarget aig len) :
+    ∀ (idx : Nat) (hidx : idx < len),
+      ⟦(map aig target).aig, (map aig target).stream.get idx hidx, assign⟧
+        =
+      ⟦target.func aig (target.stream.get idx hidx), assign⟧ := by
   intro idx hidx
   unfold map
   apply map.denote_go