Theorem: LRAT.DefaultFormula.performRatCheck_fold_preserves_formula (LeanSAT/LRAT/Formula/RatAddResult.lean)

State before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
p : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
⊢ let performRatCheck_fold_res :=
    Array.foldl (fun x ratHint => if x.snd = true then x.fst.performRatCheck p ratHint else (x.fst, false)) (f, true)
      ratHints 0;
  performRatCheck_fold_res.fst = f
Tactic:
let motive (_idx : Nat) (acc : DefaultFormula n × Bool) := acc.1 = f
State after:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
p : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
motive : Nat → DefaultFormula n × Bool → Prop := fun _idx acc => acc.fst = f
⊢ let performRatCheck_fold_res :=
    Array.foldl (fun x ratHint => if x.snd = true then x.fst.performRatCheck p ratHint else (x.fst, false)) (f, true)
      ratHints 0;
  performRatCheck_fold_res.fst = f

State before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
p : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
motive : Nat → DefaultFormula n × Bool → Prop := fun _idx acc => acc.fst = f
⊢ let performRatCheck_fold_res :=
    Array.foldl (fun x ratHint => if x.snd = true then x.fst.performRatCheck p ratHint else (x.fst, false)) (f, true)
      ratHints 0;
  performRatCheck_fold_res.fst = f
Tactic:
have h_base : motive 0 (f, true) := rfl
State after:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
p : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
motive : Nat → DefaultFormula n × Bool → Prop := fun _idx acc => acc.fst = f
h_base : motive 0 (f, true)
⊢ let performRatCheck_fold_res :=
    Array.foldl (fun x ratHint => if x.snd = true then x.fst.performRatCheck p ratHint else (x.fst, false)) (f, true)
      ratHints 0;
  performRatCheck_fold_res.fst = f

State before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
p : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
motive : Nat → DefaultFormula n × Bool → Prop := fun _idx acc => acc.fst = f
h_base : motive 0 (f, true)
⊢ let performRatCheck_fold_res :=
    Array.foldl (fun x ratHint => if x.snd = true then x.fst.performRatCheck p ratHint else (x.fst, false)) (f, true)
      ratHints 0;
  performRatCheck_fold_res.fst = f
Tactic:
have h_inductive (idx : Fin ratHints.size) (acc : DefaultFormula n × Bool) :
  motive idx.1 acc → motive (idx.1 + 1) (if acc.2 then performRatCheck acc.1 p ratHints[idx] else (acc.1, false)) := by
  intro ih
  rw [ih]
  split
  . exact performRatCheck_preserves_formula f hf p ratHints[idx]
  . rfl
State after:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
p : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
motive : Nat → DefaultFormula n × Bool → Prop := fun _idx acc => acc.fst = f
h_base : motive 0 (f, true)
h_inductive :
  ∀ (idx : Fin ratHints.size) (acc : DefaultFormula n × Bool),
    motive (↑idx) acc →
      motive (↑idx + 1) (if acc.snd = true then acc.fst.performRatCheck p ratHints[idx] else (acc.fst, false))
⊢ let performRatCheck_fold_res :=
    Array.foldl (fun x ratHint => if x.snd = true then x.fst.performRatCheck p ratHint else (x.fst, false)) (f, true)
      ratHints 0;
  performRatCheck_fold_res.fst = f

State before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
p : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
motive : Nat → DefaultFormula n × Bool → Prop := fun _idx acc => acc.fst = f
h_base : motive 0 (f, true)
h_inductive :
  ∀ (idx : Fin ratHints.size) (acc : DefaultFormula n × Bool),
    motive (↑idx) acc →
      motive (↑idx + 1) (if acc.snd = true then acc.fst.performRatCheck p ratHints[idx] else (acc.fst, false))
⊢ let performRatCheck_fold_res :=
    Array.foldl (fun x ratHint => if x.snd = true then x.fst.performRatCheck p ratHint else (x.fst, false)) (f, true)
      ratHints 0;
  performRatCheck_fold_res.fst = f
Tactic:
exact Array.foldl_induction motive h_base h_inductive
State after:
no goals

State before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
p : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
motive : Nat → DefaultFormula n × Bool → Prop := fun _idx acc => acc.fst = f
h_base : motive 0 (f, true)
idx : Fin ratHints.size
acc : DefaultFormula n × Bool
⊢ motive (↑idx) acc →
    motive (↑idx + 1) (if acc.snd = true then acc.fst.performRatCheck p ratHints[idx] else (acc.fst, false))
Tactic:
intro ih
State after:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
p : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
motive : Nat → DefaultFormula n × Bool → Prop := fun _idx acc => acc.fst = f
h_base : motive 0 (f, true)
idx : Fin ratHints.size
acc : DefaultFormula n × Bool
ih : motive (↑idx) acc
⊢ motive (↑idx + 1) (if acc.snd = true then acc.fst.performRatCheck p ratHints[idx] else (acc.fst, false))

