chore: cleanup unused variables in bv_decide (#5578)

This pulls the changes to `bv_decide` out of #5338.
leanprover · Oct 2, 2024 · 867e67b · 867e67b
1 parent 6cd80c2
commit 867e67b
Show file tree

Hide file tree

Showing 10 changed files with 54 additions and 48 deletions.
diff --git a/src/Std/Sat/AIG/CNF.lean b/src/Std/Sat/AIG/CNF.lean
@@ -598,9 +598,9 @@ where
     else
       let decl := aig.decls[upper]
       match heq : decl with
-      | .const b => state.addConst upper h heq
-      | .atom a => state.addAtom upper h heq
-      | .gate lhs rhs linv rinv =>
+      | .const _ => state.addConst upper h heq
+      | .atom _ => state.addAtom upper h heq
+      | .gate lhs rhs _ _ =>
         have := aig.invariant h heq
         let ⟨lstate, hlstate⟩ := go aig lhs (by omega) state
         let ⟨rstate, hrstate⟩ := go aig rhs (by omega) lstate

diff --git a/src/Std/Sat/AIG/RefVecOperator/Zip.lean b/src/Std/Sat/AIG/RefVecOperator/Zip.lean
@@ -85,7 +85,7 @@ where
   @[specialize]
   go (aig : AIG α) (idx : Nat) (s : RefVec aig idx) (hidx : idx ≤ len)
       (lhs rhs : RefVec aig len) (f : (aig : AIG α) → BinaryInput aig → Entrypoint α)
-      [LawfulOperator α BinaryInput f] [chainable : LawfulZipOperator α f] :
+      [LawfulOperator α BinaryInput f] [LawfulZipOperator α f] :
       RefVecEntry α len :=
     if hidx : idx < len then
       let res := f aig ⟨lhs.get idx hidx, rhs.get idx hidx⟩

diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Carry.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Carry.lean
@@ -29,9 +29,9 @@ structure OverflowInput (aig : AIG α) where
 
 def mkOverflowBit (aig : AIG α) (input : OverflowInput aig) : AIG.Entrypoint α :=
   let ⟨_, ⟨lhs, rhs⟩, cin⟩ := input
-  go aig lhs rhs 0 (by omega) cin
+  go aig lhs rhs 0 cin
 where
-  go {w : Nat} (aig : AIG α) (lhs rhs : AIG.RefVec aig w) (curr : Nat) (hcurr : curr ≤ w)
+  go {w : Nat} (aig : AIG α) (lhs rhs : AIG.RefVec aig w) (curr : Nat)
       (cin : AIG.Ref aig) :
       AIG.Entrypoint α :=
     if hidx : curr < w then
@@ -43,15 +43,15 @@ where
       let carryRef := res.ref
       let lhs := lhs.cast this
       let rhs := rhs.cast this
-      go aig lhs rhs (curr + 1) (by omega) carryRef
+      go aig lhs rhs (curr + 1) carryRef
     else
       ⟨aig, cin⟩
   termination_by w - curr
 
 namespace mkOverflowBit
 
 theorem go_le_size {aig : AIG α} {cin} {lhs rhs : AIG.RefVec aig w} :
-    aig.decls.size ≤ (go aig lhs rhs curr hcurr cin).aig.decls.size := by
+    aig.decls.size ≤ (go aig lhs rhs curr cin).aig.decls.size := by
   unfold go
   dsimp only
   split
@@ -63,8 +63,8 @@ termination_by w - curr
 
 theorem go_decl_eq {aig : AIG α} {cin} {lhs rhs : AIG.RefVec aig w} :
     ∀ (idx : Nat) (h1) (h2),
-        (go aig lhs rhs curr hcurr cin).aig.decls[idx]'h2 = aig.decls[idx]'h1 := by
-  generalize hgo : go aig lhs rhs curr hcurr cin = res
+        (go aig lhs rhs curr cin).aig.decls[idx]'h2 = aig.decls[idx]'h1 := by
+  generalize hgo : go aig lhs rhs curr cin = res
   unfold go at hgo
   dsimp only at hgo
   split at hgo

diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Mul.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Mul.lean
@@ -50,9 +50,9 @@ where
       have := AIG.LawfulVecOperator.le_size (f := AIG.RefVec.ite) ..
       let lhs := lhs.cast this
       let rhs := rhs.cast this
-      go aig lhs rhs 1 (by omega) acc
+      go aig lhs rhs 1 acc
 
-  go (aig : AIG BVBit) (lhs rhs : AIG.RefVec aig w) (curr : Nat) (hcurr : curr ≤ w)
+  go (aig : AIG BVBit) (lhs rhs : AIG.RefVec aig w) (curr : Nat)
       (acc : AIG.RefVec aig w) :
       AIG.RefVecEntry BVBit w :=
     if h : curr < w then
@@ -76,15 +76,15 @@ where
       have := by apply AIG.LawfulVecOperator.le_size (f := AIG.RefVec.ite)
       let lhs := lhs.cast this
       let rhs := rhs.cast this
-      go aig lhs rhs (curr + 1) (by omega) acc
+      go aig lhs rhs (curr + 1) acc
     else
       ⟨aig, acc⟩
 
 namespace blastMul
 
-theorem go_le_size {w : Nat} (aig : AIG BVBit) (curr : Nat) (hcurr : curr ≤ w) (acc : AIG.RefVec aig w)
+theorem go_le_size {w : Nat} (aig : AIG BVBit) (curr : Nat) (acc : AIG.RefVec aig w)
     (lhs rhs : AIG.RefVec aig w) :
-    aig.decls.size ≤ (go aig lhs rhs curr hcurr acc).aig.decls.size := by
+    aig.decls.size ≤ (go aig lhs rhs curr acc).aig.decls.size := by
   unfold go
   split
   · dsimp only
@@ -94,11 +94,11 @@ theorem go_le_size {w : Nat} (aig : AIG BVBit) (curr : Nat) (hcurr : curr ≤ w)
     apply AIG.LawfulVecOperator.le_size (f := blastShiftLeftConst)
   · simp
 
-theorem go_decl_eq {w : Nat} (aig : AIG BVBit) (curr : Nat) (hcurr : curr ≤ w) (acc : AIG.RefVec aig w)
+theorem go_decl_eq {w : Nat} (aig : AIG BVBit) (curr : Nat) (acc : AIG.RefVec aig w)
     (lhs rhs : AIG.RefVec aig w) :
     ∀ (idx : Nat) (h1) (h2),
-       (go aig lhs rhs curr hcurr acc).aig.decls[idx]'h2 = aig.decls[idx]'h1 := by
-  generalize hgo : go aig lhs rhs curr hcurr acc = res
+       (go aig lhs rhs curr acc).aig.decls[idx]'h2 = aig.decls[idx]'h1 := by
+  generalize hgo : go aig lhs rhs curr acc = res
   unfold go at hgo
   split at hgo
   · dsimp only at hgo

diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/ShiftLeft.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/ShiftLeft.lean
@@ -152,27 +152,26 @@ def blastShiftLeft (aig : AIG α) (target : AIG.ArbitraryShiftTarget aig w) :
     let acc := res.vec
     have := AIG.LawfulVecOperator.le_size (f := blastShiftLeft.twoPowShift) ..
     let distance := distance.cast this
-    go aig distance 0 (by omega) acc
+    go aig distance 0 acc
 where
-  go {n : Nat} (aig : AIG α) (distance : AIG.RefVec aig n) (curr : Nat) (hcurr : curr ≤ n - 1)
+  go {n : Nat} (aig : AIG α) (distance : AIG.RefVec aig n) (curr : Nat)
       (acc : AIG.RefVec aig w) :
       AIG.RefVecEntry α w :=
-    if h : curr < n - 1 then
+    if curr < n - 1 then
       let res := blastShiftLeft.twoPowShift aig ⟨_, acc, distance, curr + 1⟩
       let aig := res.aig
       let acc := res.vec
       have := AIG.LawfulVecOperator.le_size (f := blastShiftLeft.twoPowShift) ..
       let distance := distance.cast this
-
-      go aig distance (curr + 1) (by omega) acc
+      go aig distance (curr + 1) acc
     else
       ⟨aig, acc⟩
   termination_by n - 1 - curr
 
 
 theorem blastShiftLeft.go_le_size (aig : AIG α) (distance : AIG.RefVec aig n) (curr : Nat)
-    (hcurr : curr ≤ n - 1) (acc : AIG.RefVec aig w) :
-    aig.decls.size ≤ (go aig distance curr hcurr acc).aig.decls.size := by
+    (acc : AIG.RefVec aig w) :
+    aig.decls.size ≤ (go aig distance curr acc).aig.decls.size := by
   unfold go
   dsimp only
   split
@@ -182,10 +181,10 @@ theorem blastShiftLeft.go_le_size (aig : AIG α) (distance : AIG.RefVec aig n) (
 termination_by n - 1 - curr
 
 theorem blastShiftLeft.go_decl_eq (aig : AIG α) (distance : AIG.RefVec aig n) (curr : Nat)
-    (hcurr : curr ≤ n - 1) (acc : AIG.RefVec aig w) :
+    (acc : AIG.RefVec aig w) :
     ∀ (idx : Nat) (h1) (h2),
-        (go aig distance curr hcurr acc).aig.decls[idx]'h2 = aig.decls[idx]'h1 := by
-  generalize hgo : go aig distance curr hcurr acc = res
+        (go aig distance curr acc).aig.decls[idx]'h2 = aig.decls[idx]'h1 := by
+  generalize hgo : go aig distance curr acc = res
   unfold go at hgo
   dsimp only at hgo
   split at hgo

diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/ShiftRight.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/ShiftRight.lean
@@ -181,26 +181,25 @@ def blastShiftRight (aig : AIG α) (target : AIG.ArbitraryShiftTarget aig w) :
     let acc := res.vec
     have := AIG.LawfulVecOperator.le_size (f := blastShiftRight.twoPowShift) ..
     let distance := distance.cast this
-    go aig distance 0 (by omega) acc
+    go aig distance 0 acc
 where
-  go {n : Nat} (aig : AIG α) (distance : AIG.RefVec aig n) (curr : Nat) (hcurr : curr ≤ n - 1)
+  go {n : Nat} (aig : AIG α) (distance : AIG.RefVec aig n) (curr : Nat)
       (acc : AIG.RefVec aig w) :
       AIG.RefVecEntry α w :=
-    if h : curr < n - 1 then
+    if curr < n - 1 then
       let res := blastShiftRight.twoPowShift aig ⟨_, acc, distance, curr + 1⟩
       let aig := res.aig
       let acc := res.vec
       have := AIG.LawfulVecOperator.le_size (f := blastShiftRight.twoPowShift) ..
       let distance := distance.cast this
-
-      go aig distance (curr + 1) (by omega) acc
+      go aig distance (curr + 1) acc
     else
       ⟨aig, acc⟩
   termination_by n - 1 - curr
 
 theorem blastShiftRight.go_le_size (aig : AIG α) (distance : AIG.RefVec aig n) (curr : Nat)
-    (hcurr : curr ≤ n - 1) (acc : AIG.RefVec aig w) :
-    aig.decls.size ≤ (go aig distance curr hcurr acc).aig.decls.size := by
+    (acc : AIG.RefVec aig w) :
+    aig.decls.size ≤ (go aig distance curr acc).aig.decls.size := by
   unfold go
   dsimp only
   split
@@ -210,10 +209,10 @@ theorem blastShiftRight.go_le_size (aig : AIG α) (distance : AIG.RefVec aig n)
 termination_by n - 1 - curr
 
 theorem blastShiftRight.go_decl_eq (aig : AIG α) (distance : AIG.RefVec aig n) (curr : Nat)
-    (hcurr : curr ≤ n - 1) (acc : AIG.RefVec aig w) :
+    (acc : AIG.RefVec aig w) :
     ∀ (idx : Nat) (h1) (h2),
-        (go aig distance curr hcurr acc).aig.decls[idx]'h2 = aig.decls[idx]'h1 := by
-  generalize hgo : go aig distance curr hcurr acc = res
+        (go aig distance curr acc).aig.decls[idx]'h2 = aig.decls[idx]'h1 := by
+  generalize hgo : go aig distance curr acc = res
   unfold go at hgo
   dsimp only at hgo
   split at hgo

diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Carry.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Carry.lean
@@ -29,7 +29,7 @@ theorem go_eq_carry (aig : AIG α) (curr : Nat) (hcurr : curr ≤ w) (cin : Ref
     (hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, lhs.get idx hidx, assign⟧ = lhsExpr.getLsbD idx)
     (hright : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, rhs.get idx hidx, assign⟧ = rhsExpr.getLsbD idx)
     (hcin : ⟦aig, cin, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦aig, origCin, assign⟧) :
-    ⟦go aig lhs rhs curr hcurr cin, assign⟧
+    ⟦go aig lhs rhs curr cin, assign⟧
       =
     BitVec.carry w lhsExpr rhsExpr ⟦aig, origCin, assign⟧ := by
   unfold go
@@ -38,6 +38,7 @@ theorem go_eq_carry (aig : AIG α) (curr : Nat) (hcurr : curr ≤ w) (cin : Ref
   · rw [go_eq_carry]
     · congr 1
       rw [AIG.LawfulOperator.denote_mem_prefix (f := mkFullAdderCarry)]
+    · omega
     · intros
       rw [AIG.LawfulOperator.denote_mem_prefix (f := mkFullAdderCarry)]
       · simp [hleft]
@@ -67,6 +68,7 @@ theorem mkOverflowBit_eq_carry (aig : AIG α) (input : OverflowInput aig) (lhs r
   unfold mkOverflowBit
   dsimp only
   apply mkOverflowBit.go_eq_carry
+  · omega
   · assumption
   · assumption
   · simp [BitVec.carry_zero]

diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Mul.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Mul.lean
@@ -35,19 +35,20 @@ theorem go_denote_eq {w : Nat} (aig : AIG BVBit) (curr : Nat) (hcurr : curr + 1
                 (BitVec.mulRec lexpr rexpr curr).getLsbD idx) :
     ∀ (idx : Nat) (hidx : idx < w),
         ⟦
-          (go aig lhs rhs (curr + 1) hcurr acc).aig,
-          (go aig lhs rhs (curr + 1) hcurr acc).vec.get idx hidx,
+          (go aig lhs rhs (curr + 1) acc).aig,
+          (go aig lhs rhs (curr + 1) acc).vec.get idx hidx,
           assign.toAIGAssignment
         ⟧
           =
         (BitVec.mulRec lexpr rexpr w).getLsbD idx := by
   intro idx hidx
-  generalize hgo: go aig lhs rhs (curr + 1) hcurr acc = res
+  generalize hgo: go aig lhs rhs (curr + 1) acc = res
   unfold go at hgo
   split at hgo
   · dsimp only at hgo
     rw [← hgo]
     rw [go_denote_eq]
+    · omega
     · intro idx hidx
       simp only [RefVec.get_cast, Ref.cast_eq]
       rw [AIG.LawfulVecOperator.denote_mem_prefix (f := RefVec.ite)]
@@ -128,6 +129,7 @@ theorem denote_blast (aig : AIG BVBit) (lhs rhs : BitVec w) (assign : Assignment
     subst hw
     rw [← hb]
     rw [go_denote_eq]
+    · omega
     · intro idx hidx
       rw [AIG.LawfulVecOperator.denote_mem_prefix (f := RefVec.ite)]
       rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastConst)]

diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftLeft.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftLeft.lean
@@ -240,19 +240,20 @@ theorem go_denote_eq (aig : AIG α) (distance : AIG.RefVec aig n) (curr : Nat)
     (hright : ∀ (idx : Nat) (hidx : idx < n), ⟦aig, distance.get idx hidx, assign⟧ = rhs.getLsbD idx) :
     ∀ (idx : Nat) (hidx : idx < w),
         ⟦
-          (go aig distance curr hcurr acc).aig,
-          (go aig distance curr hcurr acc).vec.get idx hidx,
+          (go aig distance curr acc).aig,
+          (go aig distance curr acc).vec.get idx hidx,
           assign
         ⟧
           =
         (BitVec.shiftLeftRec lhs rhs (n - 1)).getLsbD idx := by
   intro idx hidx
-  generalize hgo : go aig distance curr hcurr acc = res
+  generalize hgo : go aig distance curr acc = res
   unfold go at hgo
   dsimp only at hgo
   split at hgo
   · rw [← hgo]
     rw [go_denote_eq]
+    · omega
     · intro idx hidx
       simp only [BitVec.shiftLeftRec_succ]
       rw [twoPowShift_eq (lhs := BitVec.shiftLeftRec lhs rhs curr)]
@@ -299,6 +300,7 @@ theorem denote_blastShiftLeft (aig : AIG α) (target : ArbitraryShiftTarget aig
     apply BitVec.lt_of_getLsbD
   · rw [← hg]
     rw [blastShiftLeft.go_denote_eq]
+    · omega
     · intro idx hidx
       simp only [BitVec.shiftLeftRec_zero]
       rw [blastShiftLeft.twoPowShift_eq]

diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftRight.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftRight.lean
@@ -324,19 +324,20 @@ theorem go_denote_eq (aig : AIG α) (distance : AIG.RefVec aig n) (curr : Nat)
     (hright : ∀ (idx : Nat) (hidx : idx < n), ⟦aig, distance.get idx hidx, assign⟧ = rhs.getLsbD idx) :
     ∀ (idx : Nat) (hidx : idx < w),
         ⟦
-          (go aig distance curr hcurr acc).aig,
-          (go aig distance curr hcurr acc).vec.get idx hidx,
+          (go aig distance curr acc).aig,
+          (go aig distance curr acc).vec.get idx hidx,
           assign
         ⟧
           =
         (BitVec.ushiftRightRec lhs rhs (n - 1)).getLsbD idx := by
   intro idx hidx
-  generalize hgo : go aig distance curr hcurr acc = res
+  generalize hgo : go aig distance curr acc = res
   unfold go at hgo
   dsimp only at hgo
   split at hgo
   · rw [← hgo]
     rw [go_denote_eq]
+    · omega
     · intro idx hidx
       simp only [BitVec.ushiftRightRec_succ]
       rw [twoPowShift_eq (lhs := BitVec.ushiftRightRec lhs rhs curr)]
@@ -379,6 +380,7 @@ theorem denote_blastShiftRight (aig : AIG α) (target : ArbitraryShiftTarget aig
     simp [hleft, BitVec.and_twoPow]
   · rw [← hres]
     rw [blastShiftRight.go_denote_eq]
+    · omega
     · intro idx hidx
       simp only [BitVec.ushiftRightRec_zero]
       rw [blastShiftRight.twoPowShift_eq]