internlm/Lean-Github huggingface dataset:
Theorem: AIG.mem_def
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
a : α
⊢ (a ∈ aig) = (Decl.atom a ∈ aig.decls)
Tactic:
simp [Membership.mem, mem]
Proof state after:
no goals
Theorem: AIG.denote_congr
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign1 assign2 : α → Bool
aig : AIG α
idx : Nat
hidx : idx < aig.decls.size
h : ∀ (a : α), a ∈ aig → assign1 a = assign2 a
⊢ ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign1⟧ =
    ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign2⟧
Tactic:
apply denote_idx_trichotomy
Proof state after:
case hconst
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign1 assign2 : α → Bool
aig : AIG α
idx : Nat
hidx : idx < aig.decls.size
h : ∀ (a : α), a ∈ aig → assign1 a = assign2 a
⊢ ∀ (b : Bool),
    aig.decls[idx] = Decl.const b →
      ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign1⟧ =
        ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign2⟧

case hatom
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign1 assign2 : α → Bool
aig : AIG α
idx : Nat
hidx : idx < aig.decls.size
h : ∀ (a : α), a ∈ aig → assign1 a = assign2 a
⊢ ∀ (a : α),
    aig.decls[idx] = Decl.atom a →
      ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign1⟧ =
        ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign2⟧

case hgate
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign1 assign2 : α → Bool
aig : AIG α
idx : Nat
hidx : idx < aig.decls.size
h : ∀ (a : α), a ∈ aig → assign1 a = assign2 a
⊢ ∀ (lhs rhs : Nat) (linv rinv : Bool),
    aig.decls[idx] = Decl.gate lhs rhs linv rinv →
      ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign1⟧ =
        ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign2⟧
Theorem: AIG.denote_congr
Proof state before:
case hconst
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign1 assign2 : α → Bool
aig : AIG α
idx : Nat
hidx : idx < aig.decls.size
h : ∀ (a : α), a ∈ aig → assign1 a = assign2 a
⊢ ∀ (b : Bool),
    aig.decls[idx] = Decl.const b →
      ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign1⟧ =
        ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign2⟧

case hatom
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign1 assign2 : α → Bool
aig : AIG α
idx : Nat
hidx : idx < aig.decls.size
h : ∀ (a : α), a ∈ aig → assign1 a = assign2 a
⊢ ∀ (a : α),
    aig.decls[idx] = Decl.atom a →
      ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign1⟧ =
        ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign2⟧

case hgate
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign1 assign2 : α → Bool
aig : AIG α
idx : Nat
hidx : idx < aig.decls.size
h : ∀ (a : α), a ∈ aig → assign1 a = assign2 a
⊢ ∀ (lhs rhs : Nat) (linv rinv : Bool),
    aig.decls[idx] = Decl.gate lhs rhs linv rinv →
      ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign1⟧ =
        ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign2⟧
Tactic:
. intro b heq
  simp [denote_idx_const heq]
Proof state after:
case hatom
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign1 assign2 : α → Bool
aig : AIG α
idx : Nat
hidx : idx < aig.decls.size
h : ∀ (a : α), a ∈ aig → assign1 a = assign2 a
⊢ ∀ (a : α),
    aig.decls[idx] = Decl.atom a →
      ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign1⟧ =
        ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign2⟧

case hgate
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign1 assign2 : α → Bool
aig : AIG α
idx : Nat
hidx : idx < aig.decls.size
h : ∀ (a : α), a ∈ aig → assign1 a = assign2 a
⊢ ∀ (lhs rhs : Nat) (linv rinv : Bool),
    aig.decls[idx] = Decl.gate lhs rhs linv rinv →
      ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign1⟧ =
        ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign2⟧
Theorem: AIG.denote_congr
Proof state before:
case hatom
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign1 assign2 : α → Bool
aig : AIG α
idx : Nat
hidx : idx < aig.decls.size
h : ∀ (a : α), a ∈ aig → assign1 a = assign2 a
⊢ ∀ (a : α),
    aig.decls[idx] = Decl.atom a →
      ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign1⟧ =
        ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign2⟧

