internlm/Lean-Github huggingface dataset:
Theorem: LRAT.DefaultFormula.reduce_fold_fn_preserves_induction_motive
Proof state before:
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
h : reducedToUnit l = reducedToUnit (i, b)
c_arr_idx_eq_false : c_arr[↑idx].snd = false
⊢ p ⊨ (i, b)
Tactic:
simp only [reducedToUnit.injEq] at h
Proof state after:
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
c_arr_idx_eq_false : c_arr[↑idx].snd = false
h : l = (i, b)
⊢ p ⊨ (i, b)
Theorem: LRAT.DefaultFormula.reduce_fold_fn_preserves_induction_motive
Proof state before:
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
c_arr_idx_eq_false : c_arr[↑idx].snd = false
h : l = (i, b)
⊢ p ⊨ (i, b)
Tactic:
rcases Nat.lt_or_eq_of_le $ Nat.le_of_lt_succ j_lt_idx_add_one with j_lt_idx | j_eq_idx
Proof state after:
case inl
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
c_arr_idx_eq_false : c_arr[↑idx].snd = false
h : l = (i, b)
j_lt_idx : ↑j < ↑idx
⊢ p ⊨ (i, b)

case inr
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
c_arr_idx_eq_false : c_arr[↑idx].snd = false
h : l = (i, b)
j_eq_idx : ↑j = ↑idx
⊢ p ⊨ (i, b)
Theorem: LRAT.DefaultFormula.reduce_fold_fn_preserves_induction_motive
Proof state before:
case inl
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
c_arr_idx_eq_false : c_arr[↑idx].snd = false
h : l = (i, b)
j_lt_idx : ↑j < ↑idx
⊢ p ⊨ (i, b)

case inr
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
c_arr_idx_eq_false : c_arr[↑idx].snd = false
h : l = (i, b)
j_eq_idx : ↑j = ↑idx
⊢ p ⊨ (i, b)
Tactic:
. rw [← h]
  have ih2_precondition : ∃ i : Fin c_arr.size, i.val < idx.val ∧ (p ⊨ c_arr[i]) :=
    (Exists.intro j ∘ And.intro j_lt_idx) p_entails_c_arr_j
  exact ih.2 l rfl p hp ih2_precondition
Proof state after:
case inr
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
c_arr_idx_eq_false : c_arr[↑idx].snd = false
h : l = (i, b)
j_eq_idx : ↑j = ↑idx
⊢ p ⊨ (i, b)
Theorem: LRAT.DefaultFormula.reduce_fold_fn_preserves_induction_motive
Proof state before:
case inl
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
c_arr_idx_eq_false : c_arr[↑idx].snd = false
h : l = (i, b)
j_lt_idx : ↑j < ↑idx
⊢ p ⊨ (i, b)
Tactic:
rw [← h]
Proof state after:
case inl
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
c_arr_idx_eq_false : c_arr[↑idx].snd = false
h : l = (i, b)
j_lt_idx : ↑j < ↑idx
⊢ p ⊨ l
Theorem: LRAT.DefaultFormula.reduce_fold_fn_preserves_induction_motive
Proof state before:
case inl
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
c_arr_idx_eq_false : c_arr[↑idx].snd = false
h : l = (i, b)
j_lt_idx : ↑j < ↑idx
⊢ p ⊨ l
Tactic:
have ih2_precondition : ∃ i : Fin c_arr.size, i.val < idx.val ∧ (p ⊨ c_arr[i]) :=
  (Exists.intro j ∘ And.intro j_lt_idx) p_entails_c_arr_j
