Theorem: LRAT.DefaultFormula.confirmRupHint_of_insertRat_fold_entails_hsat (LeanSAT/LRAT/Formula/RatAddSound.lean)

State before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
c : DefaultClause n
rupHints : Array Nat
p : PosFin n → Bool
pf : p ⊨ f
⊢ let fc := f.insertRatUnits c.negate;
  let confirmRupHint_fold_res :=
    Array.foldl (confirmRupHint fc.fst.clauses) (fc.fst.assignments, [], false, false) rupHints 0;
  confirmRupHint_fold_res.snd.snd.fst = true → p ⊨ c
Tactic:
intro fc confirmRupHint_fold_res confirmRupHint_success
State after:
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
⊢ p ⊨ c

State before:
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
⊢ p ⊨ c
Tactic:
let motive := confirmRupHint_fold_entails_hsat_motive fc.1
State after:
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
⊢ p ⊨ c

State before:
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
⊢ p ⊨ c
Tactic:
have h_base : motive 0 (fc.fst.assignments, [], false, false) := by
  simp only [confirmRupHint_fold_entails_hsat_motive, insertRatUnits_preserves_assignments_size, hf.2.1,
    false_implies, and_true, true_and, fc, motive]
  have fc_satisfies_assignments_invariant : assignments_invariant fc.1 :=
    insertRatUnits_preserves_assignments_invariant f hf (negate c)
  exact assignments_invariant_entails_limplies fc.1 fc_satisfies_assignments_invariant
State after:
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)
⊢ p ⊨ c

State before:
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)
⊢ p ⊨ c
Tactic:
have h_inductive (idx : Fin rupHints.size) (acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool) (ih : motive idx.1 acc) :=
  confirmRupHint_preserves_motive fc.1 rupHints idx acc ih
State after:
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])
⊢ p ⊨ c

State before:
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])
⊢ p ⊨ c
Tactic:
rcases Array.foldl_induction motive h_base h_inductive with ⟨_, h1, h2⟩
State after:
case intro.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
⊢ p ⊨ c

State before:
case intro.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
⊢ p ⊨ c
Tactic:
have fc_incompatible_confirmRupHint_fold_res := (h2 confirmRupHint_success)
State after:
case intro.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)
    (Array.foldl (fun b => confirmRupHint fc.fst.clauses b) (fc.fst.assignments, [], false, false) rupHints 0).fst
    fc.fst
⊢ p ⊨ c

State before:
case intro.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)
    (Array.foldl (fun b => confirmRupHint fc.fst.clauses b) (fc.fst.assignments, [], false, false) rupHints 0).fst
    fc.fst
⊢ p ⊨ c
Tactic:
rw [incompatible.symm] at fc_incompatible_confirmRupHint_fold_res
State after:
case intro.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
⊢ p ⊨ c

State before:
case intro.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
⊢ p ⊨ c
Tactic:
have fc_unsat :=
  unsat_of_limplies_and_incompatible (PosFin n) fc.1 confirmRupHint_fold_res.1 h1 fc_incompatible_confirmRupHint_fold_res p
State after:
case intro.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
fc_unsat : ¬(p ⊨ fc.fst)
⊢ p ⊨ c

State before:
case intro.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
fc_unsat : ¬(p ⊨ fc.fst)
⊢ p ⊨ c
Tactic:
by_cases pc : p ⊨ c
State after:
case pos
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
fc_unsat : ¬(p ⊨ fc.fst)
pc : p ⊨ c
⊢ p ⊨ c

case neg
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
fc_unsat : ¬(p ⊨ fc.fst)
pc : ¬(p ⊨ c)
⊢ p ⊨ c

State before:
case pos
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
fc_unsat : ¬(p ⊨ fc.fst)
pc : p ⊨ c
⊢ p ⊨ c

