Skip to content

Commit 10e4c95

Browse files
luisacicoliniluisacicolini
committed
chore; fix expr sorry
1 parent b78edae commit 10e4c95

File tree

3 files changed

+86
-76
lines changed

3 files changed

+86
-76
lines changed

‎src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Expr.lean‎

Lines changed: 11 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -231,12 +231,12 @@ where
231231
apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := bitblast.blastClz)
232232
omega
233233
⟨⟨res, this⟩, cache.cast (AIG.LawfulVecOperator.le_size (f := bitblast.blastClz) ..)⟩
234-
| .cpop => sorry
235-
-- let res := bitblast.blastPopCount eaig evec
236-
-- have := by
237-
-- apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := bitblast.blastPopCount)
238-
-- omega
239-
-- ⟨⟨res, this⟩, cache.cast (AIG.LawfulVecOperator.le_size (f := bitblast.blastPopCount) ..)⟩
234+
| .cpop =>
235+
let res := bitblast.blastCpop eaig evec
236+
have := by
237+
apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := bitblast.blastCpop)
238+
omega
239+
⟨⟨res, this⟩, cache.cast (AIG.LawfulVecOperator.le_size (f := bitblast.blastCpop) ..)⟩
240240
| .append lhs rhs h =>
241241
let ⟨⟨⟨aig, lhs⟩, hlaig⟩, cache⟩ := goCache aig lhs cache
242242
let ⟨⟨⟨aig, rhs⟩, hraig⟩, cache⟩ := goCache aig rhs cache
@@ -348,11 +348,11 @@ theorem go_decl_eq (aig : AIG BVBit) (expr : BVExpr w) (cache : Cache aig) :
348348
· apply Nat.le_trans <;> assumption
349349
next op expr =>
350350
match op with
351-
| .not | .rotateLeft .. | .rotateRight .. | .arithShiftRightConst .. | .reverse | .clz | .cpop => sorry
352-
-- rw [AIG.LawfulVecOperator.decl_eq]
353-
-- rw [goCache_decl_eq]
354-
-- have := (goCache aig expr cache).result.property
355-
-- exact Nat.lt_of_lt_of_le h1 this
351+
| .not | .rotateLeft .. | .rotateRight .. | .arithShiftRightConst .. | .reverse | .clz | .cpop =>
352+
rw [AIG.LawfulVecOperator.decl_eq]
353+
rw [goCache_decl_eq]
354+
have := (goCache aig expr cache).result.property
355+
exact Nat.lt_of_lt_of_le h1 this
356356
next lhsExpr rhsExpr h =>
357357
have hl := (goCache aig lhsExpr cache).result.property
358358
have hr := (goCache (goCache aig lhsExpr cache).1.1.aig rhsExpr (goCache aig lhsExpr cache).cache).result.property

‎src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean‎

