internlm/Lean-Github huggingface dataset:
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]! = neg
c_arr_idx_eq_true : c_arr[↑idx].snd = true
h : l = (i, b)
j_eq_idx : ↑j = ↑idx
p_entails_c_arr_j : p c_arr[↑idx].fst = true
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]! = neg
c_arr_idx_eq_true : c_arr[↑idx].snd = true
h : l = (i, b)
j_eq_idx : ↑j = ↑idx
p_entails_c_arr_j : p c_arr[↑idx].fst = 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:
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]! = neg
c_arr_idx_eq_true : c_arr[↑idx].snd = true
h : l = (i, b)
j_eq_idx : ↑j = ↑idx
p_entails_c_arr_j : p c_arr[↑idx].fst = true
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:
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)
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
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:
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_postcondition
Proof state before:
n : Nat
c : DefaultClause n
assignment : Array Assignment
⊢ (c.reduce assignment = reducedToEmpty → incompatible (PosFin n) c assignment) ∧
    ∀ (l : Literal (PosFin n)),
      c.reduce assignment = reducedToUnit l → ∀ (p : PosFin n → Bool), p ⊨ assignment → p ⊨ c → p ⊨ l
Tactic:
let c_arr := Array.mk c.clause
Proof state after:
n : Nat
c : DefaultClause n
assignment : Array Assignment
c_arr : Array (Literal (PosFin n)) := { data := c.clause }
⊢ (c.reduce assignment = reducedToEmpty → incompatible (PosFin n) c assignment) ∧
    ∀ (l : Literal (PosFin n)),
      c.reduce assignment = reducedToUnit l → ∀ (p : PosFin n → Bool), p ⊨ assignment → p ⊨ c → p ⊨ l
Theorem: LRAT.DefaultFormula.reduce_postcondition
Proof state before:
n : Nat
c : DefaultClause n
assignment : Array Assignment
c_arr : Array (Literal (PosFin n)) := { data := c.clause }
⊢ (c.reduce assignment = reducedToEmpty → incompatible (PosFin n) c assignment) ∧
    ∀ (l : Literal (PosFin n)),
      c.reduce assignment = reducedToUnit l → ∀ (p : PosFin n → Bool), p ⊨ assignment → p ⊨ c → p ⊨ l
Tactic:
have c_clause_rw : c.clause = c_arr.data := rfl
Proof state after:
n : Nat
c : DefaultClause n
assignment : Array Assignment
c_arr : Array (Literal (PosFin n)) := { data := c.clause }
c_clause_rw : c.clause = c_arr.data
⊢ (c.reduce assignment = reducedToEmpty → incompatible (PosFin n) c assignment) ∧
    ∀ (l : Literal (PosFin n)),
      c.reduce assignment = reducedToUnit l → ∀ (p : PosFin n → Bool), p ⊨ assignment → p ⊨ c → p ⊨ l
Theorem: LRAT.DefaultFormula.reduce_postcondition
Proof state before:
n : Nat
c : DefaultClause n
assignment : Array Assignment
c_arr : Array (Literal (PosFin n)) := { data := c.clause }
c_clause_rw : c.clause = c_arr.data
⊢ (c.reduce assignment = reducedToEmpty → incompatible (PosFin n) c assignment) ∧
    ∀ (l : Literal (PosFin n)),
      c.reduce assignment = reducedToUnit l → ∀ (p : PosFin n → Bool), p ⊨ assignment → p ⊨ c → p ⊨ l
Tactic:
rw [reduce, c_clause_rw, ← Array.foldl_eq_foldl_data]
Proof state after:
n : Nat
c : DefaultClause n
assignment : Array Assignment
c_arr : Array (Literal (PosFin n)) := { data := c.clause }
c_clause_rw : c.clause = c_arr.data
⊢ (Array.foldl (reduce_fold_fn assignment) reducedToEmpty c_arr 0 = reducedToEmpty →
      incompatible (PosFin n) c assignment) ∧
    ∀ (l : Literal (PosFin n)),
      Array.foldl (reduce_fold_fn assignment) reducedToEmpty c_arr 0 = reducedToUnit l →
        ∀ (p : PosFin n → Bool), p ⊨ assignment → p ⊨ c → p ⊨ l
