internlm/Lean-Github huggingface dataset:
Theorem: BVDecide.verifyCert_correct
Proof 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
Proof 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
Theorem: BVDecide.verifyCert_correct
Proof 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
Proof 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
Theorem: BVDecide.verifyCert_correct
Proof 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
Proof 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
Theorem: BVDecide.verifyCert_correct
Proof 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
Proof 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
Theorem: BVDecide.verifyCert_correct
Proof 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
Proof 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')
Theorem: BVDecide.verifyCert_correct
Proof 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]
Proof 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
Theorem: BVDecide.verifyCert_correct
Proof 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
Proof 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
Theorem: BVDecide.verifyCert_correct
Proof 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
Proof state after:
no goals
Theorem: BVDecide.verifyCert_correct
Proof 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
Proof state after:
no goals
Theorem: BVDecide.verifyCert_correct
Proof 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
Proof state after:
no goals