From 867e67b9f3a25486a2fa75dfd7b8d20b4a5b8672 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 2 Oct 2024 11:48:43 +1000 Subject: [PATCH] chore: cleanup unused variables in bv_decide (#5578) This pulls the changes to `bv_decide` out of #5338. --- src/Std/Sat/AIG/CNF.lean | 6 +++--- src/Std/Sat/AIG/RefVecOperator/Zip.lean | 2 +- .../Bitblast/BVExpr/Circuit/Impl/Carry.lean | 12 ++++++------ .../BVExpr/Circuit/Impl/Operations/Mul.lean | 16 ++++++++-------- .../Circuit/Impl/Operations/ShiftLeft.lean | 19 +++++++++---------- .../Circuit/Impl/Operations/ShiftRight.lean | 19 +++++++++---------- .../Bitblast/BVExpr/Circuit/Lemmas/Carry.lean | 4 +++- .../BVExpr/Circuit/Lemmas/Operations/Mul.lean | 8 +++++--- .../Circuit/Lemmas/Operations/ShiftLeft.lean | 8 +++++--- .../Circuit/Lemmas/Operations/ShiftRight.lean | 8 +++++--- 10 files changed, 54 insertions(+), 48 deletions(-) diff --git a/src/Std/Sat/AIG/CNF.lean b/src/Std/Sat/AIG/CNF.lean index 753af133b9..7e7c9d7696 100644 --- 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 index 2c9659cbaf..49c73e107b 100644 --- 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 index 0b3d757186..9f9a3cb5e1 100644 --- 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,7 +43,7 @@ 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 @@ -51,7 +51,7 @@ where 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 index b57c5b8507..6f13321b13 100644 --- 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 index 39df3d63f2..776938ba76 100644 --- 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 index 539adb9d29..221f1ebd09 100644 --- 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 index 50678be49d..71412d88a3 100644 --- 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 index 815307dd57..f36ecf40a4 100644 --- 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 index 146e32d48e..c10d0ad71c 100644 --- 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 index cd525696b3..4e189a90dd 100644 --- 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]