Theorem: AIG.denote_relabel (LeanSAT/AIG/Relabel.lean)

State before:
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
aig : AIG α
f : α → β
start : Nat
hidx : start < (relabel f aig).decls.size
assign : β → Bool
⊢ start < aig.decls.size
Tactic:
rw [← relabel_size_eq_size (f := f)]
State after:
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
aig : AIG α
f : α → β
start : Nat
hidx : start < (relabel f aig).decls.size
assign : β → Bool
⊢ start < (relabel f aig).decls.size

State before:
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
aig : AIG α
f : α → β
start : Nat
hidx : start < (relabel f aig).decls.size
assign : β → Bool
⊢ start < (relabel f aig).decls.size
Tactic:
omega
State after:
no goals

State before:
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
aig : AIG α
f : α → β
start : Nat
hidx : start < (relabel f aig).decls.size
assign : β → Bool
⊢ ⟦{ aig := relabel f aig, ref := { gate := start, hgate := hidx } }, assign⟧ =
    ⟦{ aig := aig, ref := { gate := start, hgate := ⋯ } }, assign ∘ f⟧
Tactic:
apply denote_idx_trichotomy
State after:
case hconst
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
aig : AIG α
f : α → β
start : Nat
hidx : start < (relabel f aig).decls.size
assign : β → Bool
⊢ ∀ (b : Bool),
    (relabel f aig).decls[start] = Decl.const b →
      ⟦{ aig := relabel f aig, ref := { gate := start, hgate := hidx } }, assign⟧ =
        ⟦{ aig := aig, ref := { gate := start, hgate := ⋯ } }, assign ∘ f⟧

case hatom
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
aig : AIG α
f : α → β
start : Nat
hidx : start < (relabel f aig).decls.size
assign : β → Bool
⊢ ∀ (a : β),
    (relabel f aig).decls[start] = Decl.atom a →
      ⟦{ aig := relabel f aig, ref := { gate := start, hgate := hidx } }, assign⟧ =
        ⟦{ aig := aig, ref := { gate := start, hgate := ⋯ } }, assign ∘ f⟧

case hgate
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
aig : AIG α
f : α → β
start : Nat
hidx : start < (relabel f aig).decls.size
assign : β → Bool
⊢ ∀ (lhs rhs : Nat) (linv rinv : Bool),
    (relabel f aig).decls[start] = Decl.gate lhs rhs linv rinv →
      ⟦{ aig := relabel f aig, ref := { gate := start, hgate := hidx } }, assign⟧ =
        ⟦{ aig := aig, ref := { gate := start, hgate := ⋯ } }, assign ∘ f⟧

State before:
case hconst
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
aig : AIG α
f : α → β
start : Nat
hidx : start < (relabel f aig).decls.size
assign : β → Bool
⊢ ∀ (b : Bool),
    (relabel f aig).decls[start] = Decl.const b →
      ⟦{ aig := relabel f aig, ref := { gate := start, hgate := hidx } }, assign⟧ =
        ⟦{ aig := aig, ref := { gate := start, hgate := ⋯ } }, assign ∘ f⟧

case hatom
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
aig : AIG α
f : α → β
start : Nat
hidx : start < (relabel f aig).decls.size
assign : β → Bool
⊢ ∀ (a : β),
    (relabel f aig).decls[start] = Decl.atom a →
      ⟦{ aig := relabel f aig, ref := { gate := start, hgate := hidx } }, assign⟧ =
        ⟦{ aig := aig, ref := { gate := start, hgate := ⋯ } }, assign ∘ f⟧

case hgate
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
aig : AIG α
f : α → β
start : Nat
hidx : start < (relabel f aig).decls.size
assign : β → Bool
⊢ ∀ (lhs rhs : Nat) (linv rinv : Bool),
    (relabel f aig).decls[start] = Decl.gate lhs rhs linv rinv →
      ⟦{ aig := relabel f aig, ref := { gate := start, hgate := hidx } }, assign⟧ =
        ⟦{ aig := aig, ref := { gate := start, hgate := ⋯ } }, assign ∘ f⟧
