internlm/Lean-Github huggingface dataset:
Theorem: CNF.relabel_congr
Proof state before:
α β : Type
x : CNF α
f g : α → β
w : ∀ (a : α), mem a x → f a = g a
⊢ ∀ (x_1 : Clause α), x_1 ∈ x → Clause.relabel f x_1 = Clause.relabel g x_1
Tactic:
intro c h
Proof state after:
α β : Type
x : CNF α
f g : α → β
w : ∀ (a : α), mem a x → f a = g a
c : Clause α
h : c ∈ x
⊢ Clause.relabel f c = Clause.relabel g c
Theorem: CNF.relabel_congr
Proof state before:
α β : Type
x : CNF α
f g : α → β
w : ∀ (a : α), mem a x → f a = g a
c : Clause α
h : c ∈ x
⊢ Clause.relabel f c = Clause.relabel g c
Tactic:
apply Clause.relabel_congr
Proof state after:
case w
α β : Type
x : CNF α
f g : α → β
w : ∀ (a : α), mem a x → f a = g a
c : Clause α
h : c ∈ x
⊢ ∀ (a : α), Clause.mem a c → f a = g a
Theorem: CNF.relabel_congr
Proof state before:
case w
α β : Type
x : CNF α
f g : α → β
w : ∀ (a : α), mem a x → f a = g a
c : Clause α
h : c ∈ x
⊢ ∀ (a : α), Clause.mem a c → f a = g a
Tactic:
intro a m
Proof state after:
case w
α β : Type
x : CNF α
f g : α → β
w : ∀ (a : α), mem a x → f a = g a
c : Clause α
h : c ∈ x
a : α
m : Clause.mem a c
⊢ f a = g a
Theorem: CNF.relabel_congr
Proof state before:
case w
α β : Type
x : CNF α
f g : α → β
w : ∀ (a : α), mem a x → f a = g a
c : Clause α
h : c ∈ x
a : α
m : Clause.mem a c
⊢ f a = g a
Tactic:
exact w _ (mem_of h m)
Proof state after:
no goals
Theorem: CNF.sat_relabel
Proof state before:
α✝ : Type
x : CNF α✝
β✝ : Type
g : β✝ → Bool
f : α✝ → β✝
h : x.sat (g ∘ f)
⊢ (relabel f x).sat g
Tactic:
simp_all [sat]
Proof state after:
no goals
Theorem: CNF.unsat_relabel
Proof state before:
α β : Type
x : CNF α
f : α → β
h : x.unsat
⊢ (relabel f x).unsat
Tactic:
simp_all [unsat]
Proof state after:
no goals
Theorem: CNF.nonempty_or_impossible
Proof state before:
α : Type
x : CNF α
⊢ Nonempty α ∨ ∃ n, x = List.replicate n []
Tactic:
induction x with
| nil => exact Or.inr ⟨0, rfl⟩
| cons c x ih => match c with
  | [] => cases ih with
    | inl h => left; exact h
    | inr h =>
      obtain ⟨n, rfl⟩ := h
      right
      exact ⟨n + 1, rfl⟩
  | ⟨a, b⟩ :: c => exact Or.inl ⟨a⟩