case neg
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
fc_unsat : ¬(p ⊨ fc.fst)
pc : ¬(p ⊨ c)
⊢ p ⊨ c
Tactic:
. exact pc
State after:
case neg
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
fc_unsat : ¬(p ⊨ fc.fst)
pc : ¬(p ⊨ c)
⊢ p ⊨ c

State before:
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
⊢ motive 0 (fc.fst.assignments, [], false, false)
Tactic:
simp only [confirmRupHint_fold_entails_hsat_motive, insertRatUnits_preserves_assignments_size, hf.2.1,
  false_implies, and_true, true_and, fc, motive]
State after:
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
⊢ limplies (PosFin n) (f.insertRatUnits c.negate).fst (f.insertRatUnits c.negate).fst.assignments

State before:
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
⊢ limplies (PosFin n) (f.insertRatUnits c.negate).fst (f.insertRatUnits c.negate).fst.assignments
Tactic:
have fc_satisfies_assignments_invariant : assignments_invariant fc.1 :=
  insertRatUnits_preserves_assignments_invariant f hf (negate c)
State after:
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
fc_satisfies_assignments_invariant : fc.fst.assignments_invariant
⊢ limplies (PosFin n) (f.insertRatUnits c.negate).fst (f.insertRatUnits c.negate).fst.assignments

State before:
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
fc_satisfies_assignments_invariant : fc.fst.assignments_invariant
⊢ limplies (PosFin n) (f.insertRatUnits c.negate).fst (f.insertRatUnits c.negate).fst.assignments
Tactic:
exact assignments_invariant_entails_limplies fc.1 fc_satisfies_assignments_invariant
State after:
no goals

State before:
case pos
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
fc_unsat : ¬(p ⊨ fc.fst)
pc : p ⊨ c
⊢ p ⊨ c
Tactic:
exact pc
State after:
no goals

State before:
case neg
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
fc_unsat : ¬(p ⊨ fc.fst)
pc : ¬(p ⊨ c)
⊢ p ⊨ c
Tactic:
exfalso
State after:
case neg
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
fc_unsat : ¬(p ⊨ fc.fst)
pc : ¬(p ⊨ c)
⊢ False

State before:
case neg
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
fc_unsat : ¬(p ⊨ fc.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)
⊢ False
Tactic:
simp only [formulaHSat_def, List.all_eq_true, decide_eq_true_eq, Misc.not_forall, exists_prop] at fc_unsat
State after:
case neg
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)
fc_unsat : ∃ x, x ∈ fc.fst.toList ∧ ¬(p ⊨ x)
⊢ False

State before:
case neg
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)
fc_unsat : ∃ x, x ∈ fc.fst.toList ∧ ¬(p ⊨ x)
⊢ False
Tactic:
rcases fc_unsat with ⟨unsat_c, unsat_c_in_fc, p_unsat_c⟩
State after:
case neg.intro.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)
⊢ False

State before:
case neg.intro.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)
⊢ False
Tactic:
have unsat_c_in_fc := mem_of_insertRatUnits f (negate c) unsat_c unsat_c_in_fc
State after:
case neg.intro.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)
unsat_c_in_fc : unsat_c ∈ List.map Clause.unit c.negate ∨ unsat_c ∈ f.toList
⊢ False

State before:
case neg.intro.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)
unsat_c_in_fc : unsat_c ∈ List.map Clause.unit c.negate ∨ unsat_c ∈ f.toList
⊢ False
Tactic:
simp only [Array.toList_eq, List.mem_map, Misc.Prod.exists, Misc.Bool.exists_bool] at unsat_c_in_fc
State after:
case neg.intro.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)
unsat_c_in_fc :
  (∃ a,
      (a, false) ∈ c.negate ∧ Clause.unit (a, false) = unsat_c ∨
        (a, true) ∈ c.negate ∧ Clause.unit (a, true) = unsat_c) ∨
    unsat_c ∈ f.toList
⊢ False