case hgate
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign1 assign2 : α → Bool
aig : AIG α
idx : Nat
hidx : idx < aig.decls.size
h : ∀ (a : α), a ∈ aig → assign1 a = assign2 a
⊢ ∀ (lhs rhs : Nat) (linv rinv : Bool),
    aig.decls[idx] = Decl.gate lhs rhs linv rinv →
      ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign1⟧ =
        ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign2⟧
Tactic:
. intro a heq
  simp only [denote_idx_atom heq]
  apply h
  rw [mem_def]
  rw [← heq]
  rw [Array.mem_def]
  apply Array.getElem_mem_data
Proof state after:
case hgate
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign1 assign2 : α → Bool
aig : AIG α
idx : Nat
hidx : idx < aig.decls.size
h : ∀ (a : α), a ∈ aig → assign1 a = assign2 a
⊢ ∀ (lhs rhs : Nat) (linv rinv : Bool),
    aig.decls[idx] = Decl.gate lhs rhs linv rinv →
      ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign1⟧ =
        ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign2⟧
Theorem: AIG.denote_congr
Proof state before:
case hgate
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign1 assign2 : α → Bool
aig : AIG α
idx : Nat
hidx : idx < aig.decls.size
h : ∀ (a : α), a ∈ aig → assign1 a = assign2 a
⊢ ∀ (lhs rhs : Nat) (linv rinv : Bool),
    aig.decls[idx] = Decl.gate lhs rhs linv rinv →
      ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign1⟧ =
        ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign2⟧
Tactic:
. intro lhs rhs linv rinv heq
  simp [denote_idx_gate heq]
  have := aig.inv idx lhs rhs linv rinv hidx heq
  rw [denote_congr assign1 assign2 aig lhs (by omega) h]
  rw [denote_congr assign1 assign2 aig rhs (by omega) h]
Proof state after:
no goals
Theorem: AIG.denote_congr
Proof state before:
case hconst
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign1 assign2 : α → Bool
aig : AIG α
idx : Nat
hidx : idx < aig.decls.size
h : ∀ (a : α), a ∈ aig → assign1 a = assign2 a
⊢ ∀ (b : Bool),
    aig.decls[idx] = Decl.const b →
      ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign1⟧ =
        ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign2⟧
Tactic:
intro b heq
Proof state after:
case hconst
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign1 assign2 : α → Bool
aig : AIG α
idx : Nat
hidx : idx < aig.decls.size
h : ∀ (a : α), a ∈ aig → assign1 a = assign2 a
b : Bool
heq : aig.decls[idx] = Decl.const b
⊢ ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign1⟧ =
    ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign2⟧
Theorem: AIG.denote_congr
Proof state before:
case hconst
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign1 assign2 : α → Bool
aig : AIG α
idx : Nat
hidx : idx < aig.decls.size
h : ∀ (a : α), a ∈ aig → assign1 a = assign2 a
b : Bool
heq : aig.decls[idx] = Decl.const b
⊢ ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign1⟧ =
    ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign2⟧
Tactic:
simp [denote_idx_const heq]
Proof state after:
no goals
Theorem: AIG.denote_congr
Proof state before:
case hatom
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign1 assign2 : α → Bool
aig : AIG α
idx : Nat
hidx : idx < aig.decls.size
h : ∀ (a : α), a ∈ aig → assign1 a = assign2 a
⊢ ∀ (a : α),
    aig.decls[idx] = Decl.atom a →
      ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign1⟧ =
        ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign2⟧
Tactic:
intro a heq
Proof state after:
case hatom
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign1 assign2 : α → Bool
aig : AIG α
idx : Nat
hidx : idx < aig.decls.size
h : ∀ (a : α), a ∈ aig → assign1 a = assign2 a
a : α
heq : aig.decls[idx] = Decl.atom a
⊢ ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign1⟧ =
    ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign2⟧
Theorem: AIG.denote_congr
Proof state before:
case hatom
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign1 assign2 : α → Bool
aig : AIG α
idx : Nat
hidx : idx < aig.decls.size
h : ∀ (a : α), a ∈ aig → assign1 a = assign2 a
a : α
heq : aig.decls[idx] = Decl.atom a
⊢ ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign1⟧ =
    ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign2⟧