Proof state after:
no goals
Theorem: CNF.nonempty_or_impossible
Proof state before:
case nil
α : Type
⊢ Nonempty α ∨ ∃ n, [] = List.replicate n []
Tactic:
exact Or.inr ⟨0, rfl⟩
Proof state after:
no goals
Theorem: CNF.nonempty_or_impossible
Proof state before:
case cons
α : Type
c : Clause α
x : List (Clause α)
ih : Nonempty α ∨ ∃ n, x = List.replicate n []
⊢ Nonempty α ∨ ∃ n, c :: x = List.replicate n []
Tactic:
match c with
| [] => cases ih with
| inl h => left; exact h
| inr h =>
obtain ⟨n, rfl⟩ := h
right
exact ⟨n + 1, rfl⟩
| ⟨a, b⟩ :: c => exact Or.inl ⟨a⟩
Proof state after:
no goals
Theorem: CNF.nonempty_or_impossible
Proof state before:
α : Type
c : Clause α
x : List (Clause α)
ih : Nonempty α ∨ ∃ n, x = List.replicate n []
⊢ Nonempty α ∨ ∃ n, [] :: x = List.replicate n []
Tactic:
cases ih with
| inl h => left; exact h
| inr h =>
obtain ⟨n, rfl⟩ := h
right
exact ⟨n + 1, rfl⟩
Proof state after:
no goals
Theorem: CNF.nonempty_or_impossible
Proof state before:
case inl
α : Type
c : Clause α
x : List (Clause α)
h : Nonempty α
⊢ Nonempty α ∨ ∃ n, [] :: x = List.replicate n []
Tactic:
left
Proof state after:
case inl.h
α : Type
c : Clause α
x : List (Clause α)
h : Nonempty α
⊢ Nonempty α
Theorem: CNF.nonempty_or_impossible
Proof state before:
case inl.h
α : Type
c : Clause α
x : List (Clause α)
h : Nonempty α
⊢ Nonempty α
Tactic:
exact h
Proof state after:
no goals
Theorem: CNF.nonempty_or_impossible
Proof state before:
case inr
α : Type
c : Clause α
x : List (Clause α)
h : ∃ n, x = List.replicate n []
⊢ Nonempty α ∨ ∃ n, [] :: x = List.replicate n []
Tactic:
obtain ⟨n, rfl⟩ := h
Proof state after:
case inr.intro
α : Type
c : Clause α
n : Nat
⊢ Nonempty α ∨ ∃ n_1, [] :: List.replicate n [] = List.replicate n_1 []
Theorem: CNF.nonempty_or_impossible
Proof state before:
case inr.intro
α : Type
c : Clause α
n : Nat
⊢ Nonempty α ∨ ∃ n_1, [] :: List.replicate n [] = List.replicate n_1 []
Tactic:
right
Proof state after:
case inr.intro.h
α : Type
c : Clause α
n : Nat
⊢ ∃ n_1, [] :: List.replicate n [] = List.replicate n_1 []
Theorem: CNF.nonempty_or_impossible
Proof state before:
case inr.intro.h
α : Type
c : Clause α
n : Nat
⊢ ∃ n_1, [] :: List.replicate n [] = List.replicate n_1 []
Tactic:
exact ⟨n + 1, rfl⟩
Proof state after:
no goals
Theorem: CNF.nonempty_or_impossible
Proof state before:
α : Type
c✝ : Clause α
x : List (Clause α)
ih : Nonempty α ∨ ∃ n, x = List.replicate n []
a : α
b : Bool
c : List (α × Bool)
⊢ Nonempty α ∨ ∃ n, ((a, b) :: c) :: x = List.replicate n []
Tactic:
exact Or.inl ⟨a⟩
Proof state after:
no goals
Theorem: CNF.unsat_relabel_iff
Proof state before:
α β : Type
x : CNF α
f : α → β
w : ∀ {a b : α}, mem a x → mem b x → f a = f b → a = b
⊢ (relabel f x).unsat ↔ x.unsat
Tactic:
rcases nonempty_or_impossible x with (⟨⟨a₀⟩⟩ | ⟨n, rfl⟩)
Proof state after:
case inl.intro
α β : Type
x : CNF α
f : α → β
w : ∀ {a b : α}, mem a x → mem b x → f a = f b → a = b
a₀ : α
⊢ (relabel f x).unsat ↔ x.unsat

