internlm/Lean-Github huggingface dataset:
Theorem: CNF.of_maxLiteral_eq_none
Proof state before:
c : CNF Nat
lit : Nat
hlit : mem lit c
h : List.filterMap Clause.maxLiteral c = []
⊢ False
Tactic:
dsimp [mem] at hlit
Proof state after:
c : CNF Nat
lit : Nat
hlit : ∃ c_1, c_1 ∈ c ∧ Clause.mem lit c_1
h : List.filterMap Clause.maxLiteral c = []
⊢ False
Theorem: CNF.of_maxLiteral_eq_none
Proof state before:
c : CNF Nat
lit : Nat
hlit : ∃ c_1, c_1 ∈ c ∧ Clause.mem lit c_1
h : List.filterMap Clause.maxLiteral c = []
⊢ False
Tactic:
rcases hlit with ⟨clause, ⟨hclause1, hclause2⟩⟩
Proof state after:
case intro.intro
c : CNF Nat
lit : Nat
h : List.filterMap Clause.maxLiteral c = []
clause : Clause Nat
hclause1 : clause ∈ c
hclause2 : Clause.mem lit clause
⊢ False
Theorem: CNF.of_maxLiteral_eq_none
Proof state before:
case intro.intro
c : CNF Nat
lit : Nat
h : List.filterMap Clause.maxLiteral c = []
clause : Clause Nat
hclause1 : clause ∈ c
hclause2 : Clause.mem lit clause
⊢ False
Tactic:
have := Clause.of_maxLiteral_eq_none clause (List.all_none_of_filterMap_eq_nil h clause hclause1) lit
Proof state after:
case intro.intro
c : CNF Nat
lit : Nat
h : List.filterMap Clause.maxLiteral c = []
clause : Clause Nat
hclause1 : clause ∈ c
hclause2 : Clause.mem lit clause
this : ¬Clause.mem lit clause
⊢ False
Theorem: CNF.of_maxLiteral_eq_none
Proof state before:
case intro.intro
c : CNF Nat
lit : Nat
h : List.filterMap Clause.maxLiteral c = []
clause : Clause Nat
hclause1 : clause ∈ c
hclause2 : Clause.mem lit clause
this : ¬Clause.mem lit clause
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: CNF.lt_numLiterals
Proof state before:
a : Nat
g : CNF Nat
h : mem a g
⊢ a < g.numLiterals
Tactic:
dsimp[numLiterals]
Proof state after:
a : Nat
g : CNF Nat
h : mem a g
⊢ a <
    match g.maxLiteral with
    | none => 0
    | some n => n + 1
Theorem: CNF.lt_numLiterals
Proof state before:
a : Nat
g : CNF Nat
h : mem a g
⊢ a <
    match g.maxLiteral with
    | none => 0
    | some n => n + 1
Tactic:
split <;> rename_i h2
Proof state after:
case h_1
a : Nat
g : CNF Nat
h : mem a g
x✝ : Option Nat
h2 : g.maxLiteral = none
⊢ a < 0

case h_2
a : Nat
g : CNF Nat
h : mem a g
x✝ : Option Nat
n✝ : Nat
h2 : g.maxLiteral = some n✝
⊢ a < n✝ + 1
Theorem: CNF.lt_numLiterals
Proof state before:
case h_1
a : Nat
g : CNF Nat
h : mem a g
x✝ : Option Nat
h2 : g.maxLiteral = none
⊢ a < 0

case h_2
a : Nat
g : CNF Nat
h : mem a g
x✝ : Option Nat
n✝ : Nat
h2 : g.maxLiteral = some n✝
⊢ a < n✝ + 1
Tactic:
. exfalso
  apply of_maxLiteral_eq_none g h2 a h
Proof state after:
case h_2
a : Nat
g : CNF Nat
h : mem a g
x✝ : Option Nat
n✝ : Nat
h2 : g.maxLiteral = some n✝
⊢ a < n✝ + 1
Theorem: CNF.lt_numLiterals
Proof state before:
case h_2
a : Nat
g : CNF Nat
h : mem a g
x✝ : Option Nat
n✝ : Nat
h2 : g.maxLiteral = some n✝
⊢ a < n✝ + 1
Tactic:
. have := of_maxLiteral_eq_some g h2 a h
  omega