Proof state after:
case inl
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
c_arr_idx_eq_false : c_arr[↑idx].snd = false
h : l = (i, b)
j_lt_idx : ↑j < ↑idx
ih2_precondition : ∃ i, ↑i < ↑idx ∧ (p ⊨ c_arr[i])
⊢ p ⊨ l
Theorem: LRAT.DefaultFormula.reduce_fold_fn_preserves_induction_motive
Proof state before:
case inl
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
c_arr_idx_eq_false : c_arr[↑idx].snd = false
h : l = (i, b)
j_lt_idx : ↑j < ↑idx
ih2_precondition : ∃ i, ↑i < ↑idx ∧ (p ⊨ c_arr[i])
⊢ p ⊨ l
Tactic:
exact ih.2 l rfl p hp ih2_precondition
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.reduce_fold_fn_preserves_induction_motive
Proof state before:
case inr
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
c_arr_idx_eq_false : c_arr[↑idx].snd = false
h : l = (i, b)
j_eq_idx : ↑j = ↑idx
p_entails_c_arr_j : p c_arr[↑idx].fst = false
hp : ∀ (i : PosFin n), hasAssignment (decide (p i = false)) assignment[i.val]! = false
⊢ p ⊨ (i, b)
Tactic:
specialize hp c_arr[idx.1].1
Proof state after:
case inr
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
c_arr_idx_eq_false : c_arr[↑idx].snd = false
h : l = (i, b)
j_eq_idx : ↑j = ↑idx
p_entails_c_arr_j : p c_arr[↑idx].fst = false
hp : hasAssignment (decide (p c_arr[↑idx].fst = false)) assignment[c_arr[↑idx].fst.val]! = false
⊢ p ⊨ (i, b)
Theorem: LRAT.DefaultFormula.reduce_fold_fn_preserves_induction_motive
Proof state before:
case inr
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
c_arr_idx_eq_false : c_arr[↑idx].snd = false
h : l = (i, b)
j_eq_idx : ↑j = ↑idx
p_entails_c_arr_j : p c_arr[↑idx].fst = false
hp : hasAssignment (decide (p c_arr[↑idx].fst = false)) assignment[c_arr[↑idx].fst.val]! = false
⊢ p ⊨ (i, b)
Tactic:
simp (config := { decide := true }) only [p_entails_c_arr_j, decide_True, heq] at hp
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.reduce_fold_fn_preserves_induction_motive
Proof state before:
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h : (if (!c_arr[↑idx].snd) = true then reducedToNonunit else reducedToUnit l) = reducedToUnit (i, b)
⊢ p ⊨ (i, b)
Tactic:
split at h
Proof state after:
case isTrue
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h✝ : (!c_arr[↑idx].snd) = true
h : False
⊢ p ⊨ (i, b)

case isFalse
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h✝ : ¬(!c_arr[↑idx].snd) = true
h : reducedToUnit l = reducedToUnit (i, b)
⊢ p ⊨ (i, b)
Theorem: LRAT.DefaultFormula.reduce_fold_fn_preserves_induction_motive
Proof state before:
case isTrue
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h✝ : (!c_arr[↑idx].snd) = true
h : False
⊢ p ⊨ (i, b)