Theorem: LRAT.DefaultFormula.reduce_postcondition
Proof state before:
n : Nat
c : DefaultClause n
assignment : Array Assignment
c_arr : Array (Literal (PosFin n)) := { data := c.clause }
c_clause_rw : c.clause = c_arr.data
⊢ (Array.foldl (reduce_fold_fn assignment) reducedToEmpty c_arr 0 = reducedToEmpty →
      incompatible (PosFin n) c assignment) ∧
    ∀ (l : Literal (PosFin n)),
      Array.foldl (reduce_fold_fn assignment) reducedToEmpty c_arr 0 = reducedToUnit l →
        ∀ (p : PosFin n → Bool), p ⊨ assignment → p ⊨ c → p ⊨ l
Tactic:
let motive := reduce_postcondition_induction_motive c_arr assignment
Proof state after:
n : Nat
c : DefaultClause n
assignment : Array Assignment
c_arr : Array (Literal (PosFin n)) := { data := c.clause }
c_clause_rw : c.clause = c_arr.data
motive : Nat → ReduceResult (PosFin n) → Prop := reduce_postcondition_induction_motive c_arr assignment
⊢ (Array.foldl (reduce_fold_fn assignment) reducedToEmpty c_arr 0 = reducedToEmpty →
      incompatible (PosFin n) c assignment) ∧
    ∀ (l : Literal (PosFin n)),
      Array.foldl (reduce_fold_fn assignment) reducedToEmpty c_arr 0 = reducedToUnit l →
        ∀ (p : PosFin n → Bool), p ⊨ assignment → p ⊨ c → p ⊨ l
Theorem: LRAT.DefaultFormula.reduce_postcondition
Proof state before:
n : Nat
c : DefaultClause n
assignment : Array Assignment
c_arr : Array (Literal (PosFin n)) := { data := c.clause }
c_clause_rw : c.clause = c_arr.data
motive : Nat → ReduceResult (PosFin n) → Prop := reduce_postcondition_induction_motive c_arr assignment
⊢ (Array.foldl (reduce_fold_fn assignment) reducedToEmpty c_arr 0 = reducedToEmpty →
      incompatible (PosFin n) c assignment) ∧
    ∀ (l : Literal (PosFin n)),
      Array.foldl (reduce_fold_fn assignment) reducedToEmpty c_arr 0 = reducedToUnit l →
        ∀ (p : PosFin n → Bool), p ⊨ assignment → p ⊨ c → p ⊨ l
Tactic:
have h_base : motive 0 reducedToEmpty := by
  simp only [reduce_postcondition_induction_motive, Fin.getElem_fin, forall_exists_index, and_imp, Prod.forall,
    forall_const, false_implies, implies_true, and_true, motive]
  intro p
  apply Or.inl
  intro i i_lt_zero
  exfalso
  exact Nat.not_lt_zero i.1 i_lt_zero
Proof state after:
n : Nat
c : DefaultClause n
assignment : Array Assignment
c_arr : Array (Literal (PosFin n)) := { data := c.clause }
c_clause_rw : c.clause = c_arr.data
motive : Nat → ReduceResult (PosFin n) → Prop := reduce_postcondition_induction_motive c_arr assignment
h_base : motive 0 reducedToEmpty
⊢ (Array.foldl (reduce_fold_fn assignment) reducedToEmpty c_arr 0 = reducedToEmpty →
      incompatible (PosFin n) c assignment) ∧
    ∀ (l : Literal (PosFin n)),
      Array.foldl (reduce_fold_fn assignment) reducedToEmpty c_arr 0 = reducedToUnit l →
        ∀ (p : PosFin n → Bool), p ⊨ assignment → p ⊨ c → p ⊨ l
Theorem: LRAT.DefaultFormula.reduce_postcondition
Proof state before:
n : Nat
c : DefaultClause n
assignment : Array Assignment
c_arr : Array (Literal (PosFin n)) := { data := c.clause }
c_clause_rw : c.clause = c_arr.data
motive : Nat → ReduceResult (PosFin n) → Prop := reduce_postcondition_induction_motive c_arr assignment
h_base : motive 0 reducedToEmpty
⊢ (Array.foldl (reduce_fold_fn assignment) reducedToEmpty c_arr 0 = reducedToEmpty →
      incompatible (PosFin n) c assignment) ∧
    ∀ (l : Literal (PosFin n)),
      Array.foldl (reduce_fold_fn assignment) reducedToEmpty c_arr 0 = reducedToUnit l →
        ∀ (p : PosFin n → Bool), p ⊨ assignment → p ⊨ c → p ⊨ l