State before:
case neg.intro.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)
unsat_c_in_fc :
  (∃ a,
      (a, false) ∈ c.negate ∧ Clause.unit (a, false) = unsat_c ∨
        (a, true) ∈ c.negate ∧ Clause.unit (a, true) = unsat_c) ∨
    unsat_c ∈ f.toList
⊢ False
Tactic:
rcases unsat_c_in_fc with ⟨v, ⟨v_in_neg_c, unsat_c_eq⟩ | ⟨v_in_neg_c, unsat_c_eq⟩⟩ | unsat_c_in_f
State after:
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
v_in_neg_c : (v, false) ∈ c.negate
unsat_c_eq : Clause.unit (v, false) = unsat_c
⊢ False

case neg.intro.intro.inl.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
v_in_neg_c : (v, true) ∈ c.negate
unsat_c_eq : Clause.unit (v, true) = unsat_c
⊢ False

case neg.intro.intro.inr
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)
unsat_c_in_f : unsat_c ∈ f.toList
⊢ False

State before:
case neg.intro.intro.inr
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)
unsat_c_in_f : unsat_c ∈ f.toList
⊢ False
Tactic:
. simp only [formulaHSat_def, List.all_eq_true, decide_eq_true_eq] at pf
  exact p_unsat_c $ pf unsat_c unsat_c_in_f
State after:
no goals

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
v_in_neg_c : (v, false) ∈ c.negate
unsat_c_eq : Clause.unit (v, false) = unsat_c
⊢ False
Tactic:
simp only [negate_iff, List.mem_map, Misc.Prod.exists, Misc.Bool.exists_bool] at v_in_neg_c
State after:
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

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⟩⟩
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

State before:
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
Tactic:
. simp only [negateLiteral, Bool.not_false, Prod.mk.injEq, and_false] at v'_eq_v
State after:
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

State before:
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
Tactic:
simp only [negateLiteral, Bool.not_false, Prod.mk.injEq, and_false] at v'_eq_v
State after:
no goals

State before:
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
Tactic:
simp only [negateLiteral, Bool.not_true, Prod.mk.injEq, and_true] at v'_eq_v
State after:
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 : v' = v
⊢ False

State before:
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
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 : v' = v
p_unsat_c :
  ∀ (x : PosFin n),
    ((x, false) ∈ Clause.toList (Clause.unit (v, false)) → ¬p x = false) ∧
      ((x, true) ∈ Clause.toList (Clause.unit (v, false)) → ¬p x = true)
⊢ False
Tactic:
specialize p_unsat_c v
State after:
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
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 : v' = v
p_unsat_c :
  ((v, false) ∈ Clause.toList (Clause.unit (v, false)) → ¬p v = false) ∧
    ((v, true) ∈ Clause.toList (Clause.unit (v, false)) → ¬p v = true)
⊢ False

State before:
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
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 : v' = v
p_unsat_c :
  ((v, false) ∈ Clause.toList (Clause.unit (v, false)) → ¬p v = false) ∧
    ((v, true) ∈ Clause.toList (Clause.unit (v, false)) → ¬p v = true)
⊢ False
Tactic:
rw [Clause.unit_eq] at p_unsat_c
State after:
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
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 : v' = v
p_unsat_c : ((v, false) ∈ [(v, false)] → ¬p v = false) ∧ ((v, true) ∈ [(v, false)] → ¬p v = true)
⊢ False

State before:
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
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 : v' = v
p_unsat_c : ((v, false) ∈ [(v, false)] → ¬p v = false) ∧ ((v, true) ∈ [(v, false)] → ¬p v = true)
⊢ False
Tactic:
simp only [List.mem_singleton, forall_const, Prod.mk.injEq, and_false, false_implies, and_true] at p_unsat_c
State after:
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
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 : v' = v
p_unsat_c : ¬p v = false
⊢ False

