internlm/Lean-Github huggingface dataset:
Theorem: BVPred.mkEq_denote_eq_eval_beq
Proof state before:
case mp
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ (∀ (idx : Nat) (hidx : idx < w),
      ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ =
        ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧) →
    lhs = rhs

case mpr
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ lhs = rhs →
    ∀ (idx : Nat) (hidx : idx < w),
      ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ =
        ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧
Tactic:
. intro h
  ext
  rw [← hleft, ← hright]
  . simp [h]
  . omega
  . omega
Proof state after:
case mpr
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ lhs = rhs →
    ∀ (idx : Nat) (hidx : idx < w),
      ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ =
        ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧
Theorem: BVPred.mkEq_denote_eq_eval_beq
Proof state before:
case mpr
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ lhs = rhs →
    ∀ (idx : Nat) (hidx : idx < w),
      ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ =
        ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧
Tactic:
. intro h idx hidx
  rw [hleft, hright]
  simp [h]
Proof state after:
no goals
Theorem: BVPred.mkEq_denote_eq_eval_beq
Proof state before:
case mp
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ (∀ (idx : Nat) (hidx : idx < w),
      ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ =
        ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧) →
    lhs = rhs
Tactic:
intro h
Proof state after:
case mp
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
h :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ =
      ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧
⊢ lhs = rhs
Theorem: BVPred.mkEq_denote_eq_eval_beq
Proof state before:
case mp
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
h :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ =
      ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧
⊢ lhs = rhs
Tactic:
ext
Proof state after:
case mp.pred
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
h :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ =
      ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧
i✝ : Fin w
⊢ lhs.getLsb ↑i✝ = rhs.getLsb ↑i✝
Theorem: BVPred.mkEq_denote_eq_eval_beq
Proof state before:
case mp.pred
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
h :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ =
      ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧
i✝ : Fin w
⊢ lhs.getLsb ↑i✝ = rhs.getLsb ↑i✝
Tactic:
rw [← hleft, ← hright]
Proof state after:
case mp.pred
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
h :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ =
      ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧
i✝ : Fin w
⊢ ⟦{ aig := aig, ref := pair.lhs.getRef ↑i✝ ?mp.pred.hidx }, assign⟧ =
    ⟦{ aig := aig, ref := pair.rhs.getRef ↑i✝ ?mp.pred.hidx }, assign⟧

case mp.pred.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
h :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ =
      ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧
i✝ : Fin w
⊢ ↑i✝ < w

case mp.pred.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
h :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ =
      ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧
i✝ : Fin w
⊢ ↑i✝ < w

case mp.pred.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
h :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ =
      ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧
i✝ : Fin w
⊢ ↑i✝ < w
Theorem: BVPred.mkEq_denote_eq_eval_beq
Proof state before:
case mp.pred.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
h :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ =
      ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧
i✝ : Fin w
⊢ ↑i✝ < w

case mp.pred.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
h :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ =
      ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧
i✝ : Fin w
⊢ ↑i✝ < w

case mp.pred.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
h :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ =
      ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧
i✝ : Fin w
⊢ ↑i✝ < w
Tactic:
. omega
Proof state after:
case mp.pred.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
h :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ =
      ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧
i✝ : Fin w
⊢ ↑i✝ < w

case mp.pred.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
h :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ =
      ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧
i✝ : Fin w
⊢ ↑i✝ < w
Theorem: BVPred.mkEq_denote_eq_eval_beq
Proof state before:
case mp.pred.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
h :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ =
      ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧
i✝ : Fin w
⊢ ↑i✝ < w

case mp.pred.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
h :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ =
      ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧
i✝ : Fin w
⊢ ↑i✝ < w
Tactic:
. omega
Proof state after:
no goals
Theorem: BVPred.mkEq_denote_eq_eval_beq
Proof state before:
case mp.pred
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
h :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ =
      ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧
i✝ : Fin w
⊢ ⟦{ aig := aig, ref := pair.lhs.getRef ↑i✝ ?mp.pred.hidx }, assign⟧ =
    ⟦{ aig := aig, ref := pair.rhs.getRef ↑i✝ ?mp.pred.hidx }, assign⟧