Tactic:
simp only [denote_idx_atom heq]
Proof state after:
case hatom
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign1 assign2 : α → Bool
aig : AIG α
idx : Nat
hidx : idx < aig.decls.size
h : ∀ (a : α), a ∈ aig → assign1 a = assign2 a
a : α
heq : aig.decls[idx] = Decl.atom a
⊢ assign1 a = assign2 a
Theorem: AIG.denote_congr
Proof state before:
case hatom
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign1 assign2 : α → Bool
aig : AIG α
idx : Nat
hidx : idx < aig.decls.size
h : ∀ (a : α), a ∈ aig → assign1 a = assign2 a
a : α
heq : aig.decls[idx] = Decl.atom a
⊢ assign1 a = assign2 a
Tactic:
apply h
Proof state after:
case hatom.a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign1 assign2 : α → Bool
aig : AIG α
idx : Nat
hidx : idx < aig.decls.size
h : ∀ (a : α), a ∈ aig → assign1 a = assign2 a
a : α
heq : aig.decls[idx] = Decl.atom a
⊢ a ∈ aig
Theorem: AIG.denote_congr
Proof state before:
case hatom.a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign1 assign2 : α → Bool
aig : AIG α
idx : Nat
hidx : idx < aig.decls.size
h : ∀ (a : α), a ∈ aig → assign1 a = assign2 a
a : α
heq : aig.decls[idx] = Decl.atom a
⊢ a ∈ aig
Tactic:
rw [mem_def]
Proof state after:
case hatom.a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign1 assign2 : α → Bool
aig : AIG α
idx : Nat
hidx : idx < aig.decls.size
h : ∀ (a : α), a ∈ aig → assign1 a = assign2 a
a : α
heq : aig.decls[idx] = Decl.atom a
⊢ Decl.atom a ∈ aig.decls
Theorem: AIG.denote_congr
Proof state before:
case hatom.a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign1 assign2 : α → Bool
aig : AIG α
idx : Nat
hidx : idx < aig.decls.size
h : ∀ (a : α), a ∈ aig → assign1 a = assign2 a
a : α
heq : aig.decls[idx] = Decl.atom a
⊢ Decl.atom a ∈ aig.decls
Tactic:
rw [← heq]
Proof state after:
case hatom.a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign1 assign2 : α → Bool
aig : AIG α
idx : Nat
hidx : idx < aig.decls.size
h : ∀ (a : α), a ∈ aig → assign1 a = assign2 a
a : α
heq : aig.decls[idx] = Decl.atom a
⊢ aig.decls[idx] ∈ aig.decls
Theorem: AIG.denote_congr
Proof state before:
case hatom.a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign1 assign2 : α → Bool
aig : AIG α
idx : Nat
hidx : idx < aig.decls.size
h : ∀ (a : α), a ∈ aig → assign1 a = assign2 a
a : α
heq : aig.decls[idx] = Decl.atom a
⊢ aig.decls[idx] ∈ aig.decls
Tactic:
rw [Array.mem_def]
Proof state after:
case hatom.a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign1 assign2 : α → Bool
aig : AIG α
idx : Nat
hidx : idx < aig.decls.size
h : ∀ (a : α), a ∈ aig → assign1 a = assign2 a
a : α
heq : aig.decls[idx] = Decl.atom a
⊢ aig.decls[idx] ∈ aig.decls.data
Theorem: AIG.denote_congr
Proof state before:
case hatom.a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign1 assign2 : α → Bool
aig : AIG α
idx : Nat
hidx : idx < aig.decls.size
h : ∀ (a : α), a ∈ aig → assign1 a = assign2 a
a : α
heq : aig.decls[idx] = Decl.atom a
⊢ aig.decls[idx] ∈ aig.decls.data
Tactic:
apply Array.getElem_mem_data
Proof state after:
no goals
Theorem: AIG.denote_congr
Proof state before:
case hgate
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign1 assign2 : α → Bool
aig : AIG α
idx : Nat
hidx : idx < aig.decls.size
h : ∀ (a : α), a ∈ aig → assign1 a = assign2 a
⊢ ∀ (lhs rhs : Nat) (linv rinv : Bool),
    aig.decls[idx] = Decl.gate lhs rhs linv rinv →
      ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign1⟧ =
        ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign2⟧
