-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/LRATCheckerSound.lean
theorem lratCheckerSound [DecidableEq α] [Clause α β] [Entails α σ] [Formula α β σ] (f : σ)
    (f_readyForRupAdd : ReadyForRupAdd f) (f_readyForRatAdd : ReadyForRatAdd f)
    (prf : List (Action β α)) (prfWellFormed : ∀ a : Action β α, a ∈ prf → WellFormedAction a) :
    lratChecker f prf = success → Unsatisfiable α f

Proof state:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝³ : DecidableEq α
inst✝² : Clause α β
inst✝¹ : Entails α σ
inst✝ : Formula α β σ
action : Action β α
restPrf : List (Action β α)
ih :
  ∀ (f : σ),
    ReadyForRupAdd f →
      ReadyForRatAdd f →
        (∀ (a : Action β α), a ∈ restPrf → WellFormedAction a) → lratChecker f restPrf = success → Unsatisfiable α f
f : σ
f_readyForRupAdd : ReadyForRupAdd f
f_readyForRatAdd : ReadyForRatAdd f
actionWellFormed : WellFormedAction action
restPrfWellFormed : ∀ (a : Action β α), a ∈ restPrf → WellFormedAction a
prf✝ : List (Action β α)
ids : Array Nat
restPrf' : List (Action β α)
h : lratChecker (Formula.delete f ids) restPrf' = success
hprf : action = Action.del ids ∧ restPrf = restPrf'
⊢ Unsatisfiable α f

Tactic:
rw [← hprf.2] at h

Result:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝³ : DecidableEq α
inst✝² : Clause α β
inst✝¹ : Entails α σ
inst✝ : Formula α β σ
action : Action β α
restPrf : List (Action β α)
ih :
  ∀ (f : σ),
    ReadyForRupAdd f →
      ReadyForRatAdd f →
        (∀ (a : Action β α), a ∈ restPrf → WellFormedAction a) → lratChecker f restPrf = success → Unsatisfiable α f
f : σ
f_readyForRupAdd : ReadyForRupAdd f
f_readyForRatAdd : ReadyForRatAdd f
actionWellFormed : WellFormedAction action
restPrfWellFormed : ∀ (a : Action β α), a ∈ restPrf → WellFormedAction a
prf✝ : List (Action β α)
ids : Array Nat
restPrf' : List (Action β α)
h : lratChecker (Formula.delete f ids) restPrf = success
hprf : action = Action.del ids ∧ restPrf = restPrf'
⊢ Unsatisfiable α f

Proof state:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝³ : DecidableEq α
inst✝² : Clause α β
inst✝¹ : Entails α σ
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : ReadyForRupAdd f
f_readyForRatAdd : ReadyForRatAdd f
prf : List (Action β α)
prfWellFormed : ∀ (a : Action β α), a ∈ prf → WellFormedAction a
⊢ lratChecker f prf = success → Unsatisfiable α f

Tactic:
induction prf generalizing f

Result:
case nil
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝³ : DecidableEq α
inst✝² : Clause α β
inst✝¹ : Entails α σ
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : ReadyForRupAdd f
f_readyForRatAdd : ReadyForRatAdd f
prfWellFormed : ∀ (a : Action β α), a ∈ [] → WellFormedAction a
⊢ lratChecker f [] = success → Unsatisfiable α f

case cons
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝³ : DecidableEq α
inst✝² : Clause α β
inst✝¹ : Entails α σ
inst✝ : Formula α β σ
head✝ : Action β α
tail✝ : List (Action β α)
tail_ih✝ :
  ∀ (f : σ),
    ReadyForRupAdd f →
      ReadyForRatAdd f →
        (∀ (a : Action β α), a ∈ tail✝ → WellFormedAction a) → lratChecker f tail✝ = success → Unsatisfiable α f
f : σ
f_readyForRupAdd : ReadyForRupAdd f
f_readyForRatAdd : ReadyForRatAdd f
prfWellFormed : ∀ (a : Action β α), a ∈ head✝ :: tail✝ → WellFormedAction a
⊢ lratChecker f (head✝ :: tail✝) = success → Unsatisfiable α f

Proof state:
case isFalse
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝³ : DecidableEq α
inst✝² : Clause α β
inst✝¹ : Entails α σ
inst✝ : Formula α β σ
action : Action β α
restPrf : List (Action β α)
ih :
  ∀ (f : σ),
    ReadyForRupAdd f →
      ReadyForRatAdd f →
        (∀ (a : Action β α), a ∈ restPrf → WellFormedAction a) → lratChecker f restPrf = success → Unsatisfiable α f