Lines changed: 57 additions & 61 deletions
Original file line numberDiff line numberDiff line change
@@ -220,12 +220,11 @@ theorem go_Inv_of_Inv (cache : Cache aig) (hinv : Cache.Inv assign aig cache) :
220220
split at hres
221221
all_goals
222222
rw [← hres]
223-
sorry
224-
-- dsimp only
225-
-- apply Cache.Inv_cast
226-
-- · apply LawfulVecOperator.isPrefix_aig
227-
-- · apply goCache_Inv_of_Inv
228-
-- exact hinv
223+
dsimp only
224+
apply Cache.Inv_cast
225+
· apply LawfulVecOperator.isPrefix_aig
226+
· apply goCache_Inv_of_Inv
227+
exact hinv
229228
· rw [← hres]
230229
dsimp only
231230
apply Cache.Inv_cast
@@ -387,61 +386,58 @@ theorem go_denote_eq (aig : AIG BVBit) (expr : BVExpr w) (assign : Assignment)
387386
rw [goCache_denote_eq]
388387
apply goCache_Inv_of_Inv
389388
exact hinv
390-
· sorry
391-
-- dsimp only at hres
392-
-- split at hres
393-
-- · rw [← hres]
394-
-- simp only [denote_blastNot, eval_un, BVUnOp.eval_not, hidx, BitVec.getLsbD_eq_getElem,
395-
-- BitVec.getElem_not, Bool.not_eq_eq_eq_not, Bool.not_not]
396-
-- rw [goCache_denote_eq]
397-
-- · apply BitVec.getLsbD_eq_getElem
398-
-- · exact hinv
399-
-- · rw [← hres]
400-
-- simp only [denote_blastRotateLeft, eval_un, BVUnOp.eval_rotateLeft, hidx,
401-
-- BitVec.getLsbD_eq_getElem, BitVec.getElem_rotateLeft]
402-
-- split
403-
-- all_goals
404-
-- rw [goCache_denote_eq]
405-
-- · apply BitVec.getLsbD_eq_getElem
406-
-- · exact hinv
407-
-- · rw [← hres]
408-
-- simp only [denote_blastRotateRight, eval_un, BVUnOp.eval_rotateRight, hidx,
409-
-- BitVec.getLsbD_eq_getElem, BitVec.getElem_rotateRight]
410-
-- split
411-
-- all_goals
412-
-- rw [goCache_denote_eq]
413-
-- · apply BitVec.getLsbD_eq_getElem
414-
-- · exact hinv
415-
-- · rw [← hres]
416-
-- simp only [denote_blastArithShiftRightConst, eval_un, BVUnOp.eval_arithShiftRightConst, hidx,
417-
-- BitVec.getLsbD_eq_getElem, BitVec.getElem_sshiftRight]
418-
-- split
419-
-- · rw [goCache_denote_eq]
420-
-- · apply BitVec.getLsbD_eq_getElem
421-
-- · exact hinv
422-
-- · rw [goCache_denote_eq]
423-
-- · simp [BitVec.msb_eq_getLsbD_last]
424-
-- · exact hinv
425-
-- · rw [← hres]
426-
-- simp only [denote_blastReverse, eval_un, BVUnOp.eval_reverse, hidx, BitVec.getLsbD_eq_getElem,
427-
-- BitVec.getElem_reverse, BitVec.getMsbD_eq_getLsbD, decide_true, Bool.true_and]
428-
-- rw [goCache_denote_eq]
429-
-- exact hinv
430-
-- · rw [← hres]
431-
-- simp only [eval_un, BVUnOp.eval_clz, BitVec.clz]
432-
-- rw [denote_blastClz]
433-
-- intro idx hidx
434-
-- rw [goCache_denote_eq]
435-
-- exact hinv
436-
-- next h =>
437-
-- · rw [← hres]
438-
-- simp only [eval_un, BVUnOp.eval_popCount]
439-
-- sorry
440-
-- -- rw [blastPopCount.denote_blastPopCount]
441-
-- -- intros idx hidx
442-
-- -- rw [goCache_denote_eq]
443-
-- -- exact hinv
444-
· next h =>
389+
· dsimp only at hres
390+
split at hres
391+
· rw [← hres]
392+
simp only [denote_blastNot, eval_un, BVUnOp.eval_not, hidx, BitVec.getLsbD_eq_getElem,
393+
BitVec.getElem_not, Bool.not_eq_eq_eq_not, Bool.not_not]
394+
rw [goCache_denote_eq]
395+
· apply BitVec.getLsbD_eq_getElem
396+
· exact hinv
397+
· rw [← hres]
398+
simp only [denote_blastRotateLeft, eval_un, BVUnOp.eval_rotateLeft, hidx,
399+
BitVec.getLsbD_eq_getElem, BitVec.getElem_rotateLeft]
400+
split
401+
all_goals
402+
rw [goCache_denote_eq]
403+
· apply BitVec.getLsbD_eq_getElem
404+
· exact hinv
405+
· rw [← hres]
406+
simp only [denote_blastRotateRight, eval_un, BVUnOp.eval_rotateRight, hidx,
407+
BitVec.getLsbD_eq_getElem, BitVec.getElem_rotateRight]
408+
split
409+
all_goals
410+
rw [goCache_denote_eq]
411+
· apply BitVec.getLsbD_eq_getElem
412+
· exact hinv
413+
· rw [← hres]
414+
simp only [denote_blastArithShiftRightConst, eval_un, BVUnOp.eval_arithShiftRightConst, hidx,
415+
BitVec.getLsbD_eq_getElem, BitVec.getElem_sshiftRight]
416+
split
417+
· rw [goCache_denote_eq]
418+
· apply BitVec.getLsbD_eq_getElem
419+
· exact hinv
420+
· rw [goCache_denote_eq]
421+
· simp [BitVec.msb_eq_getLsbD_last]
422+
· exact hinv
423+
· rw [← hres]
424+
simp only [denote_blastReverse, eval_un, BVUnOp.eval_reverse, hidx, BitVec.getLsbD_eq_getElem,
425+
BitVec.getElem_reverse, BitVec.getMsbD_eq_getLsbD, decide_true, Bool.true_and]
426+
rw [goCache_denote_eq]
427+
exact hinv
428+
· rw [← hres]
429+
simp only [eval_un, BVUnOp.eval_clz, BitVec.clz]
430+
rw [denote_blastClz]
431+
intro idx hidx
432+
rw [goCache_denote_eq]
433+
exact hinv
434+
· rw [← hres]
435+
simp only [eval_un, BVUnOp.eval_cpop, BitVec.cpop]
436+
rw [denote_blastCpop]
437+
intro idx hidx
438+
rw [goCache_denote_eq]
439+
exact hinv
440+
next h =>
445441
subst h
446442
rw [← hres]
447443
simp only [denote_blastAppend, RefVec.get_cast, Ref.cast_eq, eval_append, BitVec.getLsbD_append]

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