Tactic:
intro lhs rhs linv rinv heq
Proof state after:
case hgate
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign1 assign2 : α → Bool
aig : AIG α
idx : Nat
hidx : idx < aig.decls.size
h : ∀ (a : α), a ∈ aig → assign1 a = assign2 a
lhs rhs : Nat
linv rinv : Bool
heq : aig.decls[idx] = Decl.gate lhs rhs linv rinv
⊢ ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign1⟧ =
    ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign2⟧
Theorem: AIG.denote_congr
Proof state before:
case hgate
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign1 assign2 : α → Bool
aig : AIG α
idx : Nat
hidx : idx < aig.decls.size
h : ∀ (a : α), a ∈ aig → assign1 a = assign2 a
lhs rhs : Nat
linv rinv : Bool
heq : aig.decls[idx] = Decl.gate lhs rhs linv rinv
⊢ ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign1⟧ =
    ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign2⟧
Tactic:
simp [denote_idx_gate heq]
Proof state after:
case hgate
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign1 assign2 : α → Bool
aig : AIG α
idx : Nat
hidx : idx < aig.decls.size
h : ∀ (a : α), a ∈ aig → assign1 a = assign2 a
lhs rhs : Nat
linv rinv : Bool
heq : aig.decls[idx] = Decl.gate lhs rhs linv rinv
⊢ (xor ⟦{ aig := aig, ref := { gate := lhs, hgate := ⋯ } }, assign1⟧ linv &&
      xor ⟦{ aig := aig, ref := { gate := rhs, hgate := ⋯ } }, assign1⟧ rinv) =
    (xor ⟦{ aig := aig, ref := { gate := lhs, hgate := ⋯ } }, assign2⟧ linv &&
      xor ⟦{ aig := aig, ref := { gate := rhs, hgate := ⋯ } }, assign2⟧ rinv)
Theorem: AIG.denote_congr
Proof state before:
case hgate
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign1 assign2 : α → Bool
aig : AIG α
idx : Nat
hidx : idx < aig.decls.size
h : ∀ (a : α), a ∈ aig → assign1 a = assign2 a
lhs rhs : Nat
linv rinv : Bool
heq : aig.decls[idx] = Decl.gate lhs rhs linv rinv
⊢ (xor ⟦{ aig := aig, ref := { gate := lhs, hgate := ⋯ } }, assign1⟧ linv &&
      xor ⟦{ aig := aig, ref := { gate := rhs, hgate := ⋯ } }, assign1⟧ rinv) =
    (xor ⟦{ aig := aig, ref := { gate := lhs, hgate := ⋯ } }, assign2⟧ linv &&
      xor ⟦{ aig := aig, ref := { gate := rhs, hgate := ⋯ } }, assign2⟧ rinv)
Tactic:
have := aig.inv idx lhs rhs linv rinv hidx heq
Proof state after:
case hgate
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign1 assign2 : α → Bool
aig : AIG α
idx : Nat
hidx : idx < aig.decls.size
h : ∀ (a : α), a ∈ aig → assign1 a = assign2 a
lhs rhs : Nat
linv rinv : Bool
heq : aig.decls[idx] = Decl.gate lhs rhs linv rinv
this : lhs < idx ∧ rhs < idx
⊢ (xor ⟦{ aig := aig, ref := { gate := lhs, hgate := ⋯ } }, assign1⟧ linv &&
      xor ⟦{ aig := aig, ref := { gate := rhs, hgate := ⋯ } }, assign1⟧ rinv) =
    (xor ⟦{ aig := aig, ref := { gate := lhs, hgate := ⋯ } }, assign2⟧ linv &&
      xor ⟦{ aig := aig, ref := { gate := rhs, hgate := ⋯ } }, assign2⟧ rinv)
