internlm/Lean-Github huggingface dataset:
Theorem: LRAT.DefaultFormula.performRatCheck_success_of_performRatCheck_fold_success
Proof state before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
p : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
i : Fin ratHints.size
performRatCheck_fold_success :
  (Array.foldl (fun acc ratHint => if acc.snd = true then acc.fst.performRatCheck p ratHint else (acc.fst, false))
        (f, true) ratHints 0).snd =
    true
motive : Nat → DefaultFormula n × Bool → Prop :=
  fun idx acc => acc.fst = f ∧ (acc.snd = true → ∀ (i : Fin idx), (f.performRatCheck p ratHints[i]!).snd = true)
h_base : motive 0 (f, true)
fold_fn : DefaultFormula n × Bool → Nat × Array Nat → DefaultFormula n × Bool :=
  fun acc ratHint => if acc.snd = true then acc.fst.performRatCheck p ratHint else (acc.fst, false)
fold_fn_def :
  ∀ (acc : DefaultFormula n × Bool) (ratHint : Nat × Array Nat),
    fold_fn acc ratHint = if acc.snd = true then acc.fst.performRatCheck p ratHint else (acc.fst, false)
h_inductive :
  ∀ (idx : Fin ratHints.size) (acc : DefaultFormula n × Bool),
    motive (↑idx) acc → motive (↑idx + 1) (fold_fn acc ratHints[idx])
h : (f.performRatCheck p ratHints[i]!).snd = true
⊢ (f.performRatCheck p ratHints[i]).snd = true
Tactic:
simp only [getElem!, i.2, dite_true] at h
Proof state after:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
p : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
i : Fin ratHints.size
performRatCheck_fold_success :
  (Array.foldl (fun acc ratHint => if acc.snd = true then acc.fst.performRatCheck p ratHint else (acc.fst, false))
        (f, true) ratHints 0).snd =
    true
motive : Nat → DefaultFormula n × Bool → Prop :=
  fun idx acc => acc.fst = f ∧ (acc.snd = true → ∀ (i : Fin idx), (f.performRatCheck p ratHints[i]!).snd = true)
h_base : motive 0 (f, true)
fold_fn : DefaultFormula n × Bool → Nat × Array Nat → DefaultFormula n × Bool :=
  fun acc ratHint => if acc.snd = true then acc.fst.performRatCheck p ratHint else (acc.fst, false)
fold_fn_def :
  ∀ (acc : DefaultFormula n × Bool) (ratHint : Nat × Array Nat),
    fold_fn acc ratHint = if acc.snd = true then acc.fst.performRatCheck p ratHint else (acc.fst, false)
h_inductive :
  ∀ (idx : Fin ratHints.size) (acc : DefaultFormula n × Bool),
    motive (↑idx) acc → motive (↑idx + 1) (fold_fn acc ratHints[idx])
h : (f.performRatCheck p (ratHints.get ⟨↑i, ⋯⟩)).snd = true
⊢ (f.performRatCheck p ratHints[i]).snd = true
Theorem: LRAT.DefaultFormula.performRatCheck_success_of_performRatCheck_fold_success
Proof state before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
p : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
i : Fin ratHints.size
performRatCheck_fold_success :
  (Array.foldl (fun acc ratHint => if acc.snd = true then acc.fst.performRatCheck p ratHint else (acc.fst, false))
        (f, true) ratHints 0).snd =
    true
motive : Nat → DefaultFormula n × Bool → Prop :=
  fun idx acc => acc.fst = f ∧ (acc.snd = true → ∀ (i : Fin idx), (f.performRatCheck p ratHints[i]!).snd = true)
h_base : motive 0 (f, true)
fold_fn : DefaultFormula n × Bool → Nat × Array Nat → DefaultFormula n × Bool :=
  fun acc ratHint => if acc.snd = true then acc.fst.performRatCheck p ratHint else (acc.fst, false)
fold_fn_def :
  ∀ (acc : DefaultFormula n × Bool) (ratHint : Nat × Array Nat),
    fold_fn acc ratHint = if acc.snd = true then acc.fst.performRatCheck p ratHint else (acc.fst, false)
h_inductive :
  ∀ (idx : Fin ratHints.size) (acc : DefaultFormula n × Bool),
    motive (↑idx) acc → motive (↑idx + 1) (fold_fn acc ratHints[idx])
