Theorem: BVExpr.bitblast.blastAppend_eq_eval_getLsb (LeanSAT/Reflect/BVExpr/BitBlast/Lemmas/Append.lean)

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : AppendTarget aig newWidth
assign : α → Bool
idx : Nat
hidx : idx < newWidth
hr : ¬idx < target.rw
this : newWidth = target.rw + target.lw
⊢ idx - target.rw < target.lw
Tactic:
omega
State after:
no goals

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : AppendTarget aig newWidth
assign : α → Bool
⊢ ∀ (idx : Nat) (hidx : idx < newWidth),
    ⟦{ aig := (blastAppend aig target).aig, ref := (blastAppend aig target).stream.getRef idx hidx }, assign⟧ =
      if hr : idx < target.rw then ⟦{ aig := aig, ref := target.rhs.getRef idx hr }, assign⟧
      else
        let_fun this := ⋯;
        ⟦{ aig := aig, ref := target.lhs.getRef (idx - target.rw) ⋯ }, assign⟧
Tactic:
intros
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : AppendTarget aig newWidth
assign : α → Bool
idx✝ : Nat
hidx✝ : idx✝ < newWidth
⊢ ⟦{ aig := (blastAppend aig target).aig, ref := (blastAppend aig target).stream.getRef idx✝ hidx✝ }, assign⟧ =
    if hr : idx✝ < target.rw then ⟦{ aig := aig, ref := target.rhs.getRef idx✝ hr }, assign⟧
    else
      let_fun this := ⋯;
      ⟦{ aig := aig, ref := target.lhs.getRef (idx✝ - target.rw) ⋯ }, assign⟧

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : AppendTarget aig newWidth
assign : α → Bool
idx✝ : Nat
hidx✝ : idx✝ < newWidth
⊢ ⟦{ aig := (blastAppend aig target).aig, ref := (blastAppend aig target).stream.getRef idx✝ hidx✝ }, assign⟧ =
    if hr : idx✝ < target.rw then ⟦{ aig := aig, ref := target.rhs.getRef idx✝ hr }, assign⟧
    else
      let_fun this := ⋯;
      ⟦{ aig := aig, ref := target.lhs.getRef (idx✝ - target.rw) ⋯ }, assign⟧
Tactic:
unfold blastAppend
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : AppendTarget aig newWidth
assign : α → Bool
idx✝ : Nat
hidx✝ : idx✝ < newWidth
⊢ ⟦{
        aig :=
          (match target with
            | AppendTarget.mk lhs rhs h =>
              let combined := rhs.append lhs;
              { aig := aig, stream := ⋯ ▸ combined }).aig,
        ref :=
          (match target with
                | AppendTarget.mk lhs rhs h =>
                  let combined := rhs.append lhs;
                  { aig := aig, stream := ⋯ ▸ combined }).stream.getRef
            idx✝ hidx✝ },
      assign⟧ =
    if hr : idx✝ < target.rw then ⟦{ aig := aig, ref := target.rhs.getRef idx✝ hr }, assign⟧
    else
      let_fun this := ⋯;
      ⟦{ aig := aig, ref := target.lhs.getRef (idx✝ - target.rw) ⋯ }, assign⟧

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : AppendTarget aig newWidth
assign : α → Bool
idx✝ : Nat
hidx✝ : idx✝ < newWidth
⊢ ⟦{
        aig :=
          (match target with
            | AppendTarget.mk lhs rhs h =>
              let combined := rhs.append lhs;
              { aig := aig, stream := ⋯ ▸ combined }).aig,
        ref :=
          (match target with
                | AppendTarget.mk lhs rhs h =>
                  let combined := rhs.append lhs;
                  { aig := aig, stream := ⋯ ▸ combined }).stream.getRef
            idx✝ hidx✝ },
      assign⟧ =
    if hr : idx✝ < target.rw then ⟦{ aig := aig, ref := target.rhs.getRef idx✝ hr }, assign⟧
    else
      let_fun this := ⋯;
      ⟦{ aig := aig, ref := target.lhs.getRef (idx✝ - target.rw) ⋯ }, assign⟧