Tactic:
. intro b heq1
  have heq2 := relabel_const heq1
  rw [denote_idx_const heq1]
  rw [denote_idx_const heq2]
State after:
case hatom
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
aig : AIG α
f : α → β
start : Nat
hidx : start < (relabel f aig).decls.size
assign : β → Bool
⊢ ∀ (a : β),
    (relabel f aig).decls[start] = Decl.atom a →
      ⟦{ aig := relabel f aig, ref := { gate := start, hgate := hidx } }, assign⟧ =
        ⟦{ aig := aig, ref := { gate := start, hgate := ⋯ } }, assign ∘ f⟧

case hgate
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
aig : AIG α
f : α → β
start : Nat
hidx : start < (relabel f aig).decls.size
assign : β → Bool
⊢ ∀ (lhs rhs : Nat) (linv rinv : Bool),
    (relabel f aig).decls[start] = Decl.gate lhs rhs linv rinv →
      ⟦{ aig := relabel f aig, ref := { gate := start, hgate := hidx } }, assign⟧ =
        ⟦{ aig := aig, ref := { gate := start, hgate := ⋯ } }, assign ∘ f⟧

State before:
case hatom
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
aig : AIG α
f : α → β
start : Nat
hidx : start < (relabel f aig).decls.size
assign : β → Bool
⊢ ∀ (a : β),
    (relabel f aig).decls[start] = Decl.atom a →
      ⟦{ aig := relabel f aig, ref := { gate := start, hgate := hidx } }, assign⟧ =
        ⟦{ aig := aig, ref := { gate := start, hgate := ⋯ } }, assign ∘ f⟧

case hgate
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
aig : AIG α
f : α → β
start : Nat
hidx : start < (relabel f aig).decls.size
assign : β → Bool
⊢ ∀ (lhs rhs : Nat) (linv rinv : Bool),
    (relabel f aig).decls[start] = Decl.gate lhs rhs linv rinv →
      ⟦{ aig := relabel f aig, ref := { gate := start, hgate := hidx } }, assign⟧ =
        ⟦{ aig := aig, ref := { gate := start, hgate := ⋯ } }, assign ∘ f⟧
Tactic:
. intro a heq1
  rw [denote_idx_atom heq1]
  rcases relabel_atom heq1 with ⟨x, ⟨hlx, hrx⟩⟩
  rw [hrx] at heq1
  rw [denote_idx_atom hlx]
  simp [hrx]
State after:
case hgate
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
aig : AIG α
f : α → β
start : Nat
hidx : start < (relabel f aig).decls.size
assign : β → Bool
⊢ ∀ (lhs rhs : Nat) (linv rinv : Bool),
    (relabel f aig).decls[start] = Decl.gate lhs rhs linv rinv →
      ⟦{ aig := relabel f aig, ref := { gate := start, hgate := hidx } }, assign⟧ =
        ⟦{ aig := aig, ref := { gate := start, hgate := ⋯ } }, assign ∘ f⟧

State before:
case hgate
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
aig : AIG α
f : α → β
start : Nat
hidx : start < (relabel f aig).decls.size
assign : β → Bool
⊢ ∀ (lhs rhs : Nat) (linv rinv : Bool),
    (relabel f aig).decls[start] = Decl.gate lhs rhs linv rinv →
      ⟦{ aig := relabel f aig, ref := { gate := start, hgate := hidx } }, assign⟧ =
        ⟦{ aig := aig, ref := { gate := start, hgate := ⋯ } }, assign ∘ f⟧
Tactic:
. intro lhs rhs linv rinv heq1
  have heq2 := relabel_gate heq1
  rw [denote_idx_gate heq1]
  rw [denote_idx_gate heq2]
  have := aig.inv start lhs rhs linv rinv (by rw [← relabel_size_eq_size (f := f)]; omega) heq2
  rw [denote_relabel aig f lhs assign]
  rw [denote_relabel aig f rhs assign]
State after:
no goals

