-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Checker.lean
theorem check_sound (lratProof : Array IntAction) (cnf : CNF Nat) :
    check lratProof cnf → cnf.Unsat

Proof state:
case intro.intro.h_5.intro
lratProof : Array IntAction
cnf : CNF Nat
h1 :
  lratChecker (CNF.convertLRAT cnf)
      (List.filterMap
        (fun actOpt =>
          match actOpt with
          | none => none
          | some (Action.addEmpty id rupHints) => some (Action.addEmpty id rupHints)
          | some (Action.addRup id c rupHints) => some (Action.addRup id c rupHints)
          | some (Action.del ids) => some (Action.del ids)
          | some (Action.addRat id c pivot rupHints ratHints) =>
            if pivot ∈ Clause.toList c then some (Action.addRat id c pivot rupHints ratHints) else none)
        (List.map (intActionToDefaultClauseAction (cnf.numLiterals + 1)) lratProof.toList)) =
    Result.success
action : Action (DefaultClause (cnf.numLiterals + 1)) (PosFin (cnf.numLiterals + 1))
WellFormedActions : IntAction
left✝ : WellFormedActions ∈ lratProof.toList
actOpt✝ : Option (DefaultClauseAction (cnf.numLiterals + 1))
id✝ : Nat
c✝ : DefaultClause (cnf.numLiterals + 1)
pivot✝ : Literal (PosFin (cnf.numLiterals + 1))
rupHints✝ : Array Nat
ratHints✝ : Array (Nat × Array Nat)
heq✝ :
  intActionToDefaultClauseAction (cnf.numLiterals + 1) WellFormedActions =
    some (Action.addRat id✝ c✝ pivot✝ rupHints✝ ratHints✝)
hleft : pivot✝ ∈ Clause.toList c✝
hright : Action.addRat id✝ c✝ pivot✝ rupHints✝ ratHints✝ = action
⊢ WellFormedAction action

Tactic:
simp [WellFormedAction, hleft, ← hright, Clause.limplies_iff_mem]

Result:
no goals

Proof state:
lratProof : Array IntAction
cnf : CNF Nat
h1 :
  lratChecker (CNF.convertLRAT cnf)
      (List.filterMap
        (fun actOpt =>
          match actOpt with
          | none => none
          | some (Action.addEmpty id rupHints) => some (Action.addEmpty id rupHints)
          | some (Action.addRup id c rupHints) => some (Action.addRup id c rupHints)
          | some (Action.del ids) => some (Action.del ids)
          | some (Action.addRat id c pivot rupHints ratHints) =>
            if pivot ∈ Clause.toList c then some (Action.addRat id c pivot rupHints ratHints) else none)
        (List.map (intActionToDefaultClauseAction (cnf.numLiterals + 1)) lratProof.toList)) =
    Result.success
h2 : Unsatisfiable (PosFin (cnf.numLiterals + 1)) (CNF.convertLRAT cnf)
⊢ cnf.Unsat

Tactic:
apply CNF.unsat_of_convertLRAT_unsat

Result:
case a
lratProof : Array IntAction
cnf : CNF Nat
h1 :
  lratChecker (CNF.convertLRAT cnf)
      (List.filterMap
        (fun actOpt =>
          match actOpt with
          | none => none
          | some (Action.addEmpty id rupHints) => some (Action.addEmpty id rupHints)
          | some (Action.addRup id c rupHints) => some (Action.addRup id c rupHints)
          | some (Action.del ids) => some (Action.del ids)
          | some (Action.addRat id c pivot rupHints ratHints) =>
            if pivot ∈ Clause.toList c then some (Action.addRat id c pivot rupHints ratHints) else none)
        (List.map (intActionToDefaultClauseAction (cnf.numLiterals + 1)) lratProof.toList)) =
    Result.success
h2 : Unsatisfiable (PosFin (cnf.numLiterals + 1)) (CNF.convertLRAT cnf)
⊢ Unsatisfiable (PosFin (cnf.numLiterals + 1)) (CNF.convertLRAT cnf)

