internlm/Lean-Github huggingface dataset:
Theorem: LRAT.DefaultFormula.reduce_fold_fn_preserves_induction_motive
Proof state before:
case right.h_2.h_4
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)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = unassigned
h : c_arr[↑idx] = (i, b)
⊢ p ⊨ c_arr[↑idx]
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 right.h_2.h_4.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)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = unassigned
h : c_arr[↑idx] = (i, b)
j_lt_idx : ↑j < ↑idx
⊢ p ⊨ c_arr[↑idx]

case right.h_2.h_4.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)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = unassigned
h : c_arr[↑idx] = (i, b)
j_eq_idx : ↑j = ↑idx
⊢ p ⊨ c_arr[↑idx]
Theorem: LRAT.DefaultFormula.reduce_fold_fn_preserves_induction_motive
Proof state before:
case right.h_2.h_4.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)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = unassigned
h : c_arr[↑idx] = (i, b)
j_lt_idx : ↑j < ↑idx
⊢ p ⊨ c_arr[↑idx]

case right.h_2.h_4.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)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = unassigned
h : c_arr[↑idx] = (i, b)
j_eq_idx : ↑j = ↑idx
⊢ p ⊨ c_arr[↑idx]
Tactic:
. exfalso
  rcases ih.1 rfl p with ih1 | ih1
  . exact ih1 j j_lt_idx p_entails_c_arr_j
  . exact ih1 hp
Proof state after:
case right.h_2.h_4.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)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = unassigned
h : c_arr[↑idx] = (i, b)
j_eq_idx : ↑j = ↑idx
⊢ p ⊨ c_arr[↑idx]
Theorem: LRAT.DefaultFormula.reduce_fold_fn_preserves_induction_motive
Proof state before:
case right.h_2.h_4.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)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = unassigned
h : c_arr[↑idx] = (i, b)
j_eq_idx : ↑j = ↑idx
⊢ p ⊨ c_arr[↑idx]
Tactic:
. simp only [j_eq_idx] at p_entails_c_arr_j
  exact p_entails_c_arr_j
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.reduce_fold_fn_preserves_induction_motive
Proof state before:
case right.h_2.h_4.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)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = unassigned
h : c_arr[↑idx] = (i, b)
j_lt_idx : ↑j < ↑idx
⊢ p ⊨ c_arr[↑idx]
Tactic:
exfalso
Proof state after:
case right.h_2.h_4.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)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = unassigned
h : c_arr[↑idx] = (i, b)
j_lt_idx : ↑j < ↑idx
⊢ False
Theorem: LRAT.DefaultFormula.reduce_fold_fn_preserves_induction_motive
Proof state before:
case right.h_2.h_4.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)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = unassigned
h : c_arr[↑idx] = (i, b)
j_lt_idx : ↑j < ↑idx
⊢ False
Tactic:
rcases ih.1 rfl p with ih1 | ih1
Proof state after:
case right.h_2.h_4.inl.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)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = unassigned
h : c_arr[↑idx] = (i, b)
j_lt_idx : ↑j < ↑idx
ih1 : ∀ (i : Fin c_arr.size), ↑i < ↑idx → ¬(p ⊨ c_arr[i])
⊢ False

case right.h_2.h_4.inl.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)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = unassigned
h : c_arr[↑idx] = (i, b)
j_lt_idx : ↑j < ↑idx
ih1 : ¬(p ⊨ assignment)
⊢ False
Theorem: LRAT.DefaultFormula.reduce_fold_fn_preserves_induction_motive
Proof state before:
case right.h_2.h_4.inl.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)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = unassigned
h : c_arr[↑idx] = (i, b)
j_lt_idx : ↑j < ↑idx
ih1 : ∀ (i : Fin c_arr.size), ↑i < ↑idx → ¬(p ⊨ c_arr[i])
⊢ False

