internlm/Lean-Github huggingface dataset:
Theorem: AIG.toCNF.denote_as_go
Proof state before:
aig : AIG Nat
start : Nat
h1 : start < aig.decls.size
assign : aig.CNFVar → Bool
h : ⟦{ aig := aig, ref := { gate := start, hgate := h1 } }, projectLeftAssign assign⟧ = false
⊢ CNF.eval assign ([(Sum.inr ⟨start, h1⟩, true)] :: (go aig start h1 (State.empty aig)).val.cnf) = false
Tactic:
match heval1:(go aig start h1 (State.empty aig)).val.cnf.eval assign with
| true =>
  have heval2 := (go aig start h1 (.empty aig)).val.cache.inv.heval
  specialize heval2 assign heval1 start h1 go_marked
  simp [h] at heval2
  simp [heval2]
| false =>
  simp [heval1]
Proof state after:
no goals
Theorem: AIG.toCNF.denote_as_go
Proof state before:
aig : AIG Nat
start : Nat
h1 : start < aig.decls.size
assign : aig.CNFVar → Bool
h : ⟦{ aig := aig, ref := { gate := start, hgate := h1 } }, projectLeftAssign assign⟧ = false
heval1 : CNF.eval assign (go aig start h1 (State.empty aig)).val.cnf = true
⊢ CNF.eval assign ([(Sum.inr ⟨start, h1⟩, true)] :: (go aig start h1 (State.empty aig)).val.cnf) = false
Tactic:
have heval2 := (go aig start h1 (.empty aig)).val.cache.inv.heval
Proof state after:
aig : AIG Nat
start : Nat
h1 : start < aig.decls.size
assign : aig.CNFVar → Bool
h : ⟦{ aig := aig, ref := { gate := start, hgate := h1 } }, projectLeftAssign assign⟧ = false
heval1 : CNF.eval assign (go aig start h1 (State.empty aig)).val.cnf = true
heval2 :
  ∀ (assign : aig.CNFVar → Bool),
    CNF.eval assign (go aig start h1 (State.empty aig)).val.cnf = true →
      ∀ (idx : Nat) (hbound : idx < aig.decls.size),
        (go aig start h1 (State.empty aig)).val.cache.marks[idx] = true →
          ⟦{ aig := aig, ref := { gate := idx, hgate := hbound } }, projectLeftAssign assign⟧ =
            projectRightAssign assign idx hbound
⊢ CNF.eval assign ([(Sum.inr ⟨start, h1⟩, true)] :: (go aig start h1 (State.empty aig)).val.cnf) = false
Theorem: AIG.toCNF.denote_as_go
Proof state before:
aig : AIG Nat
start : Nat
h1 : start < aig.decls.size
assign : aig.CNFVar → Bool
h : ⟦{ aig := aig, ref := { gate := start, hgate := h1 } }, projectLeftAssign assign⟧ = false
heval1 : CNF.eval assign (go aig start h1 (State.empty aig)).val.cnf = true
heval2 :
  ∀ (assign : aig.CNFVar → Bool),
    CNF.eval assign (go aig start h1 (State.empty aig)).val.cnf = true →
      ∀ (idx : Nat) (hbound : idx < aig.decls.size),
        (go aig start h1 (State.empty aig)).val.cache.marks[idx] = true →
          ⟦{ aig := aig, ref := { gate := idx, hgate := hbound } }, projectLeftAssign assign⟧ =
            projectRightAssign assign idx hbound
⊢ CNF.eval assign ([(Sum.inr ⟨start, h1⟩, true)] :: (go aig start h1 (State.empty aig)).val.cnf) = false
Tactic:
specialize heval2 assign heval1 start h1 go_marked
Proof state after:
aig : AIG Nat
start : Nat
h1 : start < aig.decls.size
assign : aig.CNFVar → Bool
h : ⟦{ aig := aig, ref := { gate := start, hgate := h1 } }, projectLeftAssign assign⟧ = false
heval1 : CNF.eval assign (go aig start h1 (State.empty aig)).val.cnf = true
heval2 :
  ⟦{ aig := aig, ref := { gate := start, hgate := h1 } }, projectLeftAssign assign⟧ = projectRightAssign assign start h1