State before:
case hconst
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
aig : AIG α
f : α → β
start : Nat
hidx : start < (relabel f aig).decls.size
assign : β → Bool
⊢ ∀ (b : Bool),
    (relabel f aig).decls[start] = Decl.const b →
      ⟦{ aig := relabel f aig, ref := { gate := start, hgate := hidx } }, assign⟧ =
        ⟦{ aig := aig, ref := { gate := start, hgate := ⋯ } }, assign ∘ f⟧
Tactic:
intro b heq1
State after:
case hconst
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
aig : AIG α
f : α → β
start : Nat
hidx : start < (relabel f aig).decls.size
assign : β → Bool
b : Bool
heq1 : (relabel f aig).decls[start] = Decl.const b
⊢ ⟦{ aig := relabel f aig, ref := { gate := start, hgate := hidx } }, assign⟧ =
    ⟦{ aig := aig, ref := { gate := start, hgate := ⋯ } }, assign ∘ f⟧

State before:
case hconst
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
aig : AIG α
f : α → β
start : Nat
hidx : start < (relabel f aig).decls.size
assign : β → Bool
b : Bool
heq1 : (relabel f aig).decls[start] = Decl.const b
⊢ ⟦{ aig := relabel f aig, ref := { gate := start, hgate := hidx } }, assign⟧ =
    ⟦{ aig := aig, ref := { gate := start, hgate := ⋯ } }, assign ∘ f⟧
Tactic:
have heq2 := relabel_const heq1
State after:
case hconst
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
aig : AIG α
f : α → β
start : Nat
hidx : start < (relabel f aig).decls.size
assign : β → Bool
b : Bool
heq1 : (relabel f aig).decls[start] = Decl.const b
heq2 : aig.decls[start] = Decl.const b
⊢ ⟦{ aig := relabel f aig, ref := { gate := start, hgate := hidx } }, assign⟧ =
    ⟦{ aig := aig, ref := { gate := start, hgate := ⋯ } }, assign ∘ f⟧

State before:
case hconst
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
aig : AIG α
f : α → β
start : Nat
hidx : start < (relabel f aig).decls.size
assign : β → Bool
b : Bool
heq1 : (relabel f aig).decls[start] = Decl.const b
heq2 : aig.decls[start] = Decl.const b
⊢ ⟦{ aig := relabel f aig, ref := { gate := start, hgate := hidx } }, assign⟧ =
    ⟦{ aig := aig, ref := { gate := start, hgate := ⋯ } }, assign ∘ f⟧
Tactic:
rw [denote_idx_const heq1]
State after:
case hconst
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
aig : AIG α
f : α → β
start : Nat
hidx : start < (relabel f aig).decls.size
assign : β → Bool
b : Bool
heq1 : (relabel f aig).decls[start] = Decl.const b
heq2 : aig.decls[start] = Decl.const b
⊢ b = ⟦{ aig := aig, ref := { gate := start, hgate := ⋯ } }, assign ∘ f⟧

State before:
case hconst
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
aig : AIG α
f : α → β
start : Nat
hidx : start < (relabel f aig).decls.size
assign : β → Bool
b : Bool
heq1 : (relabel f aig).decls[start] = Decl.const b
heq2 : aig.decls[start] = Decl.const b
⊢ b = ⟦{ aig := aig, ref := { gate := start, hgate := ⋯ } }, assign ∘ f⟧
Tactic:
rw [denote_idx_const heq2]
State after:
no goals

State before:
case hatom
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
aig : AIG α
f : α → β
start : Nat
hidx : start < (relabel f aig).decls.size
assign : β → Bool
⊢ ∀ (a : β),
    (relabel f aig).decls[start] = Decl.atom a →
      ⟦{ aig := relabel f aig, ref := { gate := start, hgate := hidx } }, assign⟧ =
        ⟦{ aig := aig, ref := { gate := start, hgate := ⋯ } }, assign ∘ f⟧
Tactic:
intro a heq1
State after:
case hatom
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
aig : AIG α
f : α → β
start : Nat
hidx : start < (relabel f aig).decls.size
assign : β → Bool
a : β
heq1 : (relabel f aig).decls[start] = Decl.atom a
⊢ ⟦{ aig := relabel f aig, ref := { gate := start, hgate := hidx } }, assign⟧ =
    ⟦{ aig := aig, ref := { gate := start, hgate := ⋯ } }, assign ∘ f⟧

