-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean
theorem reduce_postcondition {n : Nat} (c : DefaultClause n) (assignment : Array Assignment) :
    (reduce c assignment = reducedToEmpty → Incompatible (PosFin n) c assignment) ∧
    (∀ l : Literal (PosFin n), reduce c assignment = reducedToUnit l → ∀ (p : (PosFin n) → Bool), p ⊨ assignment → p ⊨ c → p ⊨ l)

Proof state:
case intro.right.intro.inl.intro
n : Nat
c : DefaultClause n
assignment : Array Assignment
c_arr : Array (Literal (PosFin n)) := List.toArray c.clause
c_clause_rw : c.clause = c_arr.toList
motive : Nat → ReduceResult (PosFin n) → Prop := ReducePostconditionInductionMotive 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 (reduce_fold_fn assignment) reducedToEmpty c_arr = 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 (reduce_fold_fn assignment) reducedToEmpty c_arr = reducedToUnit l →
      ∀ (p : PosFin n → Bool), p ⊨ assignment → (∃ i, ↑i < c_arr.size ∧ (p ⊨ c_arr[i])) → p ⊨ l
l : Literal (PosFin n)
hl : Array.foldl (reduce_fold_fn assignment) reducedToEmpty c_arr = reducedToUnit l
p : PosFin n → Bool
hp : p ⊨ assignment
i : PosFin n
pc1 : (i, false) ∈ Clause.toList c
pc2 : decide (p i = false) = true
⊢ ∃ i, ↑i < c_arr.size ∧ (p ⊨ c_arr[i])

Tactic:
simp only [Clause.toList, DefaultClause.toList] at pc1

Result:
case intro.right.intro.inl.intro
n : Nat
c : DefaultClause n
assignment : Array Assignment
c_arr : Array (Literal (PosFin n)) := List.toArray c.clause
c_clause_rw : c.clause = c_arr.toList
motive : Nat → ReduceResult (PosFin n) → Prop := ReducePostconditionInductionMotive 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 (reduce_fold_fn assignment) reducedToEmpty c_arr = 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 (reduce_fold_fn assignment) reducedToEmpty c_arr = reducedToUnit l →
      ∀ (p : PosFin n → Bool), p ⊨ assignment → (∃ i, ↑i < c_arr.size ∧ (p ⊨ c_arr[i])) → p ⊨ l
l : Literal (PosFin n)
hl : Array.foldl (reduce_fold_fn assignment) reducedToEmpty c_arr = reducedToUnit l
p : PosFin n → Bool
hp : p ⊨ assignment
i : PosFin n
pc1 : (i, false) ∈ c.clause
pc2 : decide (p i = false) = true
⊢ ∃ i, ↑i < c_arr.size ∧ (p ⊨ c_arr[i])

Proof state:
case h
n : Nat
c : DefaultClause n
assignment : Array Assignment
c_arr : Array (Literal (PosFin n)) := List.toArray c.clause
c_clause_rw : c.clause = c_arr.toList
motive : Nat → ReduceResult (PosFin n) → Prop := ReducePostconditionInductionMotive c_arr assignment
this : ∀ (a : PosFin n) (b : Bool), (reducedToEmpty = reducedToUnit (a, b)) = False
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

Result:
no goals

Proof state:
case intro.left.inl.h.intro.inr.intro
n : Nat
c : DefaultClause n
assignment : Array Assignment
c_arr : Array (Literal (PosFin n)) := List.toArray c.clause
c_clause_rw : c.clause = c_arr.toList
motive : Nat → ReduceResult (PosFin n) → Prop := ReducePostconditionInductionMotive 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 (reduce_fold_fn assignment) reducedToEmpty c_arr = 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 = 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

Result:
case intro.left.inl.h.intro.inr.intro
n : Nat
c : DefaultClause n
assignment : Array Assignment
c_arr : Array (Literal (PosFin n)) := List.toArray c.clause
c_clause_rw : c.clause = c_arr.toList
motive : Nat → ReduceResult (PosFin n) → Prop := ReducePostconditionInductionMotive 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 (reduce_fold_fn assignment) reducedToEmpty c_arr = 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 = 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) ∈ c.clause
pc2 : decide (p i = true) = true
⊢ False

Proof state:
case intro.right.intro.inl.intro
n : Nat
c : DefaultClause n
assignment : Array Assignment
c_arr : Array (Literal (PosFin n)) := List.toArray c.clause
c_clause_rw : c.clause = c_arr.toList
motive : Nat → ReduceResult (PosFin n) → Prop := ReducePostconditionInductionMotive 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 (reduce_fold_fn assignment) reducedToEmpty c_arr = 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 (reduce_fold_fn assignment) reducedToEmpty c_arr = reducedToUnit l →
      ∀ (p : PosFin n → Bool), p ⊨ assignment → (∃ i, ↑i < c_arr.size ∧ (p ⊨ c_arr[i])) → p ⊨ l
l : Literal (PosFin n)
hl : Array.foldl (reduce_fold_fn assignment) reducedToEmpty c_arr = reducedToUnit l
p : PosFin n → Bool
hp : p ⊨ assignment
i : PosFin n
pc1 : (i, false) ∈ c_arr.toList
pc2 : decide (p i = false) = true
idx_exists : ∃ idx, c_arr[idx] = (i, false)
⊢ ∃ i, ↑i < c_arr.size ∧ (p ⊨ c_arr[i])

Tactic:
rcases idx_exists with ⟨idx, hidx⟩

Result:
case intro.right.intro.inl.intro.intro
n : Nat
c : DefaultClause n
assignment : Array Assignment
c_arr : Array (Literal (PosFin n)) := List.toArray c.clause
c_clause_rw : c.clause = c_arr.toList
motive : Nat → ReduceResult (PosFin n) → Prop := ReducePostconditionInductionMotive 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 (reduce_fold_fn assignment) reducedToEmpty c_arr = 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 (reduce_fold_fn assignment) reducedToEmpty c_arr = reducedToUnit l →
      ∀ (p : PosFin n → Bool), p ⊨ assignment → (∃ i, ↑i < c_arr.size ∧ (p ⊨ c_arr[i])) → p ⊨ l
l : Literal (PosFin n)
hl : Array.foldl (reduce_fold_fn assignment) reducedToEmpty c_arr = reducedToUnit l
p : PosFin n → Bool
hp : p ⊨ assignment
i : PosFin n
pc1 : (i, false) ∈ c_arr.toList
pc2 : decide (p i = false) = true
idx : Fin c_arr.size
hidx : c_arr[idx] = (i, false)
⊢ ∃ i, ↑i < c_arr.size ∧ (p ⊨ c_arr[i])

Proof state:
n : Nat
c : DefaultClause n
assignment : Array Assignment
c_arr : Array (Literal (PosFin n)) := List.toArray c.clause
⊢ c.clause = c_arr.toList

Tactic:
simp [c_arr]

Result:
no goals