Theorem: LRAT.DefaultFormula.confirmRupHint_of_insertRat_fold_entails_hsat
Proof state before:
case neg.intro.intro.inl.intro.inl.intro
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
c : DefaultClause n
rupHints : Array Nat
p : PosFin n → Bool
pf : p ⊨ f
fc : DefaultFormula n × Bool := f.insertRatUnits c.negate
confirmRupHint_fold_res : Array Assignment × List (Literal (PosFin n)) × Bool × Bool :=
  Array.foldl (confirmRupHint fc.fst.clauses) (fc.fst.assignments, [], false, false) rupHints 0
confirmRupHint_success : confirmRupHint_fold_res.snd.snd.fst = true
motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  fc.fst.confirmRupHint_fold_entails_hsat_motive
h_base : motive 0 (fc.fst.assignments, [], false, false)
h_inductive :
  ∀ (idx : Fin rupHints.size) (acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool),
    motive (↑idx) acc →
      fc.fst.confirmRupHint_fold_entails_hsat_motive (↑idx + 1) (confirmRupHint fc.fst.clauses acc rupHints[idx])
left✝ :
  (Array.foldl (fun b => confirmRupHint fc.fst.clauses b) (fc.fst.assignments, [], false, false) rupHints 0).fst.size =
    n
h1 :
  limplies (PosFin n) fc.fst
    (Array.foldl (fun b => confirmRupHint fc.fst.clauses b) (fc.fst.assignments, [], false, false) rupHints 0).fst
h2 :
  (Array.foldl (fun b => confirmRupHint fc.fst.clauses b) (fc.fst.assignments, [], false, false) rupHints
              0).snd.snd.fst =
      true →
    incompatible (PosFin n)
      (Array.foldl (fun b => confirmRupHint fc.fst.clauses b) (fc.fst.assignments, [], false, false) rupHints 0).fst
      fc.fst
fc_incompatible_confirmRupHint_fold_res :
  incompatible (PosFin n) fc.fst
    (Array.foldl (fun b => confirmRupHint fc.fst.clauses b) (fc.fst.assignments, [], false, false) rupHints 0).fst
pc :
  ∀ (x : PosFin n),
    ((x, false) ∈ Clause.toList c → decide (p x = false) = false) ∧
      ((x, true) ∈ Clause.toList c → decide (p x = true) = false)
unsat_c : DefaultClause n
unsat_c_in_fc : unsat_c ∈ fc.fst.toList
p_unsat_c : ¬(p ⊨ unsat_c)
v : PosFin n
unsat_c_eq : Clause.unit (v, false) = unsat_c
v_in_neg_c :
  ∃ a,
    (a, false) ∈ c.toList ∧ negateLiteral (a, false) = (v, false) ∨
      (a, true) ∈ c.toList ∧ negateLiteral (a, true) = (v, false)
⊢ False
Tactic:
rcases v_in_neg_c with ⟨v', ⟨_, v'_eq_v⟩ | ⟨v'_in_c, v'_eq_v⟩⟩
Proof state after:
case neg.intro.intro.inl.intro.inl.intro.intro.inl.intro
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
c : DefaultClause n
rupHints : Array Nat
p : PosFin n → Bool
pf : p ⊨ f
fc : DefaultFormula n × Bool := f.insertRatUnits c.negate
confirmRupHint_fold_res : Array Assignment × List (Literal (PosFin n)) × Bool × Bool :=
  Array.foldl (confirmRupHint fc.fst.clauses) (fc.fst.assignments, [], false, false) rupHints 0
confirmRupHint_success : confirmRupHint_fold_res.snd.snd.fst = true
motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  fc.fst.confirmRupHint_fold_entails_hsat_motive
h_base : motive 0 (fc.fst.assignments, [], false, false)
h_inductive :
  ∀ (idx : Fin rupHints.size) (acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool),
    motive (↑idx) acc →
      fc.fst.confirmRupHint_fold_entails_hsat_motive (↑idx + 1) (confirmRupHint fc.fst.clauses acc rupHints[idx])
left✝¹ :
  (Array.foldl (fun b => confirmRupHint fc.fst.clauses b) (fc.fst.assignments, [], false, false) rupHints 0).fst.size =
    n