State before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
p : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
motive : Nat → DefaultFormula n × Bool → Prop := fun _idx acc => acc.fst = f
h_base : motive 0 (f, true)
idx : Fin ratHints.size
acc : DefaultFormula n × Bool
ih : motive (↑idx) acc
⊢ motive (↑idx + 1) (if acc.snd = true then acc.fst.performRatCheck p ratHints[idx] else (acc.fst, false))
Tactic:
rw [ih]
State after:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
p : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
motive : Nat → DefaultFormula n × Bool → Prop := fun _idx acc => acc.fst = f
h_base : motive 0 (f, true)
idx : Fin ratHints.size
acc : DefaultFormula n × Bool
ih : motive (↑idx) acc
⊢ motive (↑idx + 1) (if acc.snd = true then f.performRatCheck p ratHints[idx] else (f, false))

State before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
p : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
motive : Nat → DefaultFormula n × Bool → Prop := fun _idx acc => acc.fst = f
h_base : motive 0 (f, true)
idx : Fin ratHints.size
acc : DefaultFormula n × Bool
ih : motive (↑idx) acc
⊢ motive (↑idx + 1) (if acc.snd = true then f.performRatCheck p ratHints[idx] else (f, false))
Tactic:
split
State after:
case isTrue
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
p : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
motive : Nat → DefaultFormula n × Bool → Prop := fun _idx acc => acc.fst = f
h_base : motive 0 (f, true)
idx : Fin ratHints.size
acc : DefaultFormula n × Bool
ih : motive (↑idx) acc
h✝ : acc.snd = true
⊢ motive (↑idx + 1) (f.performRatCheck p ratHints[idx])

case isFalse
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
p : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
motive : Nat → DefaultFormula n × Bool → Prop := fun _idx acc => acc.fst = f
h_base : motive 0 (f, true)
idx : Fin ratHints.size
acc : DefaultFormula n × Bool
ih : motive (↑idx) acc
h✝ : ¬acc.snd = true
⊢ motive (↑idx + 1) (f, false)

State before:
case isTrue
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
p : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
motive : Nat → DefaultFormula n × Bool → Prop := fun _idx acc => acc.fst = f
h_base : motive 0 (f, true)
idx : Fin ratHints.size
acc : DefaultFormula n × Bool
ih : motive (↑idx) acc
h✝ : acc.snd = true
⊢ motive (↑idx + 1) (f.performRatCheck p ratHints[idx])

case isFalse
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
p : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
motive : Nat → DefaultFormula n × Bool → Prop := fun _idx acc => acc.fst = f
h_base : motive 0 (f, true)
idx : Fin ratHints.size
acc : DefaultFormula n × Bool
ih : motive (↑idx) acc
h✝ : ¬acc.snd = true
⊢ motive (↑idx + 1) (f, false)
Tactic:
. exact performRatCheck_preserves_formula f hf p ratHints[idx]
State after:
case isFalse
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
p : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
motive : Nat → DefaultFormula n × Bool → Prop := fun _idx acc => acc.fst = f
h_base : motive 0 (f, true)
idx : Fin ratHints.size
acc : DefaultFormula n × Bool
ih : motive (↑idx) acc
h✝ : ¬acc.snd = true
⊢ motive (↑idx + 1) (f, false)

State before:
case isFalse
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
p : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
motive : Nat → DefaultFormula n × Bool → Prop := fun _idx acc => acc.fst = f
h_base : motive 0 (f, true)
idx : Fin ratHints.size
acc : DefaultFormula n × Bool
ih : motive (↑idx) acc
h✝ : ¬acc.snd = true
⊢ motive (↑idx + 1) (f, false)
Tactic:
. rfl
State after:
no goals

State before:
case isTrue
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
p : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
motive : Nat → DefaultFormula n × Bool → Prop := fun _idx acc => acc.fst = f
h_base : motive 0 (f, true)
idx : Fin ratHints.size
acc : DefaultFormula n × Bool
ih : motive (↑idx) acc
h✝ : acc.snd = true
⊢ motive (↑idx + 1) (f.performRatCheck p ratHints[idx])
Tactic:
exact performRatCheck_preserves_formula f hf p ratHints[idx]
State after:
no goals

State before:
case isFalse
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
p : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
motive : Nat → DefaultFormula n × Bool → Prop := fun _idx acc => acc.fst = f
h_base : motive 0 (f, true)
idx : Fin ratHints.size
acc : DefaultFormula n × Bool
ih : motive (↑idx) acc
h✝ : ¬acc.snd = true
⊢ motive (↑idx + 1) (f, false)
Tactic:
rfl
State after:
no goals