internlm/Lean-Github huggingface dataset:
Theorem: Assignment.has_of_remove_irrelevant
Proof state before:
assignment : Assignment
b : Bool
⊢ hasAssignment b (removeAssignment (!b) assignment) = true → hasAssignment b assignment = true
Tactic:
by_cases hb : b
Proof state after:
case pos
assignment : Assignment
b : Bool
hb : b = true
⊢ hasAssignment b (removeAssignment (!b) assignment) = true → hasAssignment b assignment = true

case neg
assignment : Assignment
b : Bool
hb : ¬b = true
⊢ hasAssignment b (removeAssignment (!b) assignment) = true → hasAssignment b assignment = true
Theorem: Assignment.has_of_remove_irrelevant
Proof state before:
case pos
assignment : Assignment
b : Bool
hb : b = true
⊢ hasAssignment b (removeAssignment (!b) assignment) = true → hasAssignment b assignment = true

case neg
assignment : Assignment
b : Bool
hb : ¬b = true
⊢ hasAssignment b (removeAssignment (!b) assignment) = true → hasAssignment b assignment = true
Tactic:
. simp only [hb, removeAssignment, Bool.not_true, ite_false, hasAssignment, ite_true]
  cases assignment <;> decide
Proof state after:
case neg
assignment : Assignment
b : Bool
hb : ¬b = true
⊢ hasAssignment b (removeAssignment (!b) assignment) = true → hasAssignment b assignment = true
Theorem: Assignment.has_of_remove_irrelevant
Proof state before:
case neg
assignment : Assignment
b : Bool
hb : ¬b = true
⊢ hasAssignment b (removeAssignment (!b) assignment) = true → hasAssignment b assignment = true
Tactic:
. simp only [Bool.not_eq_true] at hb
  simp only [hb, removeAssignment, Bool.not_true, ite_false, hasAssignment, ite_true]
  cases assignment <;> decide
Proof state after:
no goals
Theorem: Assignment.has_of_remove_irrelevant
Proof state before:
case pos
assignment : Assignment
b : Bool
hb : b = true
⊢ hasAssignment b (removeAssignment (!b) assignment) = true → hasAssignment b assignment = true
Tactic:
simp only [hb, removeAssignment, Bool.not_true, ite_false, hasAssignment, ite_true]
Proof state after:
case pos
assignment : Assignment
b : Bool
hb : b = true
⊢ assignment.removeNegAssignment.hasPosAssignment = true → assignment.hasPosAssignment = true
Theorem: Assignment.has_of_remove_irrelevant
Proof state before:
case pos
assignment : Assignment
b : Bool
hb : b = true
⊢ assignment.removeNegAssignment.hasPosAssignment = true → assignment.hasPosAssignment = true
Tactic:
cases assignment <;> decide
Proof state after:
no goals
Theorem: Assignment.has_of_remove_irrelevant
Proof state before:
case neg
assignment : Assignment
b : Bool
hb : ¬b = true
⊢ hasAssignment b (removeAssignment (!b) assignment) = true → hasAssignment b assignment = true
Tactic:
simp only [Bool.not_eq_true] at hb
Proof state after:
case neg
assignment : Assignment
b : Bool
hb : b = false
⊢ hasAssignment b (removeAssignment (!b) assignment) = true → hasAssignment b assignment = true
Theorem: Assignment.has_of_remove_irrelevant
Proof state before:
case neg
assignment : Assignment
b : Bool
hb : b = false
⊢ hasAssignment b (removeAssignment (!b) assignment) = true → hasAssignment b assignment = true
Tactic:
simp only [hb, removeAssignment, Bool.not_true, ite_false, hasAssignment, ite_true]
Proof state after:
case neg
assignment : Assignment
b : Bool
hb : b = false
⊢ ((if (!false) = true then removePosAssignment else removeNegAssignment) assignment).hasNegAssignment = true →
    assignment.hasNegAssignment = true
Theorem: Assignment.has_of_remove_irrelevant
Proof state before:
case neg
assignment : Assignment
b : Bool
hb : b = false
⊢ ((if (!false) = true then removePosAssignment else removeNegAssignment) assignment).hasNegAssignment = true →
    assignment.hasNegAssignment = true
