Theorem: BVDecide.verifyCert_correct (LeanSAT/Reflect/LRAT.lean)

State before:
⊢ ∀ (cnf : CNF Nat) (cert : LratCert), verifyCert (LratFormula.ofCnf cnf) cert = true → cnf.unsat
Tactic:
intro c b h1
State after:
c : CNF Nat
b : LratCert
h1 : verifyCert (LratFormula.ofCnf c) b = true
⊢ c.unsat

State before:
c : CNF Nat
b : LratCert
h1 : verifyCert (LratFormula.ofCnf c) b = true
⊢ c.unsat
Tactic:
dsimp[verifyCert] at h1
State after:
c : CNF Nat
b : LratCert
h1 :
  (match LRAT.parseLRATProof (String.toUTF8 b) with
    | some lratProof =>
      decide
        (LRAT.lratChecker (LratFormula.ofCnf c).formula
            (List.map Subtype.val
              (List.filterMap
                (fun actOpt =>
                  match actOpt with
                  | none => none
                  | some (LRAT.Action.addEmpty id rupHints) => some ⟨LRAT.Action.addEmpty id rupHints, True.intro⟩
                  | some (LRAT.Action.addRup id c_1 rupHints) => some ⟨LRAT.Action.addRup id c_1 rupHints, True.intro⟩
                  | some (LRAT.Action.del ids) => some ⟨LRAT.Action.del ids, True.intro⟩
                  | some (LRAT.Action.addRat id c_1 pivot rupHints ratHints) =>
                    if h : pivot ∈ LRAT.Clause.toList c_1 then
                      some ⟨LRAT.Action.addRat id c_1 pivot rupHints ratHints, ⋯⟩
                    else none)
                (List.map (LRAT.intActionToDefaultClauseAction ((LratFormula.ofCnf c).numVars + 1))
                  lratProof.toList))) =
          LRAT.Result.success)
    | none => false) =
    true
⊢ c.unsat

State before:
c : CNF Nat
b : LratCert
h1 :
  (match LRAT.parseLRATProof (String.toUTF8 b) with
    | some lratProof =>
      decide
        (LRAT.lratChecker (LratFormula.ofCnf c).formula
            (List.map Subtype.val
              (List.filterMap
                (fun actOpt =>
                  match actOpt with
                  | none => none
                  | some (LRAT.Action.addEmpty id rupHints) => some ⟨LRAT.Action.addEmpty id rupHints, True.intro⟩
                  | some (LRAT.Action.addRup id c_1 rupHints) => some ⟨LRAT.Action.addRup id c_1 rupHints, True.intro⟩
                  | some (LRAT.Action.del ids) => some ⟨LRAT.Action.del ids, True.intro⟩
                  | some (LRAT.Action.addRat id c_1 pivot rupHints ratHints) =>
                    if h : pivot ∈ LRAT.Clause.toList c_1 then
                      some ⟨LRAT.Action.addRat id c_1 pivot rupHints ratHints, ⋯⟩
                    else none)
                (List.map (LRAT.intActionToDefaultClauseAction ((LratFormula.ofCnf c).numVars + 1))
                  lratProof.toList))) =
          LRAT.Result.success)
    | none => false) =
    true
⊢ c.unsat
Tactic:
split at h1
State after:
case h_1
c : CNF Nat
b : LratCert
x✝ : Option (Array LRAT.IntAction)
lratProof✝ : Array LRAT.IntAction
heq✝ : LRAT.parseLRATProof (String.toUTF8 b) = some lratProof✝
h1 :
  decide
      (LRAT.lratChecker (LratFormula.ofCnf c).formula
          (List.map Subtype.val
            (List.filterMap
              (fun actOpt =>
                match actOpt with
                | none => none
                | some (LRAT.Action.addEmpty id rupHints) => some ⟨LRAT.Action.addEmpty id rupHints, True.intro⟩
                | some (LRAT.Action.addRup id c_1 rupHints) => some ⟨LRAT.Action.addRup id c_1 rupHints, True.intro⟩
                | some (LRAT.Action.del ids) => some ⟨LRAT.Action.del ids, True.intro⟩
                | some (LRAT.Action.addRat id c_1 pivot rupHints ratHints) =>
                  if h : pivot ∈ LRAT.Clause.toList c_1 then some ⟨LRAT.Action.addRat id c_1 pivot rupHints ratHints, ⋯⟩
                  else none)
              (List.map (LRAT.intActionToDefaultClauseAction ((LratFormula.ofCnf c).numVars + 1)) lratProof✝.toList))) =
        LRAT.Result.success) =
    true
⊢ c.unsat

case h_2
c : CNF Nat
b : LratCert
x✝ : Option (Array LRAT.IntAction)
heq✝ : LRAT.parseLRATProof (String.toUTF8 b) = none
h1 : false = true
⊢ c.unsat

State before:
case h_1
c : CNF Nat
b : LratCert
x✝ : Option (Array LRAT.IntAction)
lratProof✝ : Array LRAT.IntAction
heq✝ : LRAT.parseLRATProof (String.toUTF8 b) = some lratProof✝
h1 :
  decide
      (LRAT.lratChecker (LratFormula.ofCnf c).formula
          (List.map Subtype.val
            (List.filterMap
              (fun actOpt =>
                match actOpt with
                | none => none
                | some (LRAT.Action.addEmpty id rupHints) => some ⟨LRAT.Action.addEmpty id rupHints, True.intro⟩
                | some (LRAT.Action.addRup id c_1 rupHints) => some ⟨LRAT.Action.addRup id c_1 rupHints, True.intro⟩
                | some (LRAT.Action.del ids) => some ⟨LRAT.Action.del ids, True.intro⟩
                | some (LRAT.Action.addRat id c_1 pivot rupHints ratHints) =>
                  if h : pivot ∈ LRAT.Clause.toList c_1 then some ⟨LRAT.Action.addRat id c_1 pivot rupHints ratHints, ⋯⟩
                  else none)
              (List.map (LRAT.intActionToDefaultClauseAction ((LratFormula.ofCnf c).numVars + 1)) lratProof✝.toList))) =
        LRAT.Result.success) =
    true
⊢ c.unsat

case h_2
c : CNF Nat
b : LratCert
x✝ : Option (Array LRAT.IntAction)
heq✝ : LRAT.parseLRATProof (String.toUTF8 b) = none
h1 : false = true
⊢ c.unsat
Tactic:
. simp only [decide_eq_true_eq] at h1
  have h2 :=
    lratCheckerSound
      _
      (by apply CNF.convertLRAT_readfyForRupAdd)
      (by apply CNF.convertLRAT_readfyForRatAdd)
      _
      (by
        intro action h
        simp only [List.mem_map, List.mem_filterMap] at h
        rcases h with ⟨wellFormedActions, _, h2⟩
        rw [← h2]
        exact wellFormedActions.property)
      h1
  apply CNF.unsat_of_lift_unsat c
  intro assignment
  unfold CNF.convertLRAT at h2
  have h2 := (LRAT.unsat_of_cons_none_unsat _ h2) assignment
  apply eq_false_of_ne_true
  intro h3
  apply h2
  simp only [LRAT.Formula.formulaHSat_def, List.all_eq_true, decide_eq_true_eq]
  intro lratClause hlclause
  simp only [LRAT.Formula.toList, LRAT.DefaultFormula.toList, LRAT.DefaultFormula.ofArray,
    CNF.convertLRAT', Array.size_toArray, List.length_map, Array.toList_eq, Array.data_toArray,
    List.map_nil, List.append_nil, List.mem_filterMap, List.mem_map, id_eq, exists_eq_right] at hlclause
  rcases hlclause with ⟨reflectClause, ⟨hrclause1, hrclause2⟩⟩
  simp only [CNF.eval, List.all_eq_true] at h3
  split at hrclause2
  . next heq =>
    rw [← heq] at hrclause2
    simp only [Option.some.injEq] at hrclause2
    simp [CNF.Clause.convertLRAT_sat_of_sat reflectClause hrclause2, h3 reflectClause hrclause1]
  . contradiction
State after:
case h_2
c : CNF Nat
b : LratCert
x✝ : Option (Array LRAT.IntAction)
heq✝ : LRAT.parseLRATProof (String.toUTF8 b) = none
h1 : false = true
⊢ c.unsat

State before:
case h_2
c : CNF Nat
b : LratCert
x✝ : Option (Array LRAT.IntAction)
heq✝ : LRAT.parseLRATProof (String.toUTF8 b) = none
h1 : false = true
⊢ c.unsat
Tactic:
. contradiction
State after:
no goals

State before:
case h_1
c : CNF Nat
b : LratCert
x✝ : Option (Array LRAT.IntAction)
lratProof✝ : Array LRAT.IntAction
heq✝ : LRAT.parseLRATProof (String.toUTF8 b) = some lratProof✝
h1 :
  decide
      (LRAT.lratChecker (LratFormula.ofCnf c).formula
          (List.map Subtype.val
            (List.filterMap
              (fun actOpt =>
                match actOpt with
                | none => none
                | some (LRAT.Action.addEmpty id rupHints) => some ⟨LRAT.Action.addEmpty id rupHints, True.intro⟩
                | some (LRAT.Action.addRup id c_1 rupHints) => some ⟨LRAT.Action.addRup id c_1 rupHints, True.intro⟩
                | some (LRAT.Action.del ids) => some ⟨LRAT.Action.del ids, True.intro⟩
                | some (LRAT.Action.addRat id c_1 pivot rupHints ratHints) =>
                  if h : pivot ∈ LRAT.Clause.toList c_1 then some ⟨LRAT.Action.addRat id c_1 pivot rupHints ratHints, ⋯⟩
                  else none)
              (List.map (LRAT.intActionToDefaultClauseAction ((LratFormula.ofCnf c).numVars + 1)) lratProof✝.toList))) =
        LRAT.Result.success) =
    true
⊢ c.unsat
Tactic:
simp only [decide_eq_true_eq] at h1
State after:
case h_1
c : CNF Nat
b : LratCert
x✝ : Option (Array LRAT.IntAction)
lratProof✝ : Array LRAT.IntAction
heq✝ : LRAT.parseLRATProof (String.toUTF8 b) = some lratProof✝
h1 :
  LRAT.lratChecker (LratFormula.ofCnf c).formula
      (List.map Subtype.val
        (List.filterMap
          (fun actOpt =>
            match actOpt with
            | none => none
            | some (LRAT.Action.addEmpty id rupHints) => some ⟨LRAT.Action.addEmpty id rupHints, True.intro⟩
            | some (LRAT.Action.addRup id c_1 rupHints) => some ⟨LRAT.Action.addRup id c_1 rupHints, True.intro⟩
            | some (LRAT.Action.del ids) => some ⟨LRAT.Action.del ids, True.intro⟩
            | some (LRAT.Action.addRat id c_1 pivot rupHints ratHints) =>
              if h : pivot ∈ LRAT.Clause.toList c_1 then some ⟨LRAT.Action.addRat id c_1 pivot rupHints ratHints, ⋯⟩
              else none)
          (List.map (LRAT.intActionToDefaultClauseAction ((LratFormula.ofCnf c).numVars + 1)) lratProof✝.toList))) =
    LRAT.Result.success
⊢ c.unsat

State before:
case h_1
c : CNF Nat
b : LratCert
x✝ : Option (Array LRAT.IntAction)
lratProof✝ : Array LRAT.IntAction
heq✝ : LRAT.parseLRATProof (String.toUTF8 b) = some lratProof✝
h1 :
  LRAT.lratChecker (LratFormula.ofCnf c).formula
      (List.map Subtype.val
        (List.filterMap
          (fun actOpt =>
            match actOpt with
            | none => none
            | some (LRAT.Action.addEmpty id rupHints) => some ⟨LRAT.Action.addEmpty id rupHints, True.intro⟩
            | some (LRAT.Action.addRup id c_1 rupHints) => some ⟨LRAT.Action.addRup id c_1 rupHints, True.intro⟩
            | some (LRAT.Action.del ids) => some ⟨LRAT.Action.del ids, True.intro⟩
            | some (LRAT.Action.addRat id c_1 pivot rupHints ratHints) =>
              if h : pivot ∈ LRAT.Clause.toList c_1 then some ⟨LRAT.Action.addRat id c_1 pivot rupHints ratHints, ⋯⟩
              else none)
          (List.map (LRAT.intActionToDefaultClauseAction ((LratFormula.ofCnf c).numVars + 1)) lratProof✝.toList))) =
    LRAT.Result.success
⊢ c.unsat
Tactic:
have h2 :=
  lratCheckerSound
    _
    (by apply CNF.convertLRAT_readfyForRupAdd)
    (by apply CNF.convertLRAT_readfyForRatAdd)
    _
    (by
      intro action h
      simp only [List.mem_map, List.mem_filterMap] at h
      rcases h with ⟨wellFormedActions, _, h2⟩
      rw [← h2]
      exact wellFormedActions.property)
    h1
State after:
case h_1
c : CNF Nat
b : LratCert
x✝ : Option (Array LRAT.IntAction)
lratProof✝ : Array LRAT.IntAction
heq✝ : LRAT.parseLRATProof (String.toUTF8 b) = some lratProof✝
h1 :
  LRAT.lratChecker (LratFormula.ofCnf c).formula
      (List.map Subtype.val
        (List.filterMap
          (fun actOpt =>
            match actOpt with
            | none => none
            | some (LRAT.Action.addEmpty id rupHints) => some ⟨LRAT.Action.addEmpty id rupHints, True.intro⟩
            | some (LRAT.Action.addRup id c_1 rupHints) => some ⟨LRAT.Action.addRup id c_1 rupHints, True.intro⟩
            | some (LRAT.Action.del ids) => some ⟨LRAT.Action.del ids, True.intro⟩
            | some (LRAT.Action.addRat id c_1 pivot rupHints ratHints) =>
              if h : pivot ∈ LRAT.Clause.toList c_1 then some ⟨LRAT.Action.addRat id c_1 pivot rupHints ratHints, ⋯⟩
              else none)
          (List.map (LRAT.intActionToDefaultClauseAction ((LratFormula.ofCnf c).numVars + 1)) lratProof✝.toList))) =
    LRAT.Result.success
