internlm/Lean-Github huggingface dataset:
Theorem: AIG.toCNF.State.IsExtensionBy_trans_left
Proof state before:
aig : AIG Nat
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
state1 state2 state3 : State aig
h12 : state1.IsExtensionBy state2 new1 hnew1
h23 : state2.IsExtensionBy state3 new2 hnew2
⊢ state1.IsExtensionBy state3 new1 hnew1
Tactic:
apply  Cache.IsExtensionBy_trans_left
Proof state after:
case h12
aig : AIG Nat
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
state1 state2 state3 : State aig
h12 : state1.IsExtensionBy state2 new1 hnew1
h23 : state2.IsExtensionBy state3 new2 hnew2
⊢ state1.cache.IsExtensionBy ?cache2 new1 hnew1

case h23
aig : AIG Nat
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
state1 state2 state3 : State aig
h12 : state1.IsExtensionBy state2 new1 hnew1
h23 : state2.IsExtensionBy state3 new2 hnew2
⊢ ?cache2.IsExtensionBy state3.cache ?new2 ?hnew2

case cnf2
aig : AIG Nat
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
state1 state2 state3 : State aig
h12 : state1.IsExtensionBy state2 new1 hnew1
h23 : state2.IsExtensionBy state3 new2 hnew2
⊢ CNF aig.CNFVar

case new2
aig : AIG Nat
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
state1 state2 state3 : State aig
h12 : state1.IsExtensionBy state2 new1 hnew1
h23 : state2.IsExtensionBy state3 new2 hnew2
⊢ Nat

case hnew2
aig : AIG Nat
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
state1 state2 state3 : State aig
h12 : state1.IsExtensionBy state2 new1 hnew1
h23 : state2.IsExtensionBy state3 new2 hnew2
⊢ ?new2 < aig.decls.size

case cache2
aig : AIG Nat
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
state1 state2 state3 : State aig
h12 : state1.IsExtensionBy state2 new1 hnew1
h23 : state2.IsExtensionBy state3 new2 hnew2
⊢ Cache aig ?cnf2
Theorem: AIG.toCNF.State.IsExtensionBy_trans_left
Proof state before:
case h12
aig : AIG Nat
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
state1 state2 state3 : State aig
h12 : state1.IsExtensionBy state2 new1 hnew1
h23 : state2.IsExtensionBy state3 new2 hnew2
⊢ state1.cache.IsExtensionBy ?cache2 new1 hnew1

case h23
aig : AIG Nat
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
state1 state2 state3 : State aig
h12 : state1.IsExtensionBy state2 new1 hnew1
h23 : state2.IsExtensionBy state3 new2 hnew2
⊢ ?cache2.IsExtensionBy state3.cache ?new2 ?hnew2

case cnf2
aig : AIG Nat
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
state1 state2 state3 : State aig
h12 : state1.IsExtensionBy state2 new1 hnew1
h23 : state2.IsExtensionBy state3 new2 hnew2
⊢ CNF aig.CNFVar

case new2
aig : AIG Nat
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
state1 state2 state3 : State aig
h12 : state1.IsExtensionBy state2 new1 hnew1
h23 : state2.IsExtensionBy state3 new2 hnew2
⊢ Nat

case hnew2
aig : AIG Nat
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
state1 state2 state3 : State aig
h12 : state1.IsExtensionBy state2 new1 hnew1
h23 : state2.IsExtensionBy state3 new2 hnew2
⊢ ?new2 < aig.decls.size

case cache2
aig : AIG Nat
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
state1 state2 state3 : State aig
h12 : state1.IsExtensionBy state2 new1 hnew1
h23 : state2.IsExtensionBy state3 new2 hnew2
⊢ Cache aig ?cnf2
Tactic:
. exact h12
Proof state after:
case h23
aig : AIG Nat
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
state1 state2 state3 : State aig
h12 : state1.IsExtensionBy state2 new1 hnew1
h23 : state2.IsExtensionBy state3 new2 hnew2
⊢ state2.cache.IsExtensionBy state3.cache ?new2 ?hnew2

case new2
aig : AIG Nat
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
state1 state2 state3 : State aig
h12 : state1.IsExtensionBy state2 new1 hnew1
h23 : state2.IsExtensionBy state3 new2 hnew2
⊢ Nat