State before:
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
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 : v' = v
p_unsat_c : p v = true
⊢ False
Tactic:
specialize pc v
State after:
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
unsat_c : DefaultClause n
unsat_c_in_fc : unsat_c ∈ fc.fst.toList
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 : v' = v
p_unsat_c : p v = true
pc :
  ((v, false) ∈ Clause.toList c → decide (p v = false) = false) ∧
    ((v, true) ∈ Clause.toList c → decide (p v = true) = false)
⊢ False

State before:
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
unsat_c : DefaultClause n
unsat_c_in_fc : unsat_c ∈ fc.fst.toList
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 : v' = v
p_unsat_c : p v = true
pc :
  ((v, false) ∈ Clause.toList c → decide (p v = false) = false) ∧
    ((v, true) ∈ Clause.toList c → decide (p v = true) = false)
⊢ False
Tactic:
rw [v'_eq_v] at v'_in_c
State after:
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
unsat_c : DefaultClause n
unsat_c_in_fc : unsat_c ∈ fc.fst.toList
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 : v' = v
p_unsat_c : p v = true
pc :
  ((v, false) ∈ Clause.toList c → decide (p v = false) = false) ∧
    ((v, true) ∈ Clause.toList c → decide (p v = true) = false)
⊢ False

State before:
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
unsat_c : DefaultClause n
unsat_c_in_fc : unsat_c ∈ fc.fst.toList
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 : v' = v
p_unsat_c : p v = true
pc :
  ((v, false) ∈ Clause.toList c → decide (p v = false) = false) ∧
    ((v, true) ∈ Clause.toList c → decide (p v = true) = false)
⊢ False
Tactic:
have pv := pc.2 v'_in_c
State after:
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
unsat_c : DefaultClause n
unsat_c_in_fc : unsat_c ∈ fc.fst.toList
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 : v' = v
p_unsat_c : p v = true
pc :
  ((v, false) ∈ Clause.toList c → decide (p v = false) = false) ∧
    ((v, true) ∈ Clause.toList c → decide (p v = true) = false)
pv : decide (p v = true) = false
⊢ False

State before:
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
unsat_c : DefaultClause n
unsat_c_in_fc : unsat_c ∈ fc.fst.toList
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 : v' = v
p_unsat_c : p v = true
pc :
  ((v, false) ∈ Clause.toList c → decide (p v = false) = false) ∧
    ((v, true) ∈ Clause.toList c → decide (p v = true) = false)
pv : decide (p v = true) = false
⊢ False
Tactic:
simp only [p_unsat_c] at pv
State after:
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
unsat_c : DefaultClause n
unsat_c_in_fc : unsat_c ∈ fc.fst.toList
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 : v' = v
p_unsat_c : p v = true
pc :
  ((v, false) ∈ Clause.toList c → decide (p v = false) = false) ∧
    ((v, true) ∈ Clause.toList c → decide (p v = true) = false)
pv : decide True = false
⊢ False

State before:
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
unsat_c : DefaultClause n
unsat_c_in_fc : unsat_c ∈ fc.fst.toList
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 : v' = v
p_unsat_c : p v = true
pc :
  ((v, false) ∈ Clause.toList c → decide (p v = false) = false) ∧
    ((v, true) ∈ Clause.toList c → decide (p v = true) = false)
pv : decide True = false
⊢ False
Tactic:
cases pv
State after:
no goals

State before:
case neg.intro.intro.inl.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
v_in_neg_c : (v, true) ∈ c.negate
unsat_c_eq : Clause.unit (v, true) = unsat_c
⊢ False
Tactic:
simp only [negate_iff, List.mem_map, Misc.Prod.exists, Misc.Bool.exists_bool] at v_in_neg_c
State after:
case neg.intro.intro.inl.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, true) = unsat_c
v_in_neg_c :
  ∃ a,
    (a, false) ∈ c.toList ∧ negateLiteral (a, false) = (v, true) ∨
      (a, true) ∈ c.toList ∧ negateLiteral (a, true) = (v, true)
⊢ False