h : (f.performRatCheck p (ratHints.get ⟨↑i, ⋯⟩)).snd = true
⊢ (f.performRatCheck p ratHints[i]).snd = true
Tactic:
exact h
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.performRatCheck_success_of_performRatCheck_fold_success
Proof state before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
p : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
i : Fin ratHints.size
performRatCheck_fold_success :
  (Array.foldl (fun acc ratHint => if acc.snd = true then acc.fst.performRatCheck p ratHint else (acc.fst, false))
        (f, true) ratHints 0).snd =
    true
motive : Nat → DefaultFormula n × Bool → Prop :=
  fun idx acc => acc.fst = f ∧ (acc.snd = true → ∀ (i : Fin idx), (f.performRatCheck p ratHints[i]!).snd = true)
⊢ motive 0 (f, true)
Tactic:
constructor
Proof state after:
case left
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
p : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
i : Fin ratHints.size
performRatCheck_fold_success :
  (Array.foldl (fun acc ratHint => if acc.snd = true then acc.fst.performRatCheck p ratHint else (acc.fst, false))
        (f, true) ratHints 0).snd =
    true
motive : Nat → DefaultFormula n × Bool → Prop :=
  fun idx acc => acc.fst = f ∧ (acc.snd = true → ∀ (i : Fin idx), (f.performRatCheck p ratHints[i]!).snd = true)
⊢ (f, true).fst = f

case right
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
p : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
i : Fin ratHints.size
performRatCheck_fold_success :
  (Array.foldl (fun acc ratHint => if acc.snd = true then acc.fst.performRatCheck p ratHint else (acc.fst, false))
        (f, true) ratHints 0).snd =
    true
motive : Nat → DefaultFormula n × Bool → Prop :=
  fun idx acc => acc.fst = f ∧ (acc.snd = true → ∀ (i : Fin idx), (f.performRatCheck p ratHints[i]!).snd = true)
⊢ (f, true).snd = true → ∀ (i : Fin 0), (f.performRatCheck p ratHints[i]!).snd = true
Theorem: LRAT.DefaultFormula.performRatCheck_success_of_performRatCheck_fold_success
Proof state before:
case left
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
p : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
i : Fin ratHints.size
performRatCheck_fold_success :
  (Array.foldl (fun acc ratHint => if acc.snd = true then acc.fst.performRatCheck p ratHint else (acc.fst, false))
        (f, true) ratHints 0).snd =
    true
motive : Nat → DefaultFormula n × Bool → Prop :=
  fun idx acc => acc.fst = f ∧ (acc.snd = true → ∀ (i : Fin idx), (f.performRatCheck p ratHints[i]!).snd = true)
⊢ (f, true).fst = f

case right
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
p : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
i : Fin ratHints.size
performRatCheck_fold_success :
  (Array.foldl (fun acc ratHint => if acc.snd = true then acc.fst.performRatCheck p ratHint else (acc.fst, false))
        (f, true) ratHints 0).snd =
    true
motive : Nat → DefaultFormula n × Bool → Prop :=
  fun idx acc => acc.fst = f ∧ (acc.snd = true → ∀ (i : Fin idx), (f.performRatCheck p ratHints[i]!).snd = true)
⊢ (f, true).snd = true → ∀ (i : Fin 0), (f.performRatCheck p ratHints[i]!).snd = true
Tactic:
. rfl
Proof state after:
case right
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
p : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
i : Fin ratHints.size
performRatCheck_fold_success :
  (Array.foldl (fun acc ratHint => if acc.snd = true then acc.fst.performRatCheck p ratHint else (acc.fst, false))
        (f, true) ratHints 0).snd =
    true
motive : Nat → DefaultFormula n × Bool → Prop :=
  fun idx acc => acc.fst = f ∧ (acc.snd = true → ∀ (i : Fin idx), (f.performRatCheck p ratHints[i]!).snd = true)
⊢ (f, true).snd = true → ∀ (i : Fin 0), (f.performRatCheck p ratHints[i]!).snd = true
Theorem: LRAT.DefaultFormula.performRatCheck_success_of_performRatCheck_fold_success
Proof state before:
case right
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
p : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
i : Fin ratHints.size
performRatCheck_fold_success :
  (Array.foldl (fun acc ratHint => if acc.snd = true then acc.fst.performRatCheck p ratHint else (acc.fst, false))
        (f, true) ratHints 0).snd =
    true
