internlm/Lean-Github huggingface dataset:
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
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:
. 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
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_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:
. simp only at h
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.reduce_fold_fn_preserves_induction_motive
Proof state before:
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)
Tactic:
split at h <;> contradiction
Proof state after:
no goals
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)
Tactic:
split at h <;> contradiction
Proof state after:
no goals
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
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)
Tactic:
simp only at h
Proof state after:
no goals
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
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:
simp only at h
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.reduce_fold_fn_preserves_induction_motive
Proof state before:
case left.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) reducedToNonunit
h : reducedToNonunit = 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 right
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
res : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) res
⊢ ∀ (a : PosFin n) (b : Bool),
    reduce_fold_fn assignment res c_arr[↑idx] = reducedToUnit (a, b) →
      ∀ (p : PosFin n → Bool), p ⊨ assignment → ∀ (x : Fin c_arr.size), ↑x < ↑idx + 1 → p ⊨ c_arr[↑x] → p ⊨ (a, b)
Tactic:
intro i b h p hp j j_lt_idx_add_one p_entails_c_arr_j
Proof state after:
case right
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
res : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) res
i : PosFin n
b : Bool
h : reduce_fold_fn assignment res c_arr[↑idx] = reducedToUnit (i, b)
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]
⊢ p ⊨ (i, b)
Theorem: LRAT.DefaultFormula.reduce_fold_fn_preserves_induction_motive
Proof state before:
case right
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
res : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) res
i : PosFin n
b : Bool
h : reduce_fold_fn assignment res c_arr[↑idx] = reducedToUnit (i, b)
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]
⊢ p ⊨ (i, b)
Tactic:
rw [reduce_fold_fn] at h
Proof state after:
case right
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
res : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) res
i : PosFin n
b : Bool
h :
  (match res with
    | encounteredBoth => encounteredBoth
    | reducedToEmpty =>
      match assignment[c_arr[↑idx].fst.val]! with
      | pos => if c_arr[↑idx].snd = true then reducedToUnit c_arr[↑idx] else reducedToEmpty
      | neg => if (!c_arr[↑idx].snd) = true then reducedToUnit c_arr[↑idx] else reducedToEmpty
      | both => encounteredBoth
      | unassigned => reducedToUnit c_arr[↑idx]
    | reducedToUnit l' =>
      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
    | reducedToNonunit => reducedToNonunit) =
    reducedToUnit (i, b)
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]
⊢ p ⊨ (i, b)
Theorem: LRAT.DefaultFormula.reduce_fold_fn_preserves_induction_motive
Proof state before:
case right.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) reducedToNonunit
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:
case right.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)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) encounteredBoth
h : encounteredBoth = 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:
case right.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)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
h :
  (match assignment[c_arr[↑idx].fst.val]! with
    | pos => if c_arr[↑idx].snd = true then reducedToUnit c_arr[↑idx] else reducedToEmpty
    | neg => if (!c_arr[↑idx].snd) = true then reducedToUnit c_arr[↑idx] else reducedToEmpty
    | both => encounteredBoth
    | unassigned => reducedToUnit c_arr[↑idx]) =
    reducedToUnit (i, b)
⊢ p ⊨ (i, b)
Tactic:
split at h
Proof state after:
case right.h_2.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)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = pos
h : (if c_arr[↑idx].snd = true then reducedToUnit c_arr[↑idx] else reducedToEmpty) = reducedToUnit (i, b)
⊢ p ⊨ (i, b)

case right.h_2.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)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = neg
h : (if (!c_arr[↑idx].snd) = true then reducedToUnit c_arr[↑idx] else reducedToEmpty) = reducedToUnit (i, b)
⊢ p ⊨ (i, b)