case inr.intro
α β : Type
f : α → β
n : Nat
w : ∀ {a b : α}, mem a (List.replicate n []) → mem b (List.replicate n []) → f a = f b → a = b
⊢ (relabel f (List.replicate n [])).unsat ↔ unsat (List.replicate n [])
Theorem: CNF.unsat_relabel_iff
Proof state before:
case inl.intro
α β : Type
x : CNF α
f : α → β
w : ∀ {a b : α}, mem a x → mem b x → f a = f b → a = b
a₀ : α
⊢ (relabel f x).unsat ↔ x.unsat
Tactic:
refine ⟨fun h => ?_, unsat_relabel f⟩
Proof state after:
case inl.intro
α β : Type
x : CNF α
f : α → β
w : ∀ {a b : α}, mem a x → mem b x → f a = f b → a = b
a₀ : α
h : (relabel f x).unsat
⊢ x.unsat
Theorem: CNF.unsat_relabel_iff
Proof state before:
case inl.intro
α β : Type
x : CNF α
f : α → β
w : ∀ {a b : α}, mem a x → mem b x → f a = f b → a = b
a₀ : α
h : (relabel f x).unsat
⊢ x.unsat
Tactic:
have em := Classical.propDecidable
Proof state after:
case inl.intro
α β : Type
x : CNF α
f : α → β
w : ∀ {a b : α}, mem a x → mem b x → f a = f b → a = b
a₀ : α
h : (relabel f x).unsat
em : (a : Prop) → Decidable a
⊢ x.unsat
Theorem: CNF.unsat_relabel_iff
Proof state before:
case inl.intro
α β : Type
x : CNF α
f : α → β
w : ∀ {a b : α}, mem a x → mem b x → f a = f b → a = b
a₀ : α
h : (relabel f x).unsat
em : (a : Prop) → Decidable a
⊢ x.unsat
Tactic:
let g : β → α := fun b =>
  if h : ∃ a, mem a x ∧ f a = b then h.choose else a₀
Proof state after:
case inl.intro
α β : Type
x : CNF α
f : α → β
w : ∀ {a b : α}, mem a x → mem b x → f a = f b → a = b
a₀ : α
h : (relabel f x).unsat
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, mem a x ∧ f a = b then h.choose else a₀
⊢ x.unsat
Theorem: CNF.unsat_relabel_iff
Proof state before:
case inl.intro
α β : Type
x : CNF α
f : α → β
w : ∀ {a b : α}, mem a x → mem b x → f a = f b → a = b
a₀ : α
h : (relabel f x).unsat
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, mem a x ∧ f a = b then h.choose else a₀
⊢ x.unsat
Tactic:
have h' := unsat_relabel g h
Proof state after:
case inl.intro
α β : Type
x : CNF α
f : α → β
w : ∀ {a b : α}, mem a x → mem b x → f a = f b → a = b
a₀ : α
h : (relabel f x).unsat
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, mem a x ∧ f a = b then h.choose else a₀
h' : (relabel g (relabel f x)).unsat
⊢ x.unsat
Theorem: CNF.unsat_relabel_iff
Proof state before:
case inl.intro
α β : Type
x : CNF α
f : α → β
w : ∀ {a b : α}, mem a x → mem b x → f a = f b → a = b
a₀ : α
h : (relabel f x).unsat
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, mem a x ∧ f a = b then h.choose else a₀
h' : (relabel g (relabel f x)).unsat
⊢ x.unsat
Tactic:
suffices w : relabel g (relabel f x) = x by
  rwa [w] at h'
