refactor: turn the AIG framework's RefVec from Array to Vector

src/Std/Sat/AIG/Basic.lean

@@ -5,6 +5,7 @@ Authors: Henrik Böving
 -/
 prelude
 import Std.Data.HashSet
+import Init.Data.Vector.Basic
 
 namespace Std
 namespace Sat
@@ -348,8 +349,7 @@ where
 A vector of references into `aig`. This is the `AIG` analog of `BitVec`.
 -/
 structure RefVec (aig : AIG α) (w : Nat) where
-  refs : Array (Nat × Bool)
-  hlen : refs.size = w
+  refs : Vector (Nat × Bool) w
   hrefs : ∀ (h : i < w), refs[i].1 < aig.decls.size
 
 /--

src/Std/Sat/AIG/RefVec.lean

@@ -6,6 +6,7 @@ Authors: Henrik Böving
 prelude
 import Std.Sat.AIG.LawfulOperator
 import Std.Sat.AIG.CachedGatesLemmas
+import Init.Data.Vector.Lemmas
 
 namespace Std
 namespace Sat
@@ -17,13 +18,11 @@ variable {α : Type} [Hashable α] [DecidableEq α] {aig : AIG α}
 namespace RefVec
 
 def empty : RefVec aig 0 where
-  refs := #[]
-  hlen := by simp
+  refs := #v[]
   hrefs := by intros; contradiction
 
 def emptyWithCapacity (c : Nat) : RefVec aig 0 where
-  refs := Array.emptyWithCapacity c
-  hlen := by simp
+  refs := Vector.emptyWithCapacity c
   hrefs := by intros; contradiction
 
 @[simp]