Tactic:
have h_inductive (idx : Fin c_arr.size) (res : ReduceResult (PosFin n)) (ih : motive idx.1 res) :
  motive (idx.1 + 1) (reduce_fold_fn assignment res c_arr[idx]) := reduce_fold_fn_preserves_induction_motive idx res ih
Proof state after:
n : Nat
c : DefaultClause n
assignment : Array Assignment
c_arr : Array (Literal (PosFin n)) := { data := c.clause }
c_clause_rw : c.clause = c_arr.data
motive : Nat → ReduceResult (PosFin n) → Prop := reduce_postcondition_induction_motive c_arr assignment
h_base : motive 0 reducedToEmpty
h_inductive :
  ∀ (idx : Fin c_arr.size) (res : ReduceResult (PosFin n)),
    motive (↑idx) res → motive (↑idx + 1) (reduce_fold_fn assignment res c_arr[idx])
⊢ (Array.foldl (reduce_fold_fn assignment) reducedToEmpty c_arr 0 = reducedToEmpty →
      incompatible (PosFin n) c assignment) ∧
    ∀ (l : Literal (PosFin n)),
      Array.foldl (reduce_fold_fn assignment) reducedToEmpty c_arr 0 = reducedToUnit l →
        ∀ (p : PosFin n → Bool), p ⊨ assignment → p ⊨ c → p ⊨ l
Theorem: LRAT.DefaultFormula.reduce_postcondition
Proof state before:
n : Nat
c : DefaultClause n
assignment : Array Assignment
c_arr : Array (Literal (PosFin n)) := { data := c.clause }
c_clause_rw : c.clause = c_arr.data
motive : Nat → ReduceResult (PosFin n) → Prop := reduce_postcondition_induction_motive c_arr assignment
h_base : motive 0 reducedToEmpty
h_inductive :
  ∀ (idx : Fin c_arr.size) (res : ReduceResult (PosFin n)),
    motive (↑idx) res → motive (↑idx + 1) (reduce_fold_fn assignment res c_arr[idx])
⊢ (Array.foldl (reduce_fold_fn assignment) reducedToEmpty c_arr 0 = reducedToEmpty →
      incompatible (PosFin n) c assignment) ∧
    ∀ (l : Literal (PosFin n)),
      Array.foldl (reduce_fold_fn assignment) reducedToEmpty c_arr 0 = reducedToUnit l →
        ∀ (p : PosFin n → Bool), p ⊨ assignment → p ⊨ c → p ⊨ l
Tactic:
rcases Array.foldl_induction motive h_base h_inductive with ⟨h1, h2⟩
Proof state after:
case intro
n : Nat
c : DefaultClause n
assignment : Array Assignment
c_arr : Array (Literal (PosFin n)) := { data := c.clause }
c_clause_rw : c.clause = c_arr.data
motive : Nat → ReduceResult (PosFin n) → Prop := reduce_postcondition_induction_motive c_arr assignment
h_base : motive 0 reducedToEmpty
h_inductive :
  ∀ (idx : Fin c_arr.size) (res : ReduceResult (PosFin n)),
    motive (↑idx) res → motive (↑idx + 1) (reduce_fold_fn assignment res c_arr[idx])
h1 :
  Array.foldl (fun b => reduce_fold_fn assignment b) reducedToEmpty c_arr 0 = reducedToEmpty →
    ∀ (p : PosFin n → Bool), (∀ (i : Fin c_arr.size), ↑i < c_arr.size → ¬(p ⊨ c_arr[i])) ∨ ¬(p ⊨ assignment)
h2 :
  ∀ (l : Literal (PosFin n)),
    Array.foldl (fun b => reduce_fold_fn assignment b) reducedToEmpty c_arr 0 = reducedToUnit l →
      ∀ (p : PosFin n → Bool), p ⊨ assignment → (∃ i, ↑i < c_arr.size ∧ (p ⊨ c_arr[i])) → p ⊨ l
