internlm/Lean-Github huggingface dataset:
Theorem: Decl.relabel_atom
Proof 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
Proof 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
Theorem: Decl.relabel_atom
Proof 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
Proof 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
Theorem: Decl.relabel_atom
Proof 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]
Proof 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
Theorem: Decl.relabel_atom
Proof 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
Proof state after:
no goals
Theorem: Decl.relabel_atom
Proof 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
Proof state after:
no goals
Theorem: Decl.relabel_atom
Proof 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]
Proof state after:
no goals
Theorem: Decl.relabel_atom
Proof 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
Proof 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
Theorem: Decl.relabel_atom
Proof 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
Proof 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
Theorem: Decl.relabel_atom
Proof 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]
Proof state after:
no goals
Theorem: Decl.relabel_atom
Proof 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
Proof state after:
no goals
Theorem: Decl.relabel_gate
Proof state before:
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx lhs rhs : Nat
linv rinv : Bool
decls : Array (Decl α)
f : α → β
hidx : idx < decls.size
h : relabel f decls[idx] = gate lhs rhs linv rinv
⊢ decls[idx] = gate lhs rhs linv rinv
Tactic:
unfold relabel at h
Proof state after:
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx lhs rhs : Nat
linv rinv : Bool
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) =
    gate lhs rhs linv rinv
⊢ decls[idx] = gate lhs rhs linv rinv
Theorem: Decl.relabel_gate
Proof state before:
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx lhs rhs : Nat
linv rinv : Bool
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) =
    gate lhs rhs linv rinv
⊢ decls[idx] = gate lhs rhs linv rinv
Tactic:
split at h <;> simp_all
Proof state after:
no goals
Theorem: AIG.relabel_size_eq_size
Proof state before:
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
aig : AIG α
f : α → β
⊢ (relabel f aig).decls.size = aig.decls.size
Tactic:
simp [relabel]
Proof state after:
no goals
Theorem: AIG.relabel_const
Proof state before:
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
b : Bool
aig : AIG α
f : α → β
hidx : idx < (relabel f aig).decls.size
h : (relabel f aig).decls[idx] = Decl.const b
⊢ idx < aig.decls.size
Tactic:
rw [← relabel_size_eq_size (f := f)]
Proof state after:
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
b : Bool
aig : AIG α
f : α → β
hidx : idx < (relabel f aig).decls.size
h : (relabel f aig).decls[idx] = Decl.const b
⊢ idx < (relabel f aig).decls.size
Theorem: AIG.relabel_const
Proof state before:
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
b : Bool
aig : AIG α
f : α → β
hidx : idx < (relabel f aig).decls.size
h : (relabel f aig).decls[idx] = Decl.const b
⊢ idx < (relabel f aig).decls.size
Tactic:
omega
Proof state after:
no goals
Theorem: AIG.relabel_const
Proof state before:
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
b : Bool
aig : AIG α
f : α → β
hidx : idx < (relabel f aig).decls.size
h : (relabel f aig).decls[idx] = Decl.const b
⊢ aig.decls[idx] = Decl.const b
Tactic:
apply Decl.relabel_const
Proof state after:
case h
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
b : Bool
aig : AIG α
f : α → β
hidx : idx < (relabel f aig).decls.size
h : (relabel f aig).decls[idx] = Decl.const b
⊢ Decl.relabel ?f aig.decls[idx] = Decl.const b

case β
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
b : Bool
aig : AIG α
f : α → β
hidx : idx < (relabel f aig).decls.size
h : (relabel f aig).decls[idx] = Decl.const b
⊢ Type

case f
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
b : Bool
aig : AIG α
f : α → β
hidx : idx < (relabel f aig).decls.size
h : (relabel f aig).decls[idx] = Decl.const b
⊢ α → ?β
Theorem: AIG.relabel_const
Proof state before:
case h
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
b : Bool
aig : AIG α
f : α → β
hidx : idx < (relabel f aig).decls.size
h : (relabel f aig).decls[idx] = Decl.const b
⊢ Decl.relabel ?f aig.decls[idx] = Decl.const b

case β
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
b : Bool
aig : AIG α
f : α → β
hidx : idx < (relabel f aig).decls.size
h : (relabel f aig).decls[idx] = Decl.const b
⊢ Type