case hnew2
aig : AIG Nat
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
state1 state2 state3 : State aig
h12 : state1.IsExtensionBy state2 new1 hnew1
h23 : state2.IsExtensionBy state3 new2 hnew2
⊢ ?new2 < aig.decls.size
Theorem: AIG.toCNF.State.IsExtensionBy_trans_left
Proof state before:
case h23
aig : AIG Nat
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
state1 state2 state3 : State aig
h12 : state1.IsExtensionBy state2 new1 hnew1
h23 : state2.IsExtensionBy state3 new2 hnew2
⊢ state2.cache.IsExtensionBy state3.cache ?new2 ?hnew2

case new2
aig : AIG Nat
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
state1 state2 state3 : State aig
h12 : state1.IsExtensionBy state2 new1 hnew1
h23 : state2.IsExtensionBy state3 new2 hnew2
⊢ Nat

case hnew2
aig : AIG Nat
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
state1 state2 state3 : State aig
h12 : state1.IsExtensionBy state2 new1 hnew1
h23 : state2.IsExtensionBy state3 new2 hnew2
⊢ ?new2 < aig.decls.size
Tactic:
. exact h23
Proof state after:
no goals
Theorem: AIG.toCNF.State.IsExtensionBy_trans_left
Proof state before:
case h12
aig : AIG Nat
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
state1 state2 state3 : State aig
h12 : state1.IsExtensionBy state2 new1 hnew1
h23 : state2.IsExtensionBy state3 new2 hnew2
⊢ state1.cache.IsExtensionBy ?cache2 new1 hnew1
Tactic:
exact h12
Proof state after:
no goals
Theorem: AIG.toCNF.State.IsExtensionBy_trans_left
Proof state before:
case h23
aig : AIG Nat
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
state1 state2 state3 : State aig
h12 : state1.IsExtensionBy state2 new1 hnew1
h23 : state2.IsExtensionBy state3 new2 hnew2
⊢ state2.cache.IsExtensionBy state3.cache ?new2 ?hnew2
Tactic:
exact h23
Proof state after:
no goals
Theorem: AIG.toCNF.State.IsExtensionBy_trans_right
Proof state before:
aig : AIG Nat
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
state1 state2 state3 : State aig
h12 : state1.IsExtensionBy state2 new1 hnew1
h23 : state2.IsExtensionBy state3 new2 hnew2
⊢ state1.IsExtensionBy state3 new2 hnew2
Tactic:
apply  Cache.IsExtensionBy_trans_right
Proof state after:
case h12
aig : AIG Nat
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
state1 state2 state3 : State aig
h12 : state1.IsExtensionBy state2 new1 hnew1
h23 : state2.IsExtensionBy state3 new2 hnew2
⊢ state1.cache.IsExtensionBy ?cache2 ?new1 ?hnew1

case h23
aig : AIG Nat
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
state1 state2 state3 : State aig
h12 : state1.IsExtensionBy state2 new1 hnew1
h23 : state2.IsExtensionBy state3 new2 hnew2
⊢ ?cache2.IsExtensionBy state3.cache new2 hnew2

case cnf2
aig : AIG Nat
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
state1 state2 state3 : State aig
h12 : state1.IsExtensionBy state2 new1 hnew1
h23 : state2.IsExtensionBy state3 new2 hnew2
⊢ CNF aig.CNFVar

case new1
aig : AIG Nat
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
state1 state2 state3 : State aig
h12 : state1.IsExtensionBy state2 new1 hnew1
h23 : state2.IsExtensionBy state3 new2 hnew2
⊢ Nat

case hnew1
aig : AIG Nat
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
state1 state2 state3 : State aig
h12 : state1.IsExtensionBy state2 new1 hnew1
h23 : state2.IsExtensionBy state3 new2 hnew2
⊢ ?new1 < aig.decls.size

case cache2
aig : AIG Nat
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
state1 state2 state3 : State aig
h12 : state1.IsExtensionBy state2 new1 hnew1
h23 : state2.IsExtensionBy state3 new2 hnew2
⊢ Cache aig ?cnf2
Theorem: AIG.toCNF.State.IsExtensionBy_trans_right
Proof state before:
case h12
aig : AIG Nat
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
state1 state2 state3 : State aig
h12 : state1.IsExtensionBy state2 new1 hnew1
h23 : state2.IsExtensionBy state3 new2 hnew2
⊢ state1.cache.IsExtensionBy ?cache2 ?new1 ?hnew1

