-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Convert.lean
theorem CNF.unsat_of_convertLRAT_unsat (cnf : CNF Nat) :
    Unsatisfiable (PosFin (cnf.numLiterals + 1)) (CNF.convertLRAT cnf)
      →
    cnf.Unsat

Proof state:
cnf : CNF Nat
assignment : PosFin (cnf.numLiterals + 1) → Bool
h1 : ¬(assignment ⊨ DefaultFormula.ofArray (convertLRAT' (lift cnf)).toArray)
lratClause : DefaultClause (cnf.numLiterals + 1)
reflectClause : CNF.Clause (PosFin (cnf.numLiterals + 1))
hrclause1 : reflectClause ∈ lift cnf
h2 : ∀ (x : CNF.Clause (PosFin (cnf.numLiterals + 1))), x ∈ lift cnf → CNF.Clause.eval assignment x = true
x✝ : Option (DefaultClause (cnf.numLiterals + 1))
clause✝ : DefaultClause (cnf.numLiterals + 1)
heq : Clause.convertLRAT' reflectClause = some clause✝
hrclause2 : some (some clause✝) = some (some lratClause)
⊢ assignment ⊨ lratClause

Tactic:
rw [← heq] at hrclause2

Result:
cnf : CNF Nat
assignment : PosFin (cnf.numLiterals + 1) → Bool
h1 : ¬(assignment ⊨ DefaultFormula.ofArray (convertLRAT' (lift cnf)).toArray)
lratClause : DefaultClause (cnf.numLiterals + 1)
reflectClause : CNF.Clause (PosFin (cnf.numLiterals + 1))
hrclause1 : reflectClause ∈ lift cnf
h2 : ∀ (x : CNF.Clause (PosFin (cnf.numLiterals + 1))), x ∈ lift cnf → CNF.Clause.eval assignment x = true
x✝ : Option (DefaultClause (cnf.numLiterals + 1))
clause✝ : DefaultClause (cnf.numLiterals + 1)
heq : Clause.convertLRAT' reflectClause = some clause✝
hrclause2 : some (Clause.convertLRAT' reflectClause) = some (some lratClause)
⊢ assignment ⊨ lratClause

Proof state:
case a.a
cnf : CNF Nat
assignment : PosFin (cnf.numLiterals + 1) → Bool
h1 : ¬(assignment ⊨ DefaultFormula.ofArray (convertLRAT' (lift cnf)).toArray)
⊢ ¬CNF.eval assignment (lift cnf) = true

Tactic:
intro h2

Result:
case a.a
cnf : CNF Nat
assignment : PosFin (cnf.numLiterals + 1) → Bool
h1 : ¬(assignment ⊨ DefaultFormula.ofArray (convertLRAT' (lift cnf)).toArray)
h2 : CNF.eval assignment (lift cnf) = true
⊢ False

Proof state:
case a
cnf : CNF Nat
h1 :
  Unsatisfiable (PosFin (cnf.numLiterals + 1))
    (let lifted := lift cnf;
    let lratCnf := convertLRAT' lifted;
    DefaultFormula.ofArray (none :: lratCnf).toArray)
assignment : PosFin (cnf.numLiterals + 1) → Bool
⊢ CNF.eval assignment (lift cnf) = false

Tactic:
replace h1 := (unsat_of_cons_none_unsat _ h1) assignment

Result:
case a
cnf : CNF Nat
assignment : PosFin (cnf.numLiterals + 1) → Bool
h1 : ¬(assignment ⊨ DefaultFormula.ofArray (convertLRAT' (lift cnf)).toArray)
⊢ CNF.eval assignment (lift cnf) = false

Proof state:
case a.a
cnf : CNF Nat
assignment : PosFin (cnf.numLiterals + 1) → Bool
h1 : ¬(assignment ⊨ DefaultFormula.ofArray (convertLRAT' (lift cnf)).toArray)
h2 : CNF.eval assignment (lift cnf) = true
⊢ False

Tactic:
apply h1

Result:
case a.a
cnf : CNF Nat
assignment : PosFin (cnf.numLiterals + 1) → Bool
h1 : ¬(assignment ⊨ DefaultFormula.ofArray (convertLRAT' (lift cnf)).toArray)
h2 : CNF.eval assignment (lift cnf) = true
⊢ assignment ⊨ DefaultFormula.ofArray (convertLRAT' (lift cnf)).toArray

Proof state:
case a.a
cnf : CNF Nat
assignment : PosFin (cnf.numLiterals + 1) → Bool
h1 : ¬(assignment ⊨ DefaultFormula.ofArray (convertLRAT' (lift cnf)).toArray)
h2 : CNF.eval assignment (lift cnf) = true
lratClause : DefaultClause (cnf.numLiterals + 1)
hlclause :
  ∃ a,
    a ∈ lift cnf ∧
      (match Clause.convertLRAT' a with
        | some clause => some (some clause)
        | none => none) =
        some (some lratClause)
⊢ assignment ⊨ lratClause

Tactic:
rcases hlclause with ⟨reflectClause, ⟨hrclause1, hrclause2⟩⟩

Result:
case a.a.intro.intro
cnf : CNF Nat
assignment : PosFin (cnf.numLiterals + 1) → Bool
h1 : ¬(assignment ⊨ DefaultFormula.ofArray (convertLRAT' (lift cnf)).toArray)
h2 : CNF.eval assignment (lift cnf) = true
lratClause : DefaultClause (cnf.numLiterals + 1)
reflectClause : CNF.Clause (PosFin (cnf.numLiterals + 1))
hrclause1 : reflectClause ∈ lift cnf
hrclause2 :
  (match Clause.convertLRAT' reflectClause with
    | some clause => some (some clause)
    | none => none) =
    some (some lratClause)
⊢ assignment ⊨ lratClause

Proof state:
case a
cnf : CNF Nat
h1 : Unsatisfiable (PosFin (cnf.numLiterals + 1)) (convertLRAT cnf)
assignment : PosFin (cnf.numLiterals + 1) → Bool
⊢ CNF.eval assignment (lift cnf) = false

Tactic:
unfold CNF.convertLRAT at h1

Result:
case a
cnf : CNF Nat
h1 :
  Unsatisfiable (PosFin (cnf.numLiterals + 1))
    (let lifted := lift cnf;
    let lratCnf := convertLRAT' lifted;
    DefaultFormula.ofArray (none :: lratCnf).toArray)
assignment : PosFin (cnf.numLiterals + 1) → Bool
⊢ CNF.eval assignment (lift cnf) = false

Proof state:
case a
cnf : CNF Nat
h1 : Unsatisfiable (PosFin (cnf.numLiterals + 1)) (convertLRAT cnf)
⊢ (lift cnf).Unsat

Tactic:
intro assignment

Result:
case a
cnf : CNF Nat
h1 : Unsatisfiable (PosFin (cnf.numLiterals + 1)) (convertLRAT cnf)
assignment : PosFin (cnf.numLiterals + 1) → Bool
⊢ CNF.eval assignment (lift cnf) = false

Proof state:
cnf : CNF Nat
h1 : Unsatisfiable (PosFin (cnf.numLiterals + 1)) (convertLRAT cnf)
⊢ cnf.Unsat

Tactic:
apply CNF.unsat_of_lift_unsat

Result:
case a
cnf : CNF Nat
h1 : Unsatisfiable (PosFin (cnf.numLiterals + 1)) (convertLRAT cnf)
⊢ (lift cnf).Unsat

Proof state:
cnf : CNF Nat
assignment : PosFin (cnf.numLiterals + 1) → Bool
h1 : ¬(assignment ⊨ DefaultFormula.ofArray (convertLRAT' (lift cnf)).toArray)
lratClause : DefaultClause (cnf.numLiterals + 1)
reflectClause : CNF.Clause (PosFin (cnf.numLiterals + 1))
hrclause1 : reflectClause ∈ lift cnf
h2 : ∀ (x : CNF.Clause (PosFin (cnf.numLiterals + 1))), x ∈ lift cnf → CNF.Clause.eval assignment x = true
x✝ : Option (DefaultClause (cnf.numLiterals + 1))
clause✝ : DefaultClause (cnf.numLiterals + 1)
heq : Clause.convertLRAT' reflectClause = some clause✝
hrclause2 : Clause.convertLRAT' reflectClause = some lratClause
⊢ assignment ⊨ lratClause

Tactic:
simp [CNF.Clause.convertLRAT_sat_of_sat reflectClause hrclause2, h2 reflectClause hrclause1]

Result:
no goals

Proof state:
case a.a
cnf : CNF Nat
assignment : PosFin (cnf.numLiterals + 1) → Bool
h1 : ¬(assignment ⊨ DefaultFormula.ofArray (convertLRAT' (lift cnf)).toArray)
h2 : CNF.eval assignment (lift cnf) = true
lratClause : DefaultClause (cnf.numLiterals + 1)
hlclause : lratClause ∈ Formula.toList (DefaultFormula.ofArray (convertLRAT' (lift cnf)).toArray)
⊢ assignment ⊨ lratClause

Tactic:
simp only [Formula.toList, DefaultFormula.toList, DefaultFormula.ofArray,
  CNF.convertLRAT', Array.size_toArray, List.length_map, Array.toList_toArray,
  List.map_nil, List.append_nil, List.mem_filterMap, List.mem_map, id_eq, exists_eq_right] at hlclause

Result:
case a.a
cnf : CNF Nat
assignment : PosFin (cnf.numLiterals + 1) → Bool
h1 : ¬(assignment ⊨ DefaultFormula.ofArray (convertLRAT' (lift cnf)).toArray)
h2 : CNF.eval assignment (lift cnf) = true
lratClause : DefaultClause (cnf.numLiterals + 1)
hlclause :
  ∃ a,
    a ∈ lift cnf ∧
      (match Clause.convertLRAT' a with
        | some clause => some (some clause)
        | none => none) =
        some (some lratClause)
⊢ assignment ⊨ lratClause

Proof state:
case a.a.intro.intro.h_2
cnf : CNF Nat
assignment : PosFin (cnf.numLiterals + 1) → Bool
h1 : ¬(assignment ⊨ DefaultFormula.ofArray (convertLRAT' (lift cnf)).toArray)
lratClause : DefaultClause (cnf.numLiterals + 1)
reflectClause : CNF.Clause (PosFin (cnf.numLiterals + 1))
hrclause1 : reflectClause ∈ lift cnf
h2 : ∀ (x : CNF.Clause (PosFin (cnf.numLiterals + 1))), x ∈ lift cnf → CNF.Clause.eval assignment x = true
x✝ : Option (DefaultClause (cnf.numLiterals + 1))
heq✝ : Clause.convertLRAT' reflectClause = none
hrclause2 : none = some (some lratClause)
⊢ assignment ⊨ lratClause

Tactic:
contradiction

Result:
no goals