⊢ (Array.foldl (reduce_fold_fn assignment) reducedToEmpty c_arr 0 = reducedToEmpty →
      incompatible (PosFin n) c assignment) ∧
    ∀ (l : Literal (PosFin n)),
      Array.foldl (reduce_fold_fn assignment) reducedToEmpty c_arr 0 = reducedToUnit l →
        ∀ (p : PosFin n → Bool), p ⊨ assignment → p ⊨ c → p ⊨ l
Theorem: LRAT.DefaultFormula.reduce_postcondition
Proof state before:
n : Nat
c : DefaultClause n
assignment : Array Assignment
c_arr : Array (Literal (PosFin n)) := { data := c.clause }
c_clause_rw : c.clause = c_arr.data
motive : Nat → ReduceResult (PosFin n) → Prop := reduce_postcondition_induction_motive c_arr assignment
⊢ motive 0 reducedToEmpty
Tactic:
simp only [reduce_postcondition_induction_motive, Fin.getElem_fin, forall_exists_index, and_imp, Prod.forall,
  forall_const, false_implies, implies_true, and_true, motive]
Proof state after:
n : Nat
c : DefaultClause n
assignment : Array Assignment
c_arr : Array (Literal (PosFin n)) := { data := c.clause }
c_clause_rw : c.clause = c_arr.data
motive : Nat → ReduceResult (PosFin n) → Prop := reduce_postcondition_induction_motive c_arr assignment
⊢ ∀ (p : PosFin n → Bool), (∀ (i : Fin c_arr.size), ↑i < 0 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)
Theorem: LRAT.DefaultFormula.reduce_postcondition
Proof state before:
n : Nat
c : DefaultClause n
assignment : Array Assignment
c_arr : Array (Literal (PosFin n)) := { data := c.clause }
c_clause_rw : c.clause = c_arr.data
motive : Nat → ReduceResult (PosFin n) → Prop := reduce_postcondition_induction_motive c_arr assignment
⊢ ∀ (p : PosFin n → Bool), (∀ (i : Fin c_arr.size), ↑i < 0 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)
Tactic:
intro p
Proof state after:
n : Nat
c : DefaultClause n
assignment : Array Assignment
c_arr : Array (Literal (PosFin n)) := { data := c.clause }
c_clause_rw : c.clause = c_arr.data
motive : Nat → ReduceResult (PosFin n) → Prop := reduce_postcondition_induction_motive c_arr assignment
p : PosFin n → Bool
⊢ (∀ (i : Fin c_arr.size), ↑i < 0 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)
Theorem: LRAT.DefaultFormula.reduce_postcondition
Proof state before:
n : Nat
c : DefaultClause n
assignment : Array Assignment
c_arr : Array (Literal (PosFin n)) := { data := c.clause }
c_clause_rw : c.clause = c_arr.data
motive : Nat → ReduceResult (PosFin n) → Prop := reduce_postcondition_induction_motive c_arr assignment
p : PosFin n → Bool
⊢ (∀ (i : Fin c_arr.size), ↑i < 0 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)
Tactic:
apply Or.inl
Proof state after:
case h
n : Nat
c : DefaultClause n
assignment : Array Assignment
c_arr : Array (Literal (PosFin n)) := { data := c.clause }
c_clause_rw : c.clause = c_arr.data
motive : Nat → ReduceResult (PosFin n) → Prop := reduce_postcondition_induction_motive c_arr assignment
p : PosFin n → Bool
⊢ ∀ (i : Fin c_arr.size), ↑i < 0 → ¬(p ⊨ c_arr[↑i])
Theorem: LRAT.DefaultFormula.reduce_postcondition
Proof state before:
case h
n : Nat
c : DefaultClause n
assignment : Array Assignment
c_arr : Array (Literal (PosFin n)) := { data := c.clause }
c_clause_rw : c.clause = c_arr.data
motive : Nat → ReduceResult (PosFin n) → Prop := reduce_postcondition_induction_motive c_arr assignment
p : PosFin n → Bool
⊢ ∀ (i : Fin c_arr.size), ↑i < 0 → ¬(p ⊨ c_arr[↑i])
Tactic:
intro i i_lt_zero
Proof state after:
case h
n : Nat
c : DefaultClause n
assignment : Array Assignment
c_arr : Array (Literal (PosFin n)) := { data := c.clause }
c_clause_rw : c.clause = c_arr.data
motive : Nat → ReduceResult (PosFin n) → Prop := reduce_postcondition_induction_motive c_arr assignment
p : PosFin n → Bool
i : Fin c_arr.size
i_lt_zero : ↑i < 0
⊢ ¬(p ⊨ c_arr[↑i])
Theorem: LRAT.DefaultFormula.reduce_postcondition
Proof state before:
case h
n : Nat
c : DefaultClause n
assignment : Array Assignment
c_arr : Array (Literal (PosFin n)) := { data := c.clause }
c_clause_rw : c.clause = c_arr.data
motive : Nat → ReduceResult (PosFin n) → Prop := reduce_postcondition_induction_motive c_arr assignment
p : PosFin n → Bool
i : Fin c_arr.size
i_lt_zero : ↑i < 0
⊢ ¬(p ⊨ c_arr[↑i])
Tactic:
exfalso
Proof state after:
case h
n : Nat
c : DefaultClause n
assignment : Array Assignment
c_arr : Array (Literal (PosFin n)) := { data := c.clause }
c_clause_rw : c.clause = c_arr.data
motive : Nat → ReduceResult (PosFin n) → Prop := reduce_postcondition_induction_motive c_arr assignment
p : PosFin n → Bool
i : Fin c_arr.size
i_lt_zero : ↑i < 0
⊢ False
Theorem: LRAT.DefaultFormula.reduce_postcondition
Proof state before:
case h
n : Nat
c : DefaultClause n
assignment : Array Assignment
c_arr : Array (Literal (PosFin n)) := { data := c.clause }
c_clause_rw : c.clause = c_arr.data
motive : Nat → ReduceResult (PosFin n) → Prop := reduce_postcondition_induction_motive c_arr assignment
p : PosFin n → Bool
i : Fin c_arr.size
i_lt_zero : ↑i < 0
⊢ False
Tactic:
exact Nat.not_lt_zero i.1 i_lt_zero
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.reduce_postcondition
Proof state before:
case intro.left
n : Nat
c : DefaultClause n
assignment : Array Assignment
c_arr : Array (Literal (PosFin n)) := { data := c.clause }
c_clause_rw : c.clause = c_arr.data
motive : Nat → ReduceResult (PosFin n) → Prop := reduce_postcondition_induction_motive c_arr assignment
h_base : motive 0 reducedToEmpty
h_inductive :
  ∀ (idx : Fin c_arr.size) (res : ReduceResult (PosFin n)),
    motive (↑idx) res → motive (↑idx + 1) (reduce_fold_fn assignment res c_arr[idx])