Tactic:
simp [h]
Proof state after:
no goals
Theorem: BVPred.mkEq_denote_eq_eval_beq
Proof state before:
case mp.pred.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
h :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ =
      ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧
i✝ : Fin w
⊢ ↑i✝ < w
Tactic:
omega
Proof state after:
no goals
Theorem: BVPred.mkEq_denote_eq_eval_beq
Proof state before:
case mpr
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ lhs = rhs →
    ∀ (idx : Nat) (hidx : idx < w),
      ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ =
        ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧
Tactic:
intro h idx hidx
Proof state after:
case mpr
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
h : lhs = rhs
idx : Nat
hidx : idx < w
⊢ ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧
Theorem: BVPred.mkEq_denote_eq_eval_beq
Proof state before:
case mpr
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
h : lhs = rhs
idx : Nat
hidx : idx < w
⊢ ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧
Tactic:
rw [hleft, hright]
Proof state after:
case mpr
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
h : lhs = rhs
idx : Nat
hidx : idx < w
⊢ lhs.getLsb idx = rhs.getLsb idx
Theorem: BVPred.mkEq_denote_eq_eval_beq
Proof state before:
case mpr
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
h : lhs = rhs
idx : Nat
hidx : idx < w
⊢ lhs.getLsb idx = rhs.getLsb idx
Tactic:
simp [h]
Proof state after:
no goals
Theorem: bitvec_AndOrXor_2627
Proof state before:
⊢ ∀ (a c b : BitVec 64), a ^^^ c ^^^ (a ||| b) = (a ^^^ -1) &&& b ^^^ c
Tactic:
intros
Proof state after:
a✝ c✝ b✝ : BitVec 64
⊢ a✝ ^^^ c✝ ^^^ (a✝ ||| b✝) = (a✝ ^^^ -1) &&& b✝ ^^^ c✝
Theorem: bitvec_AndOrXor_2627
Proof state before:
a✝ c✝ b✝ : BitVec 64
⊢ a✝ ^^^ c✝ ^^^ (a✝ ||| b✝) = (a✝ ^^^ -1) &&& b✝ ^^^ c✝
Tactic:
bv_decide
Proof state after:
no goals
Theorem: bitvec_152
Proof state before:
⊢ ∀ (x : BitVec 64), x * -1 = 0 - x
Tactic:
intros
Proof state after:
x✝ : BitVec 64
⊢ x✝ * -1 = 0 - x✝
Theorem: bitvec_152
Proof state before:
x✝ : BitVec 64
⊢ x✝ * -1 = 0 - x✝
Tactic:
bv_decide
Proof state after:
no goals
Theorem: bitvec_InstCombineShift__582
Proof state before:
⊢ ∀ (X C : BitVec 64), X <<< C >>> C = X &&& (-1) >>> C
Tactic:
intros
Proof state after:
X✝ C✝ : BitVec 64
⊢ X✝ <<< C✝ >>> C✝ = X✝ &&& (-1) >>> C✝
Theorem: bitvec_InstCombineShift__582
Proof state before:
X✝ C✝ : BitVec 64
⊢ X✝ <<< C✝ >>> C✝ = X✝ &&& (-1) >>> C✝
Tactic:
bv_decide
Proof state after:
no goals
Theorem: bitvec_InstCombineShift__440
Proof state before:
⊢ ∀ (Y X C C2 : BitVec 64), (Y ^^^ X >>> C &&& C2) <<< C = X &&& C2 <<< C ^^^ Y <<< C
Tactic:
intros
Proof state after:
Y✝ X✝ C✝ C2✝ : BitVec 64
⊢ (Y✝ ^^^ X✝ >>> C✝ &&& C2✝) <<< C✝ = X✝ &&& C2✝ <<< C✝ ^^^ Y✝ <<< C✝
Theorem: bitvec_InstCombineShift__440
Proof state before:
Y✝ X✝ C✝ C2✝ : BitVec 64
⊢ (Y✝ ^^^ X✝ >>> C✝ &&& C2✝) <<< C✝ = X✝ &&& C2✝ <<< C✝ ^^^ Y✝ <<< C✝
Tactic:
bv_decide
Proof state after:
no goals
Theorem: bitvec_AndOrXor_2430
Proof state before:
⊢ ∀ (y x : BitVec 64), (x ||| y) ^^^ -1 = (x ^^^ -1) &&& (y ^^^ -1)
Tactic:
intros
Proof state after:
y✝ x✝ : BitVec 64
⊢ (x✝ ||| y✝) ^^^ -1 = (x✝ ^^^ -1) &&& (y✝ ^^^ -1)
Theorem: bitvec_AndOrXor_2430
Proof state before:
y✝ x✝ : BitVec 64
⊢ (x✝ ||| y✝) ^^^ -1 = (x✝ ^^^ -1) &&& (y✝ ^^^ -1)
Tactic:
bv_decide
Proof state after:
no goals
Theorem: Misc.not_forall
Proof state before:
α : Sort u_1
p : α → Prop
⊢ (¬∀ (x : α), p x) ↔ ∃ x, ¬p x
Tactic:
have em := Classical.propDecidable
Proof state after:
α : Sort u_1
p : α → Prop
em : (a : Prop) → Decidable a
⊢ (¬∀ (x : α), p x) ↔ ∃ x, ¬p x
Theorem: Misc.not_forall
Proof state before:
α : Sort u_1
p : α → Prop
em : (a : Prop) → Decidable a
⊢ (¬∀ (x : α), p x) ↔ ∃ x, ¬p x
Tactic:
apply Decidable.not_forall
Proof state after:
no goals
Theorem: Misc.dite_eq_left_iff
Proof state before:
P : Prop
α✝ : Sort u_1
a : α✝
B : ¬P → α✝
inst✝ : Decidable P
⊢ dite P (fun x => a) B = a ↔ ∀ (h : ¬P), B h = a
Tactic:
by_cases P <;> simp [*, forall_prop_of_true, forall_prop_of_false]
Proof state after:
no goals
Theorem: Misc.dite_eq_right_iff
Proof state before:
P : Prop
α✝ : Sort u_1
A : P → α✝
b : α✝
inst✝ : Decidable P
⊢ (dite P A fun x => b) = b ↔ ∀ (h : P), A h = b
Tactic:
by_cases P <;> simp [*, forall_prop_of_true, forall_prop_of_false]
Proof state after:
no goals
Theorem: Misc.Bool.exists_bool
Proof state before:
p : Bool → Prop
x✝ : ∃ b, p b
b : Bool
h : p b
⊢ p false ∨ p true
Tactic:
cases b
Proof state after:
case false
p : Bool → Prop
x✝ : ∃ b, p b
h : p false
⊢ p false ∨ p true