Tactic:
rcases target with ⟨lw, rw, lhs, rhs, ht⟩
State after:
case mk.refl
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx✝ lw✝ rw✝ : Nat
lw : aig.RefStream lw✝
rw : aig.RefStream rw✝
hidx✝ : idx✝ < rw✝ + lw✝
⊢ ⟦{
        aig :=
          (match AppendTarget.mk lw rw ⋯ with
            | AppendTarget.mk lhs rhs h =>
              let combined := rhs.append lhs;
              { aig := aig, stream := ⋯ ▸ combined }).aig,
        ref :=
          (match AppendTarget.mk lw rw ⋯ with
                | AppendTarget.mk lhs rhs h =>
                  let combined := rhs.append lhs;
                  { aig := aig, stream := ⋯ ▸ combined }).stream.getRef
            idx✝ hidx✝ },
      assign⟧ =
    if hr : idx✝ < (AppendTarget.mk lw rw ⋯).rw then
      ⟦{ aig := aig, ref := (AppendTarget.mk lw rw ⋯).rhs.getRef idx✝ hr }, assign⟧
    else
      let_fun this := ⋯;
      ⟦{ aig := aig, ref := (AppendTarget.mk lw rw ⋯).lhs.getRef (idx✝ - (AppendTarget.mk lw rw ⋯).rw) ⋯ }, assign⟧

State before:
case mk.refl
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx✝ lw✝ rw✝ : Nat
lw : aig.RefStream lw✝
rw : aig.RefStream rw✝
hidx✝ : idx✝ < rw✝ + lw✝
⊢ ⟦{
        aig :=
          (match AppendTarget.mk lw rw ⋯ with
            | AppendTarget.mk lhs rhs h =>
              let combined := rhs.append lhs;
              { aig := aig, stream := ⋯ ▸ combined }).aig,
        ref :=
          (match AppendTarget.mk lw rw ⋯ with
                | AppendTarget.mk lhs rhs h =>
                  let combined := rhs.append lhs;
                  { aig := aig, stream := ⋯ ▸ combined }).stream.getRef
            idx✝ hidx✝ },
      assign⟧ =
    if hr : idx✝ < (AppendTarget.mk lw rw ⋯).rw then
      ⟦{ aig := aig, ref := (AppendTarget.mk lw rw ⋯).rhs.getRef idx✝ hr }, assign⟧
    else
      let_fun this := ⋯;
      ⟦{ aig := aig, ref := (AppendTarget.mk lw rw ⋯).lhs.getRef (idx✝ - (AppendTarget.mk lw rw ⋯).rw) ⋯ }, assign⟧
Tactic:
dsimp
State after:
case mk.refl
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx✝ lw✝ rw✝ : Nat
lw : aig.RefStream lw✝
rw : aig.RefStream rw✝
hidx✝ : idx✝ < rw✝ + lw✝
⊢ ⟦{ aig := aig, ref := (rw.append lw).getRef idx✝ hidx✝ }, assign⟧ =
    if hr : idx✝ < rw✝ then ⟦{ aig := aig, ref := rw.getRef idx✝ hr }, assign⟧
    else ⟦{ aig := aig, ref := lw.getRef (idx✝ - rw✝) ⋯ }, assign⟧

State before:
case mk.refl
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx✝ lw✝ rw✝ : Nat
lw : aig.RefStream lw✝
rw : aig.RefStream rw✝
hidx✝ : idx✝ < rw✝ + lw✝
⊢ ⟦{ aig := aig, ref := (rw.append lw).getRef idx✝ hidx✝ }, assign⟧ =
    if hr : idx✝ < rw✝ then ⟦{ aig := aig, ref := rw.getRef idx✝ hr }, assign⟧
    else ⟦{ aig := aig, ref := lw.getRef (idx✝ - rw✝) ⋯ }, assign⟧
Tactic:
rw [AIG.RefStream.getRef_append]
State after:
case mk.refl
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx✝ lw✝ rw✝ : Nat
lw : aig.RefStream lw✝
rw : aig.RefStream rw✝
hidx✝ : idx✝ < rw✝ + lw✝
⊢ ⟦{ aig := aig, ref := if h : idx✝ < rw✝ then rw.getRef idx✝ h else lw.getRef (idx✝ - rw✝) ⋯ }, assign⟧ =
    if hr : idx✝ < rw✝ then ⟦{ aig := aig, ref := rw.getRef idx✝ hr }, assign⟧
    else ⟦{ aig := aig, ref := lw.getRef (idx✝ - rw✝) ⋯ }, assign⟧

State before:
case mk.refl
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx✝ lw✝ rw✝ : Nat
lw : aig.RefStream lw✝
rw : aig.RefStream rw✝
hidx✝ : idx✝ < rw✝ + lw✝
⊢ ⟦{ aig := aig, ref := if h : idx✝ < rw✝ then rw.getRef idx✝ h else lw.getRef (idx✝ - rw✝) ⋯ }, assign⟧ =
    if hr : idx✝ < rw✝ then ⟦{ aig := aig, ref := rw.getRef idx✝ hr }, assign⟧
    else ⟦{ aig := aig, ref := lw.getRef (idx✝ - rw✝) ⋯ }, assign⟧
Tactic:
split <;> rfl
State after:
no goals