motive : Nat → DefaultFormula n × Bool → Prop :=
  fun idx acc => acc.fst = f ∧ (acc.snd = true → ∀ (i : Fin idx), (f.performRatCheck p ratHints[i]!).snd = true)
⊢ (f, true).snd = true → ∀ (i : Fin 0), (f.performRatCheck p ratHints[i]!).snd = true
Tactic:
. intro _ i
  exact Fin.elim0 i
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.performRatCheck_success_of_performRatCheck_fold_success
Proof state before:
case left
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
p : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
i : Fin ratHints.size
performRatCheck_fold_success :
  (Array.foldl (fun acc ratHint => if acc.snd = true then acc.fst.performRatCheck p ratHint else (acc.fst, false))
        (f, true) ratHints 0).snd =
    true
motive : Nat → DefaultFormula n × Bool → Prop :=
  fun idx acc => acc.fst = f ∧ (acc.snd = true → ∀ (i : Fin idx), (f.performRatCheck p ratHints[i]!).snd = true)
⊢ (f, true).fst = f
Tactic:
rfl
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.performRatCheck_success_of_performRatCheck_fold_success
Proof state before:
case right
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
p : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
i : Fin ratHints.size
performRatCheck_fold_success :
  (Array.foldl (fun acc ratHint => if acc.snd = true then acc.fst.performRatCheck p ratHint else (acc.fst, false))
        (f, true) ratHints 0).snd =
    true
motive : Nat → DefaultFormula n × Bool → Prop :=
  fun idx acc => acc.fst = f ∧ (acc.snd = true → ∀ (i : Fin idx), (f.performRatCheck p ratHints[i]!).snd = true)
⊢ (f, true).snd = true → ∀ (i : Fin 0), (f.performRatCheck p ratHints[i]!).snd = true
Tactic:
intro _ i
Proof state after:
case right
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
p : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
i✝ : Fin ratHints.size
performRatCheck_fold_success :
  (Array.foldl (fun acc ratHint => if acc.snd = true then acc.fst.performRatCheck p ratHint else (acc.fst, false))
        (f, true) ratHints 0).snd =
    true
motive : Nat → DefaultFormula n × Bool → Prop :=
  fun idx acc => acc.fst = f ∧ (acc.snd = true → ∀ (i : Fin idx), (f.performRatCheck p ratHints[i]!).snd = true)
a✝ : (f, true).snd = true
i : Fin 0
⊢ (f.performRatCheck p ratHints[i]!).snd = true
Theorem: LRAT.DefaultFormula.performRatCheck_success_of_performRatCheck_fold_success
Proof state before:
case right
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
p : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
i✝ : Fin ratHints.size
performRatCheck_fold_success :
  (Array.foldl (fun acc ratHint => if acc.snd = true then acc.fst.performRatCheck p ratHint else (acc.fst, false))
        (f, true) ratHints 0).snd =
    true
motive : Nat → DefaultFormula n × Bool → Prop :=
  fun idx acc => acc.fst = f ∧ (acc.snd = true → ∀ (i : Fin idx), (f.performRatCheck p ratHints[i]!).snd = true)
a✝ : (f, true).snd = true
i : Fin 0
⊢ (f.performRatCheck p ratHints[i]!).snd = true
Tactic:
exact Fin.elim0 i
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.performRatCheck_success_of_performRatCheck_fold_success
Proof state before:
case right
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
p : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
i : Fin ratHints.size
performRatCheck_fold_success :
  (Array.foldl (fun acc ratHint => if acc.snd = true then acc.fst.performRatCheck p ratHint else (acc.fst, false))
        (f, true) ratHints 0).snd =
    true
motive : Nat → DefaultFormula n × Bool → Prop :=
  fun idx acc => acc.fst = f ∧ (acc.snd = true → ∀ (i : Fin idx), (f.performRatCheck p ratHints[i]!).snd = true)
h_base : motive 0 (f, true)
fold_fn : DefaultFormula n × Bool → Nat × Array Nat → DefaultFormula n × Bool :=
  fun acc ratHint => if acc.snd = true then acc.fst.performRatCheck p ratHint else (acc.fst, false)
fold_fn_def :
  ∀ (acc : DefaultFormula n × Bool) (ratHint : Nat × Array Nat),
    fold_fn acc ratHint = if acc.snd = true then acc.fst.performRatCheck p ratHint else (acc.fst, false)