h1 :
  Array.foldl (fun b => reduce_fold_fn assignment b) reducedToEmpty c_arr 0 = reducedToEmpty →
    ∀ (p : PosFin n → Bool), (∀ (i : Fin c_arr.size), ↑i < c_arr.size → ¬(p ⊨ c_arr[i])) ∨ ¬(p ⊨ assignment)
h2 :
  ∀ (l : Literal (PosFin n)),
    Array.foldl (fun b => reduce_fold_fn assignment b) reducedToEmpty c_arr 0 = reducedToUnit l →
      ∀ (p : PosFin n → Bool), p ⊨ assignment → (∃ i, ↑i < c_arr.size ∧ (p ⊨ c_arr[i])) → p ⊨ l
⊢ Array.foldl (reduce_fold_fn assignment) reducedToEmpty c_arr 0 = reducedToEmpty → incompatible (PosFin n) c assignment
Tactic:
intro h p
Proof state after:
case intro.left
n : Nat
c : DefaultClause n
assignment : Array Assignment
c_arr : Array (Literal (PosFin n)) := { data := c.clause }
c_clause_rw : c.clause = c_arr.data
motive : Nat → ReduceResult (PosFin n) → Prop := reduce_postcondition_induction_motive c_arr assignment
h_base : motive 0 reducedToEmpty
h_inductive :
  ∀ (idx : Fin c_arr.size) (res : ReduceResult (PosFin n)),
    motive (↑idx) res → motive (↑idx + 1) (reduce_fold_fn assignment res c_arr[idx])