Lines changed: 18 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -438,9 +438,10 @@ theorem denote_go
438438
· exact heq_of_eqRec_eq (congrArg (LT.lt idx) (id (Eq.symm hcast))) rfl
439439
rw [hcasteq]
440440
simp [hpar]
441+
end blastCpop
441442

442443
@[simp]
443-
theorem denote_blastCpop (aig : AIG α) (xc : RefVec aig w) (x : BitVec w) (assign : α → Bool)
444+
theorem denote_blastCpop' (aig : AIG α) (xc : RefVec aig w) (x : BitVec w) (assign : α → Bool)
444445
(hx : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, xc.get idx hidx, assign⟧ = x.getLsbD idx)
445446
:
446447
∀ (idx : Nat) (hidx : idx < w),
@@ -454,11 +455,11 @@ theorem denote_blastCpop (aig : AIG α) (xc : RefVec aig w) (x : BitVec w) (assi
454455
rw [← hgen]
455456
simp only [BitVec.ofNat_eq_ofNat, Lean.Elab.WF.paramLet, BitVec.addRecAux_succ,
456457
BitVec.addRecAux_zero]
457-
rw [denote_go (l_bv := BitVec.extractAndExtendPopulate w x)]
458+
rw [blastCpop.denote_go (l_bv := BitVec.extractAndExtendPopulate w x)]
458459
· simp [show ¬ w = 0 by omega]
459460
· omega
460461
· intros idx hidx
461-
rw [denote_blastExtractAndExtendPopulate]
462+
rw [blastCpop.denote_blastExtractAndExtendPopulate]
462463
· omega
463464
· exact hx
464465
· split at hgen
@@ -468,7 +469,20 @@ theorem denote_blastCpop (aig : AIG α) (xc : RefVec aig w) (x : BitVec w) (assi
468469
simp [BitVec.pps, BitVec.extractAndExtendPopulate, BitVec.extractAndExtendPopulateAux, hx]
469470
· simp [show w = 0 by omega]
470471

471-
end blastCpop
472+
theorem cpop_eq_cpopNatRec {x : BitVec w} :
473+
x.cpop = BitVec.ofNat w (BitVec.cpopNatRec x w 0) := by
474+
simp [BitVec.cpop]
475+
476+
@[simp]
477+
theorem denote_blastCpop (aig : AIG α) (xc : RefVec aig w) (x : BitVec w) (assign : α → Bool)
478+
(hx : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, xc.get idx hidx, assign⟧ = x.getLsbD idx)
479+
:
480+
∀ (idx : Nat) (hidx : idx < w),
481+
⟦(blastCpop aig xc).aig, (blastCpop aig xc).vec.get idx hidx, assign⟧
482+
= (BitVec.ofNat w (BitVec.cpopNatRec x w 0)).getLsbD idx := by
483+
rw [← cpop_eq_cpopNatRec]
484+
apply denote_blastCpop'
485+
simp [hx]
472486

473487
end bitblast
474488
end BVExpr

0 commit comments

Comments
 (0)