Tactic:
cases assignment <;> decide
Proof state after:
no goals
Theorem: Assignment.unassigned_of_has_neither
Proof state before:
assignment : Assignment
lacks_pos : ¬assignment.hasPosAssignment = true
lacks_neg : ¬assignment.hasNegAssignment = true
⊢ assignment = unassigned
Tactic:
simp only [hasPosAssignment, Bool.not_eq_true] at lacks_pos
Proof state after:
assignment : Assignment
lacks_neg : ¬assignment.hasNegAssignment = true
lacks_pos :
  (match assignment with
    | pos => true
    | neg => false
    | both => true
    | unassigned => false) =
    false
⊢ assignment = unassigned
Theorem: Assignment.unassigned_of_has_neither
Proof state before:
assignment : Assignment
lacks_neg : ¬assignment.hasNegAssignment = true
lacks_pos :
  (match assignment with
    | pos => true
    | neg => false
    | both => true
    | unassigned => false) =
    false
⊢ assignment = unassigned
Tactic:
split at lacks_pos <;> simp_all (config := { decide := true })
Proof state after:
no goals
Theorem: Assignment.hasPos_of_addNeg
Proof state before:
assignment : Assignment
⊢ assignment.addNegAssignment.hasPosAssignment = assignment.hasPosAssignment
Tactic:
rw [hasPosAssignment, addNegAssignment]
Proof state after:
assignment : Assignment
⊢ (match
      match assignment with
      | pos => both
      | neg => neg
      | both => both
      | unassigned => neg with
    | pos => true
    | neg => false
    | both => true
    | unassigned => false) =
    assignment.hasPosAssignment
Theorem: Assignment.hasPos_of_addNeg
Proof state before:
assignment : Assignment
⊢ (match
      match assignment with
      | pos => both
      | neg => neg
      | both => both
      | unassigned => neg with
    | pos => true
    | neg => false
    | both => true
    | unassigned => false) =
    assignment.hasPosAssignment
Tactic:
cases assignment <;> simp (config := { decide := true })
Proof state after:
no goals
Theorem: Assignment.hasNeg_of_addPos
Proof state before:
assignment : Assignment
⊢ assignment.addPosAssignment.hasNegAssignment = assignment.hasNegAssignment
Tactic:
rw [hasNegAssignment, addPosAssignment]
Proof state after:
assignment : Assignment
⊢ (match
      match assignment with
      | pos => pos
      | neg => both
      | both => both
      | unassigned => pos with
    | pos => false
    | neg => true
    | both => true
    | unassigned => false) =
    assignment.hasNegAssignment
Theorem: Assignment.hasNeg_of_addPos
Proof state before:
assignment : Assignment
⊢ (match
      match assignment with
      | pos => pos
      | neg => both
      | both => both
      | unassigned => pos with
    | pos => false
    | neg => true
    | both => true
    | unassigned => false) =
    assignment.hasNegAssignment
Tactic:
cases assignment <;> simp (config := { decide := true })
Proof state after:
no goals
Theorem: Assignment.has_iff_has_of_add_complement
Proof state before:
assignment : Assignment
b : Bool
⊢ hasAssignment b assignment = true ↔ hasAssignment b (addAssignment (decide ¬b = true) assignment) = true
Tactic:
by_cases hb : b <;> simp [hb, hasAssignment, addAssignment, hasPos_of_addNeg, hasNeg_of_addPos]
Proof state after:
no goals
Theorem: Assignment.addPos_of_addNeg_eq_both
Proof state before:
assignment : Assignment
⊢ assignment.addNegAssignment.addPosAssignment = both
Tactic:
rw [addPosAssignment, addNegAssignment]
Proof state after:
assignment : Assignment
⊢ (match
      match assignment with
      | pos => both
      | neg => neg
      | both => both
      | unassigned => neg with
    | pos => pos
    | neg => both
    | both => both
    | unassigned => pos) =
    both
Theorem: Assignment.addPos_of_addNeg_eq_both
Proof state before:
assignment : Assignment
⊢ (match
      match assignment with
      | pos => both
      | neg => neg
      | both => both
      | unassigned => neg with
    | pos => pos
    | neg => both
    | both => both
    | unassigned => pos) =
    both
Tactic:
cases assignment <;> simp
Proof state after:
no goals
Theorem: Assignment.addNeg_of_addPos_eq_both
Proof state before:
assignment : Assignment
⊢ assignment.addPosAssignment.addNegAssignment = both
Tactic:
rw [addNegAssignment, addPosAssignment]
Proof state after:
assignment : Assignment
⊢ (match
      match assignment with
      | pos => pos
      | neg => both
      | both => both
      | unassigned => pos with
    | pos => both
    | neg => neg
    | both => both
    | unassigned => neg) =
    both