h1 :
  Array.foldl (fun b => reduce_fold_fn assignment b) reducedToEmpty c_arr 0 = reducedToEmpty →
    ∀ (p : PosFin n → Bool), (∀ (i : Fin c_arr.size), ↑i < c_arr.size → ¬(p ⊨ c_arr[i])) ∨ ¬(p ⊨ assignment)
h2 :
  ∀ (l : Literal (PosFin n)),
    Array.foldl (fun b => reduce_fold_fn assignment b) reducedToEmpty c_arr 0 = reducedToUnit l →
      ∀ (p : PosFin n → Bool), p ⊨ assignment → (∃ i, ↑i < c_arr.size ∧ (p ⊨ c_arr[i])) → p ⊨ l
h : Array.foldl (reduce_fold_fn assignment) reducedToEmpty c_arr 0 = reducedToEmpty
p : PosFin n → Bool
⊢ ¬(p ⊨ c) ∨ ¬(p ⊨ assignment)
Theorem: LRAT.DefaultFormula.reduce_postcondition
Proof state before:
case intro.left
n : Nat
c : DefaultClause n
assignment : Array Assignment
c_arr : Array (Literal (PosFin n)) := { data := c.clause }
c_clause_rw : c.clause = c_arr.data
motive : Nat → ReduceResult (PosFin n) → Prop := reduce_postcondition_induction_motive c_arr assignment
h_base : motive 0 reducedToEmpty
h_inductive :
  ∀ (idx : Fin c_arr.size) (res : ReduceResult (PosFin n)),
    motive (↑idx) res → motive (↑idx + 1) (reduce_fold_fn assignment res c_arr[idx])
h1 :
  Array.foldl (fun b => reduce_fold_fn assignment b) reducedToEmpty c_arr 0 = reducedToEmpty →
    ∀ (p : PosFin n → Bool), (∀ (i : Fin c_arr.size), ↑i < c_arr.size → ¬(p ⊨ c_arr[i])) ∨ ¬(p ⊨ assignment)
h2 :
  ∀ (l : Literal (PosFin n)),
    Array.foldl (fun b => reduce_fold_fn assignment b) reducedToEmpty c_arr 0 = reducedToUnit l →
      ∀ (p : PosFin n → Bool), p ⊨ assignment → (∃ i, ↑i < c_arr.size ∧ (p ⊨ c_arr[i])) → p ⊨ l
h : Array.foldl (reduce_fold_fn assignment) reducedToEmpty c_arr 0 = reducedToEmpty
p : PosFin n → Bool
⊢ ¬(p ⊨ c) ∨ ¬(p ⊨ assignment)
Tactic:
specialize h1 h p
Proof state after:
case intro.left
n : Nat
c : DefaultClause n
assignment : Array Assignment
c_arr : Array (Literal (PosFin n)) := { data := c.clause }
c_clause_rw : c.clause = c_arr.data
motive : Nat → ReduceResult (PosFin n) → Prop := reduce_postcondition_induction_motive c_arr assignment
h_base : motive 0 reducedToEmpty
h_inductive :
  ∀ (idx : Fin c_arr.size) (res : ReduceResult (PosFin n)),
    motive (↑idx) res → motive (↑idx + 1) (reduce_fold_fn assignment res c_arr[idx])
h2 :
  ∀ (l : Literal (PosFin n)),
    Array.foldl (fun b => reduce_fold_fn assignment b) reducedToEmpty c_arr 0 = reducedToUnit l →
      ∀ (p : PosFin n → Bool), p ⊨ assignment → (∃ i, ↑i < c_arr.size ∧ (p ⊨ c_arr[i])) → p ⊨ l
h : Array.foldl (reduce_fold_fn assignment) reducedToEmpty c_arr 0 = reducedToEmpty
p : PosFin n → Bool
h1 : (∀ (i : Fin c_arr.size), ↑i < c_arr.size → ¬(p ⊨ c_arr[i])) ∨ ¬(p ⊨ assignment)
⊢ ¬(p ⊨ c) ∨ ¬(p ⊨ assignment)