Proof state after:
case inl.intro
α β : Type
x : CNF α
f : α → β
w : ∀ {a b : α}, mem a x → mem b x → f a = f b → a = b
a₀ : α
h : (relabel f x).unsat
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, mem a x ∧ f a = b then h.choose else a₀
h' : (relabel g (relabel f x)).unsat
⊢ relabel g (relabel f x) = x
Theorem: CNF.unsat_relabel_iff
Proof state before:
case inl.intro
α β : Type
x : CNF α
f : α → β
w : ∀ {a b : α}, mem a x → mem b x → f a = f b → a = b
a₀ : α
h : (relabel f x).unsat
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, mem a x ∧ f a = b then h.choose else a₀
h' : (relabel g (relabel f x)).unsat
this : ∀ (a : α), mem a x → g (f a) = a
⊢ relabel g (relabel f x) = x
Tactic:
rw [relabel_relabel, relabel_congr, relabel_id]
Proof state after:
case inl.intro
α β : Type
x : CNF α
f : α → β
w : ∀ {a b : α}, mem a x → mem b x → f a = f b → a = b
a₀ : α
h : (relabel f x).unsat
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, mem a x ∧ f a = b then h.choose else a₀
h' : (relabel g (relabel f x)).unsat
this : ∀ (a : α), mem a x → g (f a) = a
⊢ ∀ (a : α), mem a x → (g ∘ f) a = id a
Theorem: CNF.unsat_relabel_iff
Proof state before:
case inl.intro
α β : Type
x : CNF α
f : α → β
w : ∀ {a b : α}, mem a x → mem b x → f a = f b → a = b
a₀ : α
h : (relabel f x).unsat
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, mem a x ∧ f a = b then h.choose else a₀
h' : (relabel g (relabel f x)).unsat
this : ∀ (a : α), mem a x → g (f a) = a
⊢ ∀ (a : α), mem a x → (g ∘ f) a = id a
Tactic:
exact this
Proof state after:
no goals
Theorem: CNF.unsat_relabel_iff
Proof state before:
α β : Type
x : CNF α
f : α → β
w✝ : ∀ {a b : α}, mem a x → mem b x → f a = f b → a = b
a₀ : α
h : (relabel f x).unsat
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, mem a x ∧ f a = b then h.choose else a₀
h' : (relabel g (relabel f x)).unsat
w : relabel g (relabel f x) = x
⊢ x.unsat
Tactic:
rwa [w] at h'
Proof state after:
no goals
Theorem: CNF.unsat_relabel_iff
Proof state before:
α β : Type
x : CNF α
f : α → β
w : ∀ {a b : α}, mem a x → mem b x → f a = f b → a = b
a₀ : α
h : (relabel f x).unsat
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, mem a x ∧ f a = b then h.choose else a₀
h' : (relabel g (relabel f x)).unsat
⊢ ∀ (a : α), mem a x → g (f a) = a
Tactic:
intro a h
Proof state after:
α β : Type
x : CNF α
f : α → β
w : ∀ {a b : α}, mem a x → mem b x → f a = f b → a = b
a₀ : α
h✝ : (relabel f x).unsat
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, mem a x ∧ f a = b then h.choose else a₀
h' : (relabel g (relabel f x)).unsat
a : α
h : mem a x
⊢ g (f a) = a
Theorem: CNF.unsat_relabel_iff
Proof state before:
α β : Type
x : CNF α
f : α → β
w : ∀ {a b : α}, mem a x → mem b x → f a = f b → a = b
a₀ : α
h✝ : (relabel f x).unsat
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, mem a x ∧ f a = b then h.choose else a₀
h' : (relabel g (relabel f x)).unsat
a : α
h : mem a x
⊢ g (f a) = a
Tactic:
dsimp [g]
Proof state after:
α β : Type
x : CNF α
f : α → β
w : ∀ {a b : α}, mem a x → mem b x → f a = f b → a = b
a₀ : α
h✝ : (relabel f x).unsat
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, mem a x ∧ f a = b then h.choose else a₀
h' : (relabel g (relabel f x)).unsat
a : α
h : mem a x
⊢ (if h : ∃ a_1, mem a_1 x ∧ f a_1 = f a then h.choose else a₀) = a
Theorem: CNF.unsat_relabel_iff
Proof state before:
α β : Type
x : CNF α
f : α → β
w : ∀ {a b : α}, mem a x → mem b x → f a = f b → a = b
a₀ : α
h✝ : (relabel f x).unsat
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, mem a x ∧ f a = b then h.choose else a₀
h' : (relabel g (relabel f x)).unsat
a : α
h : mem a x
⊢ (if h : ∃ a_1, mem a_1 x ∧ f a_1 = f a then h.choose else a₀) = a
Tactic:
rw [dif_pos ⟨a, h, rfl⟩]
Proof state after:
α β : Type
x : CNF α
f : α → β
w : ∀ {a b : α}, mem a x → mem b x → f a = f b → a = b
a₀ : α
h✝ : (relabel f x).unsat
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, mem a x ∧ f a = b then h.choose else a₀
h' : (relabel g (relabel f x)).unsat
a : α
h : mem a x
⊢ ⋯.choose = a
Theorem: CNF.unsat_relabel_iff
Proof state before:
α β : Type
x : CNF α
f : α → β
w : ∀ {a b : α}, mem a x → mem b x → f a = f b → a = b
a₀ : α
h✝ : (relabel f x).unsat
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, mem a x ∧ f a = b then h.choose else a₀
h' : (relabel g (relabel f x)).unsat
a : α
h : mem a x
⊢ ⋯.choose = a
Tactic:
apply w _ h
Proof state after:
α β : Type
x : CNF α
f : α → β
w : ∀ {a b : α}, mem a x → mem b x → f a = f b → a = b
a₀ : α
h✝ : (relabel f x).unsat
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, mem a x ∧ f a = b then h.choose else a₀
h' : (relabel g (relabel f x)).unsat
a : α
h : mem a x
⊢ f ⋯.choose = f a