case true
p : Bool → Prop
x✝ : ∃ b, p b
h : p true
⊢ p false ∨ p true
Theorem: Misc.Bool.exists_bool
Proof state before:
case false
p : Bool → Prop
x✝ : ∃ b, p b
h : p false
⊢ p false ∨ p true

case true
p : Bool → Prop
x✝ : ∃ b, p b
h : p true
⊢ p false ∨ p true
Tactic:
exact Or.inl h
Proof state after:
case true
p : Bool → Prop
x✝ : ∃ b, p b
h : p true
⊢ p false ∨ p true
Theorem: Misc.Bool.exists_bool
Proof state before:
case true
p : Bool → Prop
x✝ : ∃ b, p b
h : p true
⊢ p false ∨ p true
Tactic:
exact Or.inr h
Proof state after:
no goals
Theorem: Misc.Bool.decide_coe
Proof state before:
b : Bool
h : Decidable (b = true)
⊢ decide (b = true) = b
Tactic:
cases b
Proof state after:
case false
h : Decidable (false = true)
⊢ decide (false = true) = false

case true
h : Decidable (true = true)
⊢ decide (true = true) = true
Theorem: Misc.Bool.decide_coe
Proof state before:
case false
h : Decidable (false = true)
⊢ decide (false = true) = false
Tactic:
exact decide_eq_false $ λ j => by cases j
Proof state after:
no goals
Theorem: Misc.Bool.decide_coe
Proof state before:
h : Decidable (false = true)
j : false = true
⊢ False
Tactic:
cases j
Proof state after:
no goals
Theorem: Misc.Bool.decide_coe
Proof state before:
case true
h : Decidable (true = true)
⊢ decide (true = true) = true
Tactic:
exact decide_eq_true $ rfl
Proof state after:
no goals
Theorem: Misc.Bool.eq_not_iff
Proof state before:
⊢ ∀ {a b : Bool}, a = !b ↔ a ≠ b
Tactic:
intro a b
Proof state after:
a b : Bool
⊢ a = !b ↔ a ≠ b
Theorem: Misc.Bool.eq_not_iff
Proof state before:
a b : Bool
⊢ a = !b ↔ a ≠ b
Tactic:
cases a <;> cases b <;> decide
Proof state after:
no goals
Theorem: Misc.Prod.lex_def
Proof state before:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
p q : α × β
h : Prod.Lex r s p q
⊢ r p.fst q.fst ∨ p.fst = q.fst ∧ s p.snd q.snd
Tactic:
cases h <;> simp [*]
Proof state after:
no goals
Theorem: Misc.Prod.lex_def
Proof state before:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
p q : α × β
h✝ : r p.fst q.fst ∨ p.fst = q.fst ∧ s p.snd q.snd
a : α
b : β
c : α
d : β
e : (a, b).fst = (c, d).fst
h : s (a, b).snd (c, d).snd
⊢ Prod.Lex r s (a, b) (c, d)
Tactic:
subst e
Proof state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
p q : α × β
h✝ : r p.fst q.fst ∨ p.fst = q.fst ∧ s p.snd q.snd
a : α
b d : β
h : s (a, b).snd ((a, b).fst, d).snd
⊢ Prod.Lex r s (a, b) ((a, b).fst, d)
Theorem: Misc.Prod.lex_def
Proof state before:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
p q : α × β
h✝ : r p.fst q.fst ∨ p.fst = q.fst ∧ s p.snd q.snd
a : α
b d : β
h : s (a, b).snd ((a, b).fst, d).snd
⊢ Prod.Lex r s (a, b) ((a, b).fst, d)
Tactic:
exact Prod.Lex.right _ h
Proof state after:
no goals
Theorem: Misc.List.nodup_cons
Proof state before:
α : Type u_1
a : α
l : List α
⊢ (a :: l).Nodup ↔ ¬a ∈ l ∧ l.Nodup
Tactic:
simp only [Nodup, pairwise_cons, forall_mem_ne]
Proof state after:
no goals
Theorem: Misc.List.nodup_append
Proof state before:
α : Type u_1
l₁ l₂ : List α
⊢ (l₁ ++ l₂).Nodup ↔ l₁.Nodup ∧ l₂.Nodup ∧ l₁.Disjoint l₂
Tactic:
simp only [Nodup, pairwise_append, disjoint_iff_ne]
Proof state after:
no goals
Theorem: Misc.List.Nodup.erase_eq_filter
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
d : l.Nodup
a : α
⊢ l.erase a = filter (fun x => x != a) l
Tactic:
induction d
Proof state after:
case nil
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
⊢ [].erase a = filter (fun x => x != a) []

case cons
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a a✝² : α
l✝ : List α
a✝¹ : ∀ (a' : α), a' ∈ l✝ → a✝² ≠ a'
a✝ : Pairwise (fun x x_1 => x ≠ x_1) l✝
a_ih✝ : l✝.erase a = filter (fun x => x != a) l✝
⊢ (a✝² :: l✝).erase a = filter (fun x => x != a) (a✝² :: l✝)