⊢ CNF.eval assign ([(Sum.inr ⟨start, h1⟩, true)] :: (go aig start h1 (State.empty aig)).val.cnf) = false
Theorem: AIG.toCNF.denote_as_go
Proof state before:
aig : AIG Nat
start : Nat
h1 : start < aig.decls.size
assign : aig.CNFVar → Bool
h : ⟦{ aig := aig, ref := { gate := start, hgate := h1 } }, projectLeftAssign assign⟧ = false
heval1 : CNF.eval assign (go aig start h1 (State.empty aig)).val.cnf = true
heval2 :
  ⟦{ aig := aig, ref := { gate := start, hgate := h1 } }, projectLeftAssign assign⟧ = projectRightAssign assign start h1
⊢ CNF.eval assign ([(Sum.inr ⟨start, h1⟩, true)] :: (go aig start h1 (State.empty aig)).val.cnf) = false
Tactic:
simp [h] at heval2
Proof state after:
aig : AIG Nat
start : Nat
h1 : start < aig.decls.size
assign : aig.CNFVar → Bool
h : ⟦{ aig := aig, ref := { gate := start, hgate := h1 } }, projectLeftAssign assign⟧ = false
heval1 : CNF.eval assign (go aig start h1 (State.empty aig)).val.cnf = true
heval2 : assign (Sum.inr ⟨start, h1⟩) = false
⊢ CNF.eval assign ([(Sum.inr ⟨start, h1⟩, true)] :: (go aig start h1 (State.empty aig)).val.cnf) = false
Theorem: AIG.toCNF.denote_as_go
Proof state before:
aig : AIG Nat
start : Nat
h1 : start < aig.decls.size
assign : aig.CNFVar → Bool
h : ⟦{ aig := aig, ref := { gate := start, hgate := h1 } }, projectLeftAssign assign⟧ = false
heval1 : CNF.eval assign (go aig start h1 (State.empty aig)).val.cnf = true
heval2 : assign (Sum.inr ⟨start, h1⟩) = false
⊢ CNF.eval assign ([(Sum.inr ⟨start, h1⟩, true)] :: (go aig start h1 (State.empty aig)).val.cnf) = false
Tactic:
simp [heval2]
Proof state after:
no goals
Theorem: AIG.toCNF.denote_as_go
Proof state before:
aig : AIG Nat
start : Nat
h1 : start < aig.decls.size
assign : aig.CNFVar → Bool
h : ⟦{ aig := aig, ref := { gate := start, hgate := h1 } }, projectLeftAssign assign⟧ = false
heval1 : CNF.eval assign (go aig start h1 (State.empty aig)).val.cnf = false
⊢ CNF.eval assign ([(Sum.inr ⟨start, h1⟩, true)] :: (go aig start h1 (State.empty aig)).val.cnf) = false
Tactic:
simp [heval1]
Proof state after:
no goals
Theorem: AIG.toCNF_equisat
Proof state before:
entry : Entrypoint Nat
⊢ (toCNF entry).unsat ↔ entry.unsat
Tactic:
dsimp [toCNF]
Proof state after:
entry : Entrypoint Nat
⊢ (CNF.relabel toCNF.inj
        ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
          (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf)).unsat ↔
    entry.unsat
Theorem: AIG.toCNF_equisat
Proof state before:
entry : Entrypoint Nat
⊢ (CNF.relabel toCNF.inj
        ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
          (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf)).unsat ↔
    entry.unsat
Tactic:
rw [CNF.unsat_relabel_iff]
Proof state after:
entry : Entrypoint Nat
⊢ CNF.unsat
      ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
        (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf) ↔
    entry.unsat

entry : Entrypoint Nat
⊢ ∀ {a b : entry.aig.CNFVar},
    CNF.mem a
        ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
          (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf) →
      CNF.mem b
          ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
            (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf) →
        toCNF.inj a = toCNF.inj b → a = b
Theorem: AIG.toCNF_equisat
Proof state before:
entry : Entrypoint Nat
⊢ CNF.unsat
      ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
        (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf) ↔
    entry.unsat

entry : Entrypoint Nat
⊢ ∀ {a b : entry.aig.CNFVar},
    CNF.mem a
        ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
          (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf) →
      CNF.mem b
          ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
            (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf) →
        toCNF.inj a = toCNF.inj b → a = b
Tactic:
. constructor
  . intro h assign1
    apply toCNF.go_as_denote
    specialize h (toCNF.cnfSatAssignment entry.aig assign1)
    simpa using h
  . intro h assign
    apply toCNF.denote_as_go
    specialize h (toCNF.projectLeftAssign assign)
    assumption