f : σ
f_readyForRupAdd : ReadyForRupAdd f
f_readyForRatAdd : ReadyForRatAdd f
actionWellFormed : WellFormedAction action
restPrfWellFormed : ∀ (a : Action β α), a ∈ restPrf → WellFormedAction a
prf✝ : List (Action β α)
id : Nat
c : β
rupHints : Array Nat
restPrf' : List (Action β α)
hprf : action :: restPrf = Action.addRup id c rupHints :: restPrf'
x✝ : σ × Bool
f' : σ
checkSuccess : Bool
heq : performRupAdd f c rupHints = (f', checkSuccess)
h✝ : ¬checkSuccess = true
⊢ rupFailure = success → Unsatisfiable α f

Tactic:
simp [false_implies]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝³ : DecidableEq α
inst✝² : Clause α β
inst✝¹ : Entails α σ
inst✝ : Formula α β σ
action : Action β α
restPrf : List (Action β α)
ih :
  ∀ (f : σ),
    ReadyForRupAdd f →
      ReadyForRatAdd f →
        (∀ (a : Action β α), a ∈ restPrf → WellFormedAction a) → lratChecker f restPrf = success → Unsatisfiable α f
f : σ
f_readyForRupAdd : ReadyForRupAdd f
f_readyForRatAdd : ReadyForRatAdd f
actionWellFormed : WellFormedAction action
restPrfWellFormed : ∀ (a : Action β α), a ∈ restPrf → WellFormedAction a
prf✝ : List (Action β α)
id : Nat
c : β
rupHints : Array Nat
restPrf' : List (Action β α)
hprf : action :: restPrf = Action.addRup id c rupHints :: restPrf'
x✝ : σ × Bool
f' : σ
checkSuccess : Bool
heq : performRupAdd f c rupHints = (f', checkSuccess)
⊢ (if checkSuccess = true then lratChecker f' restPrf' else rupFailure) = success → Unsatisfiable α f

Tactic:
split

Result:
case isTrue
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝³ : DecidableEq α
inst✝² : Clause α β
inst✝¹ : Entails α σ
inst✝ : Formula α β σ
action : Action β α
restPrf : List (Action β α)
ih :
  ∀ (f : σ),
    ReadyForRupAdd f →
      ReadyForRatAdd f →
        (∀ (a : Action β α), a ∈ restPrf → WellFormedAction a) → lratChecker f restPrf = success → Unsatisfiable α f
f : σ
f_readyForRupAdd : ReadyForRupAdd f
f_readyForRatAdd : ReadyForRatAdd f
actionWellFormed : WellFormedAction action
restPrfWellFormed : ∀ (a : Action β α), a ∈ restPrf → WellFormedAction a
prf✝ : List (Action β α)
id : Nat
c : β
rupHints : Array Nat
restPrf' : List (Action β α)
hprf : action :: restPrf = Action.addRup id c rupHints :: restPrf'
x✝ : σ × Bool
f' : σ
checkSuccess : Bool
heq : performRupAdd f c rupHints = (f', checkSuccess)
h✝ : checkSuccess = true
⊢ lratChecker f' restPrf' = success → Unsatisfiable α f

case isFalse
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝³ : DecidableEq α
inst✝² : Clause α β
inst✝¹ : Entails α σ
inst✝ : Formula α β σ
action : Action β α
restPrf : List (Action β α)
ih :
  ∀ (f : σ),
    ReadyForRupAdd f →
      ReadyForRatAdd f →
        (∀ (a : Action β α), a ∈ restPrf → WellFormedAction a) → lratChecker f restPrf = success → Unsatisfiable α f
f : σ
f_readyForRupAdd : ReadyForRupAdd f
f_readyForRatAdd : ReadyForRatAdd f
actionWellFormed : WellFormedAction action
restPrfWellFormed : ∀ (a : Action β α), a ∈ restPrf → WellFormedAction a
prf✝ : List (Action β α)
id : Nat
c : β
rupHints : Array Nat
restPrf' : List (Action β α)
hprf : action :: restPrf = Action.addRup id c rupHints :: restPrf'
x✝ : σ × Bool
f' : σ
checkSuccess : Bool
heq : performRupAdd f c rupHints = (f', checkSuccess)
h✝ : ¬checkSuccess = true
⊢ rupFailure = success → Unsatisfiable α f