case right.h_2.h_4.inl.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)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = unassigned
h : c_arr[↑idx] = (i, b)
j_lt_idx : ↑j < ↑idx
ih1 : ¬(p ⊨ assignment)
⊢ False
Tactic:
. exact ih1 j j_lt_idx p_entails_c_arr_j
Proof state after:
case right.h_2.h_4.inl.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)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = unassigned
h : c_arr[↑idx] = (i, b)
j_lt_idx : ↑j < ↑idx
ih1 : ¬(p ⊨ assignment)
⊢ False
Theorem: LRAT.DefaultFormula.reduce_fold_fn_preserves_induction_motive
Proof state before:
case right.h_2.h_4.inl.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)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = unassigned
h : c_arr[↑idx] = (i, b)
j_lt_idx : ↑j < ↑idx
ih1 : ¬(p ⊨ assignment)
⊢ False
Tactic:
. exact ih1 hp
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.reduce_fold_fn_preserves_induction_motive
Proof state before:
case right.h_2.h_4.inl.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)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = unassigned
h : c_arr[↑idx] = (i, b)
j_lt_idx : ↑j < ↑idx
ih1 : ∀ (i : Fin c_arr.size), ↑i < ↑idx → ¬(p ⊨ c_arr[i])
⊢ False
Tactic:
exact ih1 j j_lt_idx p_entails_c_arr_j
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.reduce_fold_fn_preserves_induction_motive
Proof state before:
case right.h_2.h_4.inl.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)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = unassigned
h : c_arr[↑idx] = (i, b)
j_lt_idx : ↑j < ↑idx
ih1 : ¬(p ⊨ assignment)
⊢ False
Tactic:
exact ih1 hp
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.reduce_fold_fn_preserves_induction_motive
Proof state before:
case right.h_2.h_4.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)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = unassigned
h : c_arr[↑idx] = (i, b)
j_eq_idx : ↑j = ↑idx
⊢ p ⊨ c_arr[↑idx]
Tactic:
simp only [j_eq_idx] at p_entails_c_arr_j
Proof state after:
case right.h_2.h_4.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
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 : c_arr[↑idx] = (i, b)
j_eq_idx : ↑j = ↑idx
p_entails_c_arr_j : p ⊨ c_arr[↑idx]
⊢ p ⊨ c_arr[↑idx]
Theorem: LRAT.DefaultFormula.reduce_fold_fn_preserves_induction_motive
Proof state before:
case right.h_2.h_4.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
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 : c_arr[↑idx] = (i, b)
j_eq_idx : ↑j = ↑idx
p_entails_c_arr_j : p ⊨ c_arr[↑idx]
⊢ p ⊨ c_arr[↑idx]
Tactic:
exact p_entails_c_arr_j
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)
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) =
    reducedToUnit (i, b)
⊢ p ⊨ (i, b)
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
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 : (if c_arr[↑idx].snd = true then reducedToNonunit else reducedToUnit l) = reducedToUnit (i, b)
⊢ p ⊨ (i, b)

case h_2
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)

case h_3
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]! = both
h : encounteredBoth = reducedToUnit (i, b)
⊢ p ⊨ (i, b)

case h_4
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]! = unassigned
h : reducedToNonunit = reducedToUnit (i, b)
⊢ p ⊨ (i, b)
Theorem: LRAT.DefaultFormula.reduce_fold_fn_preserves_induction_motive
Proof state before:
case h_3
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]! = both
h : encounteredBoth = reducedToUnit (i, b)
⊢ p ⊨ (i, b)

case h_4
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]! = unassigned
h : reducedToNonunit = reducedToUnit (i, b)
⊢ p ⊨ (i, b)
Tactic:
. simp only at h
Proof state after:
case h_4
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]! = unassigned
h : reducedToNonunit = reducedToUnit (i, b)
⊢ p ⊨ (i, b)
Theorem: LRAT.DefaultFormula.reduce_fold_fn_preserves_induction_motive
Proof state before:
case h_4
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]! = unassigned
h : reducedToNonunit = reducedToUnit (i, b)
⊢ p ⊨ (i, b)
Tactic:
. 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
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 : (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]! = pos
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]! = pos
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]! = pos
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]! = pos
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]! = pos
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]! = pos
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]! = pos
c_arr_idx_eq_false : ¬c_arr[↑idx].snd = true
h : reducedToUnit l = reducedToUnit (i, b)
⊢ p ⊨ (i, b)
Tactic:
simp only [Bool.not_eq_true] at c_arr_idx_eq_false
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
h : reducedToUnit l = reducedToUnit (i, b)
c_arr_idx_eq_false : c_arr[↑idx].snd = false
⊢ p ⊨ (i, b)