Proof state after:
no goals
Theorem: CNF.lt_numLiterals
Proof state before:
case h_1
a : Nat
g : CNF Nat
h : mem a g
x✝ : Option Nat
h2 : g.maxLiteral = none
⊢ a < 0
Tactic:
exfalso
Proof state after:
case h_1
a : Nat
g : CNF Nat
h : mem a g
x✝ : Option Nat
h2 : g.maxLiteral = none
⊢ False
Theorem: CNF.lt_numLiterals
Proof state before:
case h_1
a : Nat
g : CNF Nat
h : mem a g
x✝ : Option Nat
h2 : g.maxLiteral = none
⊢ False
Tactic:
apply of_maxLiteral_eq_none g h2 a h
Proof state after:
no goals
Theorem: CNF.lt_numLiterals
Proof state before:
case h_2
a : Nat
g : CNF Nat
h : mem a g
x✝ : Option Nat
n✝ : Nat
h2 : g.maxLiteral = some n✝
⊢ a < n✝ + 1
Tactic:
have := of_maxLiteral_eq_some g h2 a h
Proof state after:
case h_2
a : Nat
g : CNF Nat
h : mem a g
x✝ : Option Nat
n✝ : Nat
h2 : g.maxLiteral = some n✝
this : a ≤ n✝
⊢ a < n✝ + 1
Theorem: CNF.lt_numLiterals
Proof state before:
case h_2
a : Nat
g : CNF Nat
h : mem a g
x✝ : Option Nat
n✝ : Nat
h2 : g.maxLiteral = some n✝
this : a ≤ n✝
⊢ a < n✝ + 1
Tactic:
omega
Proof state after:
no goals
Theorem: CNF.unsat_relabelFin
Proof state before:
g : CNF Nat
⊢ g.relabelFin.unsat ↔ g.unsat
Tactic:
dsimp [relabelFin]
Proof state after:
g : CNF Nat
⊢ (if h : ∃ a, mem a g then relabel (fun i => if w : i < g.numLiterals then ⟨i, w⟩ else ⟨0, ⋯⟩) g
      else List.replicate (List.length g) []).unsat ↔
    g.unsat
Theorem: CNF.unsat_relabelFin
Proof state before:
g : CNF Nat
⊢ (if h : ∃ a, mem a g then relabel (fun i => if w : i < g.numLiterals then ⟨i, w⟩ else ⟨0, ⋯⟩) g
      else List.replicate (List.length g) []).unsat ↔
    g.unsat
Tactic:
split <;> rename_i h
Proof state after:
case isTrue
g : CNF Nat
h : ∃ a, mem a g
⊢ (relabel (fun i => if w : i < g.numLiterals then ⟨i, w⟩ else ⟨0, ⋯⟩) g).unsat ↔ g.unsat

case isFalse
g : CNF Nat
h : ¬∃ a, mem a g
⊢ unsat (List.replicate (List.length g) []) ↔ g.unsat
Theorem: CNF.unsat_relabelFin
Proof state before:
case isTrue
g : CNF Nat
h : ∃ a, mem a g
⊢ (relabel (fun i => if w : i < g.numLiterals then ⟨i, w⟩ else ⟨0, ⋯⟩) g).unsat ↔ g.unsat
Tactic:
apply unsat_relabel_iff
Proof state after:
case isTrue.w
g : CNF Nat
h : ∃ a, mem a g
⊢ ∀ {a b : Nat},
    mem a g →
      mem b g →
        ((if w : a < g.numLiterals then ⟨a, w⟩ else ⟨0, ⋯⟩) = if w : b < g.numLiterals then ⟨b, w⟩ else ⟨0, ⋯⟩) → a = b
Theorem: CNF.unsat_relabelFin
Proof state before:
case isTrue.w
g : CNF Nat
h : ∃ a, mem a g
⊢ ∀ {a b : Nat},
    mem a g →
      mem b g →
        ((if w : a < g.numLiterals then ⟨a, w⟩ else ⟨0, ⋯⟩) = if w : b < g.numLiterals then ⟨b, w⟩ else ⟨0, ⋯⟩) → a = b