h1 :
  limplies (PosFin n) fc.fst
    (Array.foldl (fun b => confirmRupHint fc.fst.clauses b) (fc.fst.assignments, [], false, false) rupHints 0).fst
h2 :
  (Array.foldl (fun b => confirmRupHint fc.fst.clauses b) (fc.fst.assignments, [], false, false) rupHints
              0).snd.snd.fst =
      true →
    incompatible (PosFin n)
      (Array.foldl (fun b => confirmRupHint fc.fst.clauses b) (fc.fst.assignments, [], false, false) rupHints 0).fst
      fc.fst
fc_incompatible_confirmRupHint_fold_res :
  incompatible (PosFin n) fc.fst
    (Array.foldl (fun b => confirmRupHint fc.fst.clauses b) (fc.fst.assignments, [], false, false) rupHints 0).fst
pc :
  ∀ (x : PosFin n),
    ((x, false) ∈ Clause.toList c → decide (p x = false) = false) ∧
      ((x, true) ∈ Clause.toList c → decide (p x = true) = false)
unsat_c : DefaultClause n
unsat_c_in_fc : unsat_c ∈ fc.fst.toList
p_unsat_c : ¬(p ⊨ unsat_c)
v : PosFin n
unsat_c_eq : Clause.unit (v, false) = unsat_c
v' : PosFin n
left✝ : (v', false) ∈ c.toList
v'_eq_v : negateLiteral (v', false) = (v, false)
⊢ False

case neg.intro.intro.inl.intro.inl.intro.intro.inr.intro
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
c : DefaultClause n
rupHints : Array Nat
p : PosFin n → Bool
pf : p ⊨ f
fc : DefaultFormula n × Bool := f.insertRatUnits c.negate
confirmRupHint_fold_res : Array Assignment × List (Literal (PosFin n)) × Bool × Bool :=
  Array.foldl (confirmRupHint fc.fst.clauses) (fc.fst.assignments, [], false, false) rupHints 0
confirmRupHint_success : confirmRupHint_fold_res.snd.snd.fst = true
motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  fc.fst.confirmRupHint_fold_entails_hsat_motive
h_base : motive 0 (fc.fst.assignments, [], false, false)
h_inductive :
  ∀ (idx : Fin rupHints.size) (acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool),
    motive (↑idx) acc →
      fc.fst.confirmRupHint_fold_entails_hsat_motive (↑idx + 1) (confirmRupHint fc.fst.clauses acc rupHints[idx])
left✝ :
  (Array.foldl (fun b => confirmRupHint fc.fst.clauses b) (fc.fst.assignments, [], false, false) rupHints 0).fst.size =
    n
h1 :
  limplies (PosFin n) fc.fst
    (Array.foldl (fun b => confirmRupHint fc.fst.clauses b) (fc.fst.assignments, [], false, false) rupHints 0).fst
h2 :
  (Array.foldl (fun b => confirmRupHint fc.fst.clauses b) (fc.fst.assignments, [], false, false) rupHints
              0).snd.snd.fst =
      true →
    incompatible (PosFin n)
      (Array.foldl (fun b => confirmRupHint fc.fst.clauses b) (fc.fst.assignments, [], false, false) rupHints 0).fst
      fc.fst
fc_incompatible_confirmRupHint_fold_res :
  incompatible (PosFin n) fc.fst
    (Array.foldl (fun b => confirmRupHint fc.fst.clauses b) (fc.fst.assignments, [], false, false) rupHints 0).fst
pc :
  ∀ (x : PosFin n),
    ((x, false) ∈ Clause.toList c → decide (p x = false) = false) ∧
      ((x, true) ∈ Clause.toList c → decide (p x = true) = false)
unsat_c : DefaultClause n
unsat_c_in_fc : unsat_c ∈ fc.fst.toList
p_unsat_c : ¬(p ⊨ unsat_c)
v : PosFin n
unsat_c_eq : Clause.unit (v, false) = unsat_c
v' : PosFin n
v'_in_c : (v', true) ∈ c.toList
v'_eq_v : negateLiteral (v', true) = (v, false)
⊢ False