internlm/Lean-Github huggingface dataset:
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])
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)
Tactic:
rcases h1 with h1 | h1
Proof state after:
case intro.left.inl
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 ⊨ c) ∨ ¬(p ⊨ assignment)

case intro.left.inr
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 : ¬(p ⊨ assignment)
⊢ ¬(p ⊨ c) ∨ ¬(p ⊨ assignment)
Theorem: LRAT.DefaultFormula.reduce_postcondition
Proof state before:
case intro.left.inr
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 : ¬(p ⊨ assignment)
⊢ ¬(p ⊨ c) ∨ ¬(p ⊨ assignment)
Tactic:
. exact Or.inr h1
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.reduce_postcondition
Proof state before:
case intro.left.inl
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 ⊨ c) ∨ ¬(p ⊨ assignment)
Tactic:
apply Or.inl
Proof state after:
case intro.left.inl.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
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 ⊨ c)
Theorem: LRAT.DefaultFormula.reduce_postcondition
Proof state before:
case intro.left.inl.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
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 ⊨ c)
Tactic:
intro pc
Proof state after:
case intro.left.inl.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
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])
pc : p ⊨ c
⊢ False
Theorem: LRAT.DefaultFormula.reduce_postcondition
Proof state before:
case intro.left.inl.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
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])
pc :
  ∃ a,
    (a, false) ∈ Clause.toList c ∧ decide (p a = false) = true ∨
      (a, true) ∈ Clause.toList c ∧ decide (p a = true) = true
⊢ False
Tactic:
rcases pc with ⟨i, ⟨pc1, pc2⟩ | ⟨pc1, pc2⟩⟩
Proof state after:
case intro.left.inl.h.intro.inl.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])
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])
i : PosFin n
pc1 : (i, false) ∈ Clause.toList c
pc2 : decide (p i = false) = true
⊢ False

case intro.left.inl.h.intro.inr.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])
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])
i : PosFin n
pc1 : (i, true) ∈ Clause.toList c
pc2 : decide (p i = true) = true
⊢ False
Theorem: LRAT.DefaultFormula.reduce_postcondition
Proof state before:
case intro.left.inl.h.intro.inr.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])
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])
i : PosFin n
pc1 : (i, true) ∈ Clause.toList c
pc2 : decide (p i = true) = true
⊢ False
Tactic:
. simp only [Clause.toList, DefaultClause.toList] at pc1
  rw [c_clause_rw] at pc1
  have idx_exists : ∃ idx : Fin c_arr.size, c_arr[idx] = (i, true) := by
    rcases List.get_of_mem pc1 with ⟨idx, hidx⟩
    rw [← Array.getElem_fin_eq_data_get] at hidx
    exact Exists.intro idx hidx
  rcases idx_exists with ⟨idx, hidx⟩
  specialize h1 idx idx.2
  rw [hidx] at h1
  exact h1 $ of_decide_eq_true pc2
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.reduce_postcondition
Proof state before:
case intro.left.inl.h.intro.inl.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])
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])
i : PosFin n
pc1 : (i, false) ∈ Clause.toList c
pc2 : decide (p i = false) = true
⊢ False
Tactic:
simp only [Clause.toList, DefaultClause.toList] at pc1
Proof state after:
case intro.left.inl.h.intro.inl.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])
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])
i : PosFin n
pc1 : (i, false) ∈ c.clause
pc2 : decide (p i = false) = true
⊢ False
Theorem: LRAT.DefaultFormula.reduce_postcondition
Proof state before:
case intro.left.inl.h.intro.inl.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])
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])
i : PosFin n
pc1 : (i, false) ∈ c.clause
pc2 : decide (p i = false) = true
⊢ False
Tactic:
rw [c_clause_rw] at pc1
Proof state after:
case intro.left.inl.h.intro.inl.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])
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])
i : PosFin n
pc1 : (i, false) ∈ c_arr.data
pc2 : decide (p i = false) = true
⊢ False
Theorem: LRAT.DefaultFormula.reduce_postcondition
Proof state before:
case intro.left.inl.h.intro.inl.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])
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])
i : PosFin n
pc1 : (i, false) ∈ c_arr.data
pc2 : decide (p i = false) = true
⊢ False
Tactic:
have idx_exists : ∃ idx : Fin c_arr.size, c_arr[idx] = (i, false) := by
  rcases List.get_of_mem pc1 with ⟨idx, hidx⟩
  rw [← Array.getElem_fin_eq_data_get] at hidx
  exact Exists.intro idx hidx
Proof state after:
case intro.left.inl.h.intro.inl.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])
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])
i : PosFin n
pc1 : (i, false) ∈ c_arr.data
pc2 : decide (p i = false) = true
idx_exists : ∃ idx, c_arr[idx] = (i, false)
⊢ False
Theorem: LRAT.DefaultFormula.reduce_postcondition
Proof state before:
case intro.left.inl.h.intro.inl.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])
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])
i : PosFin n
pc1 : (i, false) ∈ c_arr.data
pc2 : decide (p i = false) = true
idx_exists : ∃ idx, c_arr[idx] = (i, false)
⊢ False
Tactic:
rcases idx_exists with ⟨idx, hidx⟩
Proof state after:
case intro.left.inl.h.intro.inl.intro.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])
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])
i : PosFin n
pc1 : (i, false) ∈ c_arr.data
pc2 : decide (p i = false) = true
idx : Fin c_arr.size
hidx : c_arr[idx] = (i, false)
⊢ False
Theorem: LRAT.DefaultFormula.reduce_postcondition
Proof state before:
case intro.left.inl.h.intro.inl.intro.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])
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])
i : PosFin n
pc1 : (i, false) ∈ c_arr.data
pc2 : decide (p i = false) = true
idx : Fin c_arr.size
hidx : c_arr[idx] = (i, false)
⊢ False
Tactic:
specialize h1 idx idx.2
Proof state after:
case intro.left.inl.h.intro.inl.intro.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])
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
i : PosFin n
pc1 : (i, false) ∈ c_arr.data
pc2 : decide (p i = false) = true
idx : Fin c_arr.size
hidx : c_arr[idx] = (i, false)
h1 : ¬(p ⊨ c_arr[idx])
⊢ False