h2 : unsatisfiable (PosFin ((LratFormula.ofCnf c).numVars + 1)) (LratFormula.ofCnf c).formula
⊢ c.unsat

State before:
case h_1
c : CNF Nat
b : LratCert
x✝ : Option (Array LRAT.IntAction)
lratProof✝ : Array LRAT.IntAction
heq✝ : LRAT.parseLRATProof (String.toUTF8 b) = some lratProof✝
h1 :
  LRAT.lratChecker (LratFormula.ofCnf c).formula
      (List.map Subtype.val
        (List.filterMap
          (fun actOpt =>
            match actOpt with
            | none => none
            | some (LRAT.Action.addEmpty id rupHints) => some ⟨LRAT.Action.addEmpty id rupHints, True.intro⟩
            | some (LRAT.Action.addRup id c_1 rupHints) => some ⟨LRAT.Action.addRup id c_1 rupHints, True.intro⟩
            | some (LRAT.Action.del ids) => some ⟨LRAT.Action.del ids, True.intro⟩
            | some (LRAT.Action.addRat id c_1 pivot rupHints ratHints) =>
              if h : pivot ∈ LRAT.Clause.toList c_1 then some ⟨LRAT.Action.addRat id c_1 pivot rupHints ratHints, ⋯⟩
              else none)
          (List.map (LRAT.intActionToDefaultClauseAction ((LratFormula.ofCnf c).numVars + 1)) lratProof✝.toList))) =
    LRAT.Result.success
h2 : unsatisfiable (PosFin ((LratFormula.ofCnf c).numVars + 1)) (LratFormula.ofCnf c).formula
⊢ c.unsat
Tactic:
apply CNF.unsat_of_lift_unsat c
State after:
case h_1
c : CNF Nat
b : LratCert
x✝ : Option (Array LRAT.IntAction)
lratProof✝ : Array LRAT.IntAction
heq✝ : LRAT.parseLRATProof (String.toUTF8 b) = some lratProof✝
h1 :
  LRAT.lratChecker (LratFormula.ofCnf c).formula
      (List.map Subtype.val
        (List.filterMap
          (fun actOpt =>
            match actOpt with
            | none => none
            | some (LRAT.Action.addEmpty id rupHints) => some ⟨LRAT.Action.addEmpty id rupHints, True.intro⟩
            | some (LRAT.Action.addRup id c_1 rupHints) => some ⟨LRAT.Action.addRup id c_1 rupHints, True.intro⟩
            | some (LRAT.Action.del ids) => some ⟨LRAT.Action.del ids, True.intro⟩
            | some (LRAT.Action.addRat id c_1 pivot rupHints ratHints) =>
              if h : pivot ∈ LRAT.Clause.toList c_1 then some ⟨LRAT.Action.addRat id c_1 pivot rupHints ratHints, ⋯⟩
              else none)
          (List.map (LRAT.intActionToDefaultClauseAction ((LratFormula.ofCnf c).numVars + 1)) lratProof✝.toList))) =
    LRAT.Result.success
h2 : unsatisfiable (PosFin ((LratFormula.ofCnf c).numVars + 1)) (LratFormula.ofCnf c).formula
⊢ c.lift.unsat

State before:
case h_1
c : CNF Nat
b : LratCert
x✝ : Option (Array LRAT.IntAction)
lratProof✝ : Array LRAT.IntAction
heq✝ : LRAT.parseLRATProof (String.toUTF8 b) = some lratProof✝
h1 :
  LRAT.lratChecker (LratFormula.ofCnf c).formula
      (List.map Subtype.val
        (List.filterMap
          (fun actOpt =>
            match actOpt with
            | none => none
            | some (LRAT.Action.addEmpty id rupHints) => some ⟨LRAT.Action.addEmpty id rupHints, True.intro⟩
            | some (LRAT.Action.addRup id c_1 rupHints) => some ⟨LRAT.Action.addRup id c_1 rupHints, True.intro⟩
            | some (LRAT.Action.del ids) => some ⟨LRAT.Action.del ids, True.intro⟩
            | some (LRAT.Action.addRat id c_1 pivot rupHints ratHints) =>
              if h : pivot ∈ LRAT.Clause.toList c_1 then some ⟨LRAT.Action.addRat id c_1 pivot rupHints ratHints, ⋯⟩
              else none)
          (List.map (LRAT.intActionToDefaultClauseAction ((LratFormula.ofCnf c).numVars + 1)) lratProof✝.toList))) =
    LRAT.Result.success
h2 : unsatisfiable (PosFin ((LratFormula.ofCnf c).numVars + 1)) (LratFormula.ofCnf c).formula
⊢ c.lift.unsat
Tactic:
intro assignment
State after:
case h_1
c : CNF Nat
b : LratCert
x✝ : Option (Array LRAT.IntAction)
lratProof✝ : Array LRAT.IntAction
heq✝ : LRAT.parseLRATProof (String.toUTF8 b) = some lratProof✝
h1 :
  LRAT.lratChecker (LratFormula.ofCnf c).formula
      (List.map Subtype.val
        (List.filterMap
          (fun actOpt =>
            match actOpt with
            | none => none
            | some (LRAT.Action.addEmpty id rupHints) => some ⟨LRAT.Action.addEmpty id rupHints, True.intro⟩
            | some (LRAT.Action.addRup id c_1 rupHints) => some ⟨LRAT.Action.addRup id c_1 rupHints, True.intro⟩
            | some (LRAT.Action.del ids) => some ⟨LRAT.Action.del ids, True.intro⟩
            | some (LRAT.Action.addRat id c_1 pivot rupHints ratHints) =>
              if h : pivot ∈ LRAT.Clause.toList c_1 then some ⟨LRAT.Action.addRat id c_1 pivot rupHints ratHints, ⋯⟩
              else none)
          (List.map (LRAT.intActionToDefaultClauseAction ((LratFormula.ofCnf c).numVars + 1)) lratProof✝.toList))) =
    LRAT.Result.success
h2 : unsatisfiable (PosFin ((LratFormula.ofCnf c).numVars + 1)) (LratFormula.ofCnf c).formula
assignment : PosFin (c.numLiterals + 1) → Bool
⊢ CNF.eval assignment c.lift = false

State before:
case h_1
c : CNF Nat
b : LratCert
x✝ : Option (Array LRAT.IntAction)
lratProof✝ : Array LRAT.IntAction
heq✝ : LRAT.parseLRATProof (String.toUTF8 b) = some lratProof✝
h1 :
  LRAT.lratChecker (LratFormula.ofCnf c).formula
      (List.map Subtype.val
        (List.filterMap
          (fun actOpt =>
            match actOpt with
            | none => none
            | some (LRAT.Action.addEmpty id rupHints) => some ⟨LRAT.Action.addEmpty id rupHints, True.intro⟩
            | some (LRAT.Action.addRup id c_1 rupHints) => some ⟨LRAT.Action.addRup id c_1 rupHints, True.intro⟩
            | some (LRAT.Action.del ids) => some ⟨LRAT.Action.del ids, True.intro⟩
            | some (LRAT.Action.addRat id c_1 pivot rupHints ratHints) =>
              if h : pivot ∈ LRAT.Clause.toList c_1 then some ⟨LRAT.Action.addRat id c_1 pivot rupHints ratHints, ⋯⟩
              else none)
          (List.map (LRAT.intActionToDefaultClauseAction ((LratFormula.ofCnf c).numVars + 1)) lratProof✝.toList))) =
    LRAT.Result.success
h2 : unsatisfiable (PosFin ((LratFormula.ofCnf c).numVars + 1)) (LratFormula.ofCnf c).formula
assignment : PosFin (c.numLiterals + 1) → Bool
⊢ CNF.eval assignment c.lift = false
Tactic:
have h2 := (LRAT.unsat_of_cons_none_unsat _ h2) assignment
State after:
case h_1
c : CNF Nat
b : LratCert
x✝ : Option (Array LRAT.IntAction)
lratProof✝ : Array LRAT.IntAction
heq✝ : LRAT.parseLRATProof (String.toUTF8 b) = some lratProof✝
h1 :
  LRAT.lratChecker (LratFormula.ofCnf c).formula
      (List.map Subtype.val
        (List.filterMap
          (fun actOpt =>
            match actOpt with
            | none => none
            | some (LRAT.Action.addEmpty id rupHints) => some ⟨LRAT.Action.addEmpty id rupHints, True.intro⟩
            | some (LRAT.Action.addRup id c_1 rupHints) => some ⟨LRAT.Action.addRup id c_1 rupHints, True.intro⟩
            | some (LRAT.Action.del ids) => some ⟨LRAT.Action.del ids, True.intro⟩
            | some (LRAT.Action.addRat id c_1 pivot rupHints ratHints) =>
              if h : pivot ∈ LRAT.Clause.toList c_1 then some ⟨LRAT.Action.addRat id c_1 pivot rupHints ratHints, ⋯⟩
              else none)
          (List.map (LRAT.intActionToDefaultClauseAction ((LratFormula.ofCnf c).numVars + 1)) lratProof✝.toList))) =
    LRAT.Result.success