Theorem: AIG.denote_congr
Proof state before:
case hgate
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign1 assign2 : α → Bool
aig : AIG α
idx : Nat
hidx : idx < aig.decls.size
h : ∀ (a : α), a ∈ aig → assign1 a = assign2 a
lhs rhs : Nat
linv rinv : Bool
heq : aig.decls[idx] = Decl.gate lhs rhs linv rinv
this : lhs < idx ∧ rhs < idx
⊢ (xor ⟦{ aig := aig, ref := { gate := lhs, hgate := ⋯ } }, assign1⟧ linv &&
      xor ⟦{ aig := aig, ref := { gate := rhs, hgate := ⋯ } }, assign1⟧ rinv) =
    (xor ⟦{ aig := aig, ref := { gate := lhs, hgate := ⋯ } }, assign2⟧ linv &&
      xor ⟦{ aig := aig, ref := { gate := rhs, hgate := ⋯ } }, assign2⟧ rinv)
Tactic:
rw [denote_congr assign1 assign2 aig lhs (by omega) h]
Proof state after:
case hgate
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign1 assign2 : α → Bool
aig : AIG α
idx : Nat
hidx : idx < aig.decls.size
h : ∀ (a : α), a ∈ aig → assign1 a = assign2 a
lhs rhs : Nat
linv rinv : Bool
heq : aig.decls[idx] = Decl.gate lhs rhs linv rinv
this : lhs < idx ∧ rhs < idx
⊢ (xor ⟦{ aig := aig, ref := { gate := lhs, hgate := ⋯ } }, assign2⟧ linv &&
      xor ⟦{ aig := aig, ref := { gate := rhs, hgate := ⋯ } }, assign1⟧ rinv) =
    (xor ⟦{ aig := aig, ref := { gate := lhs, hgate := ⋯ } }, assign2⟧ linv &&
      xor ⟦{ aig := aig, ref := { gate := rhs, hgate := ⋯ } }, assign2⟧ rinv)
Theorem: AIG.denote_congr
Proof state before:
case hgate
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign1 assign2 : α → Bool
aig : AIG α
idx : Nat
hidx : idx < aig.decls.size
h : ∀ (a : α), a ∈ aig → assign1 a = assign2 a
lhs rhs : Nat
linv rinv : Bool
heq : aig.decls[idx] = Decl.gate lhs rhs linv rinv
this : lhs < idx ∧ rhs < idx
⊢ (xor ⟦{ aig := aig, ref := { gate := lhs, hgate := ⋯ } }, assign2⟧ linv &&
      xor ⟦{ aig := aig, ref := { gate := rhs, hgate := ⋯ } }, assign1⟧ rinv) =
    (xor ⟦{ aig := aig, ref := { gate := lhs, hgate := ⋯ } }, assign2⟧ linv &&
      xor ⟦{ aig := aig, ref := { gate := rhs, hgate := ⋯ } }, assign2⟧ rinv)