State before:
case hatom
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
aig : AIG α
f : α → β
start : Nat
hidx : start < (relabel f aig).decls.size
assign : β → Bool
a : β
heq1 : (relabel f aig).decls[start] = Decl.atom a
⊢ ⟦{ aig := relabel f aig, ref := { gate := start, hgate := hidx } }, assign⟧ =
    ⟦{ aig := aig, ref := { gate := start, hgate := ⋯ } }, assign ∘ f⟧
Tactic:
rw [denote_idx_atom heq1]
State after:
case hatom
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
aig : AIG α
f : α → β
start : Nat
hidx : start < (relabel f aig).decls.size
assign : β → Bool
a : β
heq1 : (relabel f aig).decls[start] = Decl.atom a
⊢ assign a = ⟦{ aig := aig, ref := { gate := start, hgate := ⋯ } }, assign ∘ f⟧

State before:
case hatom
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
aig : AIG α
f : α → β
start : Nat
hidx : start < (relabel f aig).decls.size
assign : β → Bool
a : β
heq1 : (relabel f aig).decls[start] = Decl.atom a
⊢ assign a = ⟦{ aig := aig, ref := { gate := start, hgate := ⋯ } }, assign ∘ f⟧
Tactic:
rcases relabel_atom heq1 with ⟨x, ⟨hlx, hrx⟩⟩
State after:
case hatom.intro.intro
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
aig : AIG α
f : α → β
start : Nat
hidx : start < (relabel f aig).decls.size
assign : β → Bool
a : β
heq1 : (relabel f aig).decls[start] = Decl.atom a
x : α
hlx : aig.decls[start] = Decl.atom x
hrx : a = f x
⊢ assign a = ⟦{ aig := aig, ref := { gate := start, hgate := ⋯ } }, assign ∘ f⟧

State before:
case hatom.intro.intro
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
aig : AIG α
f : α → β
start : Nat
hidx : start < (relabel f aig).decls.size
assign : β → Bool
a : β
heq1 : (relabel f aig).decls[start] = Decl.atom a
x : α
hlx : aig.decls[start] = Decl.atom x
hrx : a = f x
⊢ assign a = ⟦{ aig := aig, ref := { gate := start, hgate := ⋯ } }, assign ∘ f⟧
Tactic:
rw [hrx] at heq1
State after:
case hatom.intro.intro
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
aig : AIG α
f : α → β
start : Nat
hidx : start < (relabel f aig).decls.size
assign : β → Bool
a : β
x : α
heq1 : (relabel f aig).decls[start] = Decl.atom (f x)
hlx : aig.decls[start] = Decl.atom x
hrx : a = f x
⊢ assign a = ⟦{ aig := aig, ref := { gate := start, hgate := ⋯ } }, assign ∘ f⟧

State before:
case hatom.intro.intro
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
aig : AIG α
f : α → β
start : Nat
hidx : start < (relabel f aig).decls.size
assign : β → Bool
a : β
x : α
heq1 : (relabel f aig).decls[start] = Decl.atom (f x)
hlx : aig.decls[start] = Decl.atom x
hrx : a = f x
⊢ assign a = ⟦{ aig := aig, ref := { gate := start, hgate := ⋯ } }, assign ∘ f⟧
Tactic:
rw [denote_idx_atom hlx]
State after:
case hatom.intro.intro
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
aig : AIG α
f : α → β
start : Nat
hidx : start < (relabel f aig).decls.size
assign : β → Bool
a : β
x : α
heq1 : (relabel f aig).decls[start] = Decl.atom (f x)
hlx : aig.decls[start] = Decl.atom x
hrx : a = f x
⊢ assign a = (assign ∘ f) x