Proof state:
lratProof : Array IntAction
cnf : CNF Nat
h1 :
  lratChecker (CNF.convertLRAT cnf)
      (List.filterMap
        (fun actOpt =>
          match actOpt with
          | none => none
          | some (Action.addEmpty id rupHints) => some (Action.addEmpty id rupHints)
          | some (Action.addRup id c rupHints) => some (Action.addRup id c rupHints)
          | some (Action.del ids) => some (Action.del ids)
          | some (Action.addRat id c pivot rupHints ratHints) =>
            if pivot ∈ Clause.toList c then some (Action.addRat id c pivot rupHints ratHints) else none)
        (List.map (intActionToDefaultClauseAction (cnf.numLiterals + 1)) lratProof.toList)) =
    Result.success
⊢ Formula.ReadyForRatAdd (CNF.convertLRAT cnf)

Tactic:
apply CNF.convertLRAT_readyForRatAdd

Result:
no goals

Proof state:
lratProof : Array IntAction
cnf : CNF Nat
h1 :
  lratChecker (CNF.convertLRAT cnf)
      (List.filterMap
        (fun actOpt =>
          match actOpt with
          | none => none
          | some (Action.addEmpty id rupHints) => some (Action.addEmpty id rupHints)
          | some (Action.addRup id c rupHints) => some (Action.addRup id c rupHints)
          | some (Action.del ids) => some (Action.del ids)
          | some (Action.addRat id c pivot rupHints ratHints) =>
            if pivot ∈ Clause.toList c then some (Action.addRat id c pivot rupHints ratHints) else none)
        (List.map (intActionToDefaultClauseAction (cnf.numLiterals + 1)) lratProof.toList)) =
    Result.success
action : Action (DefaultClause (cnf.numLiterals + 1)) (PosFin (cnf.numLiterals + 1))
h :
  action ∈
    List.filterMap
      (fun actOpt =>
        match actOpt with
        | none => none
        | some (Action.addEmpty id rupHints) => some (Action.addEmpty id rupHints)
        | some (Action.addRup id c rupHints) => some (Action.addRup id c rupHints)
        | some (Action.del ids) => some (Action.del ids)
        | some (Action.addRat id c pivot rupHints ratHints) =>
          if pivot ∈ Clause.toList c then some (Action.addRat id c pivot rupHints ratHints) else none)
      (List.map (intActionToDefaultClauseAction (cnf.numLiterals + 1)) lratProof.toList)
⊢ WellFormedAction action

Tactic:
simp only [List.filterMap_map, List.mem_filterMap, Function.comp_apply] at h

Result:
lratProof : Array IntAction
cnf : CNF Nat
h1 :
  lratChecker (CNF.convertLRAT cnf)
      (List.filterMap
        (fun actOpt =>
          match actOpt with
          | none => none
          | some (Action.addEmpty id rupHints) => some (Action.addEmpty id rupHints)
          | some (Action.addRup id c rupHints) => some (Action.addRup id c rupHints)
          | some (Action.del ids) => some (Action.del ids)
          | some (Action.addRat id c pivot rupHints ratHints) =>
            if pivot ∈ Clause.toList c then some (Action.addRat id c pivot rupHints ratHints) else none)
        (List.map (intActionToDefaultClauseAction (cnf.numLiterals + 1)) lratProof.toList)) =
    Result.success
action : Action (DefaultClause (cnf.numLiterals + 1)) (PosFin (cnf.numLiterals + 1))
h :
  ∃ a,
    a ∈ lratProof.toList ∧
      (match intActionToDefaultClauseAction (cnf.numLiterals + 1) a with
        | none => none
        | some (Action.addEmpty id rupHints) => some (Action.addEmpty id rupHints)
        | some (Action.addRup id c rupHints) => some (Action.addRup id c rupHints)
        | some (Action.del ids) => some (Action.del ids)
        | some (Action.addRat id c pivot rupHints ratHints) =>
          if pivot ∈ Clause.toList c then some (Action.addRat id c pivot rupHints ratHints) else none) =
        some action
⊢ WellFormedAction action