Theorem: Assignment.addNeg_of_addPos_eq_both
Proof state before:
assignment : Assignment
⊢ (match
      match assignment with
      | pos => pos
      | neg => both
      | both => both
      | unassigned => pos with
    | pos => both
    | neg => neg
    | both => both
    | unassigned => neg) =
    both
Tactic:
cases assignment <;> simp
Proof state after:
no goals
Theorem: bitvec_283
Proof state before:
⊢ ∀ (Y X : BitVec 1), X * Y = X &&& Y
Tactic:
intros
Proof state after:
Y✝ X✝ : BitVec 1
⊢ X✝ * Y✝ = X✝ &&& Y✝
Theorem: bitvec_283
Proof state before:
Y✝ X✝ : BitVec 1
⊢ X✝ * Y✝ = X✝ &&& Y✝
Tactic:
bv_decide
Proof state after:
no goals
Theorem: bitvec_AndOrXor_2607
Proof state before:
⊢ ∀ (a b : BitVec 64), (a ||| b ^^^ -1) ^^^ (a ^^^ -1 ||| b) = a ^^^ b
Tactic:
intros
Proof state after:
a✝ b✝ : BitVec 64
⊢ (a✝ ||| b✝ ^^^ -1) ^^^ (a✝ ^^^ -1 ||| b✝) = a✝ ^^^ b✝
Theorem: bitvec_AndOrXor_2607
Proof state before:
a✝ b✝ : BitVec 64
⊢ (a✝ ||| b✝ ^^^ -1) ^^^ (a✝ ^^^ -1 ||| b✝) = a✝ ^^^ b✝
Tactic:
bv_decide
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastExtract.go_getRef_aux
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w newWidth : Nat
aig : AIG α
input : aig.RefStream w
lo curr : Nat
hcurr : curr ≤ newWidth
falseRef : aig.Ref
s : aig.RefStream curr
idx : Nat
hidx1 : idx < curr
⊢ idx < newWidth
Tactic:
omega
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastExtract.go_getRef_aux
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w newWidth : Nat
aig : AIG α
input : aig.RefStream w
lo curr : Nat
hcurr : curr ≤ newWidth
falseRef : aig.Ref
s : aig.RefStream curr
⊢ ∀ (idx : Nat) (hidx1 : idx < curr), (go input lo curr hcurr falseRef s).getRef idx ⋯ = s.getRef idx hidx1
Tactic:
intro idx hidx
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w newWidth : Nat
aig : AIG α
input : aig.RefStream w
lo curr : Nat
hcurr : curr ≤ newWidth
falseRef : aig.Ref
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
⊢ (go input lo curr hcurr falseRef s).getRef idx ⋯ = s.getRef idx hidx
Theorem: BVExpr.bitblast.blastExtract.go_getRef_aux
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w newWidth : Nat
aig : AIG α
input : aig.RefStream w
lo curr : Nat
hcurr : curr ≤ newWidth
falseRef : aig.Ref
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
⊢ (go input lo curr hcurr falseRef s).getRef idx ⋯ = s.getRef idx hidx
Tactic:
generalize hgo : go input lo curr hcurr falseRef s = res
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w newWidth : Nat
aig : AIG α
input : aig.RefStream w
lo curr : Nat
hcurr : curr ≤ newWidth
falseRef : aig.Ref
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : aig.RefStream newWidth
hgo : go input lo curr hcurr falseRef s = res
⊢ res.getRef idx ⋯ = s.getRef idx hidx
Theorem: BVExpr.bitblast.blastExtract.go_getRef_aux
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w newWidth : Nat
aig : AIG α
input : aig.RefStream w
lo curr : Nat
hcurr : curr ≤ newWidth
falseRef : aig.Ref
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : aig.RefStream newWidth
hgo : go input lo curr hcurr falseRef s = res
⊢ res.getRef idx ⋯ = s.getRef idx hidx
Tactic:
unfold go at hgo
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w newWidth : Nat
aig : AIG α
input : aig.RefStream w
lo curr : Nat
hcurr : curr ≤ newWidth
falseRef : aig.Ref
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : aig.RefStream newWidth
hgo :
  (if h : curr < newWidth then
      let nextRef := input.getRefD (lo + curr) falseRef;
      let s := s.pushRef nextRef;
      go input lo (curr + 1) ⋯ falseRef s
    else
      let_fun this := ⋯;
      this ▸ s) =
    res