case h23
aig : AIG Nat
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
state1 state2 state3 : State aig
h12 : state1.IsExtensionBy state2 new1 hnew1
h23 : state2.IsExtensionBy state3 new2 hnew2
⊢ ?cache2.IsExtensionBy state3.cache new2 hnew2

case cnf2
aig : AIG Nat
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
state1 state2 state3 : State aig
h12 : state1.IsExtensionBy state2 new1 hnew1
h23 : state2.IsExtensionBy state3 new2 hnew2
⊢ CNF aig.CNFVar

case new1
aig : AIG Nat
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
state1 state2 state3 : State aig
h12 : state1.IsExtensionBy state2 new1 hnew1
h23 : state2.IsExtensionBy state3 new2 hnew2
⊢ Nat

case hnew1
aig : AIG Nat
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
state1 state2 state3 : State aig
h12 : state1.IsExtensionBy state2 new1 hnew1
h23 : state2.IsExtensionBy state3 new2 hnew2
⊢ ?new1 < aig.decls.size

case cache2
aig : AIG Nat
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
state1 state2 state3 : State aig
h12 : state1.IsExtensionBy state2 new1 hnew1
h23 : state2.IsExtensionBy state3 new2 hnew2
⊢ Cache aig ?cnf2
Tactic:
. exact h12
Proof state after:
case h23
aig : AIG Nat
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
state1 state2 state3 : State aig
h12 : state1.IsExtensionBy state2 new1 hnew1
h23 : state2.IsExtensionBy state3 new2 hnew2
⊢ state2.cache.IsExtensionBy state3.cache new2 hnew2
Theorem: AIG.toCNF.State.IsExtensionBy_trans_right
Proof state before:
case h23
aig : AIG Nat
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
state1 state2 state3 : State aig
h12 : state1.IsExtensionBy state2 new1 hnew1
h23 : state2.IsExtensionBy state3 new2 hnew2
⊢ state2.cache.IsExtensionBy state3.cache new2 hnew2
Tactic:
. exact h23
Proof state after:
no goals
Theorem: AIG.toCNF.State.IsExtensionBy_trans_right
Proof state before:
case h12
aig : AIG Nat
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
state1 state2 state3 : State aig
h12 : state1.IsExtensionBy state2 new1 hnew1
h23 : state2.IsExtensionBy state3 new2 hnew2
⊢ state1.cache.IsExtensionBy ?cache2 ?new1 ?hnew1
Tactic:
exact h12
Proof state after:
no goals
Theorem: AIG.toCNF.State.IsExtensionBy_trans_right
Proof state before:
case h23
aig : AIG Nat
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
state1 state2 state3 : State aig
h12 : state1.IsExtensionBy state2 new1 hnew1
h23 : state2.IsExtensionBy state3 new2 hnew2
⊢ state2.cache.IsExtensionBy state3.cache new2 hnew2
Tactic:
exact h23
Proof state after:
no goals
Theorem: AIG.toCNF.State.IsExtensionBy_rfl
Proof state before:
aig : AIG Nat
idx : Nat
omega : idx < aig.decls.size
state : State aig
h : idx < state.cache.marks.size
hmarked : state.cache.marks[idx] = true
⊢ state.IsExtensionBy state idx ⋯
Tactic:
apply Cache.IsExtensionBy_rfl <;> assumption
Proof state after:
no goals
Theorem: AIG.toCNF.State.eval_eq
Proof state before:
aig✝ : AIG Nat
state : State aig✝
assign : aig✝.CNFVar → Bool
⊢ state.eval assign = CNF.eval assign state.cnf
Tactic:
simp [State.eval]
Proof state after:
no goals
Theorem: AIG.toCNF.State.sat_eq
Proof state before:
aig✝ : AIG Nat
state : State aig✝
assign : aig✝.CNFVar → Bool
⊢ state.sat assign = state.cnf.sat assign
Tactic:
simp [State.sat]
Proof state after:
no goals
Theorem: AIG.toCNF.State.unsat_eq
Proof state before:
aig✝ : AIG Nat
state : State aig✝
⊢ state.unsat = state.cnf.unsat
Tactic:
simp [State.unsat]
Proof state after:
no goals
Theorem: AIG.toCNF.inj_is_injection
Proof state before:
aig : AIG Nat
a b : aig.CNFVar
⊢ inj a = inj b → a = b
Tactic:
intro h
Proof state after:
aig : AIG Nat
a b : aig.CNFVar
h : inj a = inj b
⊢ a = b
Theorem: AIG.toCNF.inj_is_injection
Proof state before:
aig : AIG Nat
a b : aig.CNFVar
h : inj a = inj b
⊢ a = b
Tactic:
cases a with
| inl =>
  cases b with
  | inl =>
    dsimp [inj] at h
    apply congrArg
    apply Nat.add_left_cancel
    exact h
  | inr rhs =>
    exfalso
    dsimp [inj] at h
    have := rhs.isLt
    omega