idx : Fin ratHints.size
acc : DefaultFormula n × Bool
ih : motive (↑idx) acc
⊢ (fold_fn acc ratHints[idx]).snd = true → ∀ (i : Fin (↑idx + 1)), (f.performRatCheck p ratHints[i]!).snd = true
Tactic:
. intro h i
  rw [fold_fn_def] at h
  split at h
  . next acc_eq_true =>
    have i_lt_or_eq_idx : i.1 < idx.1 ∨ i.1 = idx.1 := by
      omega
    rcases i_lt_or_eq_idx with i_lt_idx | i_eq_idx
    . exact ih.2 acc_eq_true ⟨i.1, i_lt_idx⟩
    . simp only [getElem!, i_eq_idx, idx.2, Fin.getElem_fin, dite_true]
      simp only [Fin.getElem_fin, ih.1] at h
      exact h
  . simp only at h
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.performRatCheck_success_of_performRatCheck_fold_success
Proof state before:
case left
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
p : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
i : Fin ratHints.size
performRatCheck_fold_success :
  (Array.foldl (fun acc ratHint => if acc.snd = true then acc.fst.performRatCheck p ratHint else (acc.fst, false))
        (f, true) ratHints 0).snd =
    true
motive : Nat → DefaultFormula n × Bool → Prop :=
  fun idx acc => acc.fst = f ∧ (acc.snd = true → ∀ (i : Fin idx), (f.performRatCheck p ratHints[i]!).snd = true)
h_base : motive 0 (f, true)
fold_fn : DefaultFormula n × Bool → Nat × Array Nat → DefaultFormula n × Bool :=
  fun acc ratHint => if acc.snd = true then acc.fst.performRatCheck p ratHint else (acc.fst, false)
fold_fn_def :
  ∀ (acc : DefaultFormula n × Bool) (ratHint : Nat × Array Nat),
    fold_fn acc ratHint = if acc.snd = true then acc.fst.performRatCheck p ratHint else (acc.fst, false)
idx : Fin ratHints.size
acc : DefaultFormula n × Bool
ih : motive (↑idx) acc
⊢ (fold_fn acc ratHints[idx]).fst = f
Tactic:
simp only [Fin.getElem_fin, fold_fn_def, ih.1]
Proof state after:
case left
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
p : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
i : Fin ratHints.size
performRatCheck_fold_success :
  (Array.foldl (fun acc ratHint => if acc.snd = true then acc.fst.performRatCheck p ratHint else (acc.fst, false))
        (f, true) ratHints 0).snd =
    true
motive : Nat → DefaultFormula n × Bool → Prop :=
  fun idx acc => acc.fst = f ∧ (acc.snd = true → ∀ (i : Fin idx), (f.performRatCheck p ratHints[i]!).snd = true)
h_base : motive 0 (f, true)
fold_fn : DefaultFormula n × Bool → Nat × Array Nat → DefaultFormula n × Bool :=
  fun acc ratHint => if acc.snd = true then acc.fst.performRatCheck p ratHint else (acc.fst, false)
fold_fn_def :
  ∀ (acc : DefaultFormula n × Bool) (ratHint : Nat × Array Nat),
    fold_fn acc ratHint = if acc.snd = true then acc.fst.performRatCheck p ratHint else (acc.fst, false)
idx : Fin ratHints.size
acc : DefaultFormula n × Bool
ih : motive (↑idx) acc
⊢ (if acc.snd = true then f.performRatCheck p ratHints[↑idx] else (f, false)).fst = f
Theorem: LRAT.DefaultFormula.performRatCheck_success_of_performRatCheck_fold_success
Proof state before:
case left.isFalse
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
p : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
i : Fin ratHints.size
performRatCheck_fold_success :
  (Array.foldl (fun acc ratHint => if acc.snd = true then acc.fst.performRatCheck p ratHint else (acc.fst, false))
        (f, true) ratHints 0).snd =
    true
motive : Nat → DefaultFormula n × Bool → Prop :=
  fun idx acc => acc.fst = f ∧ (acc.snd = true → ∀ (i : Fin idx), (f.performRatCheck p ratHints[i]!).snd = true)
h_base : motive 0 (f, true)
fold_fn : DefaultFormula n × Bool → Nat × Array Nat → DefaultFormula n × Bool :=
  fun acc ratHint => if acc.snd = true then acc.fst.performRatCheck p ratHint else (acc.fst, false)
