internlm/Lean-Github huggingface dataset:
Theorem: BVExpr.bitblast.blastArithShiftRightConst.go_eq_eval_getLsb
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
assign : α → Bool
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx1 : idx < w
hidx2 : curr ≤ idx
res : aig.RefStream w
h✝² : curr < w
h✝¹ : curr < idx
h✝ : ¬distance + curr < w
hgo :
  (let s := s.pushRef (input.getRef (w - 1) ⋯);
    go input distance (curr + 1) ⋯ s) =
    res
hidx : ¬distance + idx < w
⊢ (if hidx : distance + idx < w then ⟦{ aig := aig, ref := input.getRef (distance + idx) ⋯ }, assign⟧
    else ⟦{ aig := aig, ref := input.getRef (w - 1) ⋯ }, assign⟧) =
    ⟦{ aig := aig, ref := input.getRef (w - 1) ⋯ }, assign⟧
Tactic:
simp [hidx]
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastArithShiftRightConst.go_eq_eval_getLsb
Proof state before:
case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
assign : α → Bool
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx1 : idx < w
hidx2 : curr ≤ idx
res : aig.RefStream w
h✝² : curr < w
h✝¹ : curr < idx
h✝ : ¬distance + curr < w
hgo :
  (let s := s.pushRef (input.getRef (w - 1) ⋯);
    go input distance (curr + 1) ⋯ s) =
    res
hidx : ¬distance + idx < w
⊢ curr + 1 ≤ idx
Tactic:
omega
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastArithShiftRightConst.go_eq_eval_getLsb
Proof state before:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
assign : α → Bool
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx1 : idx < w
hidx2 : curr ≤ idx
res : aig.RefStream w
h✝ : ¬curr < w
hgo :
  (let_fun hcurr := ⋯;
    hcurr ▸ s) =
    res
⊢ ⟦{ aig := aig, ref := res.getRef idx hidx1 }, assign⟧ =
    if hidx : distance + idx < w then ⟦{ aig := aig, ref := input.getRef (distance + idx) ⋯ }, assign⟧
    else ⟦{ aig := aig, ref := input.getRef (w - 1) ⋯ }, assign⟧
Tactic:
omega
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastArithShiftRightConst_eq_eval_getLsb
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
target : aig.ShiftTarget w
assign : α → Bool
idx : Nat
hidx✝ : idx < w
hidx : target.distance + idx < w
⊢ target.distance + idx < w
Tactic:
omega
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastArithShiftRightConst_eq_eval_getLsb
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
target : aig.ShiftTarget w
assign : α → Bool
idx : Nat
hidx✝ : idx < w
hidx : ¬target.distance + idx < w
⊢ w - 1 < w
Tactic:
omega
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastArithShiftRightConst_eq_eval_getLsb
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
target : aig.ShiftTarget w
assign : α → Bool
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := (blastArithShiftRightConst aig target).aig,
          ref := (blastArithShiftRightConst aig target).stream.getRef idx hidx },
        assign⟧ =
      if hidx : target.distance + idx < w then
        ⟦{ aig := aig, ref := target.stream.getRef (target.distance + idx) ⋯ }, assign⟧
      else ⟦{ aig := aig, ref := target.stream.getRef (w - 1) ⋯ }, assign⟧
Tactic:
intros
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
target : aig.ShiftTarget w
assign : α → Bool
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ⟦{ aig := (blastArithShiftRightConst aig target).aig,
        ref := (blastArithShiftRightConst aig target).stream.getRef idx✝ hidx✝ },
      assign⟧ =
    if hidx : target.distance + idx✝ < w then
      ⟦{ aig := aig, ref := target.stream.getRef (target.distance + idx✝) ⋯ }, assign⟧
    else ⟦{ aig := aig, ref := target.stream.getRef (w - 1) ⋯ }, assign⟧
Theorem: BVExpr.bitblast.blastArithShiftRightConst_eq_eval_getLsb
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
target : aig.ShiftTarget w
assign : α → Bool
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ⟦{ aig := (blastArithShiftRightConst aig target).aig,
        ref := (blastArithShiftRightConst aig target).stream.getRef idx✝ hidx✝ },
      assign⟧ =
    if hidx : target.distance + idx✝ < w then
      ⟦{ aig := aig, ref := target.stream.getRef (target.distance + idx✝) ⋯ }, assign⟧
    else ⟦{ aig := aig, ref := target.stream.getRef (w - 1) ⋯ }, assign⟧
