max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: cleanup unused variables in bv_decide (#5578)

Browse source 
This pulls the changes to `bv_decide` out of #5338.
This commit is contained in:
Kim Morrison 2024-10-02 11:48:43 +10:00 • committed by GitHub
parent 6cd80c28b7
commit 867e67b9f3
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
10 changed files with 54 additions and 48 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/Std/Sat/AIG/CNF.lean
View file

@ -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

2
src/Std/Sat/AIG/RefVecOperator/Zip.lean
View file

@ -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⟩

12
src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Carry.lean
View file

@ -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

16
src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Mul.lean
View file

@ -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

19
src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/ShiftLeft.lean
View file

@ -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

19
src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/ShiftRight.lean
View file

@ -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

4
src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Carry.lean
View file

@ -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]

8
src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Mul.lean
View file

@ -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)]

8
src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftLeft.lean
View file

@ -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]

8
src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftRight.lean
View file

@ -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]