case f
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
b : Bool
aig : AIG α
f : α → β
hidx : idx < (relabel f aig).decls.size
h : (relabel f aig).decls[idx] = Decl.const b
⊢ α → ?β
Tactic:
simpa [relabel] using h
Proof state after:
no goals
Theorem: AIG.relabel_atom
Proof state before:
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
a : β
aig : AIG α
f : α → β
hidx : idx < (relabel f aig).decls.size
h : (relabel f aig).decls[idx] = Decl.atom a
x : α
⊢ idx < aig.decls.size
Tactic:
rw [← relabel_size_eq_size (f := f)]
Proof state after:
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
a : β
aig : AIG α
f : α → β
hidx : idx < (relabel f aig).decls.size
h : (relabel f aig).decls[idx] = Decl.atom a
x : α
⊢ idx < (relabel f aig).decls.size
Theorem: AIG.relabel_atom
Proof state before:
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
a : β
aig : AIG α
f : α → β
hidx : idx < (relabel f aig).decls.size
h : (relabel f aig).decls[idx] = Decl.atom a
x : α
⊢ idx < (relabel f aig).decls.size
Tactic:
omega
Proof state after:
no goals
Theorem: AIG.relabel_atom
Proof state before:
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
a : β
aig : AIG α
f : α → β
hidx : idx < (relabel f aig).decls.size
h : (relabel f aig).decls[idx] = Decl.atom a
⊢ ∃ x, aig.decls[idx] = Decl.atom x ∧ a = f x
Tactic:
apply Decl.relabel_atom
Proof state after:
case h
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
a : β
aig : AIG α
f : α → β
hidx : idx < (relabel f aig).decls.size
h : (relabel f aig).decls[idx] = Decl.atom a
⊢ Decl.relabel (fun x => f x) aig.decls[idx] = Decl.atom a
Theorem: AIG.relabel_atom
Proof state before:
case h
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
a : β
aig : AIG α
f : α → β
hidx : idx < (relabel f aig).decls.size
h : (relabel f aig).decls[idx] = Decl.atom a
⊢ Decl.relabel (fun x => f x) aig.decls[idx] = Decl.atom a
Tactic:
simpa [relabel] using h
Proof state after:
no goals
Theorem: AIG.relabel_gate
Proof state before:
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx lhs rhs : Nat
linv rinv : Bool
aig : AIG α
f : α → β
hidx : idx < (relabel f aig).decls.size
h : (relabel f aig).decls[idx] = Decl.gate lhs rhs linv rinv
⊢ idx < aig.decls.size
Tactic:
rw [← relabel_size_eq_size (f := f)]
Proof state after:
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx lhs rhs : Nat
linv rinv : Bool
aig : AIG α
f : α → β
hidx : idx < (relabel f aig).decls.size
h : (relabel f aig).decls[idx] = Decl.gate lhs rhs linv rinv
⊢ idx < (relabel f aig).decls.size
Theorem: AIG.relabel_gate
Proof state before:
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx lhs rhs : Nat
linv rinv : Bool
aig : AIG α
f : α → β
hidx : idx < (relabel f aig).decls.size
h : (relabel f aig).decls[idx] = Decl.gate lhs rhs linv rinv
⊢ idx < (relabel f aig).decls.size
Tactic:
omega
Proof state after:
no goals
Theorem: AIG.relabel_gate
Proof state before:
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx lhs rhs : Nat
linv rinv : Bool
aig : AIG α
f : α → β
hidx : idx < (relabel f aig).decls.size
h : (relabel f aig).decls[idx] = Decl.gate lhs rhs linv rinv
⊢ aig.decls[idx] = Decl.gate lhs rhs linv rinv
Tactic:
apply Decl.relabel_gate
Proof state after:
case h
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx lhs rhs : Nat
linv rinv : Bool
aig : AIG α
f : α → β
hidx : idx < (relabel f aig).decls.size
h : (relabel f aig).decls[idx] = Decl.gate lhs rhs linv rinv
⊢ Decl.relabel ?f aig.decls[idx] = Decl.gate lhs rhs linv rinv

case β
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx lhs rhs : Nat
linv rinv : Bool
aig : AIG α
f : α → β
hidx : idx < (relabel f aig).decls.size
h : (relabel f aig).decls[idx] = Decl.gate lhs rhs linv rinv
⊢ Type

case f
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx lhs rhs : Nat
linv rinv : Bool
aig : AIG α
f : α → β
hidx : idx < (relabel f aig).decls.size
h : (relabel f aig).decls[idx] = Decl.gate lhs rhs linv rinv
⊢ α → ?β
Theorem: AIG.relabel_gate
Proof state before:
case h
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx lhs rhs : Nat
linv rinv : Bool
aig : AIG α
f : α → β
hidx : idx < (relabel f aig).decls.size
h : (relabel f aig).decls[idx] = Decl.gate lhs rhs linv rinv
⊢ Decl.relabel ?f aig.decls[idx] = Decl.gate lhs rhs linv rinv

case β
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx lhs rhs : Nat
linv rinv : Bool
aig : AIG α
f : α → β
hidx : idx < (relabel f aig).decls.size
h : (relabel f aig).decls[idx] = Decl.gate lhs rhs linv rinv
⊢ Type

case f
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx lhs rhs : Nat
linv rinv : Bool
aig : AIG α
f : α → β
hidx : idx < (relabel f aig).decls.size
h : (relabel f aig).decls[idx] = Decl.gate lhs rhs linv rinv
⊢ α → ?β
Tactic:
simpa [relabel] using h
Proof state after:
no goals
Theorem: AIG.denote_relabel
Proof 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)]
Proof 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
Theorem: AIG.denote_relabel
Proof 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
Proof state after:
no goals
Theorem: AIG.denote_relabel
Proof 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
Proof 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⟧