| inr lhs =>
  cases b with
  | inl =>
    exfalso
    dsimp [inj] at h
    have := lhs.isLt
    omega
  | inr =>
    dsimp [inj] at h
    apply congrArg
    apply Fin.eq_of_val_eq
    exact h
Proof state after:
no goals
Theorem: AIG.toCNF.inj_is_injection
Proof state before:
case inl
aig : AIG Nat
b : aig.CNFVar
val✝ : Nat
h : inj (Sum.inl val✝) = inj b
⊢ Sum.inl val✝ = b
Tactic:
cases b with
| inl =>
  dsimp [inj] at h
  apply congrArg
  apply Nat.add_left_cancel
  exact h
| inr rhs =>
  exfalso
  dsimp [inj] at h
  have := rhs.isLt
  omega
Proof state after:
no goals
Theorem: AIG.toCNF.inj_is_injection
Proof state before:
case inl.inl
aig : AIG Nat
val✝¹ val✝ : Nat
h : inj (Sum.inl val✝¹) = inj (Sum.inl val✝)
⊢ Sum.inl val✝¹ = Sum.inl val✝
Tactic:
dsimp [inj] at h
Proof state after:
case inl.inl
aig : AIG Nat
val✝¹ val✝ : Nat
h : aig.decls.size + val✝¹ = aig.decls.size + val✝
⊢ Sum.inl val✝¹ = Sum.inl val✝
Theorem: AIG.toCNF.inj_is_injection
Proof state before:
case inl.inl
aig : AIG Nat
val✝¹ val✝ : Nat
h : aig.decls.size + val✝¹ = aig.decls.size + val✝
⊢ Sum.inl val✝¹ = Sum.inl val✝
Tactic:
apply congrArg
Proof state after:
case inl.inl.h
aig : AIG Nat
val✝¹ val✝ : Nat
h : aig.decls.size + val✝¹ = aig.decls.size + val✝
⊢ val✝¹ = val✝
Theorem: AIG.toCNF.inj_is_injection
Proof state before:
case inl.inl.h
aig : AIG Nat
val✝¹ val✝ : Nat
h : aig.decls.size + val✝¹ = aig.decls.size + val✝
⊢ val✝¹ = val✝
Tactic:
apply Nat.add_left_cancel
Proof state after:
case inl.inl.h.a
aig : AIG Nat
val✝¹ val✝ : Nat
h : aig.decls.size + val✝¹ = aig.decls.size + val✝
⊢ ?inl.inl.h.n + val✝¹ = ?inl.inl.h.n + val✝

case inl.inl.h.n
aig : AIG Nat
val✝¹ val✝ : Nat
h : aig.decls.size + val✝¹ = aig.decls.size + val✝
⊢ Nat
Theorem: AIG.toCNF.inj_is_injection
Proof state before:
case inl.inl.h.a
aig : AIG Nat
val✝¹ val✝ : Nat
h : aig.decls.size + val✝¹ = aig.decls.size + val✝
⊢ ?inl.inl.h.n + val✝¹ = ?inl.inl.h.n + val✝