State before:
case hatom.intro.intro
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
aig : AIG α
f : α → β
start : Nat
hidx : start < (relabel f aig).decls.size
assign : β → Bool
a : β
x : α
heq1 : (relabel f aig).decls[start] = Decl.atom (f x)
hlx : aig.decls[start] = Decl.atom x
hrx : a = f x
⊢ assign a = (assign ∘ f) x
Tactic:
simp [hrx]
State after:
no goals

State before:
case hgate
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
aig : AIG α
f : α → β
start : Nat
hidx : start < (relabel f aig).decls.size
assign : β → Bool
⊢ ∀ (lhs rhs : Nat) (linv rinv : Bool),
    (relabel f aig).decls[start] = Decl.gate lhs rhs linv rinv →
      ⟦{ aig := relabel f aig, ref := { gate := start, hgate := hidx } }, assign⟧ =
        ⟦{ aig := aig, ref := { gate := start, hgate := ⋯ } }, assign ∘ f⟧
Tactic:
intro lhs rhs linv rinv heq1
State after:
case hgate
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
aig : AIG α
f : α → β
start : Nat
hidx : start < (relabel f aig).decls.size
assign : β → Bool
lhs rhs : Nat
linv rinv : Bool
heq1 : (relabel f aig).decls[start] = Decl.gate lhs rhs linv rinv
⊢ ⟦{ aig := relabel f aig, ref := { gate := start, hgate := hidx } }, assign⟧ =
    ⟦{ aig := aig, ref := { gate := start, hgate := ⋯ } }, assign ∘ f⟧

State before:
case hgate
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
aig : AIG α
f : α → β
start : Nat
hidx : start < (relabel f aig).decls.size
assign : β → Bool
lhs rhs : Nat
linv rinv : Bool
heq1 : (relabel f aig).decls[start] = Decl.gate lhs rhs linv rinv
⊢ ⟦{ aig := relabel f aig, ref := { gate := start, hgate := hidx } }, assign⟧ =
    ⟦{ aig := aig, ref := { gate := start, hgate := ⋯ } }, assign ∘ f⟧
Tactic:
have heq2 := relabel_gate heq1
State after:
case hgate
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
aig : AIG α
f : α → β
start : Nat
hidx : start < (relabel f aig).decls.size
assign : β → Bool
lhs rhs : Nat
linv rinv : Bool
heq1 : (relabel f aig).decls[start] = Decl.gate lhs rhs linv rinv
heq2 : aig.decls[start] = Decl.gate lhs rhs linv rinv
⊢ ⟦{ aig := relabel f aig, ref := { gate := start, hgate := hidx } }, assign⟧ =
    ⟦{ aig := aig, ref := { gate := start, hgate := ⋯ } }, assign ∘ f⟧

State before:
case hgate
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
aig : AIG α
f : α → β
start : Nat
hidx : start < (relabel f aig).decls.size
assign : β → Bool
lhs rhs : Nat
linv rinv : Bool
heq1 : (relabel f aig).decls[start] = Decl.gate lhs rhs linv rinv
heq2 : aig.decls[start] = Decl.gate lhs rhs linv rinv
⊢ ⟦{ aig := relabel f aig, ref := { gate := start, hgate := hidx } }, assign⟧ =
    ⟦{ aig := aig, ref := { gate := start, hgate := ⋯ } }, assign ∘ f⟧
Tactic:
rw [denote_idx_gate heq1]
State after:
case hgate
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
aig : AIG α
f : α → β
start : Nat
hidx : start < (relabel f aig).decls.size
assign : β → Bool
lhs rhs : Nat
linv rinv : Bool
heq1 : (relabel f aig).decls[start] = Decl.gate lhs rhs linv rinv
heq2 : aig.decls[start] = Decl.gate lhs rhs linv rinv
⊢ (xor ⟦{ aig := relabel f aig, ref := { gate := lhs, hgate := ⋯ } }, assign⟧ linv &&
      xor ⟦{ aig := relabel f aig, ref := { gate := rhs, hgate := ⋯ } }, assign⟧ rinv) =
    ⟦{ aig := aig, ref := { gate := start, hgate := ⋯ } }, assign ∘ f⟧