Tactic:
rw [denote_congr assign1 assign2 aig rhs (by omega) h]
Proof state after:
no goals
Theorem: AIG.denote_congr
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign1 assign2 : α → Bool
aig : AIG α
idx : Nat
hidx : idx < aig.decls.size
h : ∀ (a : α), a ∈ aig → assign1 a = assign2 a
lhs rhs : Nat
linv rinv : Bool
heq : aig.decls[idx] = Decl.gate lhs rhs linv rinv
this : lhs < idx ∧ rhs < idx
⊢ lhs < aig.decls.size
Tactic:
omega
Proof state after:
no goals
Theorem: AIG.denote_congr
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign1 assign2 : α → Bool
aig : AIG α
idx : Nat
hidx : idx < aig.decls.size
h : ∀ (a : α), a ∈ aig → assign1 a = assign2 a
lhs rhs : Nat
linv rinv : Bool
heq : aig.decls[idx] = Decl.gate lhs rhs linv rinv
this : lhs < idx ∧ rhs < idx
⊢ rhs < aig.decls.size
Tactic:
omega
Proof state after:
no goals
Theorem: BVDecide.Normalize.BitVec.le_ult
Proof state before:
w : Nat
x y : BitVec w
⊢ x.toNat.le y.toNat = ¬y.toNat.lt x.toNat
Tactic:
simp
Proof state after:
no goals
Theorem: BVDecide.Normalize.BitVec.truncate_eq_zeroExtend
Proof state before:
w n : Nat
x : BitVec w
⊢ BitVec.truncate n x = BitVec.zeroExtend n x
Tactic:
rfl
Proof state after:
no goals
Theorem: bitvec_AndOrXor_1241_AB__AB__AB
Proof state before:
⊢ ∀ (A B : BitVec 64), (A ||| B) &&& (A &&& B ^^^ -1) = A ^^^ B
Tactic:
intros
Proof state after:
A✝ B✝ : BitVec 64
⊢ (A✝ ||| B✝) &&& (A✝ &&& B✝ ^^^ -1) = A✝ ^^^ B✝
Theorem: bitvec_AndOrXor_1241_AB__AB__AB
Proof state before:
A✝ B✝ : BitVec 64
⊢ (A✝ ||| B✝) &&& (A✝ &&& B✝ ^^^ -1) = A✝ ^^^ B✝
Tactic:
bv_decide
Proof state after:
no goals
Theorem: List.isEmpty_false_iff_exists_mem
Proof state before:
α : Type u_1
xs : List α
⊢ xs.isEmpty = false ↔ ∃ x, x ∈ xs
Tactic:
cases xs <;> simp
Proof state after:
no goals
Theorem: List.isEmpty_true_iff
Proof state before:
α : Type u_1
xs : List α
⊢ xs.isEmpty = true ↔ xs = []
Tactic:
cases xs <;> simp
Proof state after:
no goals
Theorem: CNF.unsat_nil_iff_false
Proof state before:
α : Type
h : unsat []
⊢ False
Tactic:
simp [unsat] at h
Proof state after:
no goals
Theorem: CNF.unsat_nil_iff_false
Proof state before:
α : Type
⊢ False → unsat []
Tactic:
simp
Proof state after:
no goals
Theorem: CNF.sat_nil
Proof state before:
α : Type
assign : α → Bool
⊢ sat [] assign ↔ True
Tactic:
simp [sat]
Proof state after:
no goals
Theorem: CNF.unsat_nil_cons
Proof state before:
α✝ : Type
g : List (Clause α✝)
⊢ unsat ([] :: g) ↔ True
Tactic:
simp [unsat]
Proof state after:
no goals
Theorem: CNF.Clause.not_mem_nil
Proof state before:
α : Type
a : α
⊢ mem a [] ↔ False
Tactic:
simp [mem]
Proof state after:
no goals
Theorem: CNF.Clause.mem_cons
Proof state before:
α : Type
i : α × Bool
c : List (α × Bool)
a : α
⊢ mem a (i :: c) ↔ a = i.fst ∨ mem a c
Tactic:
rcases i with ⟨b, (_|_)⟩
Proof state after:
case mk.false
α : Type
c : List (α × Bool)
a b : α
⊢ mem a ((b, false) :: c) ↔ a = (b, false).fst ∨ mem a c

case mk.true
α : Type
c : List (α × Bool)
a b : α
⊢ mem a ((b, true) :: c) ↔ a = (b, true).fst ∨ mem a c
Theorem: CNF.Clause.mem_cons
Proof state before:
case mk.false
α : Type
c : List (α × Bool)
a b : α
⊢ mem a ((b, false) :: c) ↔ a = (b, false).fst ∨ mem a c
Tactic:
simp [mem, or_assoc]
Proof state after:
no goals
Theorem: CNF.Clause.mem_cons
Proof state before:
case mk.true
α : Type
c : List (α × Bool)
a b : α
⊢ mem a ((b, true) :: c) ↔ a = (b, true).fst ∨ mem a c
Tactic:
simp [mem]
Proof state after:
case mk.true
α : Type
c : List (α × Bool)
a b : α
⊢ (a, false) ∈ c ∨ a = b ∨ (a, true) ∈ c ↔ a = b ∨ (a, false) ∈ c ∨ (a, true) ∈ c
Theorem: CNF.Clause.mem_cons
Proof state before:
case mk.true
α : Type
c : List (α × Bool)
a b : α
⊢ (a, false) ∈ c ∨ a = b ∨ (a, true) ∈ c ↔ a = b ∨ (a, false) ∈ c ∨ (a, true) ∈ c
Tactic:
rw [or_left_comm]
Proof state after:
no goals
Theorem: CNF.Clause.mem_of
Proof state before:
α✝ : Type
a : α✝
b : Bool
c : Clause α✝
h : (a, b) ∈ c
⊢ mem a c
Tactic:
cases b
Proof state after:
case false
α✝ : Type
a : α✝
c : Clause α✝
h : (a, false) ∈ c
⊢ mem a c