fold_fn_def :
  ∀ (acc : DefaultFormula n × Bool) (ratHint : Nat × Array Nat),
    fold_fn acc ratHint = if acc.snd = true then acc.fst.performRatCheck p ratHint else (acc.fst, false)
idx : Fin ratHints.size
acc : DefaultFormula n × Bool
ih : motive (↑idx) acc
h✝ : ¬acc.snd = true
⊢ (f, false).fst = f
Tactic:
. rfl
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.performRatCheck_success_of_performRatCheck_fold_success
Proof state before:
case left.isTrue
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
p : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
i : Fin ratHints.size
performRatCheck_fold_success :
  (Array.foldl (fun acc ratHint => if acc.snd = true then acc.fst.performRatCheck p ratHint else (acc.fst, false))
        (f, true) ratHints 0).snd =
    true
motive : Nat → DefaultFormula n × Bool → Prop :=
  fun idx acc => acc.fst = f ∧ (acc.snd = true → ∀ (i : Fin idx), (f.performRatCheck p ratHints[i]!).snd = true)
h_base : motive 0 (f, true)
fold_fn : DefaultFormula n × Bool → Nat × Array Nat → DefaultFormula n × Bool :=
  fun acc ratHint => if acc.snd = true then acc.fst.performRatCheck p ratHint else (acc.fst, false)
fold_fn_def :
  ∀ (acc : DefaultFormula n × Bool) (ratHint : Nat × Array Nat),
    fold_fn acc ratHint = if acc.snd = true then acc.fst.performRatCheck p ratHint else (acc.fst, false)
idx : Fin ratHints.size
acc : DefaultFormula n × Bool
ih : motive (↑idx) acc
h✝ : acc.snd = true
⊢ (f.performRatCheck p ratHints[↑idx]).fst = f
Tactic:
rw [performRatCheck_preserves_formula]
Proof state after:
case left.isTrue.hf
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
p : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
i : Fin ratHints.size
performRatCheck_fold_success :
  (Array.foldl (fun acc ratHint => if acc.snd = true then acc.fst.performRatCheck p ratHint else (acc.fst, false))
        (f, true) ratHints 0).snd =
    true
motive : Nat → DefaultFormula n × Bool → Prop :=
  fun idx acc => acc.fst = f ∧ (acc.snd = true → ∀ (i : Fin idx), (f.performRatCheck p ratHints[i]!).snd = true)
h_base : motive 0 (f, true)
fold_fn : DefaultFormula n × Bool → Nat × Array Nat → DefaultFormula n × Bool :=
  fun acc ratHint => if acc.snd = true then acc.fst.performRatCheck p ratHint else (acc.fst, false)
fold_fn_def :
  ∀ (acc : DefaultFormula n × Bool) (ratHint : Nat × Array Nat),
    fold_fn acc ratHint = if acc.snd = true then acc.fst.performRatCheck p ratHint else (acc.fst, false)
idx : Fin ratHints.size
acc : DefaultFormula n × Bool
ih : motive (↑idx) acc
h✝ : acc.snd = true
⊢ f.ratUnits = #[] ∧ f.assignments.size = n
Theorem: LRAT.DefaultFormula.performRatCheck_success_of_performRatCheck_fold_success
Proof state before:
case left.isTrue.hf
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
p : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
i : Fin ratHints.size
performRatCheck_fold_success :
  (Array.foldl (fun acc ratHint => if acc.snd = true then acc.fst.performRatCheck p ratHint else (acc.fst, false))
        (f, true) ratHints 0).snd =
    true
motive : Nat → DefaultFormula n × Bool → Prop :=
  fun idx acc => acc.fst = f ∧ (acc.snd = true → ∀ (i : Fin idx), (f.performRatCheck p ratHints[i]!).snd = true)
h_base : motive 0 (f, true)
fold_fn : DefaultFormula n × Bool → Nat × Array Nat → DefaultFormula n × Bool :=
  fun acc ratHint => if acc.snd = true then acc.fst.performRatCheck p ratHint else (acc.fst, false)
fold_fn_def :
  ∀ (acc : DefaultFormula n × Bool) (ratHint : Nat × Array Nat),
    fold_fn acc ratHint = if acc.snd = true then acc.fst.performRatCheck p ratHint else (acc.fst, false)