Tactic:
intro a b ma mb
Proof state after:
case isTrue.w
g : CNF Nat
h : ∃ a, mem a g
a b : Nat
ma : mem a g
mb : mem b g
⊢ ((if w : a < g.numLiterals then ⟨a, w⟩ else ⟨0, ⋯⟩) = if w : b < g.numLiterals then ⟨b, w⟩ else ⟨0, ⋯⟩) → a = b
Theorem: CNF.unsat_relabelFin
Proof state before:
case isTrue.w
g : CNF Nat
h : ∃ a, mem a g
a b : Nat
ma : mem a g
mb : mem b g
⊢ ((if w : a < g.numLiterals then ⟨a, w⟩ else ⟨0, ⋯⟩) = if w : b < g.numLiterals then ⟨b, w⟩ else ⟨0, ⋯⟩) → a = b
Tactic:
replace ma := lt_numLiterals ma
Proof state after:
case isTrue.w
g : CNF Nat
h : ∃ a, mem a g
a b : Nat
mb : mem b g
ma : a < g.numLiterals
⊢ ((if w : a < g.numLiterals then ⟨a, w⟩ else ⟨0, ⋯⟩) = if w : b < g.numLiterals then ⟨b, w⟩ else ⟨0, ⋯⟩) → a = b
Theorem: CNF.unsat_relabelFin
Proof state before:
case isTrue.w
g : CNF Nat
h : ∃ a, mem a g
a b : Nat
mb : mem b g
ma : a < g.numLiterals
⊢ ((if w : a < g.numLiterals then ⟨a, w⟩ else ⟨0, ⋯⟩) = if w : b < g.numLiterals then ⟨b, w⟩ else ⟨0, ⋯⟩) → a = b
Tactic:
replace mb := lt_numLiterals mb
Proof state after:
case isTrue.w
g : CNF Nat
h : ∃ a, mem a g
a b : Nat
ma : a < g.numLiterals
mb : b < g.numLiterals
⊢ ((if w : a < g.numLiterals then ⟨a, w⟩ else ⟨0, ⋯⟩) = if w : b < g.numLiterals then ⟨b, w⟩ else ⟨0, ⋯⟩) → a = b
Theorem: CNF.unsat_relabelFin
Proof state before:
case isTrue.w
g : CNF Nat
h : ∃ a, mem a g
a b : Nat
ma : a < g.numLiterals
mb : b < g.numLiterals
⊢ ((if w : a < g.numLiterals then ⟨a, w⟩ else ⟨0, ⋯⟩) = if w : b < g.numLiterals then ⟨b, w⟩ else ⟨0, ⋯⟩) → a = b
Tactic:
split <;> rename_i a_lt
Proof state after:
case isTrue.w.isTrue
g : CNF Nat
h : ∃ a, mem a g
a b : Nat
ma : a < g.numLiterals
mb : b < g.numLiterals
a_lt : a < g.numLiterals
⊢ ⟨a, a_lt⟩ = ⟨b, mb⟩ → a = b

case isTrue.w.isFalse
g : CNF Nat
h : ∃ a, mem a g
a b : Nat
ma : a < g.numLiterals
mb : b < g.numLiterals
a_lt : ¬a < g.numLiterals
⊢ ⟨a, ma⟩ = ⟨b, mb⟩ → a = b
Theorem: CNF.unsat_relabelFin
Proof state before:
case isTrue.w.isTrue
g : CNF Nat
h : ∃ a, mem a g
a b : Nat
ma : a < g.numLiterals
mb : b < g.numLiterals
a_lt : a < g.numLiterals
⊢ ⟨a, a_lt⟩ = ⟨b, mb⟩ → a = b
Tactic:
simp
Proof state after:
no goals
Theorem: CNF.unsat_relabelFin
Proof state before:
case isTrue.w.isFalse
g : CNF Nat
h : ∃ a, mem a g
a b : Nat
ma : a < g.numLiterals
mb : b < g.numLiterals
a_lt : ¬a < g.numLiterals
⊢ ⟨a, ma⟩ = ⟨b, mb⟩ → a = b
Tactic:
contradiction
Proof state after:
no goals
Theorem: CNF.unsat_relabelFin
Proof state before:
case isFalse
g : CNF Nat
h : ¬∃ a, mem a g
⊢ unsat (List.replicate (List.length g) []) ↔ g.unsat
Tactic:
cases g with
| nil => simp
| cons c g =>
  simp only [not_mem_cons] at h
  obtain ⟨n, h⟩ := h
  cases n with
  | zero => simp at h
  | succ n =>
    simp_all