State before:
case neg.intro.intro.inl.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, true) = unsat_c
v_in_neg_c :
  ∃ a,
    (a, false) ∈ c.toList ∧ negateLiteral (a, false) = (v, true) ∨
      (a, true) ∈ c.toList ∧ negateLiteral (a, true) = (v, true)
⊢ False
Tactic:
rcases v_in_neg_c with ⟨v', ⟨v'_in_c, v'_eq_v⟩ | ⟨_, v'_eq_v⟩⟩
State after:
case neg.intro.intro.inl.intro.inr.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, true) = unsat_c
v' : PosFin n
v'_in_c : (v', false) ∈ c.toList
v'_eq_v : negateLiteral (v', false) = (v, true)
⊢ False

case neg.intro.intro.inl.intro.inr.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, true) = unsat_c
v' : PosFin n
left✝ : (v', true) ∈ c.toList
v'_eq_v : negateLiteral (v', true) = (v, true)
⊢ False

State before:
case neg.intro.intro.inl.intro.inr.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, true) = unsat_c
v' : PosFin n
left✝ : (v', true) ∈ c.toList
v'_eq_v : negateLiteral (v', true) = (v, true)
⊢ False
Tactic:
. simp only [negateLiteral, Bool.not_true, Prod.mk.injEq, and_false] at v'_eq_v
State after:
no goals

State before:
case neg.intro.intro.inl.intro.inr.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, true) = unsat_c
v' : PosFin n
v'_in_c : (v', false) ∈ c.toList
v'_eq_v : negateLiteral (v', false) = (v, true)
⊢ False
Tactic:
simp only [negateLiteral, Bool.not_false, Prod.mk.injEq, and_true] at v'_eq_v
State after:
case neg.intro.intro.inl.intro.inr.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, true) = unsat_c
v' : PosFin n
v'_in_c : (v', false) ∈ c.toList
v'_eq_v : v' = v
⊢ False

State before:
case neg.intro.intro.inl.intro.inr.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
v : PosFin n
unsat_c_eq : Clause.unit (v, true) = unsat_c
v' : PosFin n
v'_in_c : (v', false) ∈ c.toList
v'_eq_v : v' = v
p_unsat_c :
  ∀ (x : PosFin n),
    ((x, false) ∈ Clause.toList (Clause.unit (v, true)) → ¬p x = false) ∧
      ((x, true) ∈ Clause.toList (Clause.unit (v, true)) → ¬p x = true)
⊢ False
Tactic:
specialize p_unsat_c v
State after:
case neg.intro.intro.inl.intro.inr.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
v : PosFin n
unsat_c_eq : Clause.unit (v, true) = unsat_c
v' : PosFin n
v'_in_c : (v', false) ∈ c.toList
v'_eq_v : v' = v
p_unsat_c :
  ((v, false) ∈ Clause.toList (Clause.unit (v, true)) → ¬p v = false) ∧
    ((v, true) ∈ Clause.toList (Clause.unit (v, true)) → ¬p v = true)
⊢ False

State before:
case neg.intro.intro.inl.intro.inr.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
v : PosFin n
unsat_c_eq : Clause.unit (v, true) = unsat_c
v' : PosFin n
v'_in_c : (v', false) ∈ c.toList
v'_eq_v : v' = v
p_unsat_c :
  ((v, false) ∈ Clause.toList (Clause.unit (v, true)) → ¬p v = false) ∧
    ((v, true) ∈ Clause.toList (Clause.unit (v, true)) → ¬p v = true)
⊢ False
Tactic:
rw [Clause.unit_eq] at p_unsat_c
State after:
case neg.intro.intro.inl.intro.inr.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
v : PosFin n
unsat_c_eq : Clause.unit (v, true) = unsat_c
v' : PosFin n
v'_in_c : (v', false) ∈ c.toList
v'_eq_v : v' = v
p_unsat_c : ((v, false) ∈ [(v, true)] → ¬p v = false) ∧ ((v, true) ∈ [(v, true)] → ¬p v = true)
⊢ False