idx : Fin ratHints.size
acc : DefaultFormula n × Bool
ih : motive (↑idx) acc
h✝ : acc.snd = true
⊢ f.ratUnits = #[] ∧ f.assignments.size = n
Tactic:
exact hf
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.performRatCheck_success_of_performRatCheck_fold_success
Proof state before:
case left.isFalse
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
p : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
i : Fin ratHints.size
performRatCheck_fold_success :
  (Array.foldl (fun acc ratHint => if acc.snd = true then acc.fst.performRatCheck p ratHint else (acc.fst, false))
        (f, true) ratHints 0).snd =
    true
motive : Nat → DefaultFormula n × Bool → Prop :=
  fun idx acc => acc.fst = f ∧ (acc.snd = true → ∀ (i : Fin idx), (f.performRatCheck p ratHints[i]!).snd = true)
h_base : motive 0 (f, true)
fold_fn : DefaultFormula n × Bool → Nat × Array Nat → DefaultFormula n × Bool :=
  fun acc ratHint => if acc.snd = true then acc.fst.performRatCheck p ratHint else (acc.fst, false)
fold_fn_def :
  ∀ (acc : DefaultFormula n × Bool) (ratHint : Nat × Array Nat),
    fold_fn acc ratHint = if acc.snd = true then acc.fst.performRatCheck p ratHint else (acc.fst, false)
idx : Fin ratHints.size
acc : DefaultFormula n × Bool
ih : motive (↑idx) acc
h✝ : ¬acc.snd = true
⊢ (f, false).fst = f
Tactic:
rfl
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.performRatCheck_success_of_performRatCheck_fold_success
Proof state before:
case right
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
p : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
i : Fin ratHints.size
performRatCheck_fold_success :
  (Array.foldl (fun acc ratHint => if acc.snd = true then acc.fst.performRatCheck p ratHint else (acc.fst, false))
        (f, true) ratHints 0).snd =
    true
motive : Nat → DefaultFormula n × Bool → Prop :=
  fun idx acc => acc.fst = f ∧ (acc.snd = true → ∀ (i : Fin idx), (f.performRatCheck p ratHints[i]!).snd = true)
h_base : motive 0 (f, true)
fold_fn : DefaultFormula n × Bool → Nat × Array Nat → DefaultFormula n × Bool :=
  fun acc ratHint => if acc.snd = true then acc.fst.performRatCheck p ratHint else (acc.fst, false)
fold_fn_def :
  ∀ (acc : DefaultFormula n × Bool) (ratHint : Nat × Array Nat),
    fold_fn acc ratHint = if acc.snd = true then acc.fst.performRatCheck p ratHint else (acc.fst, false)
idx : Fin ratHints.size
acc : DefaultFormula n × Bool
ih : motive (↑idx) acc
⊢ (fold_fn acc ratHints[idx]).snd = true → ∀ (i : Fin (↑idx + 1)), (f.performRatCheck p ratHints[i]!).snd = true
Tactic:
intro h i
Proof state after:
case right
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
p : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
i✝ : Fin ratHints.size
performRatCheck_fold_success :
  (Array.foldl (fun acc ratHint => if acc.snd = true then acc.fst.performRatCheck p ratHint else (acc.fst, false))
        (f, true) ratHints 0).snd =
    true
motive : Nat → DefaultFormula n × Bool → Prop :=
  fun idx acc => acc.fst = f ∧ (acc.snd = true → ∀ (i : Fin idx), (f.performRatCheck p ratHints[i]!).snd = true)
h_base : motive 0 (f, true)
fold_fn : DefaultFormula n × Bool → Nat × Array Nat → DefaultFormula n × Bool :=
  fun acc ratHint => if acc.snd = true then acc.fst.performRatCheck p ratHint else (acc.fst, false)
fold_fn_def :
  ∀ (acc : DefaultFormula n × Bool) (ratHint : Nat × Array Nat),
    fold_fn acc ratHint = if acc.snd = true then acc.fst.performRatCheck p ratHint else (acc.fst, false)
idx : Fin ratHints.size
acc : DefaultFormula n × Bool
ih : motive (↑idx) acc
h : (fold_fn acc ratHints[idx]).snd = true
i : Fin (↑idx + 1)
⊢ (f.performRatCheck p ratHints[i]!).snd = true