⊢ res.getRef idx ⋯ = s.getRef idx hidx
Theorem: BVExpr.bitblast.blastExtract.go_getRef_aux
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w newWidth : Nat
aig : AIG α
input : aig.RefStream w
lo curr : Nat
hcurr : curr ≤ newWidth
falseRef : aig.Ref
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : aig.RefStream newWidth
hgo :
  (if h : curr < newWidth then
      let nextRef := input.getRefD (lo + curr) falseRef;
      let s := s.pushRef nextRef;
      go input lo (curr + 1) ⋯ falseRef s
    else
      let_fun this := ⋯;
      this ▸ s) =
    res
⊢ res.getRef idx ⋯ = s.getRef idx hidx
Tactic:
split at hgo
Proof state after:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w newWidth : Nat
aig : AIG α
input : aig.RefStream w
lo curr : Nat
hcurr : curr ≤ newWidth
falseRef : aig.Ref
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : aig.RefStream newWidth
h✝ : curr < newWidth
hgo :
  (let nextRef := input.getRefD (lo + curr) falseRef;
    let s := s.pushRef nextRef;
    go input lo (curr + 1) ⋯ falseRef s) =
    res
⊢ res.getRef idx ⋯ = s.getRef idx hidx

case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w newWidth : Nat
aig : AIG α
input : aig.RefStream w
lo curr : Nat
hcurr : curr ≤ newWidth
falseRef : aig.Ref
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : aig.RefStream newWidth
h✝ : ¬curr < newWidth
hgo :
  (let_fun this := ⋯;
    this ▸ s) =
    res
⊢ res.getRef idx ⋯ = s.getRef idx hidx
Theorem: BVExpr.bitblast.blastExtract.go_getRef_aux
Proof state before:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w newWidth : Nat
aig : AIG α
input : aig.RefStream w
lo curr : Nat
hcurr : curr ≤ newWidth
falseRef : aig.Ref
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : aig.RefStream newWidth
h✝ : curr < newWidth
hgo :
  (let nextRef := input.getRefD (lo + curr) falseRef;
    let s := s.pushRef nextRef;
    go input lo (curr + 1) ⋯ falseRef s) =
    res
⊢ res.getRef idx ⋯ = s.getRef idx hidx

case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w newWidth : Nat
aig : AIG α
input : aig.RefStream w
lo curr : Nat
hcurr : curr ≤ newWidth
falseRef : aig.Ref
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : aig.RefStream newWidth
h✝ : ¬curr < newWidth
hgo :
  (let_fun this := ⋯;
    this ▸ s) =
    res
⊢ res.getRef idx ⋯ = s.getRef idx hidx
Tactic:
. dsimp at hgo
  rw [← hgo]
  rw [go_getRef_aux]
  rw [AIG.RefStream.getRef_push_ref_lt]
Proof state after:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w newWidth : Nat
aig : AIG α
input : aig.RefStream w
lo curr : Nat
hcurr : curr ≤ newWidth
falseRef : aig.Ref
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : aig.RefStream newWidth
h✝ : ¬curr < newWidth
hgo :
  (let_fun this := ⋯;
    this ▸ s) =
    res
⊢ res.getRef idx ⋯ = s.getRef idx hidx
Theorem: BVExpr.bitblast.blastExtract.go_getRef_aux
Proof state before:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w newWidth : Nat
aig : AIG α
input : aig.RefStream w
lo curr : Nat
hcurr : curr ≤ newWidth
falseRef : aig.Ref
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : aig.RefStream newWidth
h✝ : ¬curr < newWidth
hgo :
  (let_fun this := ⋯;
    this ▸ s) =
    res
⊢ res.getRef idx ⋯ = s.getRef idx hidx
Tactic:
. dsimp at hgo
  rw [← hgo]
  simp only [RefStream.getRef, Ref.mk.injEq]
  congr
  . omega
  . simp
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastExtract.go_getRef_aux
Proof state before:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w newWidth : Nat
aig : AIG α
input : aig.RefStream w
lo curr : Nat
hcurr : curr ≤ newWidth
falseRef : aig.Ref
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : aig.RefStream newWidth
h✝ : curr < newWidth
hgo :
  (let nextRef := input.getRefD (lo + curr) falseRef;
    let s := s.pushRef nextRef;
    go input lo (curr + 1) ⋯ falseRef s) =
    res