α β : Type
x : CNF α
f : α → β
w : ∀ {a b : α}, mem a x → mem b x → f a = f b → a = b
a₀ : α
h✝ : (relabel f x).unsat
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, mem a x ∧ f a = b then h.choose else a₀
h' : (relabel g (relabel f x)).unsat
a : α
h : mem a x
⊢ mem ⋯.choose x
Theorem: CNF.unsat_relabel_iff
Proof state before:
α β : Type
x : CNF α
f : α → β
w : ∀ {a b : α}, mem a x → mem b x → f a = f b → a = b
a₀ : α
h✝ : (relabel f x).unsat
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, mem a x ∧ f a = b then h.choose else a₀
h' : (relabel g (relabel f x)).unsat
a : α
h : mem a x
⊢ f ⋯.choose = f a
Tactic:
exact (Exists.choose_spec (⟨a, h, rfl⟩ : ∃ a', mem a' x ∧ f a' = f a)).2
Proof state after:
no goals
Theorem: CNF.unsat_relabel_iff
Proof state before:
α β : Type
x : CNF α
f : α → β
w : ∀ {a b : α}, mem a x → mem b x → f a = f b → a = b
a₀ : α
h✝ : (relabel f x).unsat
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, mem a x ∧ f a = b then h.choose else a₀
h' : (relabel g (relabel f x)).unsat
a : α
h : mem a x
⊢ mem ⋯.choose x
Tactic:
exact (Exists.choose_spec (⟨a, h, rfl⟩ : ∃ a', mem a' x ∧ f a' = f a)).1
Proof state after:
no goals
Theorem: CNF.unsat_relabel_iff
Proof state before:
case inr.intro
α β : Type
f : α → β
n : Nat
w : ∀ {a b : α}, mem a (List.replicate n []) → mem b (List.replicate n []) → f a = f b → a = b
⊢ (relabel f (List.replicate n [])).unsat ↔ unsat (List.replicate n [])
Tactic:
cases n <;> simp [unsat, relabel, Clause.relabel]
Proof state after:
no goals
Theorem: bitvec_AddSub_1539_2
Proof state before:
⊢ ∀ (x C : BitVec 64), x - C = x + -C
Tactic:
intros
Proof state after:
x✝ C✝ : BitVec 64
⊢ x✝ - C✝ = x✝ + -C✝
Theorem: bitvec_AddSub_1539_2
Proof state before:
x✝ C✝ : BitVec 64
⊢ x✝ - C✝ = x✝ + -C✝
Tactic:
bv_decide
Proof state after:
no goals
Theorem: bitvec_AndOrXor_2617
Proof state before:
⊢ ∀ (a b : BitVec 64), a &&& (b ^^^ -1) ^^^ (a ^^^ -1) &&& b = a ^^^ b
Tactic:
intros
Proof state after:
a✝ b✝ : BitVec 64
⊢ a✝ &&& (b✝ ^^^ -1) ^^^ (a✝ ^^^ -1) &&& b✝ = a✝ ^^^ b✝
Theorem: bitvec_AndOrXor_2617
Proof state before:
a✝ b✝ : BitVec 64
⊢ a✝ &&& (b✝ ^^^ -1) ^^^ (a✝ ^^^ -1) &&& b✝ = a✝ ^^^ b✝
Tactic:
bv_decide
Proof state after:
no goals
Theorem: bitvec_AndOrXor_2188
Proof state before:
⊢ ∀ (A D : BitVec 64), A &&& (D ^^^ -1) ||| (A ^^^ -1) &&& D = A ^^^ D
Tactic:
intros
Proof state after:
A✝ D✝ : BitVec 64
⊢ A✝ &&& (D✝ ^^^ -1) ||| (A✝ ^^^ -1) &&& D✝ = A✝ ^^^ D✝
Theorem: bitvec_AndOrXor_2188
Proof state before:
A✝ D✝ : BitVec 64
⊢ A✝ &&& (D✝ ^^^ -1) ||| (A✝ ^^^ -1) &&& D✝ = A✝ ^^^ D✝
Tactic:
bv_decide
Proof state after:
no goals
Theorem: bitvec_AndOrXor_2587__BAA___B__A
Proof state before:
⊢ ∀ (a op1 : BitVec 64), a &&& op1 ^^^ op1 = (a ^^^ -1) &&& op1
Tactic:
intros
Proof state after:
a✝ op1✝ : BitVec 64
⊢ a✝ &&& op1✝ ^^^ op1✝ = (a✝ ^^^ -1) &&& op1✝
Theorem: bitvec_AndOrXor_2587__BAA___B__A
Proof state before:
a✝ op1✝ : BitVec 64
⊢ a✝ &&& op1✝ ^^^ op1✝ = (a✝ ^^^ -1) &&& op1✝
Tactic:
bv_decide
Proof state after:
no goals
Theorem: bitvec_AndOrXor_2231__A__B__B__C__A___A__B__C
Proof state before:
⊢ ∀ (A C B : BitVec 64), A ^^^ B ||| B ^^^ C ^^^ A = A ^^^ B ||| C
Tactic:
intros
Proof state after:
A✝ C✝ B✝ : BitVec 64
⊢ A✝ ^^^ B✝ ||| B✝ ^^^ C✝ ^^^ A✝ = A✝ ^^^ B✝ ||| C✝
Theorem: bitvec_AndOrXor_2231__A__B__B__C__A___A__B__C
Proof state before:
A✝ C✝ B✝ : BitVec 64
⊢ A✝ ^^^ B✝ ||| B✝ ^^^ C✝ ^^^ A✝ = A✝ ^^^ B✝ ||| C✝
Tactic:
bv_decide
Proof state after:
no goals
Theorem: AIG.RefStream.getRef_push_ref_eq
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefStream len
ref : aig.Ref
⊢ len < len + 1
Tactic:
omega
Proof state after:
no goals
Theorem: AIG.RefStream.getRef_push_ref_eq
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefStream len
ref : aig.Ref
⊢ (s.pushRef ref).getRef len ⋯ = ref
Tactic:
have := s.hlen
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefStream len
ref : aig.Ref
this : s.refs.size = len
⊢ (s.pushRef ref).getRef len ⋯ = ref
Theorem: AIG.RefStream.getRef_push_ref_eq
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefStream len
ref : aig.Ref
this : s.refs.size = len
⊢ (s.pushRef ref).getRef len ⋯ = ref
Tactic:
simp [getRef, pushRef, ← this]
Proof state after:
no goals
Theorem: AIG.RefStream.getRef_push_ref_eq'
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefStream len
ref : aig.Ref
idx : Nat
hidx : idx = len
⊢ idx < len + 1
Tactic:
omega
Proof state after:
no goals
Theorem: AIG.RefStream.getRef_push_ref_eq'
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefStream len
ref : aig.Ref
idx : Nat
hidx : idx = len
⊢ (s.pushRef ref).getRef idx ⋯ = ref
Tactic:
have := s.hlen
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefStream len
ref : aig.Ref
idx : Nat
hidx : idx = len
this : s.refs.size = len
⊢ (s.pushRef ref).getRef idx ⋯ = ref
Theorem: AIG.RefStream.getRef_push_ref_eq'
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefStream len
ref : aig.Ref
idx : Nat
hidx : idx = len
this : s.refs.size = len
⊢ (s.pushRef ref).getRef idx ⋯ = ref
Tactic:
simp [getRef, pushRef, ← this, hidx]
Proof state after:
no goals
Theorem: AIG.RefStream.getRef_push_ref_lt
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefStream len
ref : aig.Ref
idx : Nat
hidx : idx < len
⊢ idx < len + 1
Tactic:
omega
Proof state after:
no goals
Theorem: AIG.RefStream.getRef_push_ref_lt
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefStream len
ref : aig.Ref
idx : Nat
hidx : idx < len
⊢ (s.pushRef ref).getRef idx ⋯ = s.getRef idx hidx
Tactic:
simp [getRef, pushRef]
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefStream len
ref : aig.Ref
idx : Nat
hidx : idx < len
⊢ (s.refs.push ref.gate)[idx] = s.refs[idx]
Theorem: AIG.RefStream.getRef_push_ref_lt
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefStream len
ref : aig.Ref
idx : Nat
hidx : idx < len
⊢ (s.refs.push ref.gate)[idx] = s.refs[idx]
Tactic:
cases ref
Proof state after:
case mk
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefStream len
idx : Nat
hidx : idx < len
gate✝ : Nat
hgate✝ : gate✝ < aig.decls.size
⊢ (s.refs.push { gate := gate✝, hgate := hgate✝ }.gate)[idx] = s.refs[idx]
Theorem: AIG.RefStream.getRef_push_ref_lt
Proof state before:
case mk
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefStream len
idx : Nat
hidx : idx < len
gate✝ : Nat
hgate✝ : gate✝ < aig.decls.size
⊢ (s.refs.push { gate := gate✝, hgate := hgate✝ }.gate)[idx] = s.refs[idx]
Tactic:
simp only [Ref.mk.injEq]
Proof state after:
case mk
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefStream len
idx : Nat
hidx : idx < len
gate✝ : Nat
hgate✝ : gate✝ < aig.decls.size
⊢ (s.refs.push gate✝)[idx] = s.refs[idx]
Theorem: AIG.RefStream.getRef_push_ref_lt
Proof state before:
case mk
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefStream len
idx : Nat
hidx : idx < len
gate✝ : Nat
hgate✝ : gate✝ < aig.decls.size
⊢ (s.refs.push gate✝)[idx] = s.refs[idx]
Tactic:
rw [Array.get_push_lt]
Proof state after:
no goals
Theorem: AIG.RefStream.getRef_cast
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
aig1 aig2 : AIG α
s : aig1.RefStream len
idx : Nat
hidx : idx < len
hcast : aig1.decls.size ≤ aig2.decls.size
⊢ (s.cast hcast).getRef idx hidx = (s.getRef idx hidx).cast hcast
Tactic:
simp [cast, cast', getRef]
Proof state after:
no goals
Theorem: AIG.RefStream.getRef_append
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
lw rw : Nat
lhs : aig.RefStream lw
rhs : aig.RefStream rw
idx : Nat
hidx : idx < lw + rw
h : ¬idx < lw
⊢ idx - lw < rw
Tactic:
omega
Proof state after:
no goals
Theorem: AIG.RefStream.getRef_append
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
lw rw : Nat
lhs : aig.RefStream lw
rhs : aig.RefStream rw
idx : Nat
hidx : idx < lw + rw
⊢ (lhs.append rhs).getRef idx hidx = if h : idx < lw then lhs.getRef idx h else rhs.getRef (idx - lw) ⋯
Tactic:
simp only [getRef, append]
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
lw rw : Nat
lhs : aig.RefStream lw
rhs : aig.RefStream rw
idx : Nat
hidx : idx < lw + rw
⊢ { gate := (lhs.refs ++ rhs.refs)[idx], hgate := ⋯ } =
    if h : idx < lw then { gate := lhs.refs[idx], hgate := ⋯ } else { gate := rhs.refs[idx - lw], hgate := ⋯ }
Theorem: AIG.RefStream.getRef_append
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
lw rw : Nat
lhs : aig.RefStream lw
rhs : aig.RefStream rw
idx : Nat
hidx : idx < lw + rw
⊢ { gate := (lhs.refs ++ rhs.refs)[idx], hgate := ⋯ } =
    if h : idx < lw then { gate := lhs.refs[idx], hgate := ⋯ } else { gate := rhs.refs[idx - lw], hgate := ⋯ }
Tactic:
split
Proof state after:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
lw rw : Nat
lhs : aig.RefStream lw
rhs : aig.RefStream rw
idx : Nat
hidx : idx < lw + rw
h✝ : idx < lw
⊢ { gate := (lhs.refs ++ rhs.refs)[idx], hgate := ⋯ } = { gate := lhs.refs[idx], hgate := ⋯ }

case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
lw rw : Nat
lhs : aig.RefStream lw
rhs : aig.RefStream rw
idx : Nat
hidx : idx < lw + rw
h✝ : ¬idx < lw
⊢ { gate := (lhs.refs ++ rhs.refs)[idx], hgate := ⋯ } = { gate := rhs.refs[idx - lw], hgate := ⋯ }
Theorem: AIG.RefStream.getRef_append
Proof state before:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
lw rw : Nat
lhs : aig.RefStream lw
rhs : aig.RefStream rw
idx : Nat
hidx : idx < lw + rw
h✝ : idx < lw
⊢ { gate := (lhs.refs ++ rhs.refs)[idx], hgate := ⋯ } = { gate := lhs.refs[idx], hgate := ⋯ }

case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
lw rw : Nat
lhs : aig.RefStream lw
rhs : aig.RefStream rw
idx : Nat
hidx : idx < lw + rw
h✝ : ¬idx < lw
⊢ { gate := (lhs.refs ++ rhs.refs)[idx], hgate := ⋯ } = { gate := rhs.refs[idx - lw], hgate := ⋯ }
Tactic:
. simp [Ref.mk.injEq]
  rw [Array.get_append_left]
Proof state after:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
lw rw : Nat
lhs : aig.RefStream lw
rhs : aig.RefStream rw
idx : Nat
hidx : idx < lw + rw
h✝ : ¬idx < lw
⊢ { gate := (lhs.refs ++ rhs.refs)[idx], hgate := ⋯ } = { gate := rhs.refs[idx - lw], hgate := ⋯ }
Theorem: AIG.RefStream.getRef_append
Proof state before:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
lw rw : Nat
lhs : aig.RefStream lw
rhs : aig.RefStream rw
idx : Nat
hidx : idx < lw + rw
h✝ : ¬idx < lw
⊢ { gate := (lhs.refs ++ rhs.refs)[idx], hgate := ⋯ } = { gate := rhs.refs[idx - lw], hgate := ⋯ }
Tactic:
. simp only [Ref.mk.injEq]
  rw [Array.get_append_right]
  . simp [lhs.hlen]
  . rw [lhs.hlen]
    omega
Proof state after:
no goals