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
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h : reducedToEmpty = reducedToEmpty
c_arr_idx_eq_false : c_arr[↑idx].snd = true
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)
Tactic:
rcases ih.1 rfl p with ih1 | ih1
Proof state after:
case inl
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h : reducedToEmpty = reducedToEmpty
c_arr_idx_eq_false : c_arr[↑idx].snd = true
ih1 : ∀ (i : Fin c_arr.size), ↑i < ↑idx → ¬(p ⊨ c_arr[i])
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)

case inr
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h : reducedToEmpty = reducedToEmpty
c_arr_idx_eq_false : c_arr[↑idx].snd = true
ih1 : ¬(p ⊨ assignment)
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)
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
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h : reducedToEmpty = reducedToEmpty
c_arr_idx_eq_false : c_arr[↑idx].snd = true
ih1 : ¬(p ⊨ assignment)
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)
Tactic:
. exact Or.inr ih1
Proof state after:
no goals
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
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h : reducedToEmpty = reducedToEmpty
c_arr_idx_eq_false : c_arr[↑idx].snd = true
ih1 : ∀ (i : Fin c_arr.size), ↑i < ↑idx → ¬(p ⊨ c_arr[i])
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)
Tactic:
by_cases p ⊨ assignment
Proof state after:
case pos
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h : reducedToEmpty = reducedToEmpty
c_arr_idx_eq_false : c_arr[↑idx].snd = true
ih1 : ∀ (i : Fin c_arr.size), ↑i < ↑idx → ¬(p ⊨ c_arr[i])
h✝ : p ⊨ assignment
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)

case neg
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h : reducedToEmpty = reducedToEmpty
c_arr_idx_eq_false : c_arr[↑idx].snd = true
ih1 : ∀ (i : Fin c_arr.size), ↑i < ↑idx → ¬(p ⊨ c_arr[i])
h✝ : ¬(p ⊨ assignment)
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)
Theorem: LRAT.DefaultFormula.reduce_fold_fn_preserves_induction_motive
Proof state before:
case neg
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h : reducedToEmpty = reducedToEmpty
c_arr_idx_eq_false : c_arr[↑idx].snd = true
ih1 : ∀ (i : Fin c_arr.size), ↑i < ↑idx → ¬(p ⊨ c_arr[i])
h✝ : ¬(p ⊨ assignment)
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)
Tactic:
. next h =>
  exact Or.inr 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
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h : reducedToEmpty = reducedToEmpty
c_arr_idx_eq_false : c_arr[↑idx].snd = true
ih1 : ∀ (i : Fin c_arr.size), ↑i < ↑idx → ¬(p ⊨ c_arr[i])
p_entails_assignment : p ⊨ assignment
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)
Tactic:
apply Or.inl
Proof state after:
case h
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h : reducedToEmpty = reducedToEmpty
c_arr_idx_eq_false : c_arr[↑idx].snd = true
ih1 : ∀ (i : Fin c_arr.size), ↑i < ↑idx → ¬(p ⊨ c_arr[i])
p_entails_assignment : p ⊨ assignment
⊢ ∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])
Theorem: LRAT.DefaultFormula.reduce_fold_fn_preserves_induction_motive
Proof state before:
case h
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h : reducedToEmpty = reducedToEmpty
c_arr_idx_eq_false : c_arr[↑idx].snd = true
ih1 : ∀ (i : Fin c_arr.size), ↑i < ↑idx → ¬(p ⊨ c_arr[i])
p_entails_assignment : p ⊨ assignment
⊢ ∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])
Tactic:
intro i i_lt_idx_add_one p_entails_c_arr_i
Proof state after:
case h
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h : reducedToEmpty = reducedToEmpty
c_arr_idx_eq_false : c_arr[↑idx].snd = true
ih1 : ∀ (i : Fin c_arr.size), ↑i < ↑idx → ¬(p ⊨ c_arr[i])
p_entails_assignment : p ⊨ assignment
i : Fin c_arr.size
i_lt_idx_add_one : ↑i < ↑idx + 1
p_entails_c_arr_i : p ⊨ c_arr[↑i]
⊢ False
Theorem: LRAT.DefaultFormula.reduce_fold_fn_preserves_induction_motive
Proof state before:
case h
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h : reducedToEmpty = reducedToEmpty
c_arr_idx_eq_false : c_arr[↑idx].snd = true
ih1 : ∀ (i : Fin c_arr.size), ↑i < ↑idx → ¬(p ⊨ c_arr[i])
p_entails_assignment : p ⊨ assignment
i : Fin c_arr.size
i_lt_idx_add_one : ↑i < ↑idx + 1
p_entails_c_arr_i : p ⊨ c_arr[↑i]
⊢ False
Tactic:
rcases Nat.lt_or_eq_of_le $ Nat.le_of_lt_succ i_lt_idx_add_one with i_lt_idx | i_eq_idx
Proof state after:
case h.inl
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h : reducedToEmpty = reducedToEmpty
c_arr_idx_eq_false : c_arr[↑idx].snd = true
ih1 : ∀ (i : Fin c_arr.size), ↑i < ↑idx → ¬(p ⊨ c_arr[i])
p_entails_assignment : p ⊨ assignment
i : Fin c_arr.size
i_lt_idx_add_one : ↑i < ↑idx + 1
p_entails_c_arr_i : p ⊨ c_arr[↑i]
i_lt_idx : ↑i < ↑idx
⊢ False