Tactic:
unfold blastArithShiftRightConst
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
target : aig.ShiftTarget w
assign : α → Bool
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ⟦{
        aig :=
          (match target with
            | { stream := input, distance := distance } =>
              { aig := aig, stream := blastArithShiftRightConst.go input distance 0 ⋯ RefStream.empty }).aig,
        ref :=
          (match target with
                | { stream := input, distance := distance } =>
                  { aig := aig,
                    stream := blastArithShiftRightConst.go input distance 0 ⋯ RefStream.empty }).stream.getRef
            idx✝ hidx✝ },
      assign⟧ =
    if hidx : target.distance + idx✝ < w then
      ⟦{ aig := aig, ref := target.stream.getRef (target.distance + idx✝) ⋯ }, assign⟧
    else ⟦{ aig := aig, ref := target.stream.getRef (w - 1) ⋯ }, assign⟧
Theorem: BVExpr.bitblast.blastArithShiftRightConst_eq_eval_getLsb
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
target : aig.ShiftTarget w
assign : α → Bool
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ⟦{
        aig :=
          (match target with
            | { stream := input, distance := distance } =>
              { aig := aig, stream := blastArithShiftRightConst.go input distance 0 ⋯ RefStream.empty }).aig,
        ref :=
          (match target with
                | { stream := input, distance := distance } =>
                  { aig := aig,
                    stream := blastArithShiftRightConst.go input distance 0 ⋯ RefStream.empty }).stream.getRef
            idx✝ hidx✝ },
      assign⟧ =
    if hidx : target.distance + idx✝ < w then
      ⟦{ aig := aig, ref := target.stream.getRef (target.distance + idx✝) ⋯ }, assign⟧
    else ⟦{ aig := aig, ref := target.stream.getRef (w - 1) ⋯ }, assign⟧
Tactic:
rw [blastArithShiftRightConst.go_eq_eval_getLsb]
Proof state after:
case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
target : aig.ShiftTarget w
assign : α → Bool
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ 0 ≤ idx✝
Theorem: BVExpr.bitblast.blastArithShiftRightConst_eq_eval_getLsb
Proof state before:
case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
target : aig.ShiftTarget w
assign : α → Bool
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ 0 ≤ idx✝
Tactic:
omega
Proof state after:
no goals
Theorem: bitvec_AndOrXor_1253_A__AB___A__B
Proof state before:
⊢ ∀ (A B : BitVec 64), (A ^^^ B) &&& A = A &&& (B ^^^ -1)
Tactic:
intros
Proof state after:
A✝ B✝ : BitVec 64
⊢ (A✝ ^^^ B✝) &&& A✝ = A✝ &&& (B✝ ^^^ -1)
Theorem: bitvec_AndOrXor_1253_A__AB___A__B
Proof state before:
A✝ B✝ : BitVec 64
⊢ (A✝ ^^^ B✝) &&& A✝ = A✝ &&& (B✝ ^^^ -1)
Tactic:
bv_decide
Proof state after:
no goals
Theorem: BVExpr.bitblast.FullAdderInput.lhs_cast
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig1 aig2 : AIG α
s : FullAdderInput aig1
hcast : aig1.decls.size ≤ aig2.decls.size
⊢ (s.cast hcast).lhs = s.lhs.cast hcast
Tactic:
simp [cast]
Proof state after:
no goals
Theorem: BVExpr.bitblast.FullAdderInput.rhs_cast
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig1 aig2 : AIG α
s : FullAdderInput aig1
hcast : aig1.decls.size ≤ aig2.decls.size
⊢ (s.cast hcast).rhs = s.rhs.cast hcast
Tactic:
simp [cast]
Proof state after:
no goals
Theorem: BVExpr.bitblast.FullAdderInput.cin_cast
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig1 aig2 : AIG α
s : FullAdderInput aig1
hcast : aig1.decls.size ≤ aig2.decls.size
⊢ (s.cast hcast).cin = s.cin.cast hcast
Tactic:
simp [cast]
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastAdd.go_le_size
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
⊢ aig.decls.size ≤ (go aig curr hcurr cin s lhs rhs).aig.decls.size
Tactic:
unfold go
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
⊢ aig.decls.size ≤
    (if hidx : curr < w then
            let lin := lhs.getRef curr hidx;
            let rin := rhs.getRef curr hidx;
            let res := mkFullAdder aig { lhs := lin, rhs := rin, cin := cin };
            let aig_1 := res.aig;
            let outRef := res.out;
            let carryRef := res.cout;
            let s := s.cast ⋯;
            let lhs := lhs.cast ⋯;
            let rhs := rhs.cast ⋯;
            let s := s.pushRef outRef;
            go aig_1 (curr + 1) ⋯ carryRef s lhs rhs
          else
            let_fun hcurr := ⋯;
            { aig := aig, stream := hcurr ▸ s }).aig.decls.size
