internlm/Lean-Github huggingface dataset:
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof state before:
case un.arithShiftRightConst
w : Nat
assign : Assignment
w✝ : Nat
expr : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig expr).val.aig, ref := (go aig expr).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign expr).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
n : Nat
⊢ ⟦{ aig := (go aig (un (BVUnOp.arithShiftRightConst n) expr)).val.aig,
        ref := (go aig (un (BVUnOp.arithShiftRightConst n) expr)).val.stream.getRef idx hidx },
      assign.toAIGAssignment⟧ =
    (eval assign (un (BVUnOp.arithShiftRightConst n) expr)).getLsb idx
Tactic:
rename_i w
Proof state after:
case un.arithShiftRightConst
w✝ : Nat
assign : Assignment
w : Nat
expr : BVExpr w
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w),
    ⟦{ aig := (go aig expr).val.aig, ref := (go aig expr).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign expr).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w
n : Nat
⊢ ⟦{ aig := (go aig (un (BVUnOp.arithShiftRightConst n) expr)).val.aig,
        ref := (go aig (un (BVUnOp.arithShiftRightConst n) expr)).val.stream.getRef idx hidx },
      assign.toAIGAssignment⟧ =
    (eval assign (un (BVUnOp.arithShiftRightConst n) expr)).getLsb idx
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof state before:
case un.arithShiftRightConst
w✝ : Nat
assign : Assignment
w : Nat
expr : BVExpr w
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w),
    ⟦{ aig := (go aig expr).val.aig, ref := (go aig expr).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign expr).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w
n : Nat
⊢ ⟦{ aig := (go aig (un (BVUnOp.arithShiftRightConst n) expr)).val.aig,
        ref := (go aig (un (BVUnOp.arithShiftRightConst n) expr)).val.stream.getRef idx hidx },
      assign.toAIGAssignment⟧ =
    (eval assign (un (BVUnOp.arithShiftRightConst n) expr)).getLsb idx
Tactic:
have : ¬(w ≤ idx) := by omega
Proof state after:
case un.arithShiftRightConst
w✝ : Nat
assign : Assignment
w : Nat
expr : BVExpr w
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w),
    ⟦{ aig := (go aig expr).val.aig, ref := (go aig expr).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign expr).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w
n : Nat
this : ¬w ≤ idx
⊢ ⟦{ aig := (go aig (un (BVUnOp.arithShiftRightConst n) expr)).val.aig,
        ref := (go aig (un (BVUnOp.arithShiftRightConst n) expr)).val.stream.getRef idx hidx },
      assign.toAIGAssignment⟧ =
    (eval assign (un (BVUnOp.arithShiftRightConst n) expr)).getLsb idx
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof state before:
case un.arithShiftRightConst
w✝ : Nat
assign : Assignment
w : Nat
expr : BVExpr w
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w),
    ⟦{ aig := (go aig expr).val.aig, ref := (go aig expr).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign expr).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w
n : Nat
this : ¬w ≤ idx
⊢ ⟦{ aig := (go aig (un (BVUnOp.arithShiftRightConst n) expr)).val.aig,
        ref := (go aig (un (BVUnOp.arithShiftRightConst n) expr)).val.stream.getRef idx hidx },
      assign.toAIGAssignment⟧ =
    (eval assign (un (BVUnOp.arithShiftRightConst n) expr)).getLsb idx
Tactic:
simp [go, ih, this, BitVec.getLsb_sshiftRight, BitVec.msb_eq_getLsb_last ]
Proof state after:
no goals
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof state before:
w✝ : Nat
assign : Assignment
w : Nat
expr : BVExpr w
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w),
    ⟦{ aig := (go aig expr).val.aig, ref := (go aig expr).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign expr).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w
n : Nat
⊢ ¬w ≤ idx
Tactic:
omega
Proof state after:
no goals
Theorem: BVExpr.bitblast_denote_eq_eval_getLsb
Proof state before:
w : Nat
aig : AIG BVBit
expr : BVExpr w
assign : Assignment
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := (bitblast aig expr).aig, ref := (bitblast aig expr).stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign expr).getLsb idx
Tactic:
intros
Proof state after:
w : Nat
aig : AIG BVBit
expr : BVExpr w
assign : Assignment
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ⟦{ aig := (bitblast aig expr).aig, ref := (bitblast aig expr).stream.getRef idx✝ hidx✝ }, assign.toAIGAssignment⟧ =
    (eval assign expr).getLsb idx✝