⊢ res.getRef idx ⋯ = s.getRef idx hidx
Tactic:
dsimp at hgo
Proof state after:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w newWidth : Nat
aig : AIG α
input : aig.RefStream w
lo curr : Nat
hcurr : curr ≤ newWidth
falseRef : aig.Ref
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : aig.RefStream newWidth
h✝ : curr < newWidth
hgo : go input lo (curr + 1) ⋯ falseRef (s.pushRef (input.getRefD (lo + curr) falseRef)) = res
⊢ res.getRef idx ⋯ = s.getRef idx hidx
Theorem: BVExpr.bitblast.blastExtract.go_getRef_aux
Proof state before:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w newWidth : Nat
aig : AIG α
input : aig.RefStream w
lo curr : Nat
hcurr : curr ≤ newWidth
falseRef : aig.Ref
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : aig.RefStream newWidth
h✝ : curr < newWidth
hgo : go input lo (curr + 1) ⋯ falseRef (s.pushRef (input.getRefD (lo + curr) falseRef)) = res
⊢ res.getRef idx ⋯ = s.getRef idx hidx
Tactic:
rw [← hgo]
Proof state after:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w newWidth : Nat
aig : AIG α
input : aig.RefStream w
lo curr : Nat
hcurr : curr ≤ newWidth
falseRef : aig.Ref
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : aig.RefStream newWidth
h✝ : curr < newWidth
hgo : go input lo (curr + 1) ⋯ falseRef (s.pushRef (input.getRefD (lo + curr) falseRef)) = res
⊢ (go input lo (curr + 1) ⋯ falseRef (s.pushRef (input.getRefD (lo + curr) falseRef))).getRef idx ⋯ = s.getRef idx hidx
Theorem: BVExpr.bitblast.blastExtract.go_getRef_aux
Proof state before:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w newWidth : Nat
aig : AIG α
input : aig.RefStream w
lo curr : Nat
hcurr : curr ≤ newWidth
falseRef : aig.Ref
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : aig.RefStream newWidth
h✝ : curr < newWidth
hgo : go input lo (curr + 1) ⋯ falseRef (s.pushRef (input.getRefD (lo + curr) falseRef)) = res
⊢ (go input lo (curr + 1) ⋯ falseRef (s.pushRef (input.getRefD (lo + curr) falseRef))).getRef idx ⋯ = s.getRef idx hidx
Tactic:
rw [go_getRef_aux]
Proof state after:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w newWidth : Nat
aig : AIG α
input : aig.RefStream w
lo curr : Nat
hcurr : curr ≤ newWidth
falseRef : aig.Ref
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : aig.RefStream newWidth
h✝ : curr < newWidth
hgo : go input lo (curr + 1) ⋯ falseRef (s.pushRef (input.getRefD (lo + curr) falseRef)) = res
⊢ (s.pushRef (input.getRefD (lo + curr) falseRef)).getRef idx ?isTrue.hidx1 = s.getRef idx hidx

case isTrue.hidx1
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w newWidth : Nat
aig : AIG α
input : aig.RefStream w
lo curr : Nat
hcurr : curr ≤ newWidth
falseRef : aig.Ref
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : aig.RefStream newWidth
h✝ : curr < newWidth
hgo : go input lo (curr + 1) ⋯ falseRef (s.pushRef (input.getRefD (lo + curr) falseRef)) = res
⊢ idx < curr + 1
Theorem: BVExpr.bitblast.blastExtract.go_getRef_aux
Proof state before:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w newWidth : Nat
aig : AIG α
input : aig.RefStream w
lo curr : Nat
hcurr : curr ≤ newWidth
falseRef : aig.Ref
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : aig.RefStream newWidth
h✝ : curr < newWidth
hgo : go input lo (curr + 1) ⋯ falseRef (s.pushRef (input.getRefD (lo + curr) falseRef)) = res
⊢ (s.pushRef (input.getRefD (lo + curr) falseRef)).getRef idx ?isTrue.hidx1 = s.getRef idx hidx