Theorem: BVExpr.bitblast.blastAdd.go_le_size
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
⊢ aig.decls.size ≤
    (if hidx : curr < w then
            let lin := lhs.getRef curr hidx;
            let rin := rhs.getRef curr hidx;
            let res := mkFullAdder aig { lhs := lin, rhs := rin, cin := cin };
            let aig_1 := res.aig;
            let outRef := res.out;
            let carryRef := res.cout;
            let s := s.cast ⋯;
            let lhs := lhs.cast ⋯;
            let rhs := rhs.cast ⋯;
            let s := s.pushRef outRef;
            go aig_1 (curr + 1) ⋯ carryRef s lhs rhs
          else
            let_fun hcurr := ⋯;
            { aig := aig, stream := hcurr ▸ s }).aig.decls.size
Tactic:
dsimp
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
⊢ aig.decls.size ≤
    (if hidx : curr < w then
            go (mkFullAdder aig { lhs := lhs.getRef curr hidx, rhs := rhs.getRef curr hidx, cin := cin }).aig (curr + 1)
              ⋯ (mkFullAdder aig { lhs := lhs.getRef curr hidx, rhs := rhs.getRef curr hidx, cin := cin }).cout
              ((s.cast ⋯).pushRef
                (mkFullAdder aig { lhs := lhs.getRef curr hidx, rhs := rhs.getRef curr hidx, cin := cin }).out)
              (lhs.cast ⋯) (rhs.cast ⋯)
          else { aig := aig, stream := ⋯ ▸ s }).aig.decls.size
Theorem: BVExpr.bitblast.blastAdd.go_le_size
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
⊢ aig.decls.size ≤
    (if hidx : curr < w then
            go (mkFullAdder aig { lhs := lhs.getRef curr hidx, rhs := rhs.getRef curr hidx, cin := cin }).aig (curr + 1)
              ⋯ (mkFullAdder aig { lhs := lhs.getRef curr hidx, rhs := rhs.getRef curr hidx, cin := cin }).cout
              ((s.cast ⋯).pushRef
                (mkFullAdder aig { lhs := lhs.getRef curr hidx, rhs := rhs.getRef curr hidx, cin := cin }).out)
              (lhs.cast ⋯) (rhs.cast ⋯)
          else { aig := aig, stream := ⋯ ▸ s }).aig.decls.size