Proof state after:
entry : Entrypoint Nat
⊢ ∀ {a b : entry.aig.CNFVar},
    CNF.mem a
        ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
          (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf) →
      CNF.mem b
          ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
            (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf) →
        toCNF.inj a = toCNF.inj b → a = b
Theorem: AIG.toCNF_equisat
Proof state before:
entry : Entrypoint Nat
⊢ ∀ {a b : entry.aig.CNFVar},
    CNF.mem a
        ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
          (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf) →
      CNF.mem b
          ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
            (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf) →
        toCNF.inj a = toCNF.inj b → a = b
Tactic:
. intro a b _ _ hinj
  apply toCNF.inj_is_injection
  assumption
Proof state after:
no goals
Theorem: AIG.toCNF_equisat
Proof state before:
entry : Entrypoint Nat
⊢ CNF.unsat
      ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
        (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf) ↔
    entry.unsat
Tactic:
constructor
Proof state after:
case mp
entry : Entrypoint Nat
⊢ CNF.unsat
      ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
        (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf) →
    entry.unsat

case mpr
entry : Entrypoint Nat
⊢ entry.unsat →
    CNF.unsat
      ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
        (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf)
Theorem: AIG.toCNF_equisat
Proof state before:
case mp
entry : Entrypoint Nat
⊢ CNF.unsat
      ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
        (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf) →
    entry.unsat

case mpr
entry : Entrypoint Nat
⊢ entry.unsat →
    CNF.unsat
      ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
        (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf)
Tactic:
. intro h assign1
  apply toCNF.go_as_denote
  specialize h (toCNF.cnfSatAssignment entry.aig assign1)
  simpa using h
Proof state after:
case mpr
entry : Entrypoint Nat
⊢ entry.unsat →
    CNF.unsat
      ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
        (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf)
Theorem: AIG.toCNF_equisat
Proof state before:
case mpr
entry : Entrypoint Nat
⊢ entry.unsat →
    CNF.unsat
      ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
        (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf)
Tactic:
. intro h assign
  apply toCNF.denote_as_go
  specialize h (toCNF.projectLeftAssign assign)
  assumption
Proof state after:
no goals
Theorem: AIG.toCNF_equisat
Proof state before:
case mp
entry : Entrypoint Nat
⊢ CNF.unsat
      ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
        (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf) →
    entry.unsat
Tactic:
intro h assign1
Proof state after:
case mp
entry : Entrypoint Nat
h :
  CNF.unsat
    ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
      (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf)
assign1 : Nat → Bool
⊢ ⟦{ aig := entry.aig, ref := { gate := entry.ref.gate, hgate := ⋯ } }, assign1⟧ = false
Theorem: AIG.toCNF_equisat
Proof state before:
case mp
entry : Entrypoint Nat
h :
  CNF.unsat
    ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
      (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf)
assign1 : Nat → Bool
⊢ ⟦{ aig := entry.aig, ref := { gate := entry.ref.gate, hgate := ⋯ } }, assign1⟧ = false
Tactic:
apply toCNF.go_as_denote
Proof state after:
case mp.a
entry : Entrypoint Nat
h :
  CNF.unsat
    ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
      (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf)