State before:
case hgate
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
aig : AIG α
f : α → β
start : Nat
hidx : start < (relabel f aig).decls.size
assign : β → Bool
lhs rhs : Nat
linv rinv : Bool
heq1 : (relabel f aig).decls[start] = Decl.gate lhs rhs linv rinv
heq2 : aig.decls[start] = Decl.gate lhs rhs linv rinv
⊢ (xor ⟦{ aig := relabel f aig, ref := { gate := lhs, hgate := ⋯ } }, assign⟧ linv &&
      xor ⟦{ aig := relabel f aig, ref := { gate := rhs, hgate := ⋯ } }, assign⟧ rinv) =
    ⟦{ aig := aig, ref := { gate := start, hgate := ⋯ } }, assign ∘ f⟧
Tactic:
rw [denote_idx_gate heq2]
State after:
case hgate
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
aig : AIG α
f : α → β
start : Nat
hidx : start < (relabel f aig).decls.size
assign : β → Bool
lhs rhs : Nat
linv rinv : Bool
heq1 : (relabel f aig).decls[start] = Decl.gate lhs rhs linv rinv
heq2 : aig.decls[start] = Decl.gate lhs rhs linv rinv
⊢ (xor ⟦{ aig := relabel f aig, ref := { gate := lhs, hgate := ⋯ } }, assign⟧ linv &&
      xor ⟦{ aig := relabel f aig, ref := { gate := rhs, hgate := ⋯ } }, assign⟧ rinv) =
    (xor ⟦{ aig := aig, ref := { gate := lhs, hgate := ⋯ } }, assign ∘ f⟧ linv &&
      xor ⟦{ aig := aig, ref := { gate := rhs, hgate := ⋯ } }, assign ∘ f⟧ rinv)

State before:
case hgate
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
aig : AIG α
f : α → β
start : Nat
hidx : start < (relabel f aig).decls.size
assign : β → Bool
lhs rhs : Nat
linv rinv : Bool
heq1 : (relabel f aig).decls[start] = Decl.gate lhs rhs linv rinv
heq2 : aig.decls[start] = Decl.gate lhs rhs linv rinv
⊢ (xor ⟦{ aig := relabel f aig, ref := { gate := lhs, hgate := ⋯ } }, assign⟧ linv &&
      xor ⟦{ aig := relabel f aig, ref := { gate := rhs, hgate := ⋯ } }, assign⟧ rinv) =
    (xor ⟦{ aig := aig, ref := { gate := lhs, hgate := ⋯ } }, assign ∘ f⟧ linv &&
      xor ⟦{ aig := aig, ref := { gate := rhs, hgate := ⋯ } }, assign ∘ f⟧ rinv)
Tactic:
have := aig.inv start lhs rhs linv rinv (by rw [← relabel_size_eq_size (f := f)]; omega) heq2
State after:
case hgate
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
aig : AIG α
f : α → β
start : Nat
hidx : start < (relabel f aig).decls.size
assign : β → Bool
lhs rhs : Nat
linv rinv : Bool
heq1 : (relabel f aig).decls[start] = Decl.gate lhs rhs linv rinv
heq2 : aig.decls[start] = Decl.gate lhs rhs linv rinv
this : lhs < start ∧ rhs < start
⊢ (xor ⟦{ aig := relabel f aig, ref := { gate := lhs, hgate := ⋯ } }, assign⟧ linv &&
      xor ⟦{ aig := relabel f aig, ref := { gate := rhs, hgate := ⋯ } }, assign⟧ rinv) =
    (xor ⟦{ aig := aig, ref := { gate := lhs, hgate := ⋯ } }, assign ∘ f⟧ linv &&
      xor ⟦{ aig := aig, ref := { gate := rhs, hgate := ⋯ } }, assign ∘ f⟧ rinv)