Tactic:
split
Proof state after:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
h✝ : curr < w
⊢ aig.decls.size ≤
    (go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
            (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
            ((s.cast ⋯).pushRef
              (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
            (lhs.cast ⋯) (rhs.cast ⋯)).aig.decls.size

case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
h✝ : ¬curr < w
⊢ aig.decls.size ≤ { aig := aig, stream := ⋯ ▸ s }.aig.decls.size
Theorem: BVExpr.bitblast.blastAdd.go_le_size
Proof state before:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
h✝ : curr < w
⊢ aig.decls.size ≤
    (go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
            (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
            ((s.cast ⋯).pushRef
              (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
            (lhs.cast ⋯) (rhs.cast ⋯)).aig.decls.size

case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
h✝ : ¬curr < w
⊢ aig.decls.size ≤ { aig := aig, stream := ⋯ ▸ s }.aig.decls.size
Tactic:
. refine Nat.le_trans ?_ (by apply go_le_size)
  apply AIG.LawfulOperator.le_size_of_le_aig_size (f := mkFullAdderCarry)
  apply AIG.LawfulOperator.le_size (f := mkFullAdderOut)
Proof state after:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
h✝ : ¬curr < w
⊢ aig.decls.size ≤ { aig := aig, stream := ⋯ ▸ s }.aig.decls.size
Theorem: BVExpr.bitblast.blastAdd.go_le_size
Proof state before:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
h✝ : ¬curr < w
⊢ aig.decls.size ≤ { aig := aig, stream := ⋯ ▸ s }.aig.decls.size
Tactic:
. simp
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastAdd.go_le_size
Proof state before:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
h✝ : curr < w
⊢ aig.decls.size ≤
    (go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
            (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
            ((s.cast ⋯).pushRef
              (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
            (lhs.cast ⋯) (rhs.cast ⋯)).aig.decls.size
Tactic:
refine Nat.le_trans ?_ (by apply go_le_size)
Proof state after:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
h✝ : curr < w
⊢ aig.decls.size ≤ (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig.decls.size
Theorem: BVExpr.bitblast.blastAdd.go_le_size
Proof state before:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
h✝ : curr < w
⊢ aig.decls.size ≤ (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig.decls.size
Tactic:
apply AIG.LawfulOperator.le_size_of_le_aig_size (f := mkFullAdderCarry)
Proof state after:
case isTrue.h
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
h✝ : curr < w
⊢ aig.decls.size ≤
    (mkFullAdderOut aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig.decls.size
Theorem: BVExpr.bitblast.blastAdd.go_le_size
Proof state before:
case isTrue.h
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
h✝ : curr < w
⊢ aig.decls.size ≤
    (mkFullAdderOut aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig.decls.size
Tactic:
apply AIG.LawfulOperator.le_size (f := mkFullAdderOut)
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastAdd.go_le_size
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
h✝ : curr < w
⊢ ?m.28930 ≤
    (go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
            (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
            ((s.cast ⋯).pushRef
              (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
            (lhs.cast ⋯) (rhs.cast ⋯)).aig.decls.size
Tactic:
apply go_le_size
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastAdd.go_le_size
Proof state before:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
h✝ : ¬curr < w
⊢ aig.decls.size ≤ { aig := aig, stream := ⋯ ▸ s }.aig.decls.size
Tactic:
simp
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastAdd.go_decl_eq
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < (go aig curr hcurr cin s lhs rhs).aig.decls.size),
    (go aig curr hcurr cin s lhs rhs).aig.decls[idx] = aig.decls[idx]
Tactic:
generalize hgo : go aig curr hcurr cin s lhs rhs = res
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
res : AIG.RefStreamEntry α w
hgo : go aig curr hcurr cin s lhs rhs = res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]
Theorem: BVExpr.bitblast.blastAdd.go_decl_eq
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
res : AIG.RefStreamEntry α w
hgo : go aig curr hcurr cin s lhs rhs = res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]
Tactic:
unfold go at hgo
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
res : AIG.RefStreamEntry α w
hgo :
  (if hidx : curr < w then
      let lin := lhs.getRef curr hidx;
      let rin := rhs.getRef curr hidx;
      let res := mkFullAdder aig { lhs := lin, rhs := rin, cin := cin };
      let aig_1 := res.aig;
      let outRef := res.out;
      let carryRef := res.cout;
      let s := s.cast ⋯;
      let lhs := lhs.cast ⋯;
      let rhs := rhs.cast ⋯;
      let s := s.pushRef outRef;
      go aig_1 (curr + 1) ⋯ carryRef s lhs rhs
    else
      let_fun hcurr := ⋯;
      { aig := aig, stream := hcurr ▸ s }) =
    res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]
Theorem: BVExpr.bitblast.blastAdd.go_decl_eq
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
res : AIG.RefStreamEntry α w
hgo :
  (if hidx : curr < w then
      let lin := lhs.getRef curr hidx;
      let rin := rhs.getRef curr hidx;
      let res := mkFullAdder aig { lhs := lin, rhs := rin, cin := cin };
      let aig_1 := res.aig;
      let outRef := res.out;
      let carryRef := res.cout;
      let s := s.cast ⋯;
      let lhs := lhs.cast ⋯;
      let rhs := rhs.cast ⋯;
      let s := s.pushRef outRef;
      go aig_1 (curr + 1) ⋯ carryRef s lhs rhs
    else
      let_fun hcurr := ⋯;
      { aig := aig, stream := hcurr ▸ s }) =
    res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]
Tactic:
dsimp at hgo
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
res : AIG.RefStreamEntry α w
hgo :
  (if hidx : curr < w then
      go (mkFullAdder aig { lhs := lhs.getRef curr hidx, rhs := rhs.getRef curr hidx, cin := cin }).aig (curr + 1) ⋯
        (mkFullAdder aig { lhs := lhs.getRef curr hidx, rhs := rhs.getRef curr hidx, cin := cin }).cout
        ((s.cast ⋯).pushRef
          (mkFullAdder aig { lhs := lhs.getRef curr hidx, rhs := rhs.getRef curr hidx, cin := cin }).out)
        (lhs.cast ⋯) (rhs.cast ⋯)
    else { aig := aig, stream := ⋯ ▸ s }) =
    res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]
Theorem: BVExpr.bitblast.blastAdd.go_decl_eq
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
res : AIG.RefStreamEntry α w
hgo :
  (if hidx : curr < w then
      go (mkFullAdder aig { lhs := lhs.getRef curr hidx, rhs := rhs.getRef curr hidx, cin := cin }).aig (curr + 1) ⋯
        (mkFullAdder aig { lhs := lhs.getRef curr hidx, rhs := rhs.getRef curr hidx, cin := cin }).cout
        ((s.cast ⋯).pushRef
          (mkFullAdder aig { lhs := lhs.getRef curr hidx, rhs := rhs.getRef curr hidx, cin := cin }).out)
        (lhs.cast ⋯) (rhs.cast ⋯)
    else { aig := aig, stream := ⋯ ▸ s }) =
    res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]
Tactic:
split at hgo
Proof state after:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
res : AIG.RefStreamEntry α w
h✝ : curr < w
hgo :
  go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
      (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
      ((s.cast ⋯).pushRef (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
      (lhs.cast ⋯) (rhs.cast ⋯) =
    res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]

case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
res : AIG.RefStreamEntry α w
h✝ : ¬curr < w
hgo : { aig := aig, stream := ⋯ ▸ s } = res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]