case h.inr
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h : reducedToEmpty = reducedToEmpty
c_arr_idx_eq_false : c_arr[↑idx].snd = true
ih1 : ∀ (i : Fin c_arr.size), ↑i < ↑idx → ¬(p ⊨ c_arr[i])
p_entails_assignment : p ⊨ assignment
i : Fin c_arr.size
i_lt_idx_add_one : ↑i < ↑idx + 1
p_entails_c_arr_i : p ⊨ c_arr[↑i]
i_eq_idx : ↑i = ↑idx
⊢ False
Theorem: LRAT.DefaultFormula.reduce_fold_fn_preserves_induction_motive
Proof state before:
case h.inl
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h : reducedToEmpty = reducedToEmpty
c_arr_idx_eq_false : c_arr[↑idx].snd = true
ih1 : ∀ (i : Fin c_arr.size), ↑i < ↑idx → ¬(p ⊨ c_arr[i])
p_entails_assignment : p ⊨ assignment
i : Fin c_arr.size
i_lt_idx_add_one : ↑i < ↑idx + 1
p_entails_c_arr_i : p ⊨ c_arr[↑i]
i_lt_idx : ↑i < ↑idx
⊢ False

case h.inr
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h : reducedToEmpty = reducedToEmpty
c_arr_idx_eq_false : c_arr[↑idx].snd = true
ih1 : ∀ (i : Fin c_arr.size), ↑i < ↑idx → ¬(p ⊨ c_arr[i])
p_entails_assignment : p ⊨ assignment
i : Fin c_arr.size
i_lt_idx_add_one : ↑i < ↑idx + 1
p_entails_c_arr_i : p ⊨ c_arr[↑i]
i_eq_idx : ↑i = ↑idx
⊢ False
Tactic:
. exact ih1 i i_lt_idx p_entails_c_arr_i
Proof state after:
case h.inr
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h : reducedToEmpty = reducedToEmpty
c_arr_idx_eq_false : c_arr[↑idx].snd = true
ih1 : ∀ (i : Fin c_arr.size), ↑i < ↑idx → ¬(p ⊨ c_arr[i])
p_entails_assignment : p ⊨ assignment
i : Fin c_arr.size
i_lt_idx_add_one : ↑i < ↑idx + 1
p_entails_c_arr_i : p ⊨ c_arr[↑i]
i_eq_idx : ↑i = ↑idx
⊢ False
Theorem: LRAT.DefaultFormula.reduce_fold_fn_preserves_induction_motive
Proof state before:
case h.inl
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h : reducedToEmpty = reducedToEmpty
c_arr_idx_eq_false : c_arr[↑idx].snd = true
ih1 : ∀ (i : Fin c_arr.size), ↑i < ↑idx → ¬(p ⊨ c_arr[i])
p_entails_assignment : p ⊨ assignment
i : Fin c_arr.size
i_lt_idx_add_one : ↑i < ↑idx + 1
p_entails_c_arr_i : p ⊨ c_arr[↑i]
i_lt_idx : ↑i < ↑idx
⊢ False
Tactic:
exact ih1 i i_lt_idx p_entails_c_arr_i
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.reduce_fold_fn_preserves_induction_motive
Proof state before:
case h.inr
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h : reducedToEmpty = reducedToEmpty
c_arr_idx_eq_false : c_arr[↑idx].snd = true
ih1 : ∀ (i : Fin c_arr.size), ↑i < ↑idx → ¬(p ⊨ c_arr[i])
i : Fin c_arr.size
i_lt_idx_add_one : ↑i < ↑idx + 1
i_eq_idx : ↑i = ↑idx
p_entails_c_arr_i : p c_arr[↑idx].fst = true
p_entails_assignment : ∀ (i : PosFin n), hasAssignment (decide (p i = false)) assignment[i.val]! = false
⊢ False
Tactic:
specialize p_entails_assignment c_arr[idx.1].1
Proof state after:
case h.inr
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h : reducedToEmpty = reducedToEmpty
c_arr_idx_eq_false : c_arr[↑idx].snd = true
ih1 : ∀ (i : Fin c_arr.size), ↑i < ↑idx → ¬(p ⊨ c_arr[i])
i : Fin c_arr.size
i_lt_idx_add_one : ↑i < ↑idx + 1
i_eq_idx : ↑i = ↑idx
p_entails_c_arr_i : p c_arr[↑idx].fst = true
p_entails_assignment : hasAssignment (decide (p c_arr[↑idx].fst = false)) assignment[c_arr[↑idx].fst.val]! = false
⊢ False
Theorem: LRAT.DefaultFormula.reduce_fold_fn_preserves_induction_motive
Proof state before:
case h.inr
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h : reducedToEmpty = reducedToEmpty
c_arr_idx_eq_false : c_arr[↑idx].snd = true
ih1 : ∀ (i : Fin c_arr.size), ↑i < ↑idx → ¬(p ⊨ c_arr[i])
i : Fin c_arr.size
i_lt_idx_add_one : ↑i < ↑idx + 1
i_eq_idx : ↑i = ↑idx
p_entails_c_arr_i : p c_arr[↑idx].fst = true
p_entails_assignment : hasAssignment (decide (p c_arr[↑idx].fst = false)) assignment[c_arr[↑idx].fst.val]! = false
⊢ False
Tactic:
simp (config := { decide := true }) only [p_entails_c_arr_i, decide_True, heq] at p_entails_assignment
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.reduce_fold_fn_preserves_induction_motive
Proof state before:
case neg
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h : reducedToEmpty = reducedToEmpty
c_arr_idx_eq_false : c_arr[↑idx].snd = true
ih1 : ∀ (i : Fin c_arr.size), ↑i < ↑idx → ¬(p ⊨ c_arr[i])
h✝ : ¬(p ⊨ assignment)
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)
Tactic:
next h =>
exact Or.inr 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
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h✝ : reducedToEmpty = reducedToEmpty
c_arr_idx_eq_false : c_arr[↑idx].snd = true
ih1 : ∀ (i : Fin c_arr.size), ↑i < ↑idx → ¬(p ⊨ c_arr[i])
h : ¬(p ⊨ assignment)
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)
Tactic:
exact Or.inr h
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
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h : reducedToEmpty = reducedToEmpty
c_arr_idx_eq_false : c_arr[↑idx].snd = true
ih1 : ¬(p ⊨ assignment)
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)
Tactic:
exact Or.inr ih1
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.reduce_fold_fn_preserves_induction_motive
Proof state before:
case left.h_2.h_3
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = both
h : encounteredBoth = reducedToEmpty
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)
Tactic:
simp only at h
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.reduce_fold_fn_preserves_induction_motive
Proof state before:
case left.h_2.h_4
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = unassigned
h : reducedToUnit c_arr[↑idx] = reducedToEmpty
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)
Tactic:
simp only at h
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.reduce_fold_fn_preserves_induction_motive
Proof state before:
case left.h_3
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
l'✝ : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l'✝)
h :
  (match assignment[c_arr[↑idx].fst.val]! with
    | pos => if c_arr[↑idx].snd = true then reducedToNonunit else reducedToUnit l'✝
    | neg => if (!c_arr[↑idx].snd) = true then reducedToNonunit else reducedToUnit l'✝
    | both => encounteredBoth
    | unassigned => reducedToNonunit) =
    reducedToEmpty
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)
Tactic:
next l =>
split at h
. split at h <;> contradiction
. split at h <;> contradiction
. simp only at h
. simp only at 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
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
h :
  (match assignment[c_arr[↑idx].fst.val]! with
    | pos => if c_arr[↑idx].snd = true then reducedToNonunit else reducedToUnit l
    | neg => if (!c_arr[↑idx].snd) = true then reducedToNonunit else reducedToUnit l
    | both => encounteredBoth
    | unassigned => reducedToNonunit) =
    reducedToEmpty
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)
Tactic:
split at h
Proof state after:
case h_1
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
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 : (if c_arr[↑idx].snd = true then reducedToNonunit else reducedToUnit l) = reducedToEmpty
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)

case h_2
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
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) = reducedToEmpty
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)

case h_3
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
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]! = both
h : encounteredBoth = reducedToEmpty
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)

case h_4
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
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]! = unassigned
h : reducedToNonunit = reducedToEmpty
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)
Theorem: LRAT.DefaultFormula.reduce_fold_fn_preserves_induction_motive
Proof state before:
case h_2
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
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) = reducedToEmpty
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)

case h_3
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
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]! = both
h : encounteredBoth = reducedToEmpty
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)

case h_4
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
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]! = unassigned
h : reducedToNonunit = reducedToEmpty
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)
Tactic:
. split at h <;> contradiction
Proof state after:
case h_3
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
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]! = both
h : encounteredBoth = reducedToEmpty
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)

case h_4
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
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]! = unassigned
h : reducedToNonunit = reducedToEmpty
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)