State before:
case hgate
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
aig : AIG α
f : α → β
start : Nat
hidx : start < (relabel f aig).decls.size
assign : β → Bool
lhs rhs : Nat
linv rinv : Bool
heq1 : (relabel f aig).decls[start] = Decl.gate lhs rhs linv rinv
heq2 : aig.decls[start] = Decl.gate lhs rhs linv rinv
this : lhs < start ∧ rhs < start
⊢ (xor ⟦{ aig := relabel f aig, ref := { gate := lhs, hgate := ⋯ } }, assign⟧ linv &&
      xor ⟦{ aig := relabel f aig, ref := { gate := rhs, hgate := ⋯ } }, assign⟧ rinv) =
    (xor ⟦{ aig := aig, ref := { gate := lhs, hgate := ⋯ } }, assign ∘ f⟧ linv &&
      xor ⟦{ aig := aig, ref := { gate := rhs, hgate := ⋯ } }, assign ∘ f⟧ rinv)
Tactic:
rw [denote_relabel aig f lhs assign]
State after:
case hgate
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
aig : AIG α
f : α → β
start : Nat
hidx : start < (relabel f aig).decls.size
assign : β → Bool
lhs rhs : Nat
linv rinv : Bool
heq1 : (relabel f aig).decls[start] = Decl.gate lhs rhs linv rinv
heq2 : aig.decls[start] = Decl.gate lhs rhs linv rinv
this : lhs < start ∧ rhs < start
⊢ (xor ⟦{ aig := aig, ref := { gate := lhs, hgate := ⋯ } }, assign ∘ f⟧ linv &&
      xor ⟦{ aig := relabel f aig, ref := { gate := rhs, hgate := ⋯ } }, assign⟧ rinv) =
    (xor ⟦{ aig := aig, ref := { gate := lhs, hgate := ⋯ } }, assign ∘ f⟧ linv &&
      xor ⟦{ aig := aig, ref := { gate := rhs, hgate := ⋯ } }, assign ∘ f⟧ rinv)

State before:
case hgate
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
aig : AIG α
f : α → β
start : Nat
hidx : start < (relabel f aig).decls.size
assign : β → Bool
lhs rhs : Nat
linv rinv : Bool
heq1 : (relabel f aig).decls[start] = Decl.gate lhs rhs linv rinv
heq2 : aig.decls[start] = Decl.gate lhs rhs linv rinv
this : lhs < start ∧ rhs < start
⊢ (xor ⟦{ aig := aig, ref := { gate := lhs, hgate := ⋯ } }, assign ∘ f⟧ linv &&
      xor ⟦{ aig := relabel f aig, ref := { gate := rhs, hgate := ⋯ } }, assign⟧ rinv) =
    (xor ⟦{ aig := aig, ref := { gate := lhs, hgate := ⋯ } }, assign ∘ f⟧ linv &&
      xor ⟦{ aig := aig, ref := { gate := rhs, hgate := ⋯ } }, assign ∘ f⟧ rinv)
Tactic:
rw [denote_relabel aig f rhs assign]
State after:
no goals

State before:
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
aig : AIG α
f : α → β
start : Nat
hidx : start < (relabel f aig).decls.size
assign : β → Bool
lhs rhs : Nat
linv rinv : Bool
heq1 : (relabel f aig).decls[start] = Decl.gate lhs rhs linv rinv
heq2 : aig.decls[start] = Decl.gate lhs rhs linv rinv
⊢ start < aig.decls.size
Tactic:
rw [← relabel_size_eq_size (f := f)]
State after:
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
aig : AIG α
f : α → β
start : Nat
hidx : start < (relabel f aig).decls.size
assign : β → Bool
lhs rhs : Nat
linv rinv : Bool
heq1 : (relabel f aig).decls[start] = Decl.gate lhs rhs linv rinv
heq2 : aig.decls[start] = Decl.gate lhs rhs linv rinv
⊢ start < (relabel f aig).decls.size

State before:
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
aig : AIG α
f : α → β
start : Nat
hidx : start < (relabel f aig).decls.size
assign : β → Bool
lhs rhs : Nat
linv rinv : Bool
heq1 : (relabel f aig).decls[start] = Decl.gate lhs rhs linv rinv
heq2 : aig.decls[start] = Decl.gate lhs rhs linv rinv
⊢ start < (relabel f aig).decls.size
Tactic:
omega
State after:
no goals