case right.h_2.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)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = both
h : encounteredBoth = reducedToUnit (i, b)
⊢ p ⊨ (i, b)

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

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 : reducedToUnit c_arr[↑idx] = reducedToUnit (i, b)
⊢ p ⊨ (i, b)
Tactic:
. simp only at h
Proof state after:
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 : reducedToUnit c_arr[↑idx] = reducedToUnit (i, b)
⊢ p ⊨ (i, b)
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 : reducedToUnit c_arr[↑idx] = reducedToUnit (i, b)
⊢ p ⊨ (i, b)
Tactic:
. simp only [reducedToUnit.injEq] at h
  rw [← h]
  rcases Nat.lt_or_eq_of_le $ Nat.le_of_lt_succ j_lt_idx_add_one with j_lt_idx | j_eq_idx
  . exfalso
    rcases ih.1 rfl p with ih1 | ih1
    . exact ih1 j j_lt_idx p_entails_c_arr_j
    . exact ih1 hp
  . 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:
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]! = pos
h : (if c_arr[↑idx].snd = true then reducedToUnit c_arr[↑idx] else reducedToEmpty) = 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)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
h✝ : c_arr[↑idx].snd = true
h : reducedToUnit c_arr[↑idx] = reducedToUnit (i, b)
⊢ 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)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
h✝ : ¬c_arr[↑idx].snd = true
h : False
⊢ p ⊨ (i, b)
Theorem: LRAT.DefaultFormula.reduce_fold_fn_preserves_induction_motive
Proof state before:
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)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
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)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
c_arr_idx_eq_true : c_arr[↑idx].snd = true
h : reducedToUnit c_arr[↑idx] = reducedToUnit (i, b)
⊢ 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)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
c_arr_idx_eq_true : c_arr[↑idx].snd = true
h : c_arr[↑idx] = (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)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
c_arr_idx_eq_true : c_arr[↑idx].snd = true
h : c_arr[↑idx] = (i, b)
⊢ p ⊨ (i, b)
Tactic:
simp only [h] 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)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
h : c_arr[↑idx] = (i, b)
c_arr_idx_eq_true : b = 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
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]! = pos
h : c_arr[↑idx] = (i, b)
c_arr_idx_eq_true : b = true
hp : ∀ (i : PosFin n), hasAssignment (decide (p i = false)) assignment[i.val]! = false
⊢ p ⊨ (i, b)
Tactic:
specialize hp c_arr[idx.val].1
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
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]! = pos
h : c_arr[↑idx] = (i, b)
c_arr_idx_eq_true : b = true
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:
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
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]! = pos
h : c_arr[↑idx] = (i, b)
c_arr_idx_eq_true : b = true
hp : hasAssignment (decide (p c_arr[↑idx].fst = false)) assignment[c_arr[↑idx].fst.val]! = false
⊢ p ⊨ (i, b)
Tactic:
rw [heq] at hp
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
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]! = pos
h : c_arr[↑idx] = (i, b)
c_arr_idx_eq_true : b = true
hp : hasAssignment (decide (p c_arr[↑idx].fst = false)) pos = false
⊢ 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
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]! = pos
h : c_arr[↑idx] = (i, b)
c_arr_idx_eq_true : b = true
hp : hasAssignment (decide (p c_arr[↑idx].fst = false)) pos = false
⊢ p ⊨ (i, b)
Tactic:
by_cases p c_arr[idx.val].1
Proof state after:
case pos
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
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]! = pos
h : c_arr[↑idx] = (i, b)
c_arr_idx_eq_true : b = true
hp : hasAssignment (decide (p c_arr[↑idx].fst = false)) pos = false
h✝ : p c_arr[↑idx].fst = true
⊢ p ⊨ (i, b)

case neg
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
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]! = pos
h : c_arr[↑idx] = (i, b)
c_arr_idx_eq_true : b = true
hp : hasAssignment (decide (p c_arr[↑idx].fst = false)) pos = false
h✝ : ¬p c_arr[↑idx].fst = true
⊢ p ⊨ (i, b)
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
i : PosFin n
b : Bool
p : PosFin n → Bool
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]! = pos
h : c_arr[↑idx] = (i, b)
c_arr_idx_eq_true : b = true
hp : hasAssignment (decide (p c_arr[↑idx].fst = false)) pos = false
h✝ : ¬p c_arr[↑idx].fst = true
⊢ p ⊨ (i, b)
Tactic:
. next p_c_arr_idx_eq_false =>
  simp only [h, Bool.not_eq_true] at p_c_arr_idx_eq_false
  simp (config := { decide := true }) only [h, p_c_arr_idx_eq_false] at hp
Proof state after:
no goals