@@ -33,17 +32,15 @@ theorem emptyWithCapacity_eq : emptyWithCapacity (aig := aig) c = empty := by
 @[inline]
 def cast' {aig1 aig2 : AIG α} (s : RefVec aig1 len)
     (h :
-      (∀ {i : Nat} (h : i < len), (s.refs[i]'(by have := s.hlen; omega)).1 < aig1.decls.size)
-        → ∀ {i : Nat} (h : i < len), (s.refs[i]'(by have := s.hlen; omega)).1 < aig2.decls.size) :
+      (∀ {i : Nat} (h : i < len), s.refs[i].1 < aig1.decls.size)
+        → ∀ {i : Nat} (h : i < len), s.refs[i].1 < aig2.decls.size) :
     RefVec aig2 len :=
   { s with
     hrefs := by
       intros
       apply h
-      · intros
-        apply s.hrefs
-        assumption
-      · assumption
+      intros
+      apply s.hrefs
   }
 
 @[inline]
@@ -56,22 +53,20 @@ def cast {aig1 aig2 : AIG α} (s : RefVec aig1 len) (h : aig1.decls.size ≤ aig
 
 @[inline]
 def get (s : RefVec aig len) (idx : Nat) (hidx : idx < len) : Ref aig :=
-  let ⟨refs, hlen, hrefs⟩ := s
-  let ref := refs[idx]'(by rw [hlen]; assumption)
-  ⟨ref.1, ref.2, by apply hrefs; assumption⟩
+  let ⟨refs, hrefs⟩ := s
+  let ref := refs[idx]
+  ⟨ref.1, ref.2, hrefs ..⟩
 
 @[inline]
 def push (s : RefVec aig len) (ref : AIG.Ref aig) : RefVec aig (len + 1) :=
-  let ⟨refs, hlen, hrefs⟩ := s
+  let ⟨refs, hrefs⟩ := s
   ⟨
     refs.push (ref.gate, ref.invert),
-    by simp [hlen],
     by
       intro i hi
-      simp only [Array.getElem_push]
+      simp only [Vector.getElem_push hi]
       split
       · apply hrefs
-        omega
       · apply AIG.Ref.hgate
   ⟩
 
@@ -83,15 +78,13 @@ theorem cast_cast {aig1 aig2 aig3 : AIG α} (s : RefVec aig1 len)
 @[simp]
 theorem get_push_ref_eq (s : RefVec aig len) (ref : AIG.Ref aig) :
     (s.push ref).get len (by omega) = ref := by
-  have := s.hlen
-  simp [get, push, ← this]
+  simp [get, push]
 
 -- This variant exists because it is sometimes hard to rewrite properly with DTT.
 theorem get_push_ref_eq' (s : RefVec aig len) (ref : AIG.Ref aig) (idx : Nat)
     (hidx : idx = len) :
     (s.push ref).get idx (by omega) = ref := by
-  have := s.hlen
-  simp [get, push, ← this, hidx]
+  simp [get, push, hidx]
 
 theorem get_push_ref_lt (s : RefVec aig len) (ref : AIG.Ref aig) (idx : Nat)
     (hidx : idx < len) :
@@ -99,9 +92,9 @@ theorem get_push_ref_lt (s : RefVec aig len) (ref : AIG.Ref aig) (idx : Nat)
   simp only [get, push, Ref.mk.injEq]
   cases ref
   simp only [Ref.mk.injEq]
-  rw [Array.getElem_push_lt]
+  rw [Vector.getElem_push_lt]
   · simp
-  · simp [hlen, hidx]
+  · simp [hidx]
 
 @[simp]
 theorem get_cast {aig1 aig2 : AIG α} (s : RefVec aig1 len) (idx : Nat) (hidx : idx < len)
@@ -113,20 +106,18 @@ theorem get_cast {aig1 aig2 : AIG α} (s : RefVec aig1 len) (idx : Nat) (hidx :
 
 @[inline]
 def append (lhs : RefVec aig lw) (rhs : RefVec aig rw) : RefVec aig (lw + rw) :=
-  let ⟨lrefs, hl1, hl2⟩ := lhs
-  let ⟨rrefs, hr1, hr2⟩ := rhs
+  let ⟨lrefs, hl⟩ := lhs
+  let ⟨rrefs, hr⟩ := rhs
   ⟨
     lrefs ++ rrefs,
-    by simp [Array.size_append, hl1, hr1],
     by
       intro i h
-      by_cases hsplit : i < lrefs.size
-      · rw [Array.getElem_append_left]
-        apply hl2
+      by_cases hsplit : i < lw
+      · rw [Vector.getElem_append_left]
+        apply hl
         omega
-      · rw [Array.getElem_append_right]
-        · apply hr2
-          omega
+      · rw [Vector.getElem_append_right]
+        · apply hr
         · omega
   ⟩
 
@@ -141,15 +132,13 @@ theorem get_append (lhs : RefVec aig lw) (rhs : RefVec aig rw) (idx : Nat)
   simp only [get, append]
   split
   · simp [Ref.mk.injEq]
-    rw [Array.getElem_append_left]
+    rw [Vector.getElem_append_left]
     · simp
-    · rw [lhs.hlen]
-      assumption
+    · assumption
   · simp only [Ref.mk.injEq]
-    rw [Array.getElem_append_right]
-    · simp [lhs.hlen]
-    · rw [lhs.hlen]
-      omega
+    rw [Vector.getElem_append_right]
+    · simp
+    · omega
 
 @[inline]
 def getD (s : RefVec aig len) (idx : Nat) (alt : Ref aig) : Ref aig :=
@@ -176,7 +165,7 @@ def countKnown [Inhabited α] (aig : AIG α) (s : RefVec aig len) : Nat := Id.ru
     match decl with
     | .const .. => acc + 1
     | _ => acc
-  return s.refs.foldl (init := 0) folder
+  return s.refs.foldl (b := 0) folder
 
 end RefVec
 

src/Std/Sat/AIG/RefVecOperator/Fold.lean

@@ -186,7 +186,6 @@ theorem denote_fold_and {aig : AIG α} (s : RefVec aig len) :
       rw [AIG.LawfulOperator.denote_mem_prefix (f := mkConstCached)]
       · simp only [← h]
       · apply RefVec.hrefs
-        simp [FoldTarget.mkAnd, hidx]
   · omega
 
 end RefVec

src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Extract.lean

@@ -91,8 +91,7 @@ theorem denote_blastExtract (aig : AIG α) (target : ExtractTarget aig newWidth)
       split
       · rw [RefVec.get_in_bound]
         rw [LawfulOperator.denote_mem_prefix (f := mkConstCached)]
-        · congr 1
-        · assumption
+        congr 1
       · rw [RefVec.get_out_bound]
         · simp
         · omega

src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Ult.lean

@@ -38,7 +38,6 @@ theorem mkUlt_denote_eq (aig : AIG α) (lhs rhs : BitVec w) (input : BinaryRefVe
     rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
     rw [AIG.LawfulVecOperator.denote_mem_prefix (f := BVExpr.bitblast.blastNot)]
     apply hleft
-    assumption
   · dsimp only
     intro idx hidx
     rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]