case isTrue.hidx1
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w newWidth : Nat
aig : AIG α
input : aig.RefStream w
lo curr : Nat
hcurr : curr ≤ newWidth
falseRef : aig.Ref
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : aig.RefStream newWidth
h✝ : curr < newWidth
hgo : go input lo (curr + 1) ⋯ falseRef (s.pushRef (input.getRefD (lo + curr) falseRef)) = res
⊢ idx < curr + 1
Tactic:
rw [AIG.RefStream.getRef_push_ref_lt]
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastExtract.go_getRef_aux
Proof state before:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w newWidth : Nat
aig : AIG α
input : aig.RefStream w
lo curr : Nat
hcurr : curr ≤ newWidth
falseRef : aig.Ref
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : aig.RefStream newWidth
h✝ : ¬curr < newWidth
hgo :
  (let_fun this := ⋯;
    this ▸ s) =
    res
⊢ res.getRef idx ⋯ = s.getRef idx hidx
Tactic:
dsimp at hgo
Proof state after:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w newWidth : Nat
aig : AIG α
input : aig.RefStream w
lo curr : Nat
hcurr : curr ≤ newWidth
falseRef : aig.Ref
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : aig.RefStream newWidth
h✝ : ¬curr < newWidth
hgo : ⋯ ▸ s = res
⊢ res.getRef idx ⋯ = s.getRef idx hidx
Theorem: BVExpr.bitblast.blastExtract.go_getRef_aux
Proof state before:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w newWidth : Nat
aig : AIG α
input : aig.RefStream w
lo curr : Nat
hcurr : curr ≤ newWidth
falseRef : aig.Ref
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : aig.RefStream newWidth
h✝ : ¬curr < newWidth
hgo : ⋯ ▸ s = res
⊢ res.getRef idx ⋯ = s.getRef idx hidx
Tactic:
rw [← hgo]
Proof state after:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w newWidth : Nat
aig : AIG α
input : aig.RefStream w
lo curr : Nat
hcurr : curr ≤ newWidth
falseRef : aig.Ref
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : aig.RefStream newWidth
h✝ : ¬curr < newWidth
hgo : ⋯ ▸ s = res
⊢ (⋯ ▸ s).getRef idx ⋯ = s.getRef idx hidx
Theorem: BVExpr.bitblast.blastExtract.go_getRef_aux
Proof state before:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w newWidth : Nat
aig : AIG α
input : aig.RefStream w
lo curr : Nat
hcurr : curr ≤ newWidth
falseRef : aig.Ref
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : aig.RefStream newWidth
h✝ : ¬curr < newWidth
hgo : ⋯ ▸ s = res
⊢ (⋯ ▸ s).getRef idx ⋯ = s.getRef idx hidx
Tactic:
simp only [RefStream.getRef, Ref.mk.injEq]
Proof state after:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w newWidth : Nat
aig : AIG α
input : aig.RefStream w
lo curr : Nat
hcurr : curr ≤ newWidth
falseRef : aig.Ref
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : aig.RefStream newWidth
h✝ : ¬curr < newWidth
hgo : ⋯ ▸ s = res
⊢ (⋯ ▸ s).refs[idx] = s.refs[idx]
Theorem: BVExpr.bitblast.blastExtract.go_getRef_aux
Proof state before:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w newWidth : Nat
aig : AIG α
input : aig.RefStream w
lo curr : Nat
hcurr : curr ≤ newWidth
falseRef : aig.Ref
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : aig.RefStream newWidth
h✝ : ¬curr < newWidth
hgo : ⋯ ▸ s = res
⊢ (⋯ ▸ s).refs[idx] = s.refs[idx]
Tactic:
congr
Proof state after:
case isFalse.e_xs.h.e_5
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w newWidth : Nat
aig : AIG α
input : aig.RefStream w
lo curr : Nat
hcurr : curr ≤ newWidth
falseRef : aig.Ref
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : aig.RefStream newWidth
h✝ : ¬curr < newWidth
hgo : ⋯ ▸ s = res
⊢ newWidth = curr

case isFalse.e_xs.h.e_6
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w newWidth : Nat
aig : AIG α
input : aig.RefStream w
lo curr : Nat
hcurr : curr ≤ newWidth
falseRef : aig.Ref
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : aig.RefStream newWidth
h✝ : ¬curr < newWidth
hgo : ⋯ ▸ s = res
⊢ HEq (⋯ ▸ s) s