Proof state after:
no goals
Theorem: CNF.unsat_relabelFin
Proof state before:
case isFalse.nil
h : ¬∃ a, mem a []
⊢ unsat (List.replicate [].length []) ↔ unsat []
Tactic:
simp
Proof state after:
no goals
Theorem: CNF.unsat_relabelFin
Proof state before:
case isFalse.cons
c : Clause Nat
g : List (Clause Nat)
h : ¬∃ a, mem a (c :: g)
⊢ unsat (List.replicate (c :: g).length []) ↔ unsat (c :: g)
Tactic:
simp only [not_mem_cons] at h
Proof state after:
case isFalse.cons
c : Clause Nat
g : List (Clause Nat)
h : ∃ n, c :: g = List.replicate n []
⊢ unsat (List.replicate (c :: g).length []) ↔ unsat (c :: g)
Theorem: CNF.unsat_relabelFin
Proof state before:
case isFalse.cons
c : Clause Nat
g : List (Clause Nat)
h : ∃ n, c :: g = List.replicate n []
⊢ unsat (List.replicate (c :: g).length []) ↔ unsat (c :: g)
Tactic:
obtain ⟨n, h⟩ := h
Proof state after:
case isFalse.cons.intro
c : Clause Nat
g : List (Clause Nat)
n : Nat
h : c :: g = List.replicate n []
⊢ unsat (List.replicate (c :: g).length []) ↔ unsat (c :: g)
Theorem: CNF.unsat_relabelFin
Proof state before:
case isFalse.cons.intro
c : Clause Nat
g : List (Clause Nat)
n : Nat
h : c :: g = List.replicate n []
⊢ unsat (List.replicate (c :: g).length []) ↔ unsat (c :: g)
Tactic:
cases n with
| zero => simp at h
| succ n =>
  simp_all
Proof state after:
no goals
Theorem: CNF.unsat_relabelFin
Proof state before:
case isFalse.cons.intro.zero
c : Clause Nat
g : List (Clause Nat)
h : c :: g = List.replicate 0 []
⊢ unsat (List.replicate (c :: g).length []) ↔ unsat (c :: g)
Tactic:
simp at h
Proof state after:
no goals
Theorem: CNF.unsat_relabelFin
Proof state before:
case isFalse.cons.intro.succ
c : Clause Nat
g : List (Clause Nat)
n : Nat
h : c :: g = List.replicate (n + 1) []
⊢ unsat (List.replicate (c :: g).length []) ↔ unsat (c :: g)
Tactic:
simp_all
Proof state after:
no goals
Theorem: BVDecide.verifyCert_correct
Proof state before:
⊢ ∀ (cnf : CNF Nat) (cert : LratCert), verifyCert (LratFormula.ofCnf cnf) cert = true → cnf.unsat
Tactic:
intro c b h1
Proof state after:
c : CNF Nat
b : LratCert
h1 : verifyCert (LratFormula.ofCnf c) b = true
⊢ c.unsat
Theorem: BVDecide.verifyCert_correct
Proof state before:
c : CNF Nat
b : LratCert
h1 : verifyCert (LratFormula.ofCnf c) b = true
⊢ c.unsat
Tactic:
dsimp[verifyCert] at h1
Proof 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
Theorem: BVDecide.verifyCert_correct
Proof 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
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 :
  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
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 :
  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
Proof 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
Theorem: BVDecide.verifyCert_correct
Proof 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
Proof state after:
no goals
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 :
  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
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
⊢ c.unsat
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
⊢ 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
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
⊢ c.unsat
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.unsat
Tactic:
apply CNF.unsat_of_lift_unsat c
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
⊢ c.lift.unsat