case isFalse
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h✝ : ¬(!c_arr[↑idx].snd) = true
h : reducedToUnit l = reducedToUnit (i, b)
⊢ p ⊨ (i, b)
Tactic:
. exact False.elim h
Proof state after:
case isFalse
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h✝ : ¬(!c_arr[↑idx].snd) = true
h : reducedToUnit l = reducedToUnit (i, b)
⊢ p ⊨ (i, b)
Theorem: LRAT.DefaultFormula.reduce_fold_fn_preserves_induction_motive
Proof state before:
case isTrue
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h✝ : (!c_arr[↑idx].snd) = true
h : False
⊢ p ⊨ (i, b)
Tactic:
exact False.elim h
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.reduce_fold_fn_preserves_induction_motive
Proof state before:
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
c_arr_idx_eq_true : ¬(!c_arr[↑idx].snd) = true
h : reducedToUnit l = reducedToUnit (i, b)
⊢ p ⊨ (i, b)
Tactic:
simp only [Bool.not_eq_true', Bool.not_eq_false] at c_arr_idx_eq_true
Proof state after:
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h : reducedToUnit l = reducedToUnit (i, b)
c_arr_idx_eq_true : c_arr[↑idx].snd = true
⊢ p ⊨ (i, b)
Theorem: LRAT.DefaultFormula.reduce_fold_fn_preserves_induction_motive
Proof state before:
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h : reducedToUnit l = reducedToUnit (i, b)
c_arr_idx_eq_true : c_arr[↑idx].snd = true
⊢ p ⊨ (i, b)
Tactic:
simp only [reducedToUnit.injEq] at h
Proof state after:
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
c_arr_idx_eq_true : c_arr[↑idx].snd = true
h : l = (i, b)
⊢ p ⊨ (i, b)
Theorem: LRAT.DefaultFormula.reduce_fold_fn_preserves_induction_motive
Proof state before:
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
c_arr_idx_eq_true : c_arr[↑idx].snd = true
h : l = (i, b)
⊢ p ⊨ (i, b)
Tactic:
rcases Nat.lt_or_eq_of_le $ Nat.le_of_lt_succ j_lt_idx_add_one with j_lt_idx | j_eq_idx
Proof state after:
case inl
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
c_arr_idx_eq_true : c_arr[↑idx].snd = true
h : l = (i, b)
j_lt_idx : ↑j < ↑idx
⊢ p ⊨ (i, b)

case inr
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
c_arr_idx_eq_true : c_arr[↑idx].snd = true
h : l = (i, b)
j_eq_idx : ↑j = ↑idx
⊢ p ⊨ (i, b)
Theorem: LRAT.DefaultFormula.reduce_fold_fn_preserves_induction_motive
Proof state before:
case inl
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
c_arr_idx_eq_true : c_arr[↑idx].snd = true
h : l = (i, b)
j_lt_idx : ↑j < ↑idx
⊢ p ⊨ (i, b)

case inr
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
c_arr_idx_eq_true : c_arr[↑idx].snd = true
h : l = (i, b)
j_eq_idx : ↑j = ↑idx
⊢ p ⊨ (i, b)
Tactic:
. rw [← h]
  have ih2_precondition : ∃ i : Fin c_arr.size, i.val < idx.val ∧ (p ⊨ c_arr[i]) :=
    (Exists.intro j ∘ And.intro j_lt_idx) p_entails_c_arr_j
  exact ih.2 l rfl p hp ih2_precondition
Proof state after:
case inr
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
c_arr_idx_eq_true : c_arr[↑idx].snd = true
h : l = (i, b)
j_eq_idx : ↑j = ↑idx
⊢ p ⊨ (i, b)
Theorem: LRAT.DefaultFormula.reduce_fold_fn_preserves_induction_motive
Proof state before:
case inl
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
c_arr_idx_eq_true : c_arr[↑idx].snd = true
h : l = (i, b)
j_lt_idx : ↑j < ↑idx
⊢ p ⊨ (i, b)
Tactic:
rw [← h]
Proof state after:
case inl
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
c_arr_idx_eq_true : c_arr[↑idx].snd = true
h : l = (i, b)
j_lt_idx : ↑j < ↑idx
⊢ p ⊨ l
Theorem: LRAT.DefaultFormula.reduce_fold_fn_preserves_induction_motive
Proof state before:
case inl
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
c_arr_idx_eq_true : c_arr[↑idx].snd = true
h : l = (i, b)
j_lt_idx : ↑j < ↑idx
⊢ p ⊨ l
Tactic:
have ih2_precondition : ∃ i : Fin c_arr.size, i.val < idx.val ∧ (p ⊨ c_arr[i]) :=
  (Exists.intro j ∘ And.intro j_lt_idx) p_entails_c_arr_j
Proof state after:
case inl
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
c_arr_idx_eq_true : c_arr[↑idx].snd = true
h : l = (i, b)
j_lt_idx : ↑j < ↑idx
ih2_precondition : ∃ i, ↑i < ↑idx ∧ (p ⊨ c_arr[i])
⊢ p ⊨ l
Theorem: LRAT.DefaultFormula.reduce_fold_fn_preserves_induction_motive
Proof state before:
case inl
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
c_arr_idx_eq_true : c_arr[↑idx].snd = true
h : l = (i, b)
j_lt_idx : ↑j < ↑idx
ih2_precondition : ∃ i, ↑i < ↑idx ∧ (p ⊨ c_arr[i])
⊢ p ⊨ l
Tactic:
exact ih.2 l rfl p hp ih2_precondition
Proof state after:
no goals