Theorem: BVExpr.bitblast_denote_eq_eval_getLsb
Proof state before:
w : Nat
aig : AIG BVBit
expr : BVExpr w
assign : Assignment
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ⟦{ aig := (bitblast aig expr).aig, ref := (bitblast aig expr).stream.getRef idx✝ hidx✝ }, assign.toAIGAssignment⟧ =
    (eval assign expr).getLsb idx✝
Tactic:
rw [← bitblast.go_val_eq_bitblast]
Proof state after:
w : Nat
aig : AIG BVBit
expr : BVExpr w
assign : Assignment
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ⟦{ aig := (bitblast.go aig expr).val.aig, ref := (bitblast.go aig expr).val.stream.getRef idx✝ hidx✝ },
      assign.toAIGAssignment⟧ =
    (eval assign expr).getLsb idx✝
Theorem: BVExpr.bitblast_denote_eq_eval_getLsb
Proof state before:
w : Nat
aig : AIG BVBit
expr : BVExpr w
assign : Assignment
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ⟦{ aig := (bitblast.go aig expr).val.aig, ref := (bitblast.go aig expr).val.stream.getRef idx✝ hidx✝ },
      assign.toAIGAssignment⟧ =
    (eval assign expr).getLsb idx✝
Tactic:
rw [bitblast.go_denote_eq_eval_getLsb]
Proof state after:
no goals
Theorem: BVExpr.bitblast.mkOverflowBit.go_eq_carry
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
⊢ ⟦go aig curr hcurr cin lhs rhs, assign⟧ = BitVec.carry w lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
Tactic:
unfold go
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
⊢ ⟦if hidx : curr < w then
        let lin := lhs.getRef curr hidx;
        let rin := rhs.getRef curr hidx;
        let res := mkFullAdderCarry aig { lhs := lin, rhs := rin, cin := cin };
        let_fun this := ⋯;
        let aig_1 := res.aig;
        let carryRef := res.ref;
        let lhs_1 := lhs.cast this;
        let rhs_1 := rhs.cast this;
        go aig_1 (curr + 1) ⋯ carryRef lhs_1 rhs_1
      else { aig := aig, ref := cin },
      assign⟧ =
    BitVec.carry w lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
Theorem: BVExpr.bitblast.mkOverflowBit.go_eq_carry
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
⊢ ⟦if hidx : curr < w then
        let lin := lhs.getRef curr hidx;
        let rin := rhs.getRef curr hidx;
        let res := mkFullAdderCarry aig { lhs := lin, rhs := rin, cin := cin };
        let_fun this := ⋯;
        let aig_1 := res.aig;
        let carryRef := res.ref;
        let lhs_1 := lhs.cast this;
        let rhs_1 := rhs.cast this;
        go aig_1 (curr + 1) ⋯ carryRef lhs_1 rhs_1
      else { aig := aig, ref := cin },
      assign⟧ =
    BitVec.carry w lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
Tactic:
dsimp
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
⊢ ⟦if hidx : curr < w then
        go (mkFullAdderCarry aig { lhs := lhs.getRef curr hidx, rhs := rhs.getRef curr hidx, cin := cin }).aig
          (curr + 1) ⋯
          (mkFullAdderCarry aig { lhs := lhs.getRef curr hidx, rhs := rhs.getRef curr hidx, cin := cin }).ref
          (lhs.cast ⋯) (rhs.cast ⋯)
      else { aig := aig, ref := cin },
      assign⟧ =
    BitVec.carry w lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
Theorem: BVExpr.bitblast.mkOverflowBit.go_eq_carry
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
⊢ ⟦if hidx : curr < w then
        go (mkFullAdderCarry aig { lhs := lhs.getRef curr hidx, rhs := rhs.getRef curr hidx, cin := cin }).aig
          (curr + 1) ⋯
          (mkFullAdderCarry aig { lhs := lhs.getRef curr hidx, rhs := rhs.getRef curr hidx, cin := cin }).ref
          (lhs.cast ⋯) (rhs.cast ⋯)
      else { aig := aig, ref := cin },
      assign⟧ =
    BitVec.carry w lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