h2✝ : unsatisfiable (PosFin ((LratFormula.ofCnf c).numVars + 1)) (LratFormula.ofCnf c).formula
assignment : PosFin (c.numLiterals + 1) → Bool
h2 : ¬(assignment ⊨ LRAT.DefaultFormula.ofArray (List.toArray c.lift.convertLRAT'))
⊢ CNF.eval assignment c.lift = false

State before:
case h_1
c : CNF Nat
b : LratCert
x✝ : Option (Array LRAT.IntAction)
lratProof✝ : Array LRAT.IntAction
heq✝ : LRAT.parseLRATProof (String.toUTF8 b) = some lratProof✝
h1 :
  LRAT.lratChecker (LratFormula.ofCnf c).formula
      (List.map Subtype.val
        (List.filterMap
          (fun actOpt =>
            match actOpt with
            | none => none
            | some (LRAT.Action.addEmpty id rupHints) => some ⟨LRAT.Action.addEmpty id rupHints, True.intro⟩
            | some (LRAT.Action.addRup id c_1 rupHints) => some ⟨LRAT.Action.addRup id c_1 rupHints, True.intro⟩
            | some (LRAT.Action.del ids) => some ⟨LRAT.Action.del ids, True.intro⟩
            | some (LRAT.Action.addRat id c_1 pivot rupHints ratHints) =>
              if h : pivot ∈ LRAT.Clause.toList c_1 then some ⟨LRAT.Action.addRat id c_1 pivot rupHints ratHints, ⋯⟩
              else none)
          (List.map (LRAT.intActionToDefaultClauseAction ((LratFormula.ofCnf c).numVars + 1)) lratProof✝.toList))) =
    LRAT.Result.success
h2✝ : unsatisfiable (PosFin ((LratFormula.ofCnf c).numVars + 1)) (LratFormula.ofCnf c).formula
assignment : PosFin (c.numLiterals + 1) → Bool
h2 : ¬(assignment ⊨ LRAT.DefaultFormula.ofArray (List.toArray c.lift.convertLRAT'))
⊢ CNF.eval assignment c.lift = false
Tactic:
apply eq_false_of_ne_true
State after:
case h_1.a
c : CNF Nat
b : LratCert
x✝ : Option (Array LRAT.IntAction)
lratProof✝ : Array LRAT.IntAction
heq✝ : LRAT.parseLRATProof (String.toUTF8 b) = some lratProof✝
h1 :
  LRAT.lratChecker (LratFormula.ofCnf c).formula
      (List.map Subtype.val
        (List.filterMap
          (fun actOpt =>
            match actOpt with
            | none => none
            | some (LRAT.Action.addEmpty id rupHints) => some ⟨LRAT.Action.addEmpty id rupHints, True.intro⟩
            | some (LRAT.Action.addRup id c_1 rupHints) => some ⟨LRAT.Action.addRup id c_1 rupHints, True.intro⟩
            | some (LRAT.Action.del ids) => some ⟨LRAT.Action.del ids, True.intro⟩
            | some (LRAT.Action.addRat id c_1 pivot rupHints ratHints) =>
              if h : pivot ∈ LRAT.Clause.toList c_1 then some ⟨LRAT.Action.addRat id c_1 pivot rupHints ratHints, ⋯⟩
              else none)
          (List.map (LRAT.intActionToDefaultClauseAction ((LratFormula.ofCnf c).numVars + 1)) lratProof✝.toList))) =
    LRAT.Result.success
h2✝ : unsatisfiable (PosFin ((LratFormula.ofCnf c).numVars + 1)) (LratFormula.ofCnf c).formula
assignment : PosFin (c.numLiterals + 1) → Bool
h2 : ¬(assignment ⊨ LRAT.DefaultFormula.ofArray (List.toArray c.lift.convertLRAT'))
⊢ ¬CNF.eval assignment c.lift = true

State before:
case h_1.a
c : CNF Nat
b : LratCert
x✝ : Option (Array LRAT.IntAction)
lratProof✝ : Array LRAT.IntAction
heq✝ : LRAT.parseLRATProof (String.toUTF8 b) = some lratProof✝
h1 :
  LRAT.lratChecker (LratFormula.ofCnf c).formula
      (List.map Subtype.val
        (List.filterMap
          (fun actOpt =>
            match actOpt with
            | none => none
            | some (LRAT.Action.addEmpty id rupHints) => some ⟨LRAT.Action.addEmpty id rupHints, True.intro⟩
            | some (LRAT.Action.addRup id c_1 rupHints) => some ⟨LRAT.Action.addRup id c_1 rupHints, True.intro⟩
            | some (LRAT.Action.del ids) => some ⟨LRAT.Action.del ids, True.intro⟩
            | some (LRAT.Action.addRat id c_1 pivot rupHints ratHints) =>
              if h : pivot ∈ LRAT.Clause.toList c_1 then some ⟨LRAT.Action.addRat id c_1 pivot rupHints ratHints, ⋯⟩
              else none)
          (List.map (LRAT.intActionToDefaultClauseAction ((LratFormula.ofCnf c).numVars + 1)) lratProof✝.toList))) =
    LRAT.Result.success
h2✝ : unsatisfiable (PosFin ((LratFormula.ofCnf c).numVars + 1)) (LratFormula.ofCnf c).formula
assignment : PosFin (c.numLiterals + 1) → Bool
h2 : ¬(assignment ⊨ LRAT.DefaultFormula.ofArray (List.toArray c.lift.convertLRAT'))
⊢ ¬CNF.eval assignment c.lift = true
Tactic:
intro h3
State after:
case h_1.a
c : CNF Nat
b : LratCert
x✝ : Option (Array LRAT.IntAction)
lratProof✝ : Array LRAT.IntAction
heq✝ : LRAT.parseLRATProof (String.toUTF8 b) = some lratProof✝
h1 :
  LRAT.lratChecker (LratFormula.ofCnf c).formula
      (List.map Subtype.val
        (List.filterMap
          (fun actOpt =>
            match actOpt with
            | none => none
            | some (LRAT.Action.addEmpty id rupHints) => some ⟨LRAT.Action.addEmpty id rupHints, True.intro⟩
            | some (LRAT.Action.addRup id c_1 rupHints) => some ⟨LRAT.Action.addRup id c_1 rupHints, True.intro⟩
            | some (LRAT.Action.del ids) => some ⟨LRAT.Action.del ids, True.intro⟩
            | some (LRAT.Action.addRat id c_1 pivot rupHints ratHints) =>
              if h : pivot ∈ LRAT.Clause.toList c_1 then some ⟨LRAT.Action.addRat id c_1 pivot rupHints ratHints, ⋯⟩
              else none)
          (List.map (LRAT.intActionToDefaultClauseAction ((LratFormula.ofCnf c).numVars + 1)) lratProof✝.toList))) =
    LRAT.Result.success
h2✝ : unsatisfiable (PosFin ((LratFormula.ofCnf c).numVars + 1)) (LratFormula.ofCnf c).formula
assignment : PosFin (c.numLiterals + 1) → Bool
h2 : ¬(assignment ⊨ LRAT.DefaultFormula.ofArray (List.toArray c.lift.convertLRAT'))
h3 : CNF.eval assignment c.lift = true
⊢ False

State before:
case h_1.a
c : CNF Nat
b : LratCert
x✝ : Option (Array LRAT.IntAction)
lratProof✝ : Array LRAT.IntAction
heq✝ : LRAT.parseLRATProof (String.toUTF8 b) = some lratProof✝
h1 :
  LRAT.lratChecker (LratFormula.ofCnf c).formula
      (List.map Subtype.val
        (List.filterMap
          (fun actOpt =>
            match actOpt with
            | none => none
            | some (LRAT.Action.addEmpty id rupHints) => some ⟨LRAT.Action.addEmpty id rupHints, True.intro⟩
            | some (LRAT.Action.addRup id c_1 rupHints) => some ⟨LRAT.Action.addRup id c_1 rupHints, True.intro⟩
            | some (LRAT.Action.del ids) => some ⟨LRAT.Action.del ids, True.intro⟩
            | some (LRAT.Action.addRat id c_1 pivot rupHints ratHints) =>
              if h : pivot ∈ LRAT.Clause.toList c_1 then some ⟨LRAT.Action.addRat id c_1 pivot rupHints ratHints, ⋯⟩
              else none)
          (List.map (LRAT.intActionToDefaultClauseAction ((LratFormula.ofCnf c).numVars + 1)) lratProof✝.toList))) =
    LRAT.Result.success
h2✝ : unsatisfiable (PosFin ((LratFormula.ofCnf c).numVars + 1)) (LratFormula.ofCnf c).formula
assignment : PosFin (c.numLiterals + 1) → Bool
h2 : ¬(assignment ⊨ LRAT.DefaultFormula.ofArray (List.toArray c.lift.convertLRAT'))
h3 : CNF.eval assignment c.lift = true
⊢ False
Tactic:
apply h2
State after:
case h_1.a
c : CNF Nat
b : LratCert
x✝ : Option (Array LRAT.IntAction)
lratProof✝ : Array LRAT.IntAction
heq✝ : LRAT.parseLRATProof (String.toUTF8 b) = some lratProof✝
h1 :
  LRAT.lratChecker (LratFormula.ofCnf c).formula
      (List.map Subtype.val
        (List.filterMap
          (fun actOpt =>
            match actOpt with
            | none => none
            | some (LRAT.Action.addEmpty id rupHints) => some ⟨LRAT.Action.addEmpty id rupHints, True.intro⟩
            | some (LRAT.Action.addRup id c_1 rupHints) => some ⟨LRAT.Action.addRup id c_1 rupHints, True.intro⟩
            | some (LRAT.Action.del ids) => some ⟨LRAT.Action.del ids, True.intro⟩
            | some (LRAT.Action.addRat id c_1 pivot rupHints ratHints) =>
              if h : pivot ∈ LRAT.Clause.toList c_1 then some ⟨LRAT.Action.addRat id c_1 pivot rupHints ratHints, ⋯⟩
              else none)
          (List.map (LRAT.intActionToDefaultClauseAction ((LratFormula.ofCnf c).numVars + 1)) lratProof✝.toList))) =
    LRAT.Result.success
h2✝ : unsatisfiable (PosFin ((LratFormula.ofCnf c).numVars + 1)) (LratFormula.ofCnf c).formula
assignment : PosFin (c.numLiterals + 1) → Bool
h2 : ¬(assignment ⊨ LRAT.DefaultFormula.ofArray (List.toArray c.lift.convertLRAT'))
h3 : CNF.eval assignment c.lift = true
⊢ assignment ⊨ LRAT.DefaultFormula.ofArray (List.toArray c.lift.convertLRAT')

State before:
case h_1.a
c : CNF Nat
b : LratCert
x✝ : Option (Array LRAT.IntAction)
lratProof✝ : Array LRAT.IntAction
heq✝ : LRAT.parseLRATProof (String.toUTF8 b) = some lratProof✝
h1 :
  LRAT.lratChecker (LratFormula.ofCnf c).formula
      (List.map Subtype.val
        (List.filterMap
          (fun actOpt =>
            match actOpt with
            | none => none
            | some (LRAT.Action.addEmpty id rupHints) => some ⟨LRAT.Action.addEmpty id rupHints, True.intro⟩
            | some (LRAT.Action.addRup id c_1 rupHints) => some ⟨LRAT.Action.addRup id c_1 rupHints, True.intro⟩
            | some (LRAT.Action.del ids) => some ⟨LRAT.Action.del ids, True.intro⟩
            | some (LRAT.Action.addRat id c_1 pivot rupHints ratHints) =>
              if h : pivot ∈ LRAT.Clause.toList c_1 then some ⟨LRAT.Action.addRat id c_1 pivot rupHints ratHints, ⋯⟩
              else none)
          (List.map (LRAT.intActionToDefaultClauseAction ((LratFormula.ofCnf c).numVars + 1)) lratProof✝.toList))) =
    LRAT.Result.success
h2✝ : unsatisfiable (PosFin ((LratFormula.ofCnf c).numVars + 1)) (LratFormula.ofCnf c).formula
assignment : PosFin (c.numLiterals + 1) → Bool
h2 : ¬(assignment ⊨ LRAT.DefaultFormula.ofArray (List.toArray c.lift.convertLRAT'))
h3 : CNF.eval assignment c.lift = true
⊢ assignment ⊨ LRAT.DefaultFormula.ofArray (List.toArray c.lift.convertLRAT')
Tactic:
simp only [LRAT.Formula.formulaHSat_def, List.all_eq_true, decide_eq_true_eq]
State after:
case h_1.a
c : CNF Nat
b : LratCert
x✝ : Option (Array LRAT.IntAction)
lratProof✝ : Array LRAT.IntAction
heq✝ : LRAT.parseLRATProof (String.toUTF8 b) = some lratProof✝
h1 :
  LRAT.lratChecker (LratFormula.ofCnf c).formula
      (List.map Subtype.val
        (List.filterMap
          (fun actOpt =>
            match actOpt with
            | none => none
            | some (LRAT.Action.addEmpty id rupHints) => some ⟨LRAT.Action.addEmpty id rupHints, True.intro⟩
            | some (LRAT.Action.addRup id c_1 rupHints) => some ⟨LRAT.Action.addRup id c_1 rupHints, True.intro⟩
            | some (LRAT.Action.del ids) => some ⟨LRAT.Action.del ids, True.intro⟩
            | some (LRAT.Action.addRat id c_1 pivot rupHints ratHints) =>
              if h : pivot ∈ LRAT.Clause.toList c_1 then some ⟨LRAT.Action.addRat id c_1 pivot rupHints ratHints, ⋯⟩
              else none)
          (List.map (LRAT.intActionToDefaultClauseAction ((LratFormula.ofCnf c).numVars + 1)) lratProof✝.toList))) =
    LRAT.Result.success
h2✝ : unsatisfiable (PosFin ((LratFormula.ofCnf c).numVars + 1)) (LratFormula.ofCnf c).formula
assignment : PosFin (c.numLiterals + 1) → Bool
h2 : ¬(assignment ⊨ LRAT.DefaultFormula.ofArray (List.toArray c.lift.convertLRAT'))
h3 : CNF.eval assignment c.lift = true
⊢ ∀ (x : LRAT.DefaultClause ((LratFormula.ofCnf c).numVars + 1)),
    x ∈ LRAT.Formula.toList (LRAT.DefaultFormula.ofArray (List.toArray c.lift.convertLRAT')) → assignment ⊨ x

State before:
case h_1.a
c : CNF Nat
b : LratCert
x✝ : Option (Array LRAT.IntAction)
lratProof✝ : Array LRAT.IntAction
heq✝ : LRAT.parseLRATProof (String.toUTF8 b) = some lratProof✝
h1 :
  LRAT.lratChecker (LratFormula.ofCnf c).formula
      (List.map Subtype.val
        (List.filterMap
          (fun actOpt =>
            match actOpt with
            | none => none
            | some (LRAT.Action.addEmpty id rupHints) => some ⟨LRAT.Action.addEmpty id rupHints, True.intro⟩
            | some (LRAT.Action.addRup id c_1 rupHints) => some ⟨LRAT.Action.addRup id c_1 rupHints, True.intro⟩
            | some (LRAT.Action.del ids) => some ⟨LRAT.Action.del ids, True.intro⟩
            | some (LRAT.Action.addRat id c_1 pivot rupHints ratHints) =>
              if h : pivot ∈ LRAT.Clause.toList c_1 then some ⟨LRAT.Action.addRat id c_1 pivot rupHints ratHints, ⋯⟩
              else none)
          (List.map (LRAT.intActionToDefaultClauseAction ((LratFormula.ofCnf c).numVars + 1)) lratProof✝.toList))) =
    LRAT.Result.success
h2✝ : unsatisfiable (PosFin ((LratFormula.ofCnf c).numVars + 1)) (LratFormula.ofCnf c).formula
assignment : PosFin (c.numLiterals + 1) → Bool
h2 : ¬(assignment ⊨ LRAT.DefaultFormula.ofArray (List.toArray c.lift.convertLRAT'))
h3 : CNF.eval assignment c.lift = true
⊢ ∀ (x : LRAT.DefaultClause ((LratFormula.ofCnf c).numVars + 1)),
    x ∈ LRAT.Formula.toList (LRAT.DefaultFormula.ofArray (List.toArray c.lift.convertLRAT')) → assignment ⊨ x
Tactic:
intro lratClause hlclause
State after:
case h_1.a
c : CNF Nat
b : LratCert
x✝ : Option (Array LRAT.IntAction)
lratProof✝ : Array LRAT.IntAction
heq✝ : LRAT.parseLRATProof (String.toUTF8 b) = some lratProof✝
h1 :
  LRAT.lratChecker (LratFormula.ofCnf c).formula
      (List.map Subtype.val
        (List.filterMap
          (fun actOpt =>
            match actOpt with
            | none => none
            | some (LRAT.Action.addEmpty id rupHints) => some ⟨LRAT.Action.addEmpty id rupHints, True.intro⟩
            | some (LRAT.Action.addRup id c_1 rupHints) => some ⟨LRAT.Action.addRup id c_1 rupHints, True.intro⟩
            | some (LRAT.Action.del ids) => some ⟨LRAT.Action.del ids, True.intro⟩
            | some (LRAT.Action.addRat id c_1 pivot rupHints ratHints) =>
              if h : pivot ∈ LRAT.Clause.toList c_1 then some ⟨LRAT.Action.addRat id c_1 pivot rupHints ratHints, ⋯⟩
              else none)
          (List.map (LRAT.intActionToDefaultClauseAction ((LratFormula.ofCnf c).numVars + 1)) lratProof✝.toList))) =
    LRAT.Result.success
h2✝ : unsatisfiable (PosFin ((LratFormula.ofCnf c).numVars + 1)) (LratFormula.ofCnf c).formula
assignment : PosFin (c.numLiterals + 1) → Bool
h2 : ¬(assignment ⊨ LRAT.DefaultFormula.ofArray (List.toArray c.lift.convertLRAT'))
h3 : CNF.eval assignment c.lift = true
lratClause : LRAT.DefaultClause ((LratFormula.ofCnf c).numVars + 1)
hlclause : lratClause ∈ LRAT.Formula.toList (LRAT.DefaultFormula.ofArray (List.toArray c.lift.convertLRAT'))
⊢ assignment ⊨ lratClause

State before:
case h_1.a
c : CNF Nat
b : LratCert
x✝ : Option (Array LRAT.IntAction)
lratProof✝ : Array LRAT.IntAction
heq✝ : LRAT.parseLRATProof (String.toUTF8 b) = some lratProof✝
h1 :
  LRAT.lratChecker (LratFormula.ofCnf c).formula
      (List.map Subtype.val
        (List.filterMap
          (fun actOpt =>
            match actOpt with
            | none => none
            | some (LRAT.Action.addEmpty id rupHints) => some ⟨LRAT.Action.addEmpty id rupHints, True.intro⟩
            | some (LRAT.Action.addRup id c_1 rupHints) => some ⟨LRAT.Action.addRup id c_1 rupHints, True.intro⟩
            | some (LRAT.Action.del ids) => some ⟨LRAT.Action.del ids, True.intro⟩
            | some (LRAT.Action.addRat id c_1 pivot rupHints ratHints) =>
              if h : pivot ∈ LRAT.Clause.toList c_1 then some ⟨LRAT.Action.addRat id c_1 pivot rupHints ratHints, ⋯⟩
              else none)
          (List.map (LRAT.intActionToDefaultClauseAction ((LratFormula.ofCnf c).numVars + 1)) lratProof✝.toList))) =
    LRAT.Result.success
h2✝ : unsatisfiable (PosFin ((LratFormula.ofCnf c).numVars + 1)) (LratFormula.ofCnf c).formula
assignment : PosFin (c.numLiterals + 1) → Bool
h2 : ¬(assignment ⊨ LRAT.DefaultFormula.ofArray (List.toArray c.lift.convertLRAT'))
h3 : CNF.eval assignment c.lift = true
lratClause : LRAT.DefaultClause ((LratFormula.ofCnf c).numVars + 1)
hlclause : lratClause ∈ LRAT.Formula.toList (LRAT.DefaultFormula.ofArray (List.toArray c.lift.convertLRAT'))
⊢ assignment ⊨ lratClause
Tactic:
simp only [LRAT.Formula.toList, LRAT.DefaultFormula.toList, LRAT.DefaultFormula.ofArray,
  CNF.convertLRAT', Array.size_toArray, List.length_map, Array.toList_eq, Array.data_toArray,
  List.map_nil, List.append_nil, List.mem_filterMap, List.mem_map, id_eq, exists_eq_right] at hlclause
State after:
case h_1.a
c : CNF Nat
b : LratCert
x✝ : Option (Array LRAT.IntAction)
lratProof✝ : Array LRAT.IntAction
heq✝ : LRAT.parseLRATProof (String.toUTF8 b) = some lratProof✝
h1 :
  LRAT.lratChecker (LratFormula.ofCnf c).formula
      (List.map Subtype.val
        (List.filterMap
          (fun actOpt =>
            match actOpt with
            | none => none
            | some (LRAT.Action.addEmpty id rupHints) => some ⟨LRAT.Action.addEmpty id rupHints, True.intro⟩
            | some (LRAT.Action.addRup id c_1 rupHints) => some ⟨LRAT.Action.addRup id c_1 rupHints, True.intro⟩
            | some (LRAT.Action.del ids) => some ⟨LRAT.Action.del ids, True.intro⟩
            | some (LRAT.Action.addRat id c_1 pivot rupHints ratHints) =>
              if h : pivot ∈ LRAT.Clause.toList c_1 then some ⟨LRAT.Action.addRat id c_1 pivot rupHints ratHints, ⋯⟩
              else none)
          (List.map (LRAT.intActionToDefaultClauseAction ((LratFormula.ofCnf c).numVars + 1)) lratProof✝.toList))) =
    LRAT.Result.success
h2✝ : unsatisfiable (PosFin ((LratFormula.ofCnf c).numVars + 1)) (LratFormula.ofCnf c).formula
assignment : PosFin (c.numLiterals + 1) → Bool
h2 : ¬(assignment ⊨ LRAT.DefaultFormula.ofArray (List.toArray c.lift.convertLRAT'))
h3 : CNF.eval assignment c.lift = true
lratClause : LRAT.DefaultClause ((LratFormula.ofCnf c).numVars + 1)
hlclause :
  ∃ a,
    a ∈ c.lift ∧
      (match a.convertLRAT' with
        | some foo => some (some foo)
        | none => none) =
        some (some lratClause)
⊢ assignment ⊨ lratClause

State before:
case h_1.a
c : CNF Nat
b : LratCert
x✝ : Option (Array LRAT.IntAction)
lratProof✝ : Array LRAT.IntAction
heq✝ : LRAT.parseLRATProof (String.toUTF8 b) = some lratProof✝
h1 :
  LRAT.lratChecker (LratFormula.ofCnf c).formula
      (List.map Subtype.val
        (List.filterMap
          (fun actOpt =>
            match actOpt with
            | none => none
            | some (LRAT.Action.addEmpty id rupHints) => some ⟨LRAT.Action.addEmpty id rupHints, True.intro⟩
            | some (LRAT.Action.addRup id c_1 rupHints) => some ⟨LRAT.Action.addRup id c_1 rupHints, True.intro⟩
            | some (LRAT.Action.del ids) => some ⟨LRAT.Action.del ids, True.intro⟩
            | some (LRAT.Action.addRat id c_1 pivot rupHints ratHints) =>
              if h : pivot ∈ LRAT.Clause.toList c_1 then some ⟨LRAT.Action.addRat id c_1 pivot rupHints ratHints, ⋯⟩
              else none)
          (List.map (LRAT.intActionToDefaultClauseAction ((LratFormula.ofCnf c).numVars + 1)) lratProof✝.toList))) =
    LRAT.Result.success
h2✝ : unsatisfiable (PosFin ((LratFormula.ofCnf c).numVars + 1)) (LratFormula.ofCnf c).formula
assignment : PosFin (c.numLiterals + 1) → Bool
h2 : ¬(assignment ⊨ LRAT.DefaultFormula.ofArray (List.toArray c.lift.convertLRAT'))
h3 : CNF.eval assignment c.lift = true
lratClause : LRAT.DefaultClause ((LratFormula.ofCnf c).numVars + 1)
hlclause :
  ∃ a,
    a ∈ c.lift ∧
      (match a.convertLRAT' with
        | some foo => some (some foo)
        | none => none) =
        some (some lratClause)
⊢ assignment ⊨ lratClause
Tactic:
rcases hlclause with ⟨reflectClause, ⟨hrclause1, hrclause2⟩⟩
State after:
case h_1.a.intro.intro
c : CNF Nat
b : LratCert
x✝ : Option (Array LRAT.IntAction)
lratProof✝ : Array LRAT.IntAction
heq✝ : LRAT.parseLRATProof (String.toUTF8 b) = some lratProof✝
h1 :
  LRAT.lratChecker (LratFormula.ofCnf c).formula
      (List.map Subtype.val
        (List.filterMap
          (fun actOpt =>
            match actOpt with
            | none => none
            | some (LRAT.Action.addEmpty id rupHints) => some ⟨LRAT.Action.addEmpty id rupHints, True.intro⟩
            | some (LRAT.Action.addRup id c_1 rupHints) => some ⟨LRAT.Action.addRup id c_1 rupHints, True.intro⟩
            | some (LRAT.Action.del ids) => some ⟨LRAT.Action.del ids, True.intro⟩
            | some (LRAT.Action.addRat id c_1 pivot rupHints ratHints) =>
              if h : pivot ∈ LRAT.Clause.toList c_1 then some ⟨LRAT.Action.addRat id c_1 pivot rupHints ratHints, ⋯⟩
              else none)
          (List.map (LRAT.intActionToDefaultClauseAction ((LratFormula.ofCnf c).numVars + 1)) lratProof✝.toList))) =
    LRAT.Result.success
h2✝ : unsatisfiable (PosFin ((LratFormula.ofCnf c).numVars + 1)) (LratFormula.ofCnf c).formula
assignment : PosFin (c.numLiterals + 1) → Bool
h2 : ¬(assignment ⊨ LRAT.DefaultFormula.ofArray (List.toArray c.lift.convertLRAT'))
h3 : CNF.eval assignment c.lift = true
lratClause : LRAT.DefaultClause ((LratFormula.ofCnf c).numVars + 1)
reflectClause : CNF.Clause (PosFin (c.numLiterals + 1))
hrclause1 : reflectClause ∈ c.lift
hrclause2 :
  (match reflectClause.convertLRAT' with
    | some foo => some (some foo)
    | none => none) =
    some (some lratClause)
⊢ assignment ⊨ lratClause

State before:
case h_1.a.intro.intro
c : CNF Nat
b : LratCert
x✝ : Option (Array LRAT.IntAction)
lratProof✝ : Array LRAT.IntAction
heq✝ : LRAT.parseLRATProof (String.toUTF8 b) = some lratProof✝
h1 :
  LRAT.lratChecker (LratFormula.ofCnf c).formula
      (List.map Subtype.val
        (List.filterMap
          (fun actOpt =>
            match actOpt with
            | none => none
            | some (LRAT.Action.addEmpty id rupHints) => some ⟨LRAT.Action.addEmpty id rupHints, True.intro⟩
            | some (LRAT.Action.addRup id c_1 rupHints) => some ⟨LRAT.Action.addRup id c_1 rupHints, True.intro⟩
            | some (LRAT.Action.del ids) => some ⟨LRAT.Action.del ids, True.intro⟩
            | some (LRAT.Action.addRat id c_1 pivot rupHints ratHints) =>
              if h : pivot ∈ LRAT.Clause.toList c_1 then some ⟨LRAT.Action.addRat id c_1 pivot rupHints ratHints, ⋯⟩
              else none)
          (List.map (LRAT.intActionToDefaultClauseAction ((LratFormula.ofCnf c).numVars + 1)) lratProof✝.toList))) =
    LRAT.Result.success
h2✝ : unsatisfiable (PosFin ((LratFormula.ofCnf c).numVars + 1)) (LratFormula.ofCnf c).formula
assignment : PosFin (c.numLiterals + 1) → Bool
h2 : ¬(assignment ⊨ LRAT.DefaultFormula.ofArray (List.toArray c.lift.convertLRAT'))
h3 : CNF.eval assignment c.lift = true
lratClause : LRAT.DefaultClause ((LratFormula.ofCnf c).numVars + 1)
reflectClause : CNF.Clause (PosFin (c.numLiterals + 1))
hrclause1 : reflectClause ∈ c.lift
hrclause2 :
  (match reflectClause.convertLRAT' with
    | some foo => some (some foo)
    | none => none) =
    some (some lratClause)
⊢ assignment ⊨ lratClause
Tactic:
simp only [CNF.eval, List.all_eq_true] at h3
State after:
case h_1.a.intro.intro
c : CNF Nat
b : LratCert
x✝ : Option (Array LRAT.IntAction)
lratProof✝ : Array LRAT.IntAction
heq✝ : LRAT.parseLRATProof (String.toUTF8 b) = some lratProof✝
h1 :
  LRAT.lratChecker (LratFormula.ofCnf c).formula
      (List.map Subtype.val
        (List.filterMap
          (fun actOpt =>
            match actOpt with
            | none => none
            | some (LRAT.Action.addEmpty id rupHints) => some ⟨LRAT.Action.addEmpty id rupHints, True.intro⟩
            | some (LRAT.Action.addRup id c_1 rupHints) => some ⟨LRAT.Action.addRup id c_1 rupHints, True.intro⟩
            | some (LRAT.Action.del ids) => some ⟨LRAT.Action.del ids, True.intro⟩
            | some (LRAT.Action.addRat id c_1 pivot rupHints ratHints) =>
              if h : pivot ∈ LRAT.Clause.toList c_1 then some ⟨LRAT.Action.addRat id c_1 pivot rupHints ratHints, ⋯⟩
              else none)
          (List.map (LRAT.intActionToDefaultClauseAction ((LratFormula.ofCnf c).numVars + 1)) lratProof✝.toList))) =
    LRAT.Result.success
h2✝ : unsatisfiable (PosFin ((LratFormula.ofCnf c).numVars + 1)) (LratFormula.ofCnf c).formula
assignment : PosFin (c.numLiterals + 1) → Bool
h2 : ¬(assignment ⊨ LRAT.DefaultFormula.ofArray (List.toArray c.lift.convertLRAT'))
lratClause : LRAT.DefaultClause ((LratFormula.ofCnf c).numVars + 1)
reflectClause : CNF.Clause (PosFin (c.numLiterals + 1))
hrclause1 : reflectClause ∈ c.lift
hrclause2 :
  (match reflectClause.convertLRAT' with
    | some foo => some (some foo)
    | none => none) =
    some (some lratClause)
h3 : ∀ (x : CNF.Clause (PosFin (c.numLiterals + 1))), x ∈ c.lift → CNF.Clause.eval assignment x = true
⊢ assignment ⊨ lratClause

State before:
case h_1.a.intro.intro
c : CNF Nat
b : LratCert
x✝ : Option (Array LRAT.IntAction)
lratProof✝ : Array LRAT.IntAction
heq✝ : LRAT.parseLRATProof (String.toUTF8 b) = some lratProof✝
h1 :
  LRAT.lratChecker (LratFormula.ofCnf c).formula
      (List.map Subtype.val
        (List.filterMap
          (fun actOpt =>
            match actOpt with
            | none => none
            | some (LRAT.Action.addEmpty id rupHints) => some ⟨LRAT.Action.addEmpty id rupHints, True.intro⟩
            | some (LRAT.Action.addRup id c_1 rupHints) => some ⟨LRAT.Action.addRup id c_1 rupHints, True.intro⟩
            | some (LRAT.Action.del ids) => some ⟨LRAT.Action.del ids, True.intro⟩
            | some (LRAT.Action.addRat id c_1 pivot rupHints ratHints) =>
              if h : pivot ∈ LRAT.Clause.toList c_1 then some ⟨LRAT.Action.addRat id c_1 pivot rupHints ratHints, ⋯⟩
              else none)
          (List.map (LRAT.intActionToDefaultClauseAction ((LratFormula.ofCnf c).numVars + 1)) lratProof✝.toList))) =
    LRAT.Result.success
h2✝ : unsatisfiable (PosFin ((LratFormula.ofCnf c).numVars + 1)) (LratFormula.ofCnf c).formula
assignment : PosFin (c.numLiterals + 1) → Bool
h2 : ¬(assignment ⊨ LRAT.DefaultFormula.ofArray (List.toArray c.lift.convertLRAT'))
lratClause : LRAT.DefaultClause ((LratFormula.ofCnf c).numVars + 1)
reflectClause : CNF.Clause (PosFin (c.numLiterals + 1))
hrclause1 : reflectClause ∈ c.lift
hrclause2 :
  (match reflectClause.convertLRAT' with
    | some foo => some (some foo)
    | none => none) =
    some (some lratClause)
h3 : ∀ (x : CNF.Clause (PosFin (c.numLiterals + 1))), x ∈ c.lift → CNF.Clause.eval assignment x = true
⊢ assignment ⊨ lratClause
Tactic:
split at hrclause2
State after:
case h_1.a.intro.intro.h_1
c : CNF Nat
b : LratCert
x✝¹ : Option (Array LRAT.IntAction)
lratProof✝ : Array LRAT.IntAction
heq✝¹ : LRAT.parseLRATProof (String.toUTF8 b) = some lratProof✝
h1 :
  LRAT.lratChecker (LratFormula.ofCnf c).formula
      (List.map Subtype.val
        (List.filterMap
          (fun actOpt =>
            match actOpt with
            | none => none
            | some (LRAT.Action.addEmpty id rupHints) => some ⟨LRAT.Action.addEmpty id rupHints, True.intro⟩
            | some (LRAT.Action.addRup id c_1 rupHints) => some ⟨LRAT.Action.addRup id c_1 rupHints, True.intro⟩
            | some (LRAT.Action.del ids) => some ⟨LRAT.Action.del ids, True.intro⟩
            | some (LRAT.Action.addRat id c_1 pivot rupHints ratHints) =>
              if h : pivot ∈ LRAT.Clause.toList c_1 then some ⟨LRAT.Action.addRat id c_1 pivot rupHints ratHints, ⋯⟩
              else none)
          (List.map (LRAT.intActionToDefaultClauseAction ((LratFormula.ofCnf c).numVars + 1)) lratProof✝.toList))) =
    LRAT.Result.success
h2✝ : unsatisfiable (PosFin ((LratFormula.ofCnf c).numVars + 1)) (LratFormula.ofCnf c).formula
assignment : PosFin (c.numLiterals + 1) → Bool
h2 : ¬(assignment ⊨ LRAT.DefaultFormula.ofArray (List.toArray c.lift.convertLRAT'))
lratClause : LRAT.DefaultClause ((LratFormula.ofCnf c).numVars + 1)
reflectClause : CNF.Clause (PosFin (c.numLiterals + 1))
hrclause1 : reflectClause ∈ c.lift
h3 : ∀ (x : CNF.Clause (PosFin (c.numLiterals + 1))), x ∈ c.lift → CNF.Clause.eval assignment x = true
x✝ : Option (LRAT.DefaultClause (c.numLiterals + 1))
foo✝ : LRAT.DefaultClause (c.numLiterals + 1)
heq✝ : reflectClause.convertLRAT' = some foo✝
hrclause2 : some (some foo✝) = some (some lratClause)
⊢ assignment ⊨ lratClause

case h_1.a.intro.intro.h_2
c : CNF Nat
b : LratCert
x✝¹ : Option (Array LRAT.IntAction)
lratProof✝ : Array LRAT.IntAction
heq✝¹ : LRAT.parseLRATProof (String.toUTF8 b) = some lratProof✝
h1 :
  LRAT.lratChecker (LratFormula.ofCnf c).formula
      (List.map Subtype.val
        (List.filterMap
          (fun actOpt =>
            match actOpt with
            | none => none
            | some (LRAT.Action.addEmpty id rupHints) => some ⟨LRAT.Action.addEmpty id rupHints, True.intro⟩
            | some (LRAT.Action.addRup id c_1 rupHints) => some ⟨LRAT.Action.addRup id c_1 rupHints, True.intro⟩
            | some (LRAT.Action.del ids) => some ⟨LRAT.Action.del ids, True.intro⟩
            | some (LRAT.Action.addRat id c_1 pivot rupHints ratHints) =>
              if h : pivot ∈ LRAT.Clause.toList c_1 then some ⟨LRAT.Action.addRat id c_1 pivot rupHints ratHints, ⋯⟩
              else none)
          (List.map (LRAT.intActionToDefaultClauseAction ((LratFormula.ofCnf c).numVars + 1)) lratProof✝.toList))) =
    LRAT.Result.success
h2✝ : unsatisfiable (PosFin ((LratFormula.ofCnf c).numVars + 1)) (LratFormula.ofCnf c).formula
assignment : PosFin (c.numLiterals + 1) → Bool
h2 : ¬(assignment ⊨ LRAT.DefaultFormula.ofArray (List.toArray c.lift.convertLRAT'))
lratClause : LRAT.DefaultClause ((LratFormula.ofCnf c).numVars + 1)
reflectClause : CNF.Clause (PosFin (c.numLiterals + 1))
hrclause1 : reflectClause ∈ c.lift
h3 : ∀ (x : CNF.Clause (PosFin (c.numLiterals + 1))), x ∈ c.lift → CNF.Clause.eval assignment x = true
x✝ : Option (LRAT.DefaultClause (c.numLiterals + 1))
heq✝ : reflectClause.convertLRAT' = none
hrclause2 : none = some (some lratClause)
⊢ assignment ⊨ lratClause

State before:
case h_1.a.intro.intro.h_1
c : CNF Nat
b : LratCert
x✝¹ : Option (Array LRAT.IntAction)
lratProof✝ : Array LRAT.IntAction
heq✝¹ : LRAT.parseLRATProof (String.toUTF8 b) = some lratProof✝
h1 :
  LRAT.lratChecker (LratFormula.ofCnf c).formula
      (List.map Subtype.val
        (List.filterMap
          (fun actOpt =>
            match actOpt with
            | none => none
            | some (LRAT.Action.addEmpty id rupHints) => some ⟨LRAT.Action.addEmpty id rupHints, True.intro⟩
            | some (LRAT.Action.addRup id c_1 rupHints) => some ⟨LRAT.Action.addRup id c_1 rupHints, True.intro⟩
            | some (LRAT.Action.del ids) => some ⟨LRAT.Action.del ids, True.intro⟩
            | some (LRAT.Action.addRat id c_1 pivot rupHints ratHints) =>
              if h : pivot ∈ LRAT.Clause.toList c_1 then some ⟨LRAT.Action.addRat id c_1 pivot rupHints ratHints, ⋯⟩
              else none)
          (List.map (LRAT.intActionToDefaultClauseAction ((LratFormula.ofCnf c).numVars + 1)) lratProof✝.toList))) =
    LRAT.Result.success
h2✝ : unsatisfiable (PosFin ((LratFormula.ofCnf c).numVars + 1)) (LratFormula.ofCnf c).formula
assignment : PosFin (c.numLiterals + 1) → Bool
h2 : ¬(assignment ⊨ LRAT.DefaultFormula.ofArray (List.toArray c.lift.convertLRAT'))
lratClause : LRAT.DefaultClause ((LratFormula.ofCnf c).numVars + 1)
reflectClause : CNF.Clause (PosFin (c.numLiterals + 1))
hrclause1 : reflectClause ∈ c.lift
h3 : ∀ (x : CNF.Clause (PosFin (c.numLiterals + 1))), x ∈ c.lift → CNF.Clause.eval assignment x = true
x✝ : Option (LRAT.DefaultClause (c.numLiterals + 1))
foo✝ : LRAT.DefaultClause (c.numLiterals + 1)
heq✝ : reflectClause.convertLRAT' = some foo✝
hrclause2 : some (some foo✝) = some (some lratClause)
⊢ assignment ⊨ lratClause

case h_1.a.intro.intro.h_2
c : CNF Nat
b : LratCert
x✝¹ : Option (Array LRAT.IntAction)
lratProof✝ : Array LRAT.IntAction
heq✝¹ : LRAT.parseLRATProof (String.toUTF8 b) = some lratProof✝
h1 :
  LRAT.lratChecker (LratFormula.ofCnf c).formula
      (List.map Subtype.val
        (List.filterMap
          (fun actOpt =>
            match actOpt with
            | none => none
            | some (LRAT.Action.addEmpty id rupHints) => some ⟨LRAT.Action.addEmpty id rupHints, True.intro⟩
            | some (LRAT.Action.addRup id c_1 rupHints) => some ⟨LRAT.Action.addRup id c_1 rupHints, True.intro⟩
            | some (LRAT.Action.del ids) => some ⟨LRAT.Action.del ids, True.intro⟩
            | some (LRAT.Action.addRat id c_1 pivot rupHints ratHints) =>
              if h : pivot ∈ LRAT.Clause.toList c_1 then some ⟨LRAT.Action.addRat id c_1 pivot rupHints ratHints, ⋯⟩
              else none)
          (List.map (LRAT.intActionToDefaultClauseAction ((LratFormula.ofCnf c).numVars + 1)) lratProof✝.toList))) =
    LRAT.Result.success
h2✝ : unsatisfiable (PosFin ((LratFormula.ofCnf c).numVars + 1)) (LratFormula.ofCnf c).formula
assignment : PosFin (c.numLiterals + 1) → Bool
h2 : ¬(assignment ⊨ LRAT.DefaultFormula.ofArray (List.toArray c.lift.convertLRAT'))
lratClause : LRAT.DefaultClause ((LratFormula.ofCnf c).numVars + 1)
reflectClause : CNF.Clause (PosFin (c.numLiterals + 1))
hrclause1 : reflectClause ∈ c.lift
h3 : ∀ (x : CNF.Clause (PosFin (c.numLiterals + 1))), x ∈ c.lift → CNF.Clause.eval assignment x = true
x✝ : Option (LRAT.DefaultClause (c.numLiterals + 1))
heq✝ : reflectClause.convertLRAT' = none
hrclause2 : none = some (some lratClause)
⊢ assignment ⊨ lratClause
Tactic:
. next heq =>
  rw [← heq] at hrclause2
  simp only [Option.some.injEq] at hrclause2
  simp [CNF.Clause.convertLRAT_sat_of_sat reflectClause hrclause2, h3 reflectClause hrclause1]
State after:
case h_1.a.intro.intro.h_2
c : CNF Nat
b : LratCert
x✝¹ : Option (Array LRAT.IntAction)
lratProof✝ : Array LRAT.IntAction
heq✝¹ : LRAT.parseLRATProof (String.toUTF8 b) = some lratProof✝
h1 :
  LRAT.lratChecker (LratFormula.ofCnf c).formula
      (List.map Subtype.val
        (List.filterMap
          (fun actOpt =>
            match actOpt with
            | none => none
            | some (LRAT.Action.addEmpty id rupHints) => some ⟨LRAT.Action.addEmpty id rupHints, True.intro⟩
            | some (LRAT.Action.addRup id c_1 rupHints) => some ⟨LRAT.Action.addRup id c_1 rupHints, True.intro⟩
            | some (LRAT.Action.del ids) => some ⟨LRAT.Action.del ids, True.intro⟩
            | some (LRAT.Action.addRat id c_1 pivot rupHints ratHints) =>
              if h : pivot ∈ LRAT.Clause.toList c_1 then some ⟨LRAT.Action.addRat id c_1 pivot rupHints ratHints, ⋯⟩
              else none)
          (List.map (LRAT.intActionToDefaultClauseAction ((LratFormula.ofCnf c).numVars + 1)) lratProof✝.toList))) =
    LRAT.Result.success
h2✝ : unsatisfiable (PosFin ((LratFormula.ofCnf c).numVars + 1)) (LratFormula.ofCnf c).formula
assignment : PosFin (c.numLiterals + 1) → Bool
h2 : ¬(assignment ⊨ LRAT.DefaultFormula.ofArray (List.toArray c.lift.convertLRAT'))
lratClause : LRAT.DefaultClause ((LratFormula.ofCnf c).numVars + 1)
reflectClause : CNF.Clause (PosFin (c.numLiterals + 1))
hrclause1 : reflectClause ∈ c.lift
h3 : ∀ (x : CNF.Clause (PosFin (c.numLiterals + 1))), x ∈ c.lift → CNF.Clause.eval assignment x = true
x✝ : Option (LRAT.DefaultClause (c.numLiterals + 1))
heq✝ : reflectClause.convertLRAT' = none
hrclause2 : none = some (some lratClause)
⊢ assignment ⊨ lratClause

State before:
case h_1.a.intro.intro.h_2
c : CNF Nat
b : LratCert
x✝¹ : Option (Array LRAT.IntAction)
lratProof✝ : Array LRAT.IntAction
heq✝¹ : LRAT.parseLRATProof (String.toUTF8 b) = some lratProof✝
h1 :
  LRAT.lratChecker (LratFormula.ofCnf c).formula
      (List.map Subtype.val
        (List.filterMap
          (fun actOpt =>
            match actOpt with
            | none => none
            | some (LRAT.Action.addEmpty id rupHints) => some ⟨LRAT.Action.addEmpty id rupHints, True.intro⟩
            | some (LRAT.Action.addRup id c_1 rupHints) => some ⟨LRAT.Action.addRup id c_1 rupHints, True.intro⟩
            | some (LRAT.Action.del ids) => some ⟨LRAT.Action.del ids, True.intro⟩
            | some (LRAT.Action.addRat id c_1 pivot rupHints ratHints) =>
              if h : pivot ∈ LRAT.Clause.toList c_1 then some ⟨LRAT.Action.addRat id c_1 pivot rupHints ratHints, ⋯⟩
              else none)
          (List.map (LRAT.intActionToDefaultClauseAction ((LratFormula.ofCnf c).numVars + 1)) lratProof✝.toList))) =
    LRAT.Result.success
h2✝ : unsatisfiable (PosFin ((LratFormula.ofCnf c).numVars + 1)) (LratFormula.ofCnf c).formula
assignment : PosFin (c.numLiterals + 1) → Bool
h2 : ¬(assignment ⊨ LRAT.DefaultFormula.ofArray (List.toArray c.lift.convertLRAT'))
lratClause : LRAT.DefaultClause ((LratFormula.ofCnf c).numVars + 1)
reflectClause : CNF.Clause (PosFin (c.numLiterals + 1))
hrclause1 : reflectClause ∈ c.lift
h3 : ∀ (x : CNF.Clause (PosFin (c.numLiterals + 1))), x ∈ c.lift → CNF.Clause.eval assignment x = true
x✝ : Option (LRAT.DefaultClause (c.numLiterals + 1))
heq✝ : reflectClause.convertLRAT' = none
hrclause2 : none = some (some lratClause)
⊢ assignment ⊨ lratClause
Tactic:
. contradiction
State after:
no goals

State before:
c : CNF Nat
b : LratCert
x✝ : Option (Array LRAT.IntAction)
lratProof✝ : Array LRAT.IntAction
heq✝ : LRAT.parseLRATProof (String.toUTF8 b) = some lratProof✝
h1 :
  LRAT.lratChecker (LratFormula.ofCnf c).formula
      (List.map Subtype.val
        (List.filterMap
          (fun actOpt =>
            match actOpt with
            | none => none
            | some (LRAT.Action.addEmpty id rupHints) => some ⟨LRAT.Action.addEmpty id rupHints, True.intro⟩
            | some (LRAT.Action.addRup id c_1 rupHints) => some ⟨LRAT.Action.addRup id c_1 rupHints, True.intro⟩
            | some (LRAT.Action.del ids) => some ⟨LRAT.Action.del ids, True.intro⟩
            | some (LRAT.Action.addRat id c_1 pivot rupHints ratHints) =>
              if h : pivot ∈ LRAT.Clause.toList c_1 then some ⟨LRAT.Action.addRat id c_1 pivot rupHints ratHints, ⋯⟩
              else none)
          (List.map (LRAT.intActionToDefaultClauseAction ((LratFormula.ofCnf c).numVars + 1)) lratProof✝.toList))) =
    LRAT.Result.success
⊢ LRAT.Formula.readyForRupAdd (LratFormula.ofCnf c).formula
Tactic:
apply CNF.convertLRAT_readfyForRupAdd
State after:
no goals

State before:
c : CNF Nat
b : LratCert
x✝ : Option (Array LRAT.IntAction)
lratProof✝ : Array LRAT.IntAction
heq✝ : LRAT.parseLRATProof (String.toUTF8 b) = some lratProof✝
h1 :
  LRAT.lratChecker (LratFormula.ofCnf c).formula
      (List.map Subtype.val
        (List.filterMap
          (fun actOpt =>
            match actOpt with
            | none => none
            | some (LRAT.Action.addEmpty id rupHints) => some ⟨LRAT.Action.addEmpty id rupHints, True.intro⟩
            | some (LRAT.Action.addRup id c_1 rupHints) => some ⟨LRAT.Action.addRup id c_1 rupHints, True.intro⟩
            | some (LRAT.Action.del ids) => some ⟨LRAT.Action.del ids, True.intro⟩
            | some (LRAT.Action.addRat id c_1 pivot rupHints ratHints) =>
              if h : pivot ∈ LRAT.Clause.toList c_1 then some ⟨LRAT.Action.addRat id c_1 pivot rupHints ratHints, ⋯⟩
              else none)
          (List.map (LRAT.intActionToDefaultClauseAction ((LratFormula.ofCnf c).numVars + 1)) lratProof✝.toList))) =
    LRAT.Result.success
⊢ LRAT.Formula.readyForRatAdd (LratFormula.ofCnf c).formula
Tactic:
apply CNF.convertLRAT_readfyForRatAdd
State after:
no goals

State before:
c : CNF Nat
b : LratCert
x✝ : Option (Array LRAT.IntAction)
lratProof✝ : Array LRAT.IntAction
heq✝ : LRAT.parseLRATProof (String.toUTF8 b) = some lratProof✝
h1 :
  LRAT.lratChecker (LratFormula.ofCnf c).formula
      (List.map Subtype.val
        (List.filterMap
          (fun actOpt =>
            match actOpt with
            | none => none
            | some (LRAT.Action.addEmpty id rupHints) => some ⟨LRAT.Action.addEmpty id rupHints, True.intro⟩
            | some (LRAT.Action.addRup id c_1 rupHints) => some ⟨LRAT.Action.addRup id c_1 rupHints, True.intro⟩
            | some (LRAT.Action.del ids) => some ⟨LRAT.Action.del ids, True.intro⟩
            | some (LRAT.Action.addRat id c_1 pivot rupHints ratHints) =>
              if h : pivot ∈ LRAT.Clause.toList c_1 then some ⟨LRAT.Action.addRat id c_1 pivot rupHints ratHints, ⋯⟩
              else none)
          (List.map (LRAT.intActionToDefaultClauseAction ((LratFormula.ofCnf c).numVars + 1)) lratProof✝.toList))) =
    LRAT.Result.success
⊢ ∀
    (a :
      LRAT.Action (LRAT.DefaultClause ((LratFormula.ofCnf c).numVars + 1))
        (PosFin ((LratFormula.ofCnf c).numVars + 1))),
    a ∈
        List.map Subtype.val
          (List.filterMap
            (fun actOpt =>
              match actOpt with
              | none => none
              | some (LRAT.Action.addEmpty id rupHints) => some ⟨LRAT.Action.addEmpty id rupHints, True.intro⟩
              | some (LRAT.Action.addRup id c_1 rupHints) => some ⟨LRAT.Action.addRup id c_1 rupHints, True.intro⟩
              | some (LRAT.Action.del ids) => some ⟨LRAT.Action.del ids, True.intro⟩
              | some (LRAT.Action.addRat id c_1 pivot rupHints ratHints) =>
                if h : pivot ∈ LRAT.Clause.toList c_1 then some ⟨LRAT.Action.addRat id c_1 pivot rupHints ratHints, ⋯⟩
                else none)
            (List.map (LRAT.intActionToDefaultClauseAction ((LratFormula.ofCnf c).numVars + 1)) lratProof✝.toList)) →
      LRAT.wellFormedAction a
Tactic:
intro action h
State after:
c : CNF Nat
b : LratCert
x✝ : Option (Array LRAT.IntAction)
lratProof✝ : Array LRAT.IntAction
heq✝ : LRAT.parseLRATProof (String.toUTF8 b) = some lratProof✝
h1 :
  LRAT.lratChecker (LratFormula.ofCnf c).formula
      (List.map Subtype.val
        (List.filterMap
          (fun actOpt =>
            match actOpt with
            | none => none
            | some (LRAT.Action.addEmpty id rupHints) => some ⟨LRAT.Action.addEmpty id rupHints, True.intro⟩
            | some (LRAT.Action.addRup id c_1 rupHints) => some ⟨LRAT.Action.addRup id c_1 rupHints, True.intro⟩
            | some (LRAT.Action.del ids) => some ⟨LRAT.Action.del ids, True.intro⟩
            | some (LRAT.Action.addRat id c_1 pivot rupHints ratHints) =>
              if h : pivot ∈ LRAT.Clause.toList c_1 then some ⟨LRAT.Action.addRat id c_1 pivot rupHints ratHints, ⋯⟩
              else none)
          (List.map (LRAT.intActionToDefaultClauseAction ((LratFormula.ofCnf c).numVars + 1)) lratProof✝.toList))) =
    LRAT.Result.success
action :
  LRAT.Action (LRAT.DefaultClause ((LratFormula.ofCnf c).numVars + 1)) (PosFin ((LratFormula.ofCnf c).numVars + 1))
h :
  action ∈
    List.map Subtype.val
      (List.filterMap
        (fun actOpt =>
          match actOpt with
          | none => none
          | some (LRAT.Action.addEmpty id rupHints) => some ⟨LRAT.Action.addEmpty id rupHints, True.intro⟩
          | some (LRAT.Action.addRup id c_1 rupHints) => some ⟨LRAT.Action.addRup id c_1 rupHints, True.intro⟩
          | some (LRAT.Action.del ids) => some ⟨LRAT.Action.del ids, True.intro⟩
          | some (LRAT.Action.addRat id c_1 pivot rupHints ratHints) =>
            if h : pivot ∈ LRAT.Clause.toList c_1 then some ⟨LRAT.Action.addRat id c_1 pivot rupHints ratHints, ⋯⟩
            else none)
        (List.map (LRAT.intActionToDefaultClauseAction ((LratFormula.ofCnf c).numVars + 1)) lratProof✝.toList))
⊢ LRAT.wellFormedAction action

State before:
c : CNF Nat
b : LratCert
x✝ : Option (Array LRAT.IntAction)
lratProof✝ : Array LRAT.IntAction
heq✝ : LRAT.parseLRATProof (String.toUTF8 b) = some lratProof✝
h1 :
  LRAT.lratChecker (LratFormula.ofCnf c).formula
      (List.map Subtype.val
        (List.filterMap
          (fun actOpt =>
            match actOpt with
            | none => none
            | some (LRAT.Action.addEmpty id rupHints) => some ⟨LRAT.Action.addEmpty id rupHints, True.intro⟩
            | some (LRAT.Action.addRup id c_1 rupHints) => some ⟨LRAT.Action.addRup id c_1 rupHints, True.intro⟩
            | some (LRAT.Action.del ids) => some ⟨LRAT.Action.del ids, True.intro⟩
            | some (LRAT.Action.addRat id c_1 pivot rupHints ratHints) =>
              if h : pivot ∈ LRAT.Clause.toList c_1 then some ⟨LRAT.Action.addRat id c_1 pivot rupHints ratHints, ⋯⟩
              else none)
          (List.map (LRAT.intActionToDefaultClauseAction ((LratFormula.ofCnf c).numVars + 1)) lratProof✝.toList))) =
    LRAT.Result.success
action :
  LRAT.Action (LRAT.DefaultClause ((LratFormula.ofCnf c).numVars + 1)) (PosFin ((LratFormula.ofCnf c).numVars + 1))
h :
  action ∈
    List.map Subtype.val
      (List.filterMap
        (fun actOpt =>
          match actOpt with
          | none => none
          | some (LRAT.Action.addEmpty id rupHints) => some ⟨LRAT.Action.addEmpty id rupHints, True.intro⟩
          | some (LRAT.Action.addRup id c_1 rupHints) => some ⟨LRAT.Action.addRup id c_1 rupHints, True.intro⟩
          | some (LRAT.Action.del ids) => some ⟨LRAT.Action.del ids, True.intro⟩
          | some (LRAT.Action.addRat id c_1 pivot rupHints ratHints) =>
            if h : pivot ∈ LRAT.Clause.toList c_1 then some ⟨LRAT.Action.addRat id c_1 pivot rupHints ratHints, ⋯⟩
            else none)
        (List.map (LRAT.intActionToDefaultClauseAction ((LratFormula.ofCnf c).numVars + 1)) lratProof✝.toList))
⊢ LRAT.wellFormedAction action
Tactic:
simp only [List.mem_map, List.mem_filterMap] at h
State after:
c : CNF Nat
b : LratCert
x✝ : Option (Array LRAT.IntAction)
lratProof✝ : Array LRAT.IntAction
heq✝ : LRAT.parseLRATProof (String.toUTF8 b) = some lratProof✝
h1 :
  LRAT.lratChecker (LratFormula.ofCnf c).formula
      (List.map Subtype.val
        (List.filterMap
          (fun actOpt =>
            match actOpt with
            | none => none
            | some (LRAT.Action.addEmpty id rupHints) => some ⟨LRAT.Action.addEmpty id rupHints, True.intro⟩
            | some (LRAT.Action.addRup id c_1 rupHints) => some ⟨LRAT.Action.addRup id c_1 rupHints, True.intro⟩
            | some (LRAT.Action.del ids) => some ⟨LRAT.Action.del ids, True.intro⟩
            | some (LRAT.Action.addRat id c_1 pivot rupHints ratHints) =>
              if h : pivot ∈ LRAT.Clause.toList c_1 then some ⟨LRAT.Action.addRat id c_1 pivot rupHints ratHints, ⋯⟩
              else none)
          (List.map (LRAT.intActionToDefaultClauseAction ((LratFormula.ofCnf c).numVars + 1)) lratProof✝.toList))) =
    LRAT.Result.success
action :
  LRAT.Action (LRAT.DefaultClause ((LratFormula.ofCnf c).numVars + 1)) (PosFin ((LratFormula.ofCnf c).numVars + 1))
h :
  ∃ a,
    (∃ a_1,
        (∃ a, a ∈ lratProof✝.toList ∧ LRAT.intActionToDefaultClauseAction ((LratFormula.ofCnf c).numVars + 1) a = a_1) ∧
          (match a_1 with
            | none => none
            | some (LRAT.Action.addEmpty id rupHints) => some ⟨LRAT.Action.addEmpty id rupHints, True.intro⟩
            | some (LRAT.Action.addRup id c_1 rupHints) => some ⟨LRAT.Action.addRup id c_1 rupHints, True.intro⟩
            | some (LRAT.Action.del ids) => some ⟨LRAT.Action.del ids, True.intro⟩
            | some (LRAT.Action.addRat id c_1 pivot rupHints ratHints) =>
              if h : pivot ∈ LRAT.Clause.toList c_1 then some ⟨LRAT.Action.addRat id c_1 pivot rupHints ratHints, ⋯⟩
              else none) =
            some a) ∧
      a.val = action
⊢ LRAT.wellFormedAction action

State before:
c : CNF Nat
b : LratCert
x✝ : Option (Array LRAT.IntAction)
lratProof✝ : Array LRAT.IntAction
heq✝ : LRAT.parseLRATProof (String.toUTF8 b) = some lratProof✝
h1 :
  LRAT.lratChecker (LratFormula.ofCnf c).formula
      (List.map Subtype.val
        (List.filterMap
          (fun actOpt =>
            match actOpt with
            | none => none
            | some (LRAT.Action.addEmpty id rupHints) => some ⟨LRAT.Action.addEmpty id rupHints, True.intro⟩
            | some (LRAT.Action.addRup id c_1 rupHints) => some ⟨LRAT.Action.addRup id c_1 rupHints, True.intro⟩
            | some (LRAT.Action.del ids) => some ⟨LRAT.Action.del ids, True.intro⟩
            | some (LRAT.Action.addRat id c_1 pivot rupHints ratHints) =>
              if h : pivot ∈ LRAT.Clause.toList c_1 then some ⟨LRAT.Action.addRat id c_1 pivot rupHints ratHints, ⋯⟩
              else none)
          (List.map (LRAT.intActionToDefaultClauseAction ((LratFormula.ofCnf c).numVars + 1)) lratProof✝.toList))) =
    LRAT.Result.success
action :
  LRAT.Action (LRAT.DefaultClause ((LratFormula.ofCnf c).numVars + 1)) (PosFin ((LratFormula.ofCnf c).numVars + 1))
h :
  ∃ a,
    (∃ a_1,
        (∃ a, a ∈ lratProof✝.toList ∧ LRAT.intActionToDefaultClauseAction ((LratFormula.ofCnf c).numVars + 1) a = a_1) ∧
          (match a_1 with
            | none => none
            | some (LRAT.Action.addEmpty id rupHints) => some ⟨LRAT.Action.addEmpty id rupHints, True.intro⟩
            | some (LRAT.Action.addRup id c_1 rupHints) => some ⟨LRAT.Action.addRup id c_1 rupHints, True.intro⟩
            | some (LRAT.Action.del ids) => some ⟨LRAT.Action.del ids, True.intro⟩
            | some (LRAT.Action.addRat id c_1 pivot rupHints ratHints) =>
              if h : pivot ∈ LRAT.Clause.toList c_1 then some ⟨LRAT.Action.addRat id c_1 pivot rupHints ratHints, ⋯⟩
              else none) =
            some a) ∧
      a.val = action
⊢ LRAT.wellFormedAction action
Tactic:
rcases h with ⟨wellFormedActions, _, h2⟩
State after:
case intro.intro
c : CNF Nat
b : LratCert
x✝ : Option (Array LRAT.IntAction)
lratProof✝ : Array LRAT.IntAction
heq✝ : LRAT.parseLRATProof (String.toUTF8 b) = some lratProof✝
h1 :
  LRAT.lratChecker (LratFormula.ofCnf c).formula
      (List.map Subtype.val
        (List.filterMap
          (fun actOpt =>
            match actOpt with
            | none => none
            | some (LRAT.Action.addEmpty id rupHints) => some ⟨LRAT.Action.addEmpty id rupHints, True.intro⟩
            | some (LRAT.Action.addRup id c_1 rupHints) => some ⟨LRAT.Action.addRup id c_1 rupHints, True.intro⟩
            | some (LRAT.Action.del ids) => some ⟨LRAT.Action.del ids, True.intro⟩
            | some (LRAT.Action.addRat id c_1 pivot rupHints ratHints) =>
              if h : pivot ∈ LRAT.Clause.toList c_1 then some ⟨LRAT.Action.addRat id c_1 pivot rupHints ratHints, ⋯⟩
              else none)
          (List.map (LRAT.intActionToDefaultClauseAction ((LratFormula.ofCnf c).numVars + 1)) lratProof✝.toList))) =
    LRAT.Result.success
action :
  LRAT.Action (LRAT.DefaultClause ((LratFormula.ofCnf c).numVars + 1)) (PosFin ((LratFormula.ofCnf c).numVars + 1))
wellFormedActions : { act // LRAT.wellFormedAction act }
left✝ :
  ∃ a,
    (∃ a_1, a_1 ∈ lratProof✝.toList ∧ LRAT.intActionToDefaultClauseAction ((LratFormula.ofCnf c).numVars + 1) a_1 = a) ∧
      (match a with
        | none => none
        | some (LRAT.Action.addEmpty id rupHints) => some ⟨LRAT.Action.addEmpty id rupHints, True.intro⟩
        | some (LRAT.Action.addRup id c_1 rupHints) => some ⟨LRAT.Action.addRup id c_1 rupHints, True.intro⟩
        | some (LRAT.Action.del ids) => some ⟨LRAT.Action.del ids, True.intro⟩
        | some (LRAT.Action.addRat id c_1 pivot rupHints ratHints) =>
          if h : pivot ∈ LRAT.Clause.toList c_1 then some ⟨LRAT.Action.addRat id c_1 pivot rupHints ratHints, ⋯⟩
          else none) =
        some wellFormedActions
h2 : wellFormedActions.val = action
⊢ LRAT.wellFormedAction action

State before:
case intro.intro
c : CNF Nat
b : LratCert
x✝ : Option (Array LRAT.IntAction)
lratProof✝ : Array LRAT.IntAction
heq✝ : LRAT.parseLRATProof (String.toUTF8 b) = some lratProof✝
h1 :
  LRAT.lratChecker (LratFormula.ofCnf c).formula
      (List.map Subtype.val
        (List.filterMap
          (fun actOpt =>
            match actOpt with
            | none => none
            | some (LRAT.Action.addEmpty id rupHints) => some ⟨LRAT.Action.addEmpty id rupHints, True.intro⟩
            | some (LRAT.Action.addRup id c_1 rupHints) => some ⟨LRAT.Action.addRup id c_1 rupHints, True.intro⟩
            | some (LRAT.Action.del ids) => some ⟨LRAT.Action.del ids, True.intro⟩
            | some (LRAT.Action.addRat id c_1 pivot rupHints ratHints) =>
              if h : pivot ∈ LRAT.Clause.toList c_1 then some ⟨LRAT.Action.addRat id c_1 pivot rupHints ratHints, ⋯⟩
              else none)
          (List.map (LRAT.intActionToDefaultClauseAction ((LratFormula.ofCnf c).numVars + 1)) lratProof✝.toList))) =
    LRAT.Result.success
action :
  LRAT.Action (LRAT.DefaultClause ((LratFormula.ofCnf c).numVars + 1)) (PosFin ((LratFormula.ofCnf c).numVars + 1))
wellFormedActions : { act // LRAT.wellFormedAction act }
left✝ :
  ∃ a,
    (∃ a_1, a_1 ∈ lratProof✝.toList ∧ LRAT.intActionToDefaultClauseAction ((LratFormula.ofCnf c).numVars + 1) a_1 = a) ∧
      (match a with
        | none => none
        | some (LRAT.Action.addEmpty id rupHints) => some ⟨LRAT.Action.addEmpty id rupHints, True.intro⟩
        | some (LRAT.Action.addRup id c_1 rupHints) => some ⟨LRAT.Action.addRup id c_1 rupHints, True.intro⟩
        | some (LRAT.Action.del ids) => some ⟨LRAT.Action.del ids, True.intro⟩
        | some (LRAT.Action.addRat id c_1 pivot rupHints ratHints) =>
          if h : pivot ∈ LRAT.Clause.toList c_1 then some ⟨LRAT.Action.addRat id c_1 pivot rupHints ratHints, ⋯⟩
          else none) =
        some wellFormedActions
h2 : wellFormedActions.val = action
⊢ LRAT.wellFormedAction action
Tactic:
rw [← h2]
State after:
case intro.intro
c : CNF Nat
b : LratCert
x✝ : Option (Array LRAT.IntAction)
lratProof✝ : Array LRAT.IntAction
heq✝ : LRAT.parseLRATProof (String.toUTF8 b) = some lratProof✝
h1 :
  LRAT.lratChecker (LratFormula.ofCnf c).formula
      (List.map Subtype.val
        (List.filterMap
          (fun actOpt =>
            match actOpt with
            | none => none
            | some (LRAT.Action.addEmpty id rupHints) => some ⟨LRAT.Action.addEmpty id rupHints, True.intro⟩
            | some (LRAT.Action.addRup id c_1 rupHints) => some ⟨LRAT.Action.addRup id c_1 rupHints, True.intro⟩
            | some (LRAT.Action.del ids) => some ⟨LRAT.Action.del ids, True.intro⟩
            | some (LRAT.Action.addRat id c_1 pivot rupHints ratHints) =>
              if h : pivot ∈ LRAT.Clause.toList c_1 then some ⟨LRAT.Action.addRat id c_1 pivot rupHints ratHints, ⋯⟩
              else none)
          (List.map (LRAT.intActionToDefaultClauseAction ((LratFormula.ofCnf c).numVars + 1)) lratProof✝.toList))) =
    LRAT.Result.success
action :
  LRAT.Action (LRAT.DefaultClause ((LratFormula.ofCnf c).numVars + 1)) (PosFin ((LratFormula.ofCnf c).numVars + 1))
wellFormedActions : { act // LRAT.wellFormedAction act }
left✝ :
  ∃ a,
    (∃ a_1, a_1 ∈ lratProof✝.toList ∧ LRAT.intActionToDefaultClauseAction ((LratFormula.ofCnf c).numVars + 1) a_1 = a) ∧
      (match a with
        | none => none
        | some (LRAT.Action.addEmpty id rupHints) => some ⟨LRAT.Action.addEmpty id rupHints, True.intro⟩
        | some (LRAT.Action.addRup id c_1 rupHints) => some ⟨LRAT.Action.addRup id c_1 rupHints, True.intro⟩
        | some (LRAT.Action.del ids) => some ⟨LRAT.Action.del ids, True.intro⟩
        | some (LRAT.Action.addRat id c_1 pivot rupHints ratHints) =>
          if h : pivot ∈ LRAT.Clause.toList c_1 then some ⟨LRAT.Action.addRat id c_1 pivot rupHints ratHints, ⋯⟩
          else none) =
        some wellFormedActions
h2 : wellFormedActions.val = action
⊢ LRAT.wellFormedAction wellFormedActions.val

State before:
case intro.intro
c : CNF Nat
b : LratCert
x✝ : Option (Array LRAT.IntAction)
lratProof✝ : Array LRAT.IntAction
heq✝ : LRAT.parseLRATProof (String.toUTF8 b) = some lratProof✝
h1 :
  LRAT.lratChecker (LratFormula.ofCnf c).formula
      (List.map Subtype.val
        (List.filterMap
          (fun actOpt =>
            match actOpt with
            | none => none
            | some (LRAT.Action.addEmpty id rupHints) => some ⟨LRAT.Action.addEmpty id rupHints, True.intro⟩
            | some (LRAT.Action.addRup id c_1 rupHints) => some ⟨LRAT.Action.addRup id c_1 rupHints, True.intro⟩
            | some (LRAT.Action.del ids) => some ⟨LRAT.Action.del ids, True.intro⟩
            | some (LRAT.Action.addRat id c_1 pivot rupHints ratHints) =>
              if h : pivot ∈ LRAT.Clause.toList c_1 then some ⟨LRAT.Action.addRat id c_1 pivot rupHints ratHints, ⋯⟩
              else none)
          (List.map (LRAT.intActionToDefaultClauseAction ((LratFormula.ofCnf c).numVars + 1)) lratProof✝.toList))) =
    LRAT.Result.success
action :
  LRAT.Action (LRAT.DefaultClause ((LratFormula.ofCnf c).numVars + 1)) (PosFin ((LratFormula.ofCnf c).numVars + 1))
wellFormedActions : { act // LRAT.wellFormedAction act }
left✝ :
  ∃ a,
    (∃ a_1, a_1 ∈ lratProof✝.toList ∧ LRAT.intActionToDefaultClauseAction ((LratFormula.ofCnf c).numVars + 1) a_1 = a) ∧
      (match a with
        | none => none
        | some (LRAT.Action.addEmpty id rupHints) => some ⟨LRAT.Action.addEmpty id rupHints, True.intro⟩
        | some (LRAT.Action.addRup id c_1 rupHints) => some ⟨LRAT.Action.addRup id c_1 rupHints, True.intro⟩
        | some (LRAT.Action.del ids) => some ⟨LRAT.Action.del ids, True.intro⟩
        | some (LRAT.Action.addRat id c_1 pivot rupHints ratHints) =>
          if h : pivot ∈ LRAT.Clause.toList c_1 then some ⟨LRAT.Action.addRat id c_1 pivot rupHints ratHints, ⋯⟩
          else none) =
        some wellFormedActions
h2 : wellFormedActions.val = action
⊢ LRAT.wellFormedAction wellFormedActions.val
Tactic:
exact wellFormedActions.property
State after:
no goals

State before:
case h_1.a.intro.intro.h_1
c : CNF Nat
b : LratCert
x✝¹ : Option (Array LRAT.IntAction)
lratProof✝ : Array LRAT.IntAction
heq✝¹ : LRAT.parseLRATProof (String.toUTF8 b) = some lratProof✝
h1 :
  LRAT.lratChecker (LratFormula.ofCnf c).formula
      (List.map Subtype.val
        (List.filterMap
          (fun actOpt =>
            match actOpt with
            | none => none
            | some (LRAT.Action.addEmpty id rupHints) => some ⟨LRAT.Action.addEmpty id rupHints, True.intro⟩
            | some (LRAT.Action.addRup id c_1 rupHints) => some ⟨LRAT.Action.addRup id c_1 rupHints, True.intro⟩
            | some (LRAT.Action.del ids) => some ⟨LRAT.Action.del ids, True.intro⟩
            | some (LRAT.Action.addRat id c_1 pivot rupHints ratHints) =>
              if h : pivot ∈ LRAT.Clause.toList c_1 then some ⟨LRAT.Action.addRat id c_1 pivot rupHints ratHints, ⋯⟩
              else none)
          (List.map (LRAT.intActionToDefaultClauseAction ((LratFormula.ofCnf c).numVars + 1)) lratProof✝.toList))) =
    LRAT.Result.success
h2✝ : unsatisfiable (PosFin ((LratFormula.ofCnf c).numVars + 1)) (LratFormula.ofCnf c).formula
assignment : PosFin (c.numLiterals + 1) → Bool
h2 : ¬(assignment ⊨ LRAT.DefaultFormula.ofArray (List.toArray c.lift.convertLRAT'))
lratClause : LRAT.DefaultClause ((LratFormula.ofCnf c).numVars + 1)
reflectClause : CNF.Clause (PosFin (c.numLiterals + 1))
hrclause1 : reflectClause ∈ c.lift
h3 : ∀ (x : CNF.Clause (PosFin (c.numLiterals + 1))), x ∈ c.lift → CNF.Clause.eval assignment x = true
x✝ : Option (LRAT.DefaultClause (c.numLiterals + 1))
foo✝ : LRAT.DefaultClause (c.numLiterals + 1)
heq✝ : reflectClause.convertLRAT' = some foo✝
hrclause2 : some (some foo✝) = some (some lratClause)
⊢ assignment ⊨ lratClause
Tactic:
next heq =>
rw [← heq] at hrclause2
simp only [Option.some.injEq] at hrclause2
simp [CNF.Clause.convertLRAT_sat_of_sat reflectClause hrclause2, h3 reflectClause hrclause1]
State after:
no goals

State before:
c : CNF Nat
b : LratCert
x✝¹ : Option (Array LRAT.IntAction)
lratProof✝ : Array LRAT.IntAction
heq✝ : LRAT.parseLRATProof (String.toUTF8 b) = some lratProof✝
h1 :
  LRAT.lratChecker (LratFormula.ofCnf c).formula
      (List.map Subtype.val
        (List.filterMap
          (fun actOpt =>
            match actOpt with
            | none => none
            | some (LRAT.Action.addEmpty id rupHints) => some ⟨LRAT.Action.addEmpty id rupHints, True.intro⟩
            | some (LRAT.Action.addRup id c_1 rupHints) => some ⟨LRAT.Action.addRup id c_1 rupHints, True.intro⟩
            | some (LRAT.Action.del ids) => some ⟨LRAT.Action.del ids, True.intro⟩
            | some (LRAT.Action.addRat id c_1 pivot rupHints ratHints) =>
              if h : pivot ∈ LRAT.Clause.toList c_1 then some ⟨LRAT.Action.addRat id c_1 pivot rupHints ratHints, ⋯⟩
              else none)
          (List.map (LRAT.intActionToDefaultClauseAction ((LratFormula.ofCnf c).numVars + 1)) lratProof✝.toList))) =
    LRAT.Result.success
h2✝ : unsatisfiable (PosFin ((LratFormula.ofCnf c).numVars + 1)) (LratFormula.ofCnf c).formula
assignment : PosFin (c.numLiterals + 1) → Bool
h2 : ¬(assignment ⊨ LRAT.DefaultFormula.ofArray (List.toArray c.lift.convertLRAT'))
lratClause : LRAT.DefaultClause ((LratFormula.ofCnf c).numVars + 1)
reflectClause : CNF.Clause (PosFin (c.numLiterals + 1))
hrclause1 : reflectClause ∈ c.lift
h3 : ∀ (x : CNF.Clause (PosFin (c.numLiterals + 1))), x ∈ c.lift → CNF.Clause.eval assignment x = true
x✝ : Option (LRAT.DefaultClause (c.numLiterals + 1))
foo✝ : LRAT.DefaultClause (c.numLiterals + 1)
heq : reflectClause.convertLRAT' = some foo✝
hrclause2 : some (some foo✝) = some (some lratClause)
⊢ assignment ⊨ lratClause
Tactic:
rw [← heq] at hrclause2
State after:
c : CNF Nat
b : LratCert
x✝¹ : Option (Array LRAT.IntAction)
lratProof✝ : Array LRAT.IntAction
heq✝ : LRAT.parseLRATProof (String.toUTF8 b) = some lratProof✝
h1 :
  LRAT.lratChecker (LratFormula.ofCnf c).formula
      (List.map Subtype.val
        (List.filterMap
          (fun actOpt =>
            match actOpt with
            | none => none
            | some (LRAT.Action.addEmpty id rupHints) => some ⟨LRAT.Action.addEmpty id rupHints, True.intro⟩
            | some (LRAT.Action.addRup id c_1 rupHints) => some ⟨LRAT.Action.addRup id c_1 rupHints, True.intro⟩
            | some (LRAT.Action.del ids) => some ⟨LRAT.Action.del ids, True.intro⟩
            | some (LRAT.Action.addRat id c_1 pivot rupHints ratHints) =>
              if h : pivot ∈ LRAT.Clause.toList c_1 then some ⟨LRAT.Action.addRat id c_1 pivot rupHints ratHints, ⋯⟩
              else none)
          (List.map (LRAT.intActionToDefaultClauseAction ((LratFormula.ofCnf c).numVars + 1)) lratProof✝.toList))) =
    LRAT.Result.success
h2✝ : unsatisfiable (PosFin ((LratFormula.ofCnf c).numVars + 1)) (LratFormula.ofCnf c).formula
assignment : PosFin (c.numLiterals + 1) → Bool
h2 : ¬(assignment ⊨ LRAT.DefaultFormula.ofArray (List.toArray c.lift.convertLRAT'))
lratClause : LRAT.DefaultClause ((LratFormula.ofCnf c).numVars + 1)
reflectClause : CNF.Clause (PosFin (c.numLiterals + 1))
hrclause1 : reflectClause ∈ c.lift
h3 : ∀ (x : CNF.Clause (PosFin (c.numLiterals + 1))), x ∈ c.lift → CNF.Clause.eval assignment x = true
x✝ : Option (LRAT.DefaultClause (c.numLiterals + 1))
foo✝ : LRAT.DefaultClause (c.numLiterals + 1)
heq : reflectClause.convertLRAT' = some foo✝
hrclause2 : some reflectClause.convertLRAT' = some (some lratClause)
⊢ assignment ⊨ lratClause

State before:
c : CNF Nat
b : LratCert
x✝¹ : Option (Array LRAT.IntAction)
lratProof✝ : Array LRAT.IntAction
heq✝ : LRAT.parseLRATProof (String.toUTF8 b) = some lratProof✝
h1 :
  LRAT.lratChecker (LratFormula.ofCnf c).formula
      (List.map Subtype.val
        (List.filterMap
          (fun actOpt =>
            match actOpt with
            | none => none
            | some (LRAT.Action.addEmpty id rupHints) => some ⟨LRAT.Action.addEmpty id rupHints, True.intro⟩
            | some (LRAT.Action.addRup id c_1 rupHints) => some ⟨LRAT.Action.addRup id c_1 rupHints, True.intro⟩
            | some (LRAT.Action.del ids) => some ⟨LRAT.Action.del ids, True.intro⟩
            | some (LRAT.Action.addRat id c_1 pivot rupHints ratHints) =>
              if h : pivot ∈ LRAT.Clause.toList c_1 then some ⟨LRAT.Action.addRat id c_1 pivot rupHints ratHints, ⋯⟩
              else none)
          (List.map (LRAT.intActionToDefaultClauseAction ((LratFormula.ofCnf c).numVars + 1)) lratProof✝.toList))) =
    LRAT.Result.success
h2✝ : unsatisfiable (PosFin ((LratFormula.ofCnf c).numVars + 1)) (LratFormula.ofCnf c).formula
assignment : PosFin (c.numLiterals + 1) → Bool
h2 : ¬(assignment ⊨ LRAT.DefaultFormula.ofArray (List.toArray c.lift.convertLRAT'))
lratClause : LRAT.DefaultClause ((LratFormula.ofCnf c).numVars + 1)
reflectClause : CNF.Clause (PosFin (c.numLiterals + 1))
hrclause1 : reflectClause ∈ c.lift
h3 : ∀ (x : CNF.Clause (PosFin (c.numLiterals + 1))), x ∈ c.lift → CNF.Clause.eval assignment x = true
x✝ : Option (LRAT.DefaultClause (c.numLiterals + 1))
foo✝ : LRAT.DefaultClause (c.numLiterals + 1)
heq : reflectClause.convertLRAT' = some foo✝
hrclause2 : some reflectClause.convertLRAT' = some (some lratClause)
⊢ assignment ⊨ lratClause
Tactic:
simp only [Option.some.injEq] at hrclause2
State after:
c : CNF Nat
b : LratCert
x✝¹ : Option (Array LRAT.IntAction)
lratProof✝ : Array LRAT.IntAction
heq✝ : LRAT.parseLRATProof (String.toUTF8 b) = some lratProof✝
h1 :
  LRAT.lratChecker (LratFormula.ofCnf c).formula
      (List.map Subtype.val
        (List.filterMap
          (fun actOpt =>
            match actOpt with
            | none => none
            | some (LRAT.Action.addEmpty id rupHints) => some ⟨LRAT.Action.addEmpty id rupHints, True.intro⟩
            | some (LRAT.Action.addRup id c_1 rupHints) => some ⟨LRAT.Action.addRup id c_1 rupHints, True.intro⟩
            | some (LRAT.Action.del ids) => some ⟨LRAT.Action.del ids, True.intro⟩
            | some (LRAT.Action.addRat id c_1 pivot rupHints ratHints) =>
              if h : pivot ∈ LRAT.Clause.toList c_1 then some ⟨LRAT.Action.addRat id c_1 pivot rupHints ratHints, ⋯⟩
              else none)
          (List.map (LRAT.intActionToDefaultClauseAction ((LratFormula.ofCnf c).numVars + 1)) lratProof✝.toList))) =
    LRAT.Result.success
h2✝ : unsatisfiable (PosFin ((LratFormula.ofCnf c).numVars + 1)) (LratFormula.ofCnf c).formula
assignment : PosFin (c.numLiterals + 1) → Bool
h2 : ¬(assignment ⊨ LRAT.DefaultFormula.ofArray (List.toArray c.lift.convertLRAT'))
lratClause : LRAT.DefaultClause ((LratFormula.ofCnf c).numVars + 1)
reflectClause : CNF.Clause (PosFin (c.numLiterals + 1))
hrclause1 : reflectClause ∈ c.lift
h3 : ∀ (x : CNF.Clause (PosFin (c.numLiterals + 1))), x ∈ c.lift → CNF.Clause.eval assignment x = true
x✝ : Option (LRAT.DefaultClause (c.numLiterals + 1))
foo✝ : LRAT.DefaultClause (c.numLiterals + 1)
heq : reflectClause.convertLRAT' = some foo✝
hrclause2 : reflectClause.convertLRAT' = some lratClause
⊢ assignment ⊨ lratClause

State before:
c : CNF Nat
b : LratCert
x✝¹ : Option (Array LRAT.IntAction)
lratProof✝ : Array LRAT.IntAction
heq✝ : LRAT.parseLRATProof (String.toUTF8 b) = some lratProof✝
h1 :
  LRAT.lratChecker (LratFormula.ofCnf c).formula
      (List.map Subtype.val
        (List.filterMap
          (fun actOpt =>
            match actOpt with
            | none => none
            | some (LRAT.Action.addEmpty id rupHints) => some ⟨LRAT.Action.addEmpty id rupHints, True.intro⟩
            | some (LRAT.Action.addRup id c_1 rupHints) => some ⟨LRAT.Action.addRup id c_1 rupHints, True.intro⟩
            | some (LRAT.Action.del ids) => some ⟨LRAT.Action.del ids, True.intro⟩
            | some (LRAT.Action.addRat id c_1 pivot rupHints ratHints) =>
              if h : pivot ∈ LRAT.Clause.toList c_1 then some ⟨LRAT.Action.addRat id c_1 pivot rupHints ratHints, ⋯⟩
              else none)
          (List.map (LRAT.intActionToDefaultClauseAction ((LratFormula.ofCnf c).numVars + 1)) lratProof✝.toList))) =
    LRAT.Result.success
h2✝ : unsatisfiable (PosFin ((LratFormula.ofCnf c).numVars + 1)) (LratFormula.ofCnf c).formula
assignment : PosFin (c.numLiterals + 1) → Bool
h2 : ¬(assignment ⊨ LRAT.DefaultFormula.ofArray (List.toArray c.lift.convertLRAT'))
lratClause : LRAT.DefaultClause ((LratFormula.ofCnf c).numVars + 1)
reflectClause : CNF.Clause (PosFin (c.numLiterals + 1))
hrclause1 : reflectClause ∈ c.lift
h3 : ∀ (x : CNF.Clause (PosFin (c.numLiterals + 1))), x ∈ c.lift → CNF.Clause.eval assignment x = true
x✝ : Option (LRAT.DefaultClause (c.numLiterals + 1))
foo✝ : LRAT.DefaultClause (c.numLiterals + 1)
heq : reflectClause.convertLRAT' = some foo✝
hrclause2 : reflectClause.convertLRAT' = some lratClause
⊢ assignment ⊨ lratClause
Tactic:
simp [CNF.Clause.convertLRAT_sat_of_sat reflectClause hrclause2, h3 reflectClause hrclause1]
State after:
no goals

State before:
case h_1.a.intro.intro.h_2
c : CNF Nat
b : LratCert
x✝¹ : Option (Array LRAT.IntAction)
lratProof✝ : Array LRAT.IntAction
heq✝¹ : LRAT.parseLRATProof (String.toUTF8 b) = some lratProof✝
h1 :
  LRAT.lratChecker (LratFormula.ofCnf c).formula
      (List.map Subtype.val
        (List.filterMap
          (fun actOpt =>
            match actOpt with
            | none => none
            | some (LRAT.Action.addEmpty id rupHints) => some ⟨LRAT.Action.addEmpty id rupHints, True.intro⟩
            | some (LRAT.Action.addRup id c_1 rupHints) => some ⟨LRAT.Action.addRup id c_1 rupHints, True.intro⟩
            | some (LRAT.Action.del ids) => some ⟨LRAT.Action.del ids, True.intro⟩
            | some (LRAT.Action.addRat id c_1 pivot rupHints ratHints) =>
              if h : pivot ∈ LRAT.Clause.toList c_1 then some ⟨LRAT.Action.addRat id c_1 pivot rupHints ratHints, ⋯⟩
              else none)
          (List.map (LRAT.intActionToDefaultClauseAction ((LratFormula.ofCnf c).numVars + 1)) lratProof✝.toList))) =
    LRAT.Result.success
h2✝ : unsatisfiable (PosFin ((LratFormula.ofCnf c).numVars + 1)) (LratFormula.ofCnf c).formula
assignment : PosFin (c.numLiterals + 1) → Bool
h2 : ¬(assignment ⊨ LRAT.DefaultFormula.ofArray (List.toArray c.lift.convertLRAT'))
lratClause : LRAT.DefaultClause ((LratFormula.ofCnf c).numVars + 1)
reflectClause : CNF.Clause (PosFin (c.numLiterals + 1))
hrclause1 : reflectClause ∈ c.lift
h3 : ∀ (x : CNF.Clause (PosFin (c.numLiterals + 1))), x ∈ c.lift → CNF.Clause.eval assignment x = true
x✝ : Option (LRAT.DefaultClause (c.numLiterals + 1))
heq✝ : reflectClause.convertLRAT' = none
hrclause2 : none = some (some lratClause)
⊢ assignment ⊨ lratClause
Tactic:
contradiction
State after:
no goals

State before:
case h_2
c : CNF Nat
b : LratCert
x✝ : Option (Array LRAT.IntAction)
heq✝ : LRAT.parseLRATProof (String.toUTF8 b) = none
h1 : false = true
⊢ c.unsat
Tactic:
contradiction
State after:
no goals