assign1 : Nat → Bool
⊢ (⟦{ aig := entry.aig, ref := { gate := entry.ref.gate, hgate := ⋯ } }, assign1⟧ &&
      (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.eval
        (toCNF.cnfSatAssignment entry.aig assign1)) =
    false
Theorem: AIG.toCNF_equisat
Proof state before:
case mp.a
entry : Entrypoint Nat
h :
  CNF.unsat
    ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
      (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf)
assign1 : Nat → Bool
⊢ (⟦{ aig := entry.aig, ref := { gate := entry.ref.gate, hgate := ⋯ } }, assign1⟧ &&
      (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.eval
        (toCNF.cnfSatAssignment entry.aig assign1)) =
    false
Tactic:
specialize h (toCNF.cnfSatAssignment entry.aig assign1)
Proof state after:
case mp.a
entry : Entrypoint Nat
assign1 : Nat → Bool
h :
  CNF.eval (toCNF.cnfSatAssignment entry.aig assign1)
      ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
        (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf) =
    false
⊢ (⟦{ aig := entry.aig, ref := { gate := entry.ref.gate, hgate := ⋯ } }, assign1⟧ &&
      (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.eval
        (toCNF.cnfSatAssignment entry.aig assign1)) =
    false
Theorem: AIG.toCNF_equisat
Proof state before:
case mp.a
entry : Entrypoint Nat
assign1 : Nat → Bool
h :
  CNF.eval (toCNF.cnfSatAssignment entry.aig assign1)
      ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
        (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf) =
    false
⊢ (⟦{ aig := entry.aig, ref := { gate := entry.ref.gate, hgate := ⋯ } }, assign1⟧ &&
      (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.eval
        (toCNF.cnfSatAssignment entry.aig assign1)) =
    false
Tactic:
simpa using h
Proof state after:
no goals
Theorem: AIG.toCNF_equisat
Proof state before:
case mpr
entry : Entrypoint Nat
⊢ entry.unsat →
    CNF.unsat
      ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
        (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf)
Tactic:
intro h assign
Proof state after:
case mpr
entry : Entrypoint Nat
h : entry.unsat
assign : entry.aig.CNFVar → Bool
⊢ CNF.eval assign
      ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
        (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf) =
    false
Theorem: AIG.toCNF_equisat
Proof state before:
case mpr
entry : Entrypoint Nat
h : entry.unsat
assign : entry.aig.CNFVar → Bool
⊢ CNF.eval assign
      ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
        (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf) =
    false
Tactic:
apply toCNF.denote_as_go
Proof state after:
case mpr.a
entry : Entrypoint Nat
h : entry.unsat
assign : entry.aig.CNFVar → Bool
⊢ ⟦{ aig := entry.aig, ref := { gate := entry.ref.gate, hgate := ⋯ } }, toCNF.projectLeftAssign assign⟧ = false
Theorem: AIG.toCNF_equisat
Proof state before:
case mpr.a
entry : Entrypoint Nat
h : entry.unsat
assign : entry.aig.CNFVar → Bool
⊢ ⟦{ aig := entry.aig, ref := { gate := entry.ref.gate, hgate := ⋯ } }, toCNF.projectLeftAssign assign⟧ = false
Tactic:
specialize h (toCNF.projectLeftAssign assign)
Proof state after:
case mpr.a
entry : Entrypoint Nat
assign : entry.aig.CNFVar → Bool
h : ⟦{ aig := entry.aig, ref := { gate := entry.ref.gate, hgate := ⋯ } }, toCNF.projectLeftAssign assign⟧ = false
⊢ ⟦{ aig := entry.aig, ref := { gate := entry.ref.gate, hgate := ⋯ } }, toCNF.projectLeftAssign assign⟧ = false
Theorem: AIG.toCNF_equisat
Proof state before:
case mpr.a
entry : Entrypoint Nat
assign : entry.aig.CNFVar → Bool
h : ⟦{ aig := entry.aig, ref := { gate := entry.ref.gate, hgate := ⋯ } }, toCNF.projectLeftAssign assign⟧ = false
⊢ ⟦{ aig := entry.aig, ref := { gate := entry.ref.gate, hgate := ⋯ } }, toCNF.projectLeftAssign assign⟧ = false
Tactic:
assumption
Proof state after:
no goals
Theorem: AIG.toCNF_equisat
Proof state before:
entry : Entrypoint Nat
⊢ ∀ {a b : entry.aig.CNFVar},
    CNF.mem a
        ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
          (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf) →
      CNF.mem b
          ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
            (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf) →
        toCNF.inj a = toCNF.inj b → a = b
Tactic:
intro a b _ _ hinj
Proof state after:
entry : Entrypoint Nat
a b : entry.aig.CNFVar
a✝¹ :
  CNF.mem a
    ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
      (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf)
a✝ :
  CNF.mem b
    ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
      (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf)
hinj : toCNF.inj a = toCNF.inj b
⊢ a = b
Theorem: AIG.toCNF_equisat
Proof state before:
entry : Entrypoint Nat
a b : entry.aig.CNFVar
a✝¹ :
  CNF.mem a
    ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
      (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf)
a✝ :
  CNF.mem b
    ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
      (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf)
hinj : toCNF.inj a = toCNF.inj b
⊢ a = b
Tactic:
apply toCNF.inj_is_injection
Proof state after:
case a
entry : Entrypoint Nat
a b : entry.aig.CNFVar
a✝¹ :
  CNF.mem a
    ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
      (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf)
a✝ :
  CNF.mem b
    ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
      (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf)
hinj : toCNF.inj a = toCNF.inj b
⊢ toCNF.inj a = toCNF.inj b
Theorem: AIG.toCNF_equisat
Proof state before:
case a
entry : Entrypoint Nat
a b : entry.aig.CNFVar
a✝¹ :
  CNF.mem a
    ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
      (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf)
a✝ :
  CNF.mem b
    ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
      (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf)
hinj : toCNF.inj a = toCNF.inj b
⊢ toCNF.inj a = toCNF.inj b
Tactic:
assumption
Proof state after:
no goals
Theorem: bitvec_AndOrXor_1683_2
Proof state before:
⊢ ∀ (a b : BitVec 64), (decide (b ≤ a) || decide ((a != b) = true)) = true
Tactic:
intros
Proof state after:
a✝ b✝ : BitVec 64
⊢ (decide (b✝ ≤ a✝) || decide ((a✝ != b✝) = true)) = true
Theorem: bitvec_AndOrXor_1683_2
Proof state before:
a✝ b✝ : BitVec 64
⊢ (decide (b✝ ≤ a✝) || decide ((a✝ != b✝) = true)) = true
Tactic:
bv_decide
Proof state after:
no goals
Theorem: bitvec_AndOrXor_1247_AB__AB__AB
Proof state before:
⊢ ∀ (A B : BitVec 64), (A &&& B ^^^ -1) &&& (A ||| B) = A ^^^ B
Tactic:
intros
Proof state after:
A✝ B✝ : BitVec 64
⊢ (A✝ &&& B✝ ^^^ -1) &&& (A✝ ||| B✝) = A✝ ^^^ B✝
Theorem: bitvec_AndOrXor_1247_AB__AB__AB
Proof state before:
A✝ B✝ : BitVec 64
⊢ (A✝ &&& B✝ ^^^ -1) &&& (A✝ ||| B✝) = A✝ ^^^ B✝
Tactic:
bv_decide
Proof state after:
no goals
Theorem: BVPred.mkUlt_denote_eq_eval_ult
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
input : aig.BinaryRefStream w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ ⟦{ aig := (mkUlt aig input).aig, ref := (mkUlt aig input).ref }, assign⟧ = lhs.ult rhs
Tactic:
rw [BitVec.ult_eq_not_carry]
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
input : aig.BinaryRefStream w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ ⟦{ aig := (mkUlt aig input).aig, ref := (mkUlt aig input).ref }, assign⟧ = !BitVec.carry w lhs (~~~rhs) true
Theorem: BVPred.mkUlt_denote_eq_eval_ult
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
input : aig.BinaryRefStream w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ ⟦{ aig := (mkUlt aig input).aig, ref := (mkUlt aig input).ref }, assign⟧ = !BitVec.carry w lhs (~~~rhs) true
Tactic:
unfold mkUlt
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
input : aig.BinaryRefStream w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ ⟦{
        aig :=
          (match input with
            | { lhs := lhsRefs, rhs := rhsRefs } =>
              let res := BVExpr.bitblast.blastNot aig rhsRefs;
              let aig_1 := res.aig;
              let rhsRefs_1 := res.stream;
              let res_1 := aig_1.mkConstCached true;
              let aig_2 := res_1.aig;
              let trueRef := res_1.ref;
              let lhsRefs := lhsRefs.cast ⋯;
              let rhsRefs := rhsRefs_1.cast ⋯;
              let res :=
                BVExpr.bitblast.mkOverflowBit aig_2
                  { w := w, stream := { lhs := lhsRefs, rhs := rhsRefs }, cin := trueRef };
              let aig := res.aig;
              let overflowRef := res.ref;
              aig.mkNotCached overflowRef).aig,
        ref :=
          (match input with
            | { lhs := lhsRefs, rhs := rhsRefs } =>
              let res := BVExpr.bitblast.blastNot aig rhsRefs;
              let aig_1 := res.aig;
              let rhsRefs_1 := res.stream;
              let res_1 := aig_1.mkConstCached true;
              let aig_2 := res_1.aig;
              let trueRef := res_1.ref;
              let lhsRefs := lhsRefs.cast ⋯;
              let rhsRefs := rhsRefs_1.cast ⋯;
              let res :=
                BVExpr.bitblast.mkOverflowBit aig_2
                  { w := w, stream := { lhs := lhsRefs, rhs := rhsRefs }, cin := trueRef };
              let aig := res.aig;
              let overflowRef := res.ref;
              aig.mkNotCached overflowRef).ref },
      assign⟧ =
    !BitVec.carry w lhs (~~~rhs) true