Tactic:
split
Proof state after:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : curr < w
⊢ ⟦go (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
        (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).ref (lhs.cast ⋯)
        (rhs.cast ⋯),
      assign⟧ =
    BitVec.carry w lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧

case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : ¬curr < w
⊢ ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry w lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
Theorem: BVExpr.bitblast.mkOverflowBit.go_eq_carry
Proof state before:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : curr < w
⊢ ⟦go (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
        (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).ref (lhs.cast ⋯)
        (rhs.cast ⋯),
      assign⟧ =
    BitVec.carry w lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧

case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : ¬curr < w
⊢ ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry w lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
Tactic:
. rw [go_eq_carry]
  . congr 1
    rw [AIG.LawfulOperator.denote_mem_prefix (f := mkFullAdderCarry)]
  . intros
    rw [AIG.LawfulOperator.denote_mem_prefix (f := mkFullAdderCarry)]
    . simp [hleft]
    . simp [Ref.hgate]
  . intros
    rw [AIG.LawfulOperator.denote_mem_prefix (f := mkFullAdderCarry)]
    . simp [hright]
    . simp [Ref.hgate]
  . simp [BitVec.carry_succ]
    rw [AIG.LawfulOperator.denote_mem_prefix (f := mkFullAdderCarry)]
    rw [hleft, hright, hcin]
    rw [Bool.atLeastTwo_eq_halfAdder]
Proof state after:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : ¬curr < w
⊢ ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry w lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
Theorem: BVExpr.bitblast.mkOverflowBit.go_eq_carry
Proof state before:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : ¬curr < w
⊢ ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry w lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
Tactic:
. have : w = curr := by omega
  rw [hcin]
  simp [this]
Proof state after:
no goals
Theorem: BVExpr.bitblast.mkOverflowBit.go_eq_carry
Proof state before:
case isTrue.hright
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : curr < w
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig,
          ref := (rhs.cast ⋯).getRef idx hidx },
        assign⟧ =
      rhsExpr.getLsb idx

case isTrue.hcin
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : curr < w
⊢ ⟦{ aig := (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig,
        ref := (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).ref },
      assign⟧ =
    BitVec.carry (curr + 1) lhsExpr rhsExpr
      ⟦{ aig := (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig,
          ref := { gate := origCin.gate, hgate := ⋯ } },
        assign⟧
Tactic:
. intros
  rw [AIG.LawfulOperator.denote_mem_prefix (f := mkFullAdderCarry)]
  . simp [hright]
  . simp [Ref.hgate]
Proof state after:
case isTrue.hcin
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : curr < w
⊢ ⟦{ aig := (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig,
        ref := (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).ref },
      assign⟧ =
    BitVec.carry (curr + 1) lhsExpr rhsExpr
      ⟦{ aig := (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig,
          ref := { gate := origCin.gate, hgate := ⋯ } },
        assign⟧
Theorem: BVExpr.bitblast.mkOverflowBit.go_eq_carry
Proof state before:
case isTrue.hcin
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : curr < w
⊢ ⟦{ aig := (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig,
        ref := (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).ref },
      assign⟧ =
    BitVec.carry (curr + 1) lhsExpr rhsExpr
      ⟦{ aig := (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig,
          ref := { gate := origCin.gate, hgate := ⋯ } },
        assign⟧
Tactic:
. simp [BitVec.carry_succ]
  rw [AIG.LawfulOperator.denote_mem_prefix (f := mkFullAdderCarry)]
  rw [hleft, hright, hcin]
  rw [Bool.atLeastTwo_eq_halfAdder]
Proof state after:
no goals
Theorem: BVExpr.bitblast.mkOverflowBit.go_eq_carry
Proof state before:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : curr < w
⊢ BitVec.carry w ?isTrue.lhsExpr ?isTrue.rhsExpr
      ⟦{ aig := (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig,
          ref := ?isTrue.origCin },
        assign⟧ =
    BitVec.carry w lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
Tactic:
congr 1
Proof state after:
case isTrue.e_c
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : curr < w
⊢ ⟦{ aig := (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig,
        ref := ?isTrue.origCin },
      assign⟧ =
    ⟦{ aig := aig, ref := origCin }, assign⟧
Theorem: BVExpr.bitblast.mkOverflowBit.go_eq_carry
Proof state before:
case isTrue.e_c
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : curr < w
⊢ ⟦{ aig := (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig,
        ref := ?isTrue.origCin },
      assign⟧ =
    ⟦{ aig := aig, ref := origCin }, assign⟧
Tactic:
rw [AIG.LawfulOperator.denote_mem_prefix (f := mkFullAdderCarry)]
Proof state after:
no goals