case true
α✝ : Type
a : α✝
c : Clause α✝
h : (a, true) ∈ c
⊢ mem a c
Theorem: CNF.Clause.mem_of
Proof state before:
case false
α✝ : Type
a : α✝
c : Clause α✝
h : (a, false) ∈ c
⊢ mem a c
Tactic:
left
Proof state after:
case false.h
α✝ : Type
a : α✝
c : Clause α✝
h : (a, false) ∈ c
⊢ (a, false) ∈ c
Theorem: CNF.Clause.mem_of
Proof state before:
case false.h
α✝ : Type
a : α✝
c : Clause α✝
h : (a, false) ∈ c
⊢ (a, false) ∈ c
Tactic:
exact h
Proof state after:
no goals
Theorem: CNF.Clause.mem_of
Proof state before:
case true
α✝ : Type
a : α✝
c : Clause α✝
h : (a, true) ∈ c
⊢ mem a c
Tactic:
right
Proof state after:
case true.h
α✝ : Type
a : α✝
c : Clause α✝
h : (a, true) ∈ c
⊢ (a, true) ∈ c
Theorem: CNF.Clause.mem_of
Proof state before:
case true.h
α✝ : Type
a : α✝
c : Clause α✝
h : (a, true) ∈ c
⊢ (a, true) ∈ c
Tactic:
exact h
Proof state after:
no goals
Theorem: CNF.Clause.eval_congr
Proof state before:
α : Type
f g : α → Bool
c : Clause α
w : ∀ (i : α), mem i c → f i = g i
⊢ eval f c = eval g c
Tactic:
induction c
Proof state after:
case nil
α : Type
f g : α → Bool
w : ∀ (i : α), mem i [] → f i = g i
⊢ eval f [] = eval g []

case cons
α : Type
f g : α → Bool
head✝ : α × Bool
tail✝ : List (α × Bool)
tail_ih✝ : (∀ (i : α), mem i tail✝ → f i = g i) → eval f tail✝ = eval g tail✝
w : ∀ (i : α), mem i (head✝ :: tail✝) → f i = g i
⊢ eval f (head✝ :: tail✝) = eval g (head✝ :: tail✝)
Theorem: CNF.Clause.eval_congr
Proof state before:
α : Type
f g : α → Bool
w : ∀ (i : α), mem i [] → f i = g i
⊢ eval f [] = eval g []
Tactic:
case nil => rfl
Proof state after:
no goals
Theorem: CNF.Clause.eval_congr
Proof state before:
α : Type
f g : α → Bool
w : ∀ (i : α), mem i [] → f i = g i
⊢ eval f [] = eval g []
Tactic:
rfl
Proof state after:
no goals
Theorem: CNF.Clause.eval_congr
Proof state before:
α : Type
f g : α → Bool
i : α × Bool
c : List (α × Bool)
ih : (∀ (i : α), mem i c → f i = g i) → eval f c = eval g c
w : ∀ (i_1 : α), mem i_1 (i :: c) → f i_1 = g i_1
⊢ eval f (i :: c) = eval g (i :: c)
Tactic:
simp only [eval_succ]
Proof state after:
α : Type
f g : α → Bool
i : α × Bool
c : List (α × Bool)
ih : (∀ (i : α), mem i c → f i = g i) → eval f c = eval g c
w : ∀ (i_1 : α), mem i_1 (i :: c) → f i_1 = g i_1
⊢ (f i.fst == i.snd || eval f c) = (g i.fst == i.snd || eval g c)