internlm/Lean-Github huggingface dataset:
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
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
this : w = curr
⊢ ⟦{ 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
this : w = curr
⊢ ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry w lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
Tactic:
rw [hcin]
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
this : w = curr
⊢ BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, 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
this : w = curr
⊢ BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧ =
    BitVec.carry w lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
Tactic:
simp [this]
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⟧
h✝ : ¬curr < w
⊢ w = curr
Tactic:
omega
Proof state after:
no goals
Theorem: BVExpr.bitblast.mkOverflowBit_eq_carry
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : OverflowInput aig
lhs rhs : BitVec input.w
assign : α → Bool
hleft :
  ∀ (idx : Nat) (hidx : idx < input.w),
    ⟦{ aig := aig, ref := input.stream.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright :
  ∀ (idx : Nat) (hidx : idx < input.w),
    ⟦{ aig := aig, ref := input.stream.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ ⟦mkOverflowBit aig input, assign⟧ = BitVec.carry input.w lhs rhs ⟦{ aig := aig, ref := input.cin }, assign⟧
Tactic:
unfold mkOverflowBit
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : OverflowInput aig
lhs rhs : BitVec input.w
assign : α → Bool
hleft :
  ∀ (idx : Nat) (hidx : idx < input.w),
    ⟦{ aig := aig, ref := input.stream.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright :
  ∀ (idx : Nat) (hidx : idx < input.w),
    ⟦{ aig := aig, ref := input.stream.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ ⟦match input with
      | { w := w, stream := { lhs := lhs, rhs := rhs }, cin := cin } => mkOverflowBit.go aig 0 ⋯ cin lhs rhs,
      assign⟧ =
    BitVec.carry input.w lhs rhs ⟦{ aig := aig, ref := input.cin }, assign⟧
Theorem: BVExpr.bitblast.mkOverflowBit_eq_carry
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : OverflowInput aig
lhs rhs : BitVec input.w
assign : α → Bool
hleft :
  ∀ (idx : Nat) (hidx : idx < input.w),
    ⟦{ aig := aig, ref := input.stream.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright :
  ∀ (idx : Nat) (hidx : idx < input.w),
    ⟦{ aig := aig, ref := input.stream.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ ⟦match input with
      | { w := w, stream := { lhs := lhs, rhs := rhs }, cin := cin } => mkOverflowBit.go aig 0 ⋯ cin lhs rhs,
      assign⟧ =
    BitVec.carry input.w lhs rhs ⟦{ aig := aig, ref := input.cin }, assign⟧
Tactic:
dsimp
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : OverflowInput aig
lhs rhs : BitVec input.w
assign : α → Bool
hleft :
  ∀ (idx : Nat) (hidx : idx < input.w),
    ⟦{ aig := aig, ref := input.stream.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright :
  ∀ (idx : Nat) (hidx : idx < input.w),
    ⟦{ aig := aig, ref := input.stream.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ ⟦mkOverflowBit.go aig 0 ⋯ input.cin input.2.lhs input.2.rhs, assign⟧ =
    BitVec.carry input.w lhs rhs ⟦{ aig := aig, ref := input.cin }, assign⟧
Theorem: BVExpr.bitblast.mkOverflowBit_eq_carry
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : OverflowInput aig
lhs rhs : BitVec input.w
assign : α → Bool
hleft :
  ∀ (idx : Nat) (hidx : idx < input.w),
    ⟦{ aig := aig, ref := input.stream.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright :
  ∀ (idx : Nat) (hidx : idx < input.w),
    ⟦{ aig := aig, ref := input.stream.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ ⟦mkOverflowBit.go aig 0 ⋯ input.cin input.2.lhs input.2.rhs, assign⟧ =
    BitVec.carry input.w lhs rhs ⟦{ aig := aig, ref := input.cin }, assign⟧
Tactic:
apply mkOverflowBit.go_eq_carry
Proof state after:
case hleft
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : OverflowInput aig
lhs rhs : BitVec input.w
assign : α → Bool
hleft :
  ∀ (idx : Nat) (hidx : idx < input.w),
    ⟦{ aig := aig, ref := input.stream.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright :
  ∀ (idx : Nat) (hidx : idx < input.w),
    ⟦{ aig := aig, ref := input.stream.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ ∀ (idx : Nat) (hidx : idx < input.w), ⟦{ aig := aig, ref := input.2.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx

case hright
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : OverflowInput aig
lhs rhs : BitVec input.w
assign : α → Bool
hleft :
  ∀ (idx : Nat) (hidx : idx < input.w),
    ⟦{ aig := aig, ref := input.stream.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright :
  ∀ (idx : Nat) (hidx : idx < input.w),
    ⟦{ aig := aig, ref := input.stream.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ ∀ (idx : Nat) (hidx : idx < input.w), ⟦{ aig := aig, ref := input.2.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx

case hcin
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : OverflowInput aig
lhs rhs : BitVec input.w
assign : α → Bool
hleft :
  ∀ (idx : Nat) (hidx : idx < input.w),
    ⟦{ aig := aig, ref := input.stream.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright :
  ∀ (idx : Nat) (hidx : idx < input.w),
    ⟦{ aig := aig, ref := input.stream.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ ⟦{ aig := aig, ref := input.cin }, assign⟧ = BitVec.carry 0 lhs rhs ⟦{ aig := aig, ref := input.cin }, assign⟧
Theorem: BVExpr.bitblast.mkOverflowBit_eq_carry
Proof state before:
case hleft
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : OverflowInput aig
lhs rhs : BitVec input.w
assign : α → Bool
hleft :
  ∀ (idx : Nat) (hidx : idx < input.w),
    ⟦{ aig := aig, ref := input.stream.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright :
  ∀ (idx : Nat) (hidx : idx < input.w),
    ⟦{ aig := aig, ref := input.stream.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ ∀ (idx : Nat) (hidx : idx < input.w), ⟦{ aig := aig, ref := input.2.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx

case hright
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : OverflowInput aig
lhs rhs : BitVec input.w
assign : α → Bool
hleft :
  ∀ (idx : Nat) (hidx : idx < input.w),
    ⟦{ aig := aig, ref := input.stream.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright :
  ∀ (idx : Nat) (hidx : idx < input.w),
    ⟦{ aig := aig, ref := input.stream.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ ∀ (idx : Nat) (hidx : idx < input.w), ⟦{ aig := aig, ref := input.2.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx

case hcin
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : OverflowInput aig
lhs rhs : BitVec input.w
assign : α → Bool
hleft :
  ∀ (idx : Nat) (hidx : idx < input.w),
    ⟦{ aig := aig, ref := input.stream.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright :
  ∀ (idx : Nat) (hidx : idx < input.w),
    ⟦{ aig := aig, ref := input.stream.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ ⟦{ aig := aig, ref := input.cin }, assign⟧ = BitVec.carry 0 lhs rhs ⟦{ aig := aig, ref := input.cin }, assign⟧
Tactic:
. assumption
Proof state after:
case hright
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : OverflowInput aig
lhs rhs : BitVec input.w
assign : α → Bool
hleft :
  ∀ (idx : Nat) (hidx : idx < input.w),
    ⟦{ aig := aig, ref := input.stream.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright :
  ∀ (idx : Nat) (hidx : idx < input.w),
    ⟦{ aig := aig, ref := input.stream.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ ∀ (idx : Nat) (hidx : idx < input.w), ⟦{ aig := aig, ref := input.2.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx

case hcin
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : OverflowInput aig
lhs rhs : BitVec input.w
assign : α → Bool
hleft :
  ∀ (idx : Nat) (hidx : idx < input.w),
    ⟦{ aig := aig, ref := input.stream.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright :
  ∀ (idx : Nat) (hidx : idx < input.w),
    ⟦{ aig := aig, ref := input.stream.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ ⟦{ aig := aig, ref := input.cin }, assign⟧ = BitVec.carry 0 lhs rhs ⟦{ aig := aig, ref := input.cin }, assign⟧
Theorem: BVExpr.bitblast.mkOverflowBit_eq_carry
Proof state before:
case hright
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : OverflowInput aig
lhs rhs : BitVec input.w
assign : α → Bool
hleft :
  ∀ (idx : Nat) (hidx : idx < input.w),
    ⟦{ aig := aig, ref := input.stream.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright :
  ∀ (idx : Nat) (hidx : idx < input.w),
    ⟦{ aig := aig, ref := input.stream.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ ∀ (idx : Nat) (hidx : idx < input.w), ⟦{ aig := aig, ref := input.2.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx

case hcin
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : OverflowInput aig
lhs rhs : BitVec input.w
assign : α → Bool
hleft :
  ∀ (idx : Nat) (hidx : idx < input.w),
    ⟦{ aig := aig, ref := input.stream.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright :
  ∀ (idx : Nat) (hidx : idx < input.w),
    ⟦{ aig := aig, ref := input.stream.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ ⟦{ aig := aig, ref := input.cin }, assign⟧ = BitVec.carry 0 lhs rhs ⟦{ aig := aig, ref := input.cin }, assign⟧
Tactic:
. assumption
Proof state after:
case hcin
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : OverflowInput aig
lhs rhs : BitVec input.w
assign : α → Bool
hleft :
  ∀ (idx : Nat) (hidx : idx < input.w),
    ⟦{ aig := aig, ref := input.stream.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright :
  ∀ (idx : Nat) (hidx : idx < input.w),
    ⟦{ aig := aig, ref := input.stream.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ ⟦{ aig := aig, ref := input.cin }, assign⟧ = BitVec.carry 0 lhs rhs ⟦{ aig := aig, ref := input.cin }, assign⟧
Theorem: BVExpr.bitblast.mkOverflowBit_eq_carry
Proof state before:
case hcin
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : OverflowInput aig
lhs rhs : BitVec input.w
assign : α → Bool
hleft :
  ∀ (idx : Nat) (hidx : idx < input.w),
    ⟦{ aig := aig, ref := input.stream.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright :
  ∀ (idx : Nat) (hidx : idx < input.w),
    ⟦{ aig := aig, ref := input.stream.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ ⟦{ aig := aig, ref := input.cin }, assign⟧ = BitVec.carry 0 lhs rhs ⟦{ aig := aig, ref := input.cin }, assign⟧
Tactic:
. simp [BitVec.carry_zero]
Proof state after:
no goals
Theorem: BVExpr.bitblast.mkOverflowBit_eq_carry
Proof state before:
case hleft
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : OverflowInput aig
lhs rhs : BitVec input.w
assign : α → Bool
hleft :
  ∀ (idx : Nat) (hidx : idx < input.w),
    ⟦{ aig := aig, ref := input.stream.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright :
  ∀ (idx : Nat) (hidx : idx < input.w),
    ⟦{ aig := aig, ref := input.stream.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ ∀ (idx : Nat) (hidx : idx < input.w), ⟦{ aig := aig, ref := input.2.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
Tactic:
assumption
Proof state after:
no goals
Theorem: BVExpr.bitblast.mkOverflowBit_eq_carry
Proof state before:
case hright
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : OverflowInput aig
lhs rhs : BitVec input.w
assign : α → Bool
hleft :
  ∀ (idx : Nat) (hidx : idx < input.w),
    ⟦{ aig := aig, ref := input.stream.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright :
  ∀ (idx : Nat) (hidx : idx < input.w),
    ⟦{ aig := aig, ref := input.stream.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ ∀ (idx : Nat) (hidx : idx < input.w), ⟦{ aig := aig, ref := input.2.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
Tactic:
assumption
Proof state after:
no goals
Theorem: BVExpr.bitblast.mkOverflowBit_eq_carry
Proof state before:
case hcin
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : OverflowInput aig
lhs rhs : BitVec input.w
assign : α → Bool
hleft :
  ∀ (idx : Nat) (hidx : idx < input.w),
    ⟦{ aig := aig, ref := input.stream.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright :
  ∀ (idx : Nat) (hidx : idx < input.w),
    ⟦{ aig := aig, ref := input.stream.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ ⟦{ aig := aig, ref := input.cin }, assign⟧ = BitVec.carry 0 lhs rhs ⟦{ aig := aig, ref := input.cin }, assign⟧
Tactic:
simp [BitVec.carry_zero]
Proof state after:
no goals
Theorem: not_as_aig
Proof state before:
b : Bool
⊢ (true && !b) = !b
Tactic:
cases b <;> decide
Proof state after:
no goals
Theorem: or_as_aig
Proof state before:
a b : Bool
⊢ (!(!a && !b)) = (a || b)
Tactic:
cases a <;> cases b <;> decide
Proof state after:
no goals
Theorem: xor_as_aig
Proof state before:
a b : Bool
⊢ (!(a && b) && !(!a && !b)) = xor a b
Tactic:
cases a <;> cases b <;> decide
Proof state after:
no goals
Theorem: beq_as_aig
Proof state before:
a b : Bool
⊢ (!(a && !b) && !(!a && b)) = (a == b)
Tactic:
cases a <;> cases b <;> decide
Proof state after:
no goals
Theorem: imp_as_aig
Proof state before:
a b : Bool
⊢ (!(a && !b)) = (!a || b)
Tactic:
cases a <;> cases b <;> decide
Proof state after:
no goals
Theorem: AIG.mkNotCached_le_size
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
gate : aig.Ref
⊢ aig.decls.size ≤ (aig.mkNotCached gate).aig.decls.size
Tactic:
simp only [mkNotCached]
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
gate : aig.Ref
⊢ aig.decls.size ≤
    ((aig.mkConstCached true).aig.mkGateCached
            { lhs := { ref := (aig.mkConstCached true).ref, inv := false },
              rhs := { ref := gate.cast ⋯, inv := true } }).aig.decls.size
Theorem: AIG.mkNotCached_le_size
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
gate : aig.Ref
⊢ aig.decls.size ≤
    ((aig.mkConstCached true).aig.mkGateCached
            { lhs := { ref := (aig.mkConstCached true).ref, inv := false },
              rhs := { ref := gate.cast ⋯, inv := true } }).aig.decls.size
Tactic:
apply LawfulOperator.le_size_of_le_aig_size
Proof state after:
case h
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
gate : aig.Ref
⊢ aig.decls.size ≤ (aig.mkConstCached true).aig.decls.size
Theorem: AIG.mkNotCached_le_size
Proof state before:
case h
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
gate : aig.Ref
⊢ aig.decls.size ≤ (aig.mkConstCached true).aig.decls.size
Tactic:
apply mkConstCached_le_size
Proof state after:
no goals
Theorem: AIG.mkNotCached_decl_eq
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
idx : Nat
aig : AIG α
gate : aig.Ref
h : idx < aig.decls.size
h2 : idx < (aig.mkNotCached gate).aig.decls.size
⊢ (aig.mkNotCached gate).aig.decls[idx] = aig.decls[idx]
Tactic:
simp only [mkNotCached]
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
idx : Nat
aig : AIG α
gate : aig.Ref
h : idx < aig.decls.size
h2 : idx < (aig.mkNotCached gate).aig.decls.size
⊢ ((aig.mkConstCached true).aig.mkGateCached
            { lhs := { ref := (aig.mkConstCached true).ref, inv := false },
              rhs := { ref := gate.cast ⋯, inv := true } }).aig.decls[idx] =
    aig.decls[idx]
Theorem: AIG.mkNotCached_decl_eq
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
idx : Nat
aig : AIG α
gate : aig.Ref
h : idx < aig.decls.size
h2 : idx < (aig.mkNotCached gate).aig.decls.size
⊢ ((aig.mkConstCached true).aig.mkGateCached
            { lhs := { ref := (aig.mkConstCached true).ref, inv := false },
              rhs := { ref := gate.cast ⋯, inv := true } }).aig.decls[idx] =
    aig.decls[idx]
Tactic:
rw [AIG.LawfulOperator.decl_eq (f := mkGateCached)]
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
idx : Nat
aig : AIG α
gate : aig.Ref
h : idx < aig.decls.size
h2 : idx < (aig.mkNotCached gate).aig.decls.size
⊢ (aig.mkConstCached true).aig.decls[idx] = aig.decls[idx]

case h1
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
idx : Nat
aig : AIG α
gate : aig.Ref
h : idx < aig.decls.size
h2 : idx < (aig.mkNotCached gate).aig.decls.size
⊢ idx < (aig.mkConstCached true).aig.decls.size
Theorem: AIG.mkNotCached_decl_eq
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
idx : Nat
aig : AIG α
gate : aig.Ref
h : idx < aig.decls.size
h2 : idx < (aig.mkNotCached gate).aig.decls.size
⊢ (aig.mkConstCached true).aig.decls[idx] = aig.decls[idx]

case h1
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
idx : Nat
aig : AIG α
gate : aig.Ref
h : idx < aig.decls.size
h2 : idx < (aig.mkNotCached gate).aig.decls.size
⊢ idx < (aig.mkConstCached true).aig.decls.size
Tactic:
rw [AIG.LawfulOperator.decl_eq (f := mkConstCached)]
Proof state after:
case h2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
idx : Nat
aig : AIG α
gate : aig.Ref
h : idx < aig.decls.size
h2 : idx < (aig.mkNotCached gate).aig.decls.size
⊢ idx < (aig.mkConstCached true).aig.decls.size
Theorem: AIG.mkNotCached_decl_eq
Proof state before:
case h2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
idx : Nat
aig : AIG α
gate : aig.Ref
h : idx < aig.decls.size
h2 : idx < (aig.mkNotCached gate).aig.decls.size
⊢ idx < (aig.mkConstCached true).aig.decls.size
Tactic:
apply LawfulOperator.lt_size_of_lt_aig_size (f := mkConstCached)
Proof state after:
case h2.h
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
idx : Nat
aig : AIG α
gate : aig.Ref
h : idx < aig.decls.size
h2 : idx < (aig.mkNotCached gate).aig.decls.size
⊢ idx < aig.decls.size
Theorem: AIG.mkNotCached_decl_eq
Proof state before:
case h2.h
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
idx : Nat
aig : AIG α
gate : aig.Ref
h : idx < aig.decls.size
h2 : idx < (aig.mkNotCached gate).aig.decls.size
⊢ idx < aig.decls.size
Tactic:
assumption
Proof state after:
no goals
Theorem: AIG.denote_mkNotCached
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
gate : aig.Ref
⊢ ⟦aig.mkNotCached gate, assign⟧ = !⟦{ aig := aig, ref := { gate := gate.gate, hgate := ⋯ } }, assign⟧
Tactic:
rw [← not_as_aig]
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
gate : aig.Ref
⊢ ⟦aig.mkNotCached gate, assign⟧ = (true && !⟦{ aig := aig, ref := { gate := gate.gate, hgate := ⋯ } }, assign⟧)
Theorem: AIG.denote_mkNotCached
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
gate : aig.Ref
⊢ ⟦aig.mkNotCached gate, assign⟧ = (true && !⟦{ aig := aig, ref := { gate := gate.gate, hgate := ⋯ } }, assign⟧)
Tactic:
simp [mkNotCached, LawfulOperator.denote_mem_prefix (f := mkConstCached) gate.hgate]
Proof state after:
no goals
Theorem: AIG.mkAndCached_le_size
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.BinaryInput
⊢ aig.decls.size ≤ (aig.mkAndCached input).aig.decls.size
Tactic:
simp only [mkAndCached]
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.BinaryInput
⊢ aig.decls.size ≤ (aig.mkGateCached (input.asGateInput false false)).aig.decls.size
Theorem: AIG.mkAndCached_le_size
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.BinaryInput
⊢ aig.decls.size ≤ (aig.mkGateCached (input.asGateInput false false)).aig.decls.size
Tactic:
apply LawfulOperator.le_size_of_le_aig_size
Proof state after:
case h
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.BinaryInput
⊢ aig.decls.size ≤ aig.decls.size