State before:
case neg.intro.intro.inl.intro.inr.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
v : PosFin n
unsat_c_eq : Clause.unit (v, true) = unsat_c
v' : PosFin n
v'_in_c : (v', false) ∈ c.toList
v'_eq_v : v' = v
p_unsat_c : ((v, false) ∈ [(v, true)] → ¬p v = false) ∧ ((v, true) ∈ [(v, true)] → ¬p v = true)
⊢ False
Tactic:
simp only [List.mem_singleton, forall_const, Prod.mk.injEq, and_false, false_implies, and_true] at p_unsat_c
State after:
case neg.intro.intro.inl.intro.inr.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
v : PosFin n
unsat_c_eq : Clause.unit (v, true) = unsat_c
v' : PosFin n
v'_in_c : (v', false) ∈ c.toList
v'_eq_v : v' = v
p_unsat_c : True ∧ ¬p v = true
⊢ False

State before:
case neg.intro.intro.inl.intro.inr.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
v : PosFin n
unsat_c_eq : Clause.unit (v, true) = unsat_c
v' : PosFin n
v'_in_c : (v', false) ∈ c.toList
v'_eq_v : v' = v
p_unsat_c : True ∧ ¬p v = true
⊢ False
Tactic:
specialize pc v
State after:
case neg.intro.intro.inl.intro.inr.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
unsat_c : DefaultClause n
unsat_c_in_fc : unsat_c ∈ fc.fst.toList
v : PosFin n
unsat_c_eq : Clause.unit (v, true) = unsat_c
v' : PosFin n
v'_in_c : (v', false) ∈ c.toList
v'_eq_v : v' = v
p_unsat_c : True ∧ ¬p v = true
pc :
  ((v, false) ∈ Clause.toList c → decide (p v = false) = false) ∧
    ((v, true) ∈ Clause.toList c → decide (p v = true) = false)
⊢ False

State before:
case neg.intro.intro.inl.intro.inr.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
unsat_c : DefaultClause n
unsat_c_in_fc : unsat_c ∈ fc.fst.toList
v : PosFin n
unsat_c_eq : Clause.unit (v, true) = unsat_c
v' : PosFin n
v'_in_c : (v', false) ∈ c.toList
v'_eq_v : v' = v
p_unsat_c : True ∧ ¬p v = true
pc :
  ((v, false) ∈ Clause.toList c → decide (p v = false) = false) ∧
    ((v, true) ∈ Clause.toList c → decide (p v = true) = false)
