Theorem: AIG.RefStream.denote_ite (LeanSAT/AIG/If.lean)

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
assign : α → Bool
aig : AIG α
input : IfInput aig w
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := (ite aig input).aig, ref := (ite aig input).stream.getRef idx hidx }, assign⟧ =
      if ⟦{ aig := aig, ref := input.discr }, assign⟧ = true then
        ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧
      else ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧
Tactic:
intro idx hidx
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
assign : α → Bool
aig : AIG α
input : IfInput aig w
idx : Nat
hidx : idx < w
⊢ ⟦{ aig := (ite aig input).aig, ref := (ite aig input).stream.getRef idx hidx }, assign⟧ =
    if ⟦{ aig := aig, ref := input.discr }, assign⟧ = true then
      ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧
    else ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
assign : α → Bool
aig : AIG α
input : IfInput aig w
idx : Nat
hidx : idx < w
⊢ ⟦{ aig := (ite aig input).aig, ref := (ite aig input).stream.getRef idx hidx }, assign⟧ =
    if ⟦{ aig := aig, ref := input.discr }, assign⟧ = true then
      ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧
    else ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧
Tactic:
unfold ite
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
assign : α → Bool
aig : AIG α
input : IfInput aig w
idx : Nat
hidx : idx < w
⊢ ⟦{
        aig :=
          (match input with
            | { discr := discr, lhs := lhs, rhs := rhs } => ite.go aig 0 ⋯ discr lhs rhs empty).aig,
        ref :=
          (match input with
                | { discr := discr, lhs := lhs, rhs := rhs } => ite.go aig 0 ⋯ discr lhs rhs empty).stream.getRef
            idx hidx },
      assign⟧ =
    if ⟦{ aig := aig, ref := input.discr }, assign⟧ = true then
      ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧
    else ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
assign : α → Bool
aig : AIG α
input : IfInput aig w
idx : Nat
hidx : idx < w
⊢ ⟦{
        aig :=
          (match input with
            | { discr := discr, lhs := lhs, rhs := rhs } => ite.go aig 0 ⋯ discr lhs rhs empty).aig,
        ref :=
          (match input with
                | { discr := discr, lhs := lhs, rhs := rhs } => ite.go aig 0 ⋯ discr lhs rhs empty).stream.getRef
            idx hidx },
      assign⟧ =
    if ⟦{ aig := aig, ref := input.discr }, assign⟧ = true then
      ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧
    else ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧
Tactic:
dsimp
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
assign : α → Bool
aig : AIG α
input : IfInput aig w
idx : Nat
hidx : idx < w
⊢ ⟦{ aig := (ite.go aig 0 ⋯ input.discr input.lhs input.rhs empty).aig,
        ref := (ite.go aig 0 ⋯ input.discr input.lhs input.rhs empty).stream.getRef idx hidx },
      assign⟧ =
    if ⟦{ aig := aig, ref := input.discr }, assign⟧ = true then
      ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧
    else ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
assign : α → Bool
aig : AIG α
input : IfInput aig w
idx : Nat
hidx : idx < w
⊢ ⟦{ aig := (ite.go aig 0 ⋯ input.discr input.lhs input.rhs empty).aig,
        ref := (ite.go aig 0 ⋯ input.discr input.lhs input.rhs empty).stream.getRef idx hidx },
      assign⟧ =
    if ⟦{ aig := aig, ref := input.discr }, assign⟧ = true then
      ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧
    else ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧
Tactic:
rw [ite.denote_go]
State after:
case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
assign : α → Bool
aig : AIG α
input : IfInput aig w
idx : Nat
hidx : idx < w
⊢ 0 ≤ idx

State before:
case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
assign : α → Bool
aig : AIG α
input : IfInput aig w
idx : Nat
hidx : idx < w
⊢ 0 ≤ idx
Tactic:
omega
State after:
no goals