-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Reflect.lean
theorem verifyCert_correct : ∀ cnf cert, verifyCert cnf cert = true → cnf.Unsat

Proof state:
case h_2
c : CNF Nat
b : String
x✝ : Except String (Array LRAT.IntAction)
a✝ : String
heq✝ : LRAT.parseLRATProof b.toUTF8 = Except.error a✝
h1 : false = true
⊢ c.Unsat

Tactic:
. contradiction

Result:
no goals

Proof state:
⊢ ∀ (cnf : CNF Nat) (cert : String), verifyCert cnf cert = true → cnf.Unsat

Tactic:
intro c b h1

Result:
c : CNF Nat
b : String
h1 : verifyCert c b = true
⊢ c.Unsat

Proof state:
case h_1.a
c : CNF Nat
b : String
x✝ : Except String (Array LRAT.IntAction)
lratProof✝ : Array LRAT.IntAction
heq✝ : LRAT.parseLRATProof b.toUTF8 = Except.ok lratProof✝
h1 : LRAT.check lratProof✝ c = true
⊢ LRAT.check ?h_1.lratProof c = true

case h_1.lratProof
c : CNF Nat
b : String
x✝ : Except String (Array LRAT.IntAction)
lratProof✝ : Array LRAT.IntAction
heq✝ : LRAT.parseLRATProof b.toUTF8 = Except.ok lratProof✝
h1 : LRAT.check lratProof✝ c = true
⊢ Array LRAT.IntAction

Tactic:
assumption

Result:
no goals

Proof state:
case h_1
c : CNF Nat
b : String
x✝ : Except String (Array LRAT.IntAction)
lratProof✝ : Array LRAT.IntAction
heq✝ : LRAT.parseLRATProof b.toUTF8 = Except.ok lratProof✝
h1 : LRAT.check lratProof✝ c = true
⊢ c.Unsat

Tactic:
apply LRAT.check_sound

Result:
case h_1.a
c : CNF Nat
b : String
x✝ : Except String (Array LRAT.IntAction)
lratProof✝ : Array LRAT.IntAction
heq✝ : LRAT.parseLRATProof b.toUTF8 = Except.ok lratProof✝
h1 : LRAT.check lratProof✝ c = true
⊢ LRAT.check ?h_1.lratProof c = true

case h_1.lratProof
c : CNF Nat
b : String
x✝ : Except String (Array LRAT.IntAction)
lratProof✝ : Array LRAT.IntAction
heq✝ : LRAT.parseLRATProof b.toUTF8 = Except.ok lratProof✝
h1 : LRAT.check lratProof✝ c = true
⊢ Array LRAT.IntAction

Proof state:
c : CNF Nat
b : String
h1 : verifyCert c b = true
⊢ c.Unsat

Tactic:
unfold verifyCert at h1

Result:
c : CNF Nat
b : String
h1 :
  (match LRAT.parseLRATProof b.toUTF8 with
    | Except.ok lratProof => LRAT.check lratProof c
    | Except.error a => false) =
    true
⊢ c.Unsat

Proof state:
case h_1
c : CNF Nat
b : String
x✝ : Except String (Array LRAT.IntAction)
lratProof✝ : Array LRAT.IntAction
heq✝ : LRAT.parseLRATProof b.toUTF8 = Except.ok lratProof✝
h1 : LRAT.check lratProof✝ c = true
⊢ c.Unsat

case h_2
c : CNF Nat
b : String
x✝ : Except String (Array LRAT.IntAction)
a✝ : String
heq✝ : LRAT.parseLRATProof b.toUTF8 = Except.error a✝
h1 : false = true
⊢ c.Unsat

Tactic:
. apply LRAT.check_sound
  assumption

Result:
case h_2
c : CNF Nat
b : String
x✝ : Except String (Array LRAT.IntAction)
a✝ : String
heq✝ : LRAT.parseLRATProof b.toUTF8 = Except.error a✝
h1 : false = true
⊢ c.Unsat

Proof state:
c : CNF Nat
b : String
h1 :
  (match LRAT.parseLRATProof b.toUTF8 with
    | Except.ok lratProof => LRAT.check lratProof c
    | Except.error a => false) =
    true
⊢ c.Unsat

Tactic:
split at h1

Result:
case h_1
c : CNF Nat
b : String
x✝ : Except String (Array LRAT.IntAction)
lratProof✝ : Array LRAT.IntAction
heq✝ : LRAT.parseLRATProof b.toUTF8 = Except.ok lratProof✝
h1 : LRAT.check lratProof✝ c = true
⊢ c.Unsat

case h_2
c : CNF Nat
b : String
x✝ : Except String (Array LRAT.IntAction)
a✝ : String
heq✝ : LRAT.parseLRATProof b.toUTF8 = Except.error a✝
h1 : false = true
⊢ c.Unsat

Proof state:
case h_2
c : CNF Nat
b : String
x✝ : Except String (Array LRAT.IntAction)
a✝ : String
heq✝ : LRAT.parseLRATProof b.toUTF8 = Except.error a✝
h1 : false = true
⊢ c.Unsat

Tactic:
contradiction

Result:
no goals