⊢ False
Tactic:
rw [v'_eq_v] at v'_in_c
State after:
case neg.intro.intro.inl.intro.inr.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
unsat_c : DefaultClause n
unsat_c_in_fc : unsat_c ∈ fc.fst.toList
v : PosFin n
unsat_c_eq : Clause.unit (v, true) = unsat_c
v' : PosFin n
v'_in_c : (v, false) ∈ c.toList
v'_eq_v : v' = v
p_unsat_c : True ∧ ¬p v = true
pc :
  ((v, false) ∈ Clause.toList c → decide (p v = false) = false) ∧
    ((v, true) ∈ Clause.toList c → decide (p v = true) = false)
⊢ False

State before:
case neg.intro.intro.inl.intro.inr.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
unsat_c : DefaultClause n
unsat_c_in_fc : unsat_c ∈ fc.fst.toList
v : PosFin n
unsat_c_eq : Clause.unit (v, true) = unsat_c
v' : PosFin n
v'_in_c : (v, false) ∈ c.toList
v'_eq_v : v' = v
p_unsat_c : True ∧ ¬p v = true
pc :
  ((v, false) ∈ Clause.toList c → decide (p v = false) = false) ∧
    ((v, true) ∈ Clause.toList c → decide (p v = true) = false)
⊢ False
Tactic:
have pv := pc.1 v'_in_c
State after:
case neg.intro.intro.inl.intro.inr.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
unsat_c : DefaultClause n
unsat_c_in_fc : unsat_c ∈ fc.fst.toList
v : PosFin n
unsat_c_eq : Clause.unit (v, true) = unsat_c
v' : PosFin n
v'_in_c : (v, false) ∈ c.toList
v'_eq_v : v' = v
p_unsat_c : True ∧ ¬p v = true
pc :
  ((v, false) ∈ Clause.toList c → decide (p v = false) = false) ∧
    ((v, true) ∈ Clause.toList c → decide (p v = true) = false)
pv : decide (p v = false) = false
⊢ False

State before:
case neg.intro.intro.inl.intro.inr.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
unsat_c : DefaultClause n
unsat_c_in_fc : unsat_c ∈ fc.fst.toList
v : PosFin n
unsat_c_eq : Clause.unit (v, true) = unsat_c
v' : PosFin n
v'_in_c : (v, false) ∈ c.toList
v'_eq_v : v' = v
p_unsat_c : True ∧ ¬p v = true
pc :
  ((v, false) ∈ Clause.toList c → decide (p v = false) = false) ∧
    ((v, true) ∈ Clause.toList c → decide (p v = true) = false)
pv : decide (p v = false) = false
⊢ False
Tactic:
simp only [p_unsat_c] at pv
State after:
case neg.intro.intro.inl.intro.inr.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
unsat_c : DefaultClause n
unsat_c_in_fc : unsat_c ∈ fc.fst.toList
v : PosFin n
unsat_c_eq : Clause.unit (v, true) = unsat_c
v' : PosFin n
v'_in_c : (v, false) ∈ c.toList
v'_eq_v : v' = v
p_unsat_c : True ∧ ¬p v = true
pc :
  ((v, false) ∈ Clause.toList c → decide (p v = false) = false) ∧
    ((v, true) ∈ Clause.toList c → decide (p v = true) = false)
pv : decide True = false
⊢ False

State before:
case neg.intro.intro.inl.intro.inr.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
unsat_c : DefaultClause n
unsat_c_in_fc : unsat_c ∈ fc.fst.toList
v : PosFin n
unsat_c_eq : Clause.unit (v, true) = unsat_c
v' : PosFin n
v'_in_c : (v, false) ∈ c.toList
v'_eq_v : v' = v
p_unsat_c : True ∧ ¬p v = true
pc :
  ((v, false) ∈ Clause.toList c → decide (p v = false) = false) ∧
    ((v, true) ∈ Clause.toList c → decide (p v = true) = false)
pv : decide True = false
⊢ False
Tactic:
cases pv
State after:
no goals

State before:
case neg.intro.intro.inl.intro.inr.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, true) = unsat_c
v' : PosFin n
left✝ : (v', true) ∈ c.toList
v'_eq_v : negateLiteral (v', true) = (v, true)
⊢ False
Tactic:
simp only [negateLiteral, Bool.not_true, Prod.mk.injEq, and_false] at v'_eq_v
State after:
no goals

State before:
case neg.intro.intro.inr
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)
unsat_c_in_f : unsat_c ∈ f.toList
⊢ False
Tactic:
simp only [formulaHSat_def, List.all_eq_true, decide_eq_true_eq] at pf
State after:
case neg.intro.intro.inr
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
c : DefaultClause n
rupHints : Array Nat
p : PosFin n → Bool
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)
unsat_c_in_f : unsat_c ∈ f.toList
pf : ∀ (x : DefaultClause n), x ∈ f.toList → p ⊨ x
⊢ False

State before:
case neg.intro.intro.inr
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
c : DefaultClause n
rupHints : Array Nat
p : PosFin n → Bool
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)
unsat_c_in_f : unsat_c ∈ f.toList
pf : ∀ (x : DefaultClause n), x ∈ f.toList → p ⊨ x
⊢ False
Tactic:
exact p_unsat_c $ pf unsat_c unsat_c_in_f
State after:
no goals