case inl.inl.h.n
aig : AIG Nat
val✝¹ val✝ : Nat
h : aig.decls.size + val✝¹ = aig.decls.size + val✝
⊢ Nat
Tactic:
exact h
Proof state after:
no goals
Theorem: AIG.toCNF.inj_is_injection
Proof state before:
case inl.inr
aig : AIG Nat
val✝ : Nat
rhs : Fin aig.decls.size
h : inj (Sum.inl val✝) = inj (Sum.inr rhs)
⊢ Sum.inl val✝ = Sum.inr rhs
Tactic:
exfalso
Proof state after:
case inl.inr
aig : AIG Nat
val✝ : Nat
rhs : Fin aig.decls.size
h : inj (Sum.inl val✝) = inj (Sum.inr rhs)
⊢ False
Theorem: AIG.toCNF.inj_is_injection
Proof state before:
case inl.inr
aig : AIG Nat
val✝ : Nat
rhs : Fin aig.decls.size
h : inj (Sum.inl val✝) = inj (Sum.inr rhs)
⊢ False
Tactic:
dsimp [inj] at h
Proof state after:
case inl.inr
aig : AIG Nat
val✝ : Nat
rhs : Fin aig.decls.size
h : aig.decls.size + val✝ = ↑rhs
⊢ False
Theorem: AIG.toCNF.inj_is_injection
Proof state before:
case inl.inr
aig : AIG Nat
val✝ : Nat
rhs : Fin aig.decls.size
h : aig.decls.size + val✝ = ↑rhs
⊢ False
Tactic:
have := rhs.isLt
Proof state after:
case inl.inr
aig : AIG Nat
val✝ : Nat
rhs : Fin aig.decls.size
h : aig.decls.size + val✝ = ↑rhs
this : ↑rhs < aig.decls.size
⊢ False
Theorem: AIG.toCNF.inj_is_injection
Proof state before:
case inl.inr
aig : AIG Nat
val✝ : Nat
rhs : Fin aig.decls.size
h : aig.decls.size + val✝ = ↑rhs
this : ↑rhs < aig.decls.size
⊢ False
Tactic:
omega
Proof state after:
no goals
Theorem: AIG.toCNF.inj_is_injection
Proof state before:
case inr
aig : AIG Nat
b : aig.CNFVar
lhs : Fin aig.decls.size
h : inj (Sum.inr lhs) = inj b
⊢ Sum.inr lhs = b
Tactic:
cases b with
| inl =>
  exfalso
  dsimp [inj] at h
  have := lhs.isLt
  omega
| inr =>
  dsimp [inj] at h
  apply congrArg
  apply Fin.eq_of_val_eq
  exact h
Proof state after:
no goals
Theorem: AIG.toCNF.inj_is_injection
Proof state before:
case inr.inl
aig : AIG Nat
lhs : Fin aig.decls.size
val✝ : Nat
h : inj (Sum.inr lhs) = inj (Sum.inl val✝)
⊢ Sum.inr lhs = Sum.inl val✝
Tactic:
exfalso
Proof state after:
case inr.inl
aig : AIG Nat
lhs : Fin aig.decls.size
val✝ : Nat
h : inj (Sum.inr lhs) = inj (Sum.inl val✝)
⊢ False
Theorem: AIG.toCNF.inj_is_injection
Proof state before:
case inr.inl
aig : AIG Nat
lhs : Fin aig.decls.size
val✝ : Nat
h : inj (Sum.inr lhs) = inj (Sum.inl val✝)
⊢ False
Tactic:
dsimp [inj] at h
Proof state after:
case inr.inl
aig : AIG Nat
lhs : Fin aig.decls.size
val✝ : Nat
h : ↑lhs = aig.decls.size + val✝
⊢ False
Theorem: AIG.toCNF.inj_is_injection
Proof state before:
case inr.inl
aig : AIG Nat
lhs : Fin aig.decls.size
val✝ : Nat
h : ↑lhs = aig.decls.size + val✝
⊢ False
Tactic:
have := lhs.isLt
Proof state after:
case inr.inl
aig : AIG Nat
lhs : Fin aig.decls.size
val✝ : Nat
h : ↑lhs = aig.decls.size + val✝
this : ↑lhs < aig.decls.size
⊢ False
Theorem: AIG.toCNF.inj_is_injection
Proof state before:
case inr.inl
aig : AIG Nat
lhs : Fin aig.decls.size
val✝ : Nat
h : ↑lhs = aig.decls.size + val✝
this : ↑lhs < aig.decls.size
⊢ False
Tactic:
omega
Proof state after:
no goals
Theorem: AIG.toCNF.inj_is_injection
Proof state before:
case inr.inr
aig : AIG Nat
lhs val✝ : Fin aig.decls.size
h : inj (Sum.inr lhs) = inj (Sum.inr val✝)
⊢ Sum.inr lhs = Sum.inr val✝
Tactic:
dsimp [inj] at h
Proof state after:
case inr.inr
aig : AIG Nat
lhs val✝ : Fin aig.decls.size
h : ↑lhs = ↑val✝
⊢ Sum.inr lhs = Sum.inr val✝
Theorem: AIG.toCNF.inj_is_injection
Proof state before:
case inr.inr
aig : AIG Nat
lhs val✝ : Fin aig.decls.size
h : ↑lhs = ↑val✝
⊢ Sum.inr lhs = Sum.inr val✝
Tactic:
apply congrArg
Proof state after:
case inr.inr.h
aig : AIG Nat
lhs val✝ : Fin aig.decls.size
h : ↑lhs = ↑val✝
⊢ lhs = val✝
Theorem: AIG.toCNF.inj_is_injection
Proof state before:
case inr.inr.h
aig : AIG Nat
lhs val✝ : Fin aig.decls.size
h : ↑lhs = ↑val✝
⊢ lhs = val✝
Tactic:
apply Fin.eq_of_val_eq
Proof state after:
case inr.inr.h.a
aig : AIG Nat
lhs val✝ : Fin aig.decls.size
h : ↑lhs = ↑val✝
⊢ ↑lhs = ↑val✝
Theorem: AIG.toCNF.inj_is_injection
Proof state before:
case inr.inr.h.a
aig : AIG Nat
lhs val✝ : Fin aig.decls.size
h : ↑lhs = ↑val✝
⊢ ↑lhs = ↑val✝
Tactic:
exact h
Proof state after:
no goals
Theorem: AIG.toCNF.go_marked
Proof state before:
aig : AIG Nat
start : Nat
h : start < aig.decls.size
state : State aig
⊢ start < (go aig start h state).val.cache.marks.size
Tactic:
have := (go aig start h state).val.cache.hmarks
Proof state after:
aig : AIG Nat
start : Nat
h : start < aig.decls.size
state : State aig
this : (go aig start h state).val.cache.marks.size = aig.decls.size
⊢ start < (go aig start h state).val.cache.marks.size
Theorem: AIG.toCNF.go_marked
Proof state before:
aig : AIG Nat
start : Nat
h : start < aig.decls.size
state : State aig
this : (go aig start h state).val.cache.marks.size = aig.decls.size
⊢ start < (go aig start h state).val.cache.marks.size
Tactic:
omega
Proof state after:
no goals
Theorem: AIG.toCNF.go_sat
Proof state before:
aig : AIG Nat
start : Nat
h1 : start < aig.decls.size
assign1 : Nat → Bool
state : State aig
⊢ (go aig start h1 state).val.sat (cnfSatAssignment aig assign1)
Tactic:
have := (go aig start h1 state).val.inv assign1
Proof state after:
aig : AIG Nat
start : Nat
h1 : start < aig.decls.size
assign1 : Nat → Bool
state : State aig
this : (go aig start h1 state).val.cnf.sat (cnfSatAssignment aig assign1)
⊢ (go aig start h1 state).val.sat (cnfSatAssignment aig assign1)
Theorem: AIG.toCNF.go_sat
Proof state before:
aig : AIG Nat
start : Nat
h1 : start < aig.decls.size
assign1 : Nat → Bool
state : State aig
this : (go aig start h1 state).val.cnf.sat (cnfSatAssignment aig assign1)
⊢ (go aig start h1 state).val.sat (cnfSatAssignment aig assign1)
Tactic:
simp [this]
Proof state after:
no goals
Theorem: AIG.toCNF.go_as_denote
Proof state before:
sat? : Bool
aig : AIG Nat
start : Nat
h1 : start < aig.decls.size
assign1 : Nat → Bool
⊢ (⟦{ aig := aig, ref := { gate := start, hgate := h1 } }, assign1⟧ &&
        (go aig start h1 (State.empty aig)).val.eval (cnfSatAssignment aig assign1)) =
      sat? →
    ⟦{ aig := aig, ref := { gate := start, hgate := h1 } }, assign1⟧ = sat?
Tactic:
intro h
Proof state after:
sat? : Bool
aig : AIG Nat
start : Nat
h1 : start < aig.decls.size
assign1 : Nat → Bool
h :
  (⟦{ aig := aig, ref := { gate := start, hgate := h1 } }, assign1⟧ &&
      (go aig start h1 (State.empty aig)).val.eval (cnfSatAssignment aig assign1)) =
    sat?
⊢ ⟦{ aig := aig, ref := { gate := start, hgate := h1 } }, assign1⟧ = sat?
Theorem: AIG.toCNF.go_as_denote
Proof state before:
sat? : Bool
aig : AIG Nat
start : Nat
h1 : start < aig.decls.size
assign1 : Nat → Bool
h :
  (⟦{ aig := aig, ref := { gate := start, hgate := h1 } }, assign1⟧ &&
      (go aig start h1 (State.empty aig)).val.eval (cnfSatAssignment aig assign1)) =
    sat?
⊢ ⟦{ aig := aig, ref := { gate := start, hgate := h1 } }, assign1⟧ = sat?
Tactic:
have := go_sat aig start h1 assign1 (.empty aig)
Proof state after:
sat? : Bool
aig : AIG Nat
start : Nat
h1 : start < aig.decls.size
assign1 : Nat → Bool
h :
  (⟦{ aig := aig, ref := { gate := start, hgate := h1 } }, assign1⟧ &&
      (go aig start h1 (State.empty aig)).val.eval (cnfSatAssignment aig assign1)) =
    sat?
this : (go aig start h1 (State.empty aig)).val.sat (cnfSatAssignment aig assign1)
⊢ ⟦{ aig := aig, ref := { gate := start, hgate := h1 } }, assign1⟧ = sat?
Theorem: AIG.toCNF.go_as_denote
Proof state before:
sat? : Bool
aig : AIG Nat
start : Nat
h1 : start < aig.decls.size
assign1 : Nat → Bool
h :
  (⟦{ aig := aig, ref := { gate := start, hgate := h1 } }, assign1⟧ &&
      (go aig start h1 (State.empty aig)).val.eval (cnfSatAssignment aig assign1)) =
    sat?
this : (go aig start h1 (State.empty aig)).val.sat (cnfSatAssignment aig assign1)
⊢ ⟦{ aig := aig, ref := { gate := start, hgate := h1 } }, assign1⟧ = sat?
Tactic:
simp [CNF.sat] at this
Proof state after:
sat? : Bool
aig : AIG Nat
start : Nat
h1 : start < aig.decls.size
assign1 : Nat → Bool
h :
  (⟦{ aig := aig, ref := { gate := start, hgate := h1 } }, assign1⟧ &&
      (go aig start h1 (State.empty aig)).val.eval (cnfSatAssignment aig assign1)) =
    sat?
this : CNF.eval (cnfSatAssignment aig assign1) (go aig start h1 (State.empty aig)).val.cnf = true
⊢ ⟦{ aig := aig, ref := { gate := start, hgate := h1 } }, assign1⟧ = sat?
Theorem: AIG.toCNF.go_as_denote
Proof state before:
sat? : Bool
aig : AIG Nat
start : Nat
h1 : start < aig.decls.size
assign1 : Nat → Bool
h :
  (⟦{ aig := aig, ref := { gate := start, hgate := h1 } }, assign1⟧ &&
      (go aig start h1 (State.empty aig)).val.eval (cnfSatAssignment aig assign1)) =
    sat?
this : CNF.eval (cnfSatAssignment aig assign1) (go aig start h1 (State.empty aig)).val.cnf = true
⊢ ⟦{ aig := aig, ref := { gate := start, hgate := h1 } }, assign1⟧ = sat?
Tactic:
simpa [this] using h
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
⊢ ⟦{ 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:
intro h
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
⊢ CNF.eval assign ([(Sum.inr ⟨start, h1⟩, true)] :: (go aig start h1 (State.empty aig)).val.cnf) = false