Theorem: Decl.relabel_atom (LeanSAT/AIG/Relabel.lean)

State before:
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
a : β
decls : Array (Decl α)
f : α → β
hidx : idx < decls.size
h : relabel f decls[idx] = atom a
⊢ ∃ x, decls[idx] = atom x ∧ a = f x
Tactic:
unfold relabel at h
State after:
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
a : β
decls : Array (Decl α)
f : α → β
hidx : idx < decls.size
h :
  (match decls[idx] with
    | const b => const b
    | atom a => atom (f a)
    | gate lhs rhs linv rinv => gate lhs rhs linv rinv) =
    atom a
⊢ ∃ x, decls[idx] = atom x ∧ a = f x

State before:
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
a : β
decls : Array (Decl α)
f : α → β
hidx : idx < decls.size
h :
  (match decls[idx] with
    | const b => const b
    | atom a => atom (f a)
    | gate lhs rhs linv rinv => gate lhs rhs linv rinv) =
    atom a
⊢ ∃ x, decls[idx] = atom x ∧ a = f x
Tactic:
split at h
State after:
case h_1
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
a : β
decls : Array (Decl α)
f : α → β
hidx : idx < decls.size
decl✝ : Decl α
b✝ : Bool
heq✝ : decls[idx] = const b✝
h : const b✝ = atom a
⊢ ∃ x, decls[idx] = atom x ∧ a = f x

case h_2
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
a : β
decls : Array (Decl α)
f : α → β
hidx : idx < decls.size
decl✝ : Decl α
a✝ : α
heq✝ : decls[idx] = atom a✝
h : atom (f a✝) = atom a
⊢ ∃ x, decls[idx] = atom x ∧ a = f x

case h_3
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
a : β
decls : Array (Decl α)
f : α → β
hidx : idx < decls.size
decl✝ : Decl α
lhs✝ rhs✝ : Nat
linv✝ rinv✝ : Bool
heq✝ : decls[idx] = gate lhs✝ rhs✝ linv✝ rinv✝
h : gate lhs✝ rhs✝ linv✝ rinv✝ = atom a
⊢ ∃ x, decls[idx] = atom x ∧ a = f x

State before:
case h_1
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
a : β
decls : Array (Decl α)
f : α → β
hidx : idx < decls.size
decl✝ : Decl α
b✝ : Bool
heq✝ : decls[idx] = const b✝
h : const b✝ = atom a
⊢ ∃ x, decls[idx] = atom x ∧ a = f x

case h_2
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
a : β
decls : Array (Decl α)
f : α → β
hidx : idx < decls.size
decl✝ : Decl α
a✝ : α
heq✝ : decls[idx] = atom a✝
h : atom (f a✝) = atom a
⊢ ∃ x, decls[idx] = atom x ∧ a = f x

case h_3
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
a : β
decls : Array (Decl α)
f : α → β
hidx : idx < decls.size
decl✝ : Decl α
lhs✝ rhs✝ : Nat
linv✝ rinv✝ : Bool
heq✝ : decls[idx] = gate lhs✝ rhs✝ linv✝ rinv✝
h : gate lhs✝ rhs✝ linv✝ rinv✝ = atom a
⊢ ∃ x, decls[idx] = atom x ∧ a = f x
Tactic:
. contradiction
State after:
case h_2
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
a : β
decls : Array (Decl α)
f : α → β
hidx : idx < decls.size
decl✝ : Decl α
a✝ : α
heq✝ : decls[idx] = atom a✝
h : atom (f a✝) = atom a
⊢ ∃ x, decls[idx] = atom x ∧ a = f x

case h_3
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
a : β
decls : Array (Decl α)
f : α → β
hidx : idx < decls.size
decl✝ : Decl α
lhs✝ rhs✝ : Nat
linv✝ rinv✝ : Bool
heq✝ : decls[idx] = gate lhs✝ rhs✝ linv✝ rinv✝
h : gate lhs✝ rhs✝ linv✝ rinv✝ = atom a
⊢ ∃ x, decls[idx] = atom x ∧ a = f x

State before:
case h_2
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
a : β
decls : Array (Decl α)
f : α → β
hidx : idx < decls.size
decl✝ : Decl α
a✝ : α
heq✝ : decls[idx] = atom a✝
h : atom (f a✝) = atom a
⊢ ∃ x, decls[idx] = atom x ∧ a = f x

case h_3
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
a : β
decls : Array (Decl α)
f : α → β
hidx : idx < decls.size
decl✝ : Decl α
lhs✝ rhs✝ : Nat
linv✝ rinv✝ : Bool
heq✝ : decls[idx] = gate lhs✝ rhs✝ linv✝ rinv✝
h : gate lhs✝ rhs✝ linv✝ rinv✝ = atom a
⊢ ∃ x, decls[idx] = atom x ∧ a = f x
Tactic:
. next x heq =>
  injection h with h
  exists x
  simp [heq, h]
State after:
case h_3
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
a : β
decls : Array (Decl α)
f : α → β
hidx : idx < decls.size
decl✝ : Decl α
lhs✝ rhs✝ : Nat
linv✝ rinv✝ : Bool
heq✝ : decls[idx] = gate lhs✝ rhs✝ linv✝ rinv✝
h : gate lhs✝ rhs✝ linv✝ rinv✝ = atom a
⊢ ∃ x, decls[idx] = atom x ∧ a = f x

State before:
case h_3
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
a : β
decls : Array (Decl α)
f : α → β
hidx : idx < decls.size
decl✝ : Decl α
lhs✝ rhs✝ : Nat
linv✝ rinv✝ : Bool
heq✝ : decls[idx] = gate lhs✝ rhs✝ linv✝ rinv✝
h : gate lhs✝ rhs✝ linv✝ rinv✝ = atom a
⊢ ∃ x, decls[idx] = atom x ∧ a = f x
Tactic:
. contradiction
State after:
no goals

State before:
case h_1
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
a : β
decls : Array (Decl α)
f : α → β
hidx : idx < decls.size
decl✝ : Decl α
b✝ : Bool
heq✝ : decls[idx] = const b✝
h : const b✝ = atom a
⊢ ∃ x, decls[idx] = atom x ∧ a = f x
Tactic:
contradiction
State after:
no goals

State before:
case h_2
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
a : β
decls : Array (Decl α)
f : α → β
hidx : idx < decls.size
decl✝ : Decl α
a✝ : α
heq✝ : decls[idx] = atom a✝
h : atom (f a✝) = atom a
⊢ ∃ x, decls[idx] = atom x ∧ a = f x
Tactic:
next x heq =>
injection h with h
exists x
simp [heq, h]
State after:
no goals

State before:
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
a : β
decls : Array (Decl α)
f : α → β
hidx : idx < decls.size
decl✝ : Decl α
x : α
heq : decls[idx] = atom x
h : atom (f x) = atom a
⊢ ∃ x, decls[idx] = atom x ∧ a = f x
Tactic:
injection h with h
State after:
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
a : β
decls : Array (Decl α)
f : α → β
hidx : idx < decls.size
decl✝ : Decl α
x : α
heq : decls[idx] = atom x
h : f x = a
⊢ ∃ x, decls[idx] = atom x ∧ a = f x

State before:
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
a : β
decls : Array (Decl α)
f : α → β
hidx : idx < decls.size
decl✝ : Decl α
x : α
heq : decls[idx] = atom x
h : f x = a
⊢ ∃ x, decls[idx] = atom x ∧ a = f x
Tactic:
exists x
State after:
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
a : β
decls : Array (Decl α)
f : α → β
hidx : idx < decls.size
decl✝ : Decl α
x : α
heq : decls[idx] = atom x
h : f x = a
⊢ decls[idx] = atom x ∧ a = f x

State before:
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
a : β
decls : Array (Decl α)
f : α → β
hidx : idx < decls.size
decl✝ : Decl α
x : α
heq : decls[idx] = atom x
h : f x = a
⊢ decls[idx] = atom x ∧ a = f x
Tactic:
simp [heq, h]
State after:
no goals

State before:
case h_3
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
a : β
decls : Array (Decl α)
f : α → β
hidx : idx < decls.size
decl✝ : Decl α
lhs✝ rhs✝ : Nat
linv✝ rinv✝ : Bool
heq✝ : decls[idx] = gate lhs✝ rhs✝ linv✝ rinv✝
h : gate lhs✝ rhs✝ linv✝ rinv✝ = atom a
⊢ ∃ x, decls[idx] = atom x ∧ a = f x
Tactic:
contradiction
State after:
no goals