Theorem: LRAT.DefaultFormula.confirmRupHint_preserves_motive (LeanSAT/LRAT/Formula/RupAddSound.lean)

State before:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
ih : f.confirmRupHint_fold_entails_hsat_motive (↑idx) acc
⊢ f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1) (confirmRupHint f.clauses acc rupHints[idx])
Tactic:
rcases ih with ⟨hsize, h1, h2⟩
State after:
case intro.intro
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
⊢ f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1) (confirmRupHint f.clauses acc rupHints[idx])

State before:
case intro.intro
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
⊢ f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1) (confirmRupHint f.clauses acc rupHints[idx])
Tactic:
simp only [confirmRupHint, Bool.or_eq_true, Prod.mk.eta, Fin.getElem_fin]
State after:
case intro.intro
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
⊢ f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1)
    (if acc.2.2.snd = true ∨ acc.2.2.fst = true then acc
    else
      match f.clauses[rupHints[↑idx]]? with
      | some (some c) =>
        match c.reduce acc.fst with
        | encounteredBoth => (acc.fst, acc.2.fst, true, false)
        | reducedToEmpty => (acc.fst, acc.2.fst, true, false)
        | reducedToUnit (l, b) =>
          if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
          else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
        | reducedToNonunit => (acc.fst, acc.2.fst, false, true)
      | some none => (acc.fst, acc.2.fst, false, true)
      | none => (acc.fst, acc.2.fst, false, true))

State before:
case intro.intro
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
⊢ f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1)
    (if acc.2.2.snd = true ∨ acc.2.2.fst = true then acc
    else
      match f.clauses[rupHints[↑idx]]? with
      | some (some c) =>
        match c.reduce acc.fst with
        | encounteredBoth => (acc.fst, acc.2.fst, true, false)
        | reducedToEmpty => (acc.fst, acc.2.fst, true, false)
        | reducedToUnit (l, b) =>
          if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
          else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
        | reducedToNonunit => (acc.fst, acc.2.fst, false, true)
      | some none => (acc.fst, acc.2.fst, false, true)
      | none => (acc.fst, acc.2.fst, false, true))
Tactic:
split
State after:
case intro.intro.isTrue
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
h✝ : acc.2.2.snd = true ∨ acc.2.2.fst = true
⊢ f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1) acc

case intro.intro.isFalse
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
h✝ : ¬(acc.2.2.snd = true ∨ acc.2.2.fst = true)
⊢ f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1)
    (match f.clauses[rupHints[↑idx]]? with
    | some (some c) =>
      match c.reduce acc.fst with
      | encounteredBoth => (acc.fst, acc.2.fst, true, false)
      | reducedToEmpty => (acc.fst, acc.2.fst, true, false)
      | reducedToUnit (l, b) =>
        if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
        else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
      | reducedToNonunit => (acc.fst, acc.2.fst, false, true)
    | some none => (acc.fst, acc.2.fst, false, true)
    | none => (acc.fst, acc.2.fst, false, true))

State before:
case intro.intro.isTrue
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
h✝ : acc.2.2.snd = true ∨ acc.2.2.fst = true
⊢ f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1) acc

case intro.intro.isFalse
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
h✝ : ¬(acc.2.2.snd = true ∨ acc.2.2.fst = true)
⊢ f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1)
    (match f.clauses[rupHints[↑idx]]? with
    | some (some c) =>
      match c.reduce acc.fst with
      | encounteredBoth => (acc.fst, acc.2.fst, true, false)
      | reducedToEmpty => (acc.fst, acc.2.fst, true, false)
      | reducedToUnit (l, b) =>
        if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
        else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
      | reducedToNonunit => (acc.fst, acc.2.fst, false, true)
    | some none => (acc.fst, acc.2.fst, false, true)
    | none => (acc.fst, acc.2.fst, false, true))
Tactic:
. exact ⟨hsize, h1, h2⟩
State after:
case intro.intro.isFalse
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
h✝ : ¬(acc.2.2.snd = true ∨ acc.2.2.fst = true)
⊢ f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1)
    (match f.clauses[rupHints[↑idx]]? with
    | some (some c) =>
      match c.reduce acc.fst with
      | encounteredBoth => (acc.fst, acc.2.fst, true, false)
      | reducedToEmpty => (acc.fst, acc.2.fst, true, false)
      | reducedToUnit (l, b) =>
        if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
        else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
      | reducedToNonunit => (acc.fst, acc.2.fst, false, true)
    | some none => (acc.fst, acc.2.fst, false, true)
    | none => (acc.fst, acc.2.fst, false, true))

State before:
case intro.intro.isTrue
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
h✝ : acc.2.2.snd = true ∨ acc.2.2.fst = true
⊢ f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1) acc
Tactic:
exact ⟨hsize, h1, h2⟩
State after:
no goals

State before:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : ¬(acc.2.2.snd = true ∨ acc.2.2.fst = true)
⊢ f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1)
    (match f.clauses[rupHints[↑idx]]? with
    | some (some c) =>
      match c.reduce acc.fst with
      | encounteredBoth => (acc.fst, acc.2.fst, true, false)
      | reducedToEmpty => (acc.fst, acc.2.fst, true, false)
      | reducedToUnit (l, b) =>
        if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
        else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
      | reducedToNonunit => (acc.fst, acc.2.fst, false, true)
    | some none => (acc.fst, acc.2.fst, false, true)
    | none => (acc.fst, acc.2.fst, false, true))
Tactic:
simp only [not_or, Bool.not_eq_true] at acc2_eq_false
State after:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
⊢ f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1)
    (match f.clauses[rupHints[↑idx]]? with
    | some (some c) =>
      match c.reduce acc.fst with
      | encounteredBoth => (acc.fst, acc.2.fst, true, false)
      | reducedToEmpty => (acc.fst, acc.2.fst, true, false)
      | reducedToUnit (l, b) =>
        if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
        else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
      | reducedToNonunit => (acc.fst, acc.2.fst, false, true)
    | some none => (acc.fst, acc.2.fst, false, true)
    | none => (acc.fst, acc.2.fst, false, true))

State before:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
⊢ f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1)
    (match f.clauses[rupHints[↑idx]]? with
    | some (some c) =>
      match c.reduce acc.fst with
      | encounteredBoth => (acc.fst, acc.2.fst, true, false)
      | reducedToEmpty => (acc.fst, acc.2.fst, true, false)
      | reducedToUnit (l, b) =>
        if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
        else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
      | reducedToNonunit => (acc.fst, acc.2.fst, false, true)
    | some none => (acc.fst, acc.2.fst, false, true)
    | none => (acc.fst, acc.2.fst, false, true))
Tactic:
split
State after:
case h_1
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝ : Option (Option (DefaultClause n))
c✝ : DefaultClause n
heq✝ : f.clauses[rupHints[↑idx]]? = some (some c✝)
⊢ f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1)
    (match c✝.reduce acc.fst with
    | encounteredBoth => (acc.fst, acc.2.fst, true, false)
    | reducedToEmpty => (acc.fst, acc.2.fst, true, false)
    | reducedToUnit (l, b) =>
      if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
      else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
    | reducedToNonunit => (acc.fst, acc.2.fst, false, true))

case h_2
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝ : Option (Option (DefaultClause n))
heq✝ : f.clauses[rupHints[↑idx]]? = some none
⊢ f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1) (acc.fst, acc.2.fst, false, true)

case h_3
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝ : Option (Option (DefaultClause n))
heq✝ : f.clauses[rupHints[↑idx]]? = none
⊢ f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1) (acc.fst, acc.2.fst, false, true)

State before:
case h_2
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝ : Option (Option (DefaultClause n))
heq✝ : f.clauses[rupHints[↑idx]]? = some none
⊢ f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1) (acc.fst, acc.2.fst, false, true)

case h_3
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝ : Option (Option (DefaultClause n))
heq✝ : f.clauses[rupHints[↑idx]]? = none
⊢ f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1) (acc.fst, acc.2.fst, false, true)
Tactic:
. apply And.intro hsize ∘ And.intro h1
  simp only [false_implies]
State after:
case h_3
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝ : Option (Option (DefaultClause n))
heq✝ : f.clauses[rupHints[↑idx]]? = none
⊢ f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1) (acc.fst, acc.2.fst, false, true)

State before:
case h_3
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝ : Option (Option (DefaultClause n))
heq✝ : f.clauses[rupHints[↑idx]]? = none
⊢ f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1) (acc.fst, acc.2.fst, false, true)
Tactic:
. apply And.intro hsize ∘ And.intro h1
  simp only [false_implies]
State after:
no goals

State before:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
⊢ f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1)
    (match c.reduce acc.fst with
    | encounteredBoth => (acc.fst, acc.2.fst, true, false)
    | reducedToEmpty => (acc.fst, acc.2.fst, true, false)
    | reducedToUnit (l, b) =>
      if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
      else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
    | reducedToNonunit => (acc.fst, acc.2.fst, false, true))
Tactic:
have c_in_f : c ∈ toList f := by
  simp only [toList, Array.toList_eq, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
    exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool]
  apply Or.inl
  simp only [getElem?] at hc
  split at hc
  . simp only [Option.some.injEq] at hc
    rw [← hc]
    apply Array.getElem_mem_data
  . exact False.elim hc
State after:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
⊢ f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1)
    (match c.reduce acc.fst with
    | encounteredBoth => (acc.fst, acc.2.fst, true, false)
    | reducedToEmpty => (acc.fst, acc.2.fst, true, false)
    | reducedToUnit (l, b) =>
      if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
      else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
    | reducedToNonunit => (acc.fst, acc.2.fst, false, true))

State before:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
⊢ f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1)
    (match c.reduce acc.fst with
    | encounteredBoth => (acc.fst, acc.2.fst, true, false)
    | reducedToEmpty => (acc.fst, acc.2.fst, true, false)
    | reducedToUnit (l, b) =>
      if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
      else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
    | reducedToNonunit => (acc.fst, acc.2.fst, false, true))
Tactic:
split
State after:
case h_1
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
heq✝ : c.reduce acc.fst = encounteredBoth
⊢ f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1) (acc.fst, acc.2.fst, true, false)

case h_2
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
heq✝ : c.reduce acc.fst = reducedToEmpty
⊢ f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1) (acc.fst, acc.2.fst, true, false)

case h_3
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l✝ : PosFin n
b✝ : Bool
heq✝ : c.reduce acc.fst = reducedToUnit (l✝, b✝)
⊢ f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1)
    (if hasAssignment b✝ acc.fst[l✝.val]! = true then (acc.fst, acc.2.fst, false, false)
    else (acc.fst.modify l✝.val (addAssignment b✝), (l✝, b✝) :: acc.2.fst, false, false))

case h_4
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
heq✝ : c.reduce acc.fst = reducedToNonunit
⊢ f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1) (acc.fst, acc.2.fst, false, true)

State before:
case h_1
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
heq✝ : c.reduce acc.fst = encounteredBoth
⊢ f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1) (acc.fst, acc.2.fst, true, false)

case h_2
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
heq✝ : c.reduce acc.fst = reducedToEmpty
⊢ f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1) (acc.fst, acc.2.fst, true, false)

case h_3
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l✝ : PosFin n
b✝ : Bool
heq✝ : c.reduce acc.fst = reducedToUnit (l✝, b✝)
⊢ f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1)
    (if hasAssignment b✝ acc.fst[l✝.val]! = true then (acc.fst, acc.2.fst, false, false)
    else (acc.fst.modify l✝.val (addAssignment b✝), (l✝, b✝) :: acc.2.fst, false, false))

case h_4
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
heq✝ : c.reduce acc.fst = reducedToNonunit
⊢ f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1) (acc.fst, acc.2.fst, false, true)
Tactic:
. next heq =>
  simp only [confirmRupHint_fold_entails_hsat_motive, h1, imp_self, and_self, hsize,
    incompatible_of_unsat (PosFin n) acc.1 f (encounteredBoth_entails_unsat c acc.1 heq)]
State after:
case h_2
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
heq✝ : c.reduce acc.fst = reducedToEmpty
⊢ f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1) (acc.fst, acc.2.fst, true, false)

case h_3
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l✝ : PosFin n
b✝ : Bool
heq✝ : c.reduce acc.fst = reducedToUnit (l✝, b✝)
⊢ f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1)
    (if hasAssignment b✝ acc.fst[l✝.val]! = true then (acc.fst, acc.2.fst, false, false)
    else (acc.fst.modify l✝.val (addAssignment b✝), (l✝, b✝) :: acc.2.fst, false, false))

case h_4
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
heq✝ : c.reduce acc.fst = reducedToNonunit
⊢ f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1) (acc.fst, acc.2.fst, false, true)

State before:
case h_4
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
heq✝ : c.reduce acc.fst = reducedToNonunit
⊢ f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1) (acc.fst, acc.2.fst, false, true)
Tactic:
. apply And.intro hsize ∘ And.intro h1
  simp only [false_implies]
State after:
no goals

State before:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
⊢ c ∈ f.toList
Tactic:
simp only [toList, Array.toList_eq, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
  exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool]
State after:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
⊢ some c ∈ f.clauses.data ∨
    (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c) ∨
      ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c

State before:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
⊢ some c ∈ f.clauses.data ∨
    (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c) ∨
      ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c
Tactic:
apply Or.inl
State after:
case h
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
⊢ some c ∈ f.clauses.data

State before:
case h
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
⊢ some c ∈ f.clauses.data
Tactic:
simp only [getElem?] at hc
State after:
case h
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : (if h : rupHints[↑idx] < f.clauses.size then some (f.clauses.get ⟨rupHints[↑idx], h⟩) else none) = some (some c)
⊢ some c ∈ f.clauses.data

State before:
case h
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : (if h : rupHints[↑idx] < f.clauses.size then some (f.clauses.get ⟨rupHints[↑idx], h⟩) else none) = some (some c)
⊢ some c ∈ f.clauses.data
Tactic:
split at hc
State after:
case h.isTrue
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝ : Option (Option (DefaultClause n))
c : DefaultClause n
h✝ : rupHints[↑idx] < f.clauses.size
hc : some (f.clauses.get ⟨rupHints[↑idx], h✝⟩) = some (some c)
⊢ some c ∈ f.clauses.data

case h.isFalse
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝ : Option (Option (DefaultClause n))
c : DefaultClause n
h✝ : ¬rupHints[↑idx] < f.clauses.size
hc : False
⊢ some c ∈ f.clauses.data

State before:
case h.isTrue
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝ : Option (Option (DefaultClause n))
c : DefaultClause n
h✝ : rupHints[↑idx] < f.clauses.size
hc : some (f.clauses.get ⟨rupHints[↑idx], h✝⟩) = some (some c)
⊢ some c ∈ f.clauses.data

case h.isFalse
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝ : Option (Option (DefaultClause n))
c : DefaultClause n
h✝ : ¬rupHints[↑idx] < f.clauses.size
hc : False
⊢ some c ∈ f.clauses.data
Tactic:
. simp only [Option.some.injEq] at hc
  rw [← hc]
  apply Array.getElem_mem_data
State after:
case h.isFalse
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝ : Option (Option (DefaultClause n))
c : DefaultClause n
h✝ : ¬rupHints[↑idx] < f.clauses.size
hc : False
⊢ some c ∈ f.clauses.data

State before:
case h.isFalse
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝ : Option (Option (DefaultClause n))
c : DefaultClause n
h✝ : ¬rupHints[↑idx] < f.clauses.size
hc : False
⊢ some c ∈ f.clauses.data
Tactic:
. exact False.elim hc
State after:
no goals

State before:
case h.isTrue
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝ : Option (Option (DefaultClause n))
c : DefaultClause n
h✝ : rupHints[↑idx] < f.clauses.size
hc : some (f.clauses.get ⟨rupHints[↑idx], h✝⟩) = some (some c)
⊢ some c ∈ f.clauses.data
Tactic:
simp only [Option.some.injEq] at hc
State after:
case h.isTrue
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝ : Option (Option (DefaultClause n))
c : DefaultClause n
h✝ : rupHints[↑idx] < f.clauses.size
hc : f.clauses.get ⟨rupHints[↑idx], h✝⟩ = some c
⊢ some c ∈ f.clauses.data

State before:
case h.isTrue
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝ : Option (Option (DefaultClause n))
c : DefaultClause n
h✝ : rupHints[↑idx] < f.clauses.size
hc : f.clauses.get ⟨rupHints[↑idx], h✝⟩ = some c
⊢ some c ∈ f.clauses.data
Tactic:
rw [← hc]
State after:
case h.isTrue
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝ : Option (Option (DefaultClause n))
c : DefaultClause n
h✝ : rupHints[↑idx] < f.clauses.size
hc : f.clauses.get ⟨rupHints[↑idx], h✝⟩ = some c
⊢ f.clauses.get ⟨rupHints[↑idx], h✝⟩ ∈ f.clauses.data

State before:
case h.isTrue
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝ : Option (Option (DefaultClause n))
c : DefaultClause n
h✝ : rupHints[↑idx] < f.clauses.size
hc : f.clauses.get ⟨rupHints[↑idx], h✝⟩ = some c
⊢ f.clauses.get ⟨rupHints[↑idx], h✝⟩ ∈ f.clauses.data
Tactic:
apply Array.getElem_mem_data
State after:
no goals

State before:
case h.isFalse
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝ : Option (Option (DefaultClause n))
c : DefaultClause n
h✝ : ¬rupHints[↑idx] < f.clauses.size
hc : False
⊢ some c ∈ f.clauses.data
Tactic:
exact False.elim hc
State after:
no goals

State before:
case h_1
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
heq✝ : c.reduce acc.fst = encounteredBoth
⊢ f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1) (acc.fst, acc.2.fst, true, false)
Tactic:
next heq =>
simp only [confirmRupHint_fold_entails_hsat_motive, h1, imp_self, and_self, hsize,
  incompatible_of_unsat (PosFin n) acc.1 f (encounteredBoth_entails_unsat c acc.1 heq)]
State after:
no goals

State before:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
heq : c.reduce acc.fst = encounteredBoth
⊢ f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1) (acc.fst, acc.2.fst, true, false)
Tactic:
simp only [confirmRupHint_fold_entails_hsat_motive, h1, imp_self, and_self, hsize,
  incompatible_of_unsat (PosFin n) acc.1 f (encounteredBoth_entails_unsat c acc.1 heq)]
State after:
no goals

State before:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
heq : c.reduce acc.fst = reducedToEmpty
⊢ f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1) (acc.fst, acc.2.fst, true, false)
Tactic:
simp only [confirmRupHint_fold_entails_hsat_motive, h1, hsize, forall_const, true_and]
State after:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
heq : c.reduce acc.fst = reducedToEmpty
⊢ incompatible (PosFin n) acc.fst f

State before:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
heq : c.reduce acc.fst = reducedToEmpty
⊢ incompatible (PosFin n) acc.fst f
Tactic:
intro p
State after:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
heq : c.reduce acc.fst = reducedToEmpty
p : PosFin n → Bool
⊢ ¬(p ⊨ acc.fst) ∨ ¬(p ⊨ f)

State before:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
heq : c.reduce acc.fst = reducedToEmpty
p : PosFin n → Bool
⊢ ¬(p ⊨ acc.fst) ∨ ¬(p ⊨ f)
Tactic:
rcases reducedToEmpty_entails_incompatible c acc.1 heq p with pc | pacc
State after:
case inl
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
heq : c.reduce acc.fst = reducedToEmpty
p : PosFin n → Bool
pc : ¬(p ⊨ c)
⊢ ¬(p ⊨ acc.fst) ∨ ¬(p ⊨ f)

case inr
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
heq : c.reduce acc.fst = reducedToEmpty
p : PosFin n → Bool
pacc : ¬(p ⊨ acc.fst)
⊢ ¬(p ⊨ acc.fst) ∨ ¬(p ⊨ f)

State before:
case inr
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
heq : c.reduce acc.fst = reducedToEmpty
p : PosFin n → Bool
pacc : ¬(p ⊨ acc.fst)
⊢ ¬(p ⊨ acc.fst) ∨ ¬(p ⊨ f)
Tactic:
. exact Or.inl pacc
State after:
no goals

State before:
case inl
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
heq : c.reduce acc.fst = reducedToEmpty
p : PosFin n → Bool
pc : ¬(p ⊨ c)
⊢ ¬(p ⊨ acc.fst) ∨ ¬(p ⊨ f)
Tactic:
apply Or.inr
State after:
case inl.h
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
heq : c.reduce acc.fst = reducedToEmpty
p : PosFin n → Bool
pc : ¬(p ⊨ c)
⊢ ¬(p ⊨ f)

State before:
case inl.h
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
heq : c.reduce acc.fst = reducedToEmpty
p : PosFin n → Bool
pc : ¬(p ⊨ c)
⊢ ¬(p ⊨ f)
Tactic:
intro pf
State after:
case inl.h
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
heq : c.reduce acc.fst = reducedToEmpty
p : PosFin n → Bool
pc : ¬(p ⊨ c)
pf : p ⊨ f
⊢ False

State before:
case inl.h
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
heq : c.reduce acc.fst = reducedToEmpty
p : PosFin n → Bool
pc : ¬(p ⊨ c)
pf :
  ∀ (x : DefaultClause n),
    x ∈ f.toList → decide (((Clause.toList x).any fun l => decide (p l.fst = l.snd)) = true) = true
⊢ False
Tactic:
specialize pf c c_in_f
State after:
case inl.h
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
heq : c.reduce acc.fst = reducedToEmpty
p : PosFin n → Bool
pc : ¬(p ⊨ c)
pf : decide (((Clause.toList c).any fun l => decide (p l.fst = l.snd)) = true) = true
⊢ False

State before:
case inl.h
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
heq : c.reduce acc.fst = reducedToEmpty
p : PosFin n → Bool
pc : ¬((Clause.toList c).any fun l => decide (p l.fst = l.snd)) = true
pf : decide (((Clause.toList c).any fun l => decide (p l.fst = l.snd)) = true) = true
⊢ False
Tactic:
exact pc $ of_decide_eq_true pf
State after:
no goals

State before:
case inr
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
heq : c.reduce acc.fst = reducedToEmpty
p : PosFin n → Bool
pacc : ¬(p ⊨ acc.fst)
⊢ ¬(p ⊨ acc.fst) ∨ ¬(p ⊨ f)
Tactic:
exact Or.inl pacc
State after:
no goals

State before:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
⊢ f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1)
    (if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
    else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false))
Tactic:
simp only [confirmRupHint_fold_entails_hsat_motive]
State after:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
⊢ (if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
          else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)).fst.size =
      n ∧
    limplies (PosFin n) f
        (if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
          else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)).fst ∧
      ((if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
                else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)).snd.snd.fst =
          true →
        incompatible (PosFin n)
          (if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
            else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)).fst
          f)

State before:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
⊢ (if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
          else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)).fst.size =
      n ∧
    limplies (PosFin n) f
        (if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
          else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)).fst ∧
      ((if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
                else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)).snd.snd.fst =
          true →
        incompatible (PosFin n)
          (if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
            else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)).fst
          f)
Tactic:
split
State after:
case isTrue
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : hasAssignment b acc.fst[l.val]! = true
⊢ (acc.fst, acc.2.fst, false, false).fst.size = n ∧
    limplies (PosFin n) f (acc.fst, acc.2.fst, false, false).fst ∧
      (False → incompatible (PosFin n) (acc.fst, acc.2.fst, false, false).fst f)

case isFalse
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
⊢ (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false).fst.size = n ∧
    limplies (PosFin n) f (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false).fst ∧
      (False →
        incompatible (PosFin n) (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false).fst f)

State before:
case isTrue
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : hasAssignment b acc.fst[l.val]! = true
⊢ (acc.fst, acc.2.fst, false, false).fst.size = n ∧
    limplies (PosFin n) f (acc.fst, acc.2.fst, false, false).fst ∧
      (False → incompatible (PosFin n) (acc.fst, acc.2.fst, false, false).fst f)

case isFalse
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
⊢ (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false).fst.size = n ∧
    limplies (PosFin n) f (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false).fst ∧
      (False →
        incompatible (PosFin n) (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false).fst f)
Tactic:
. simp only [h1, hsize, false_implies, and_self]
State after:
case isFalse
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
⊢ (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false).fst.size = n ∧
    limplies (PosFin n) f (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false).fst ∧
      (False →
        incompatible (PosFin n) (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false).fst f)

State before:
case isTrue
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : hasAssignment b acc.fst[l.val]! = true
⊢ (acc.fst, acc.2.fst, false, false).fst.size = n ∧
    limplies (PosFin n) f (acc.fst, acc.2.fst, false, false).fst ∧
      (False → incompatible (PosFin n) (acc.fst, acc.2.fst, false, false).fst f)
Tactic:
simp only [h1, hsize, false_implies, and_self]
State after:
no goals

State before:
case isFalse
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
⊢ (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false).fst.size = n ∧
    limplies (PosFin n) f (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false).fst ∧
      (False →
        incompatible (PosFin n) (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false).fst f)
Tactic:
simp only [Array.modify_preserves_size, hsize, false_implies, and_true, true_and]
State after:
case isFalse
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
⊢ limplies (PosFin n) f (acc.fst.modify l.val (addAssignment b))

State before:
case isFalse
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
⊢ limplies (PosFin n) f (acc.fst.modify l.val (addAssignment b))
Tactic:
intro p pf
State after:
case isFalse
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
⊢ p ⊨ acc.fst.modify l.val (addAssignment b)

State before:
case isFalse
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
⊢ p ⊨ acc.fst.modify l.val (addAssignment b)
Tactic:
have pacc := h1 p pf
State after:
case isFalse
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pacc : p ⊨ acc.fst
⊢ p ⊨ acc.fst.modify l.val (addAssignment b)

State before:
case isFalse
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pacc : p ⊨ acc.fst
pc : p ⊨ c
⊢ p ⊨ acc.fst.modify l.val (addAssignment b)
Tactic:
have plb := reducedToUnit_entails_limplies c acc.1 ⟨l, b⟩ heq p pacc pc
State after:
case isFalse
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pacc : p ⊨ acc.fst
pc : p ⊨ c
plb : p ⊨ (l, b)
⊢ p ⊨ acc.fst.modify l.val (addAssignment b)

State before:
case isFalse
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pacc : p ⊨ acc.fst
pc : p ⊨ c
plb : p ⊨ (l, b)
⊢ ∀ (i : PosFin n), hasAssignment (decide (p i = false)) (acc.fst.modify l.val (addAssignment b))[i.val]! = false
Tactic:
intro i
State after:
case isFalse
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pacc : p ⊨ acc.fst
pc : p ⊨ c
plb : p ⊨ (l, b)
i : PosFin n
⊢ hasAssignment (decide (p i = false)) (acc.fst.modify l.val (addAssignment b))[i.val]! = false

State before:
case isFalse
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pacc : p ⊨ acc.fst
pc : p ⊨ c
plb : p ⊨ (l, b)
i : PosFin n
⊢ hasAssignment (decide (p i = false)) (acc.fst.modify l.val (addAssignment b))[i.val]! = false
Tactic:
specialize pacc i
State after:
case isFalse
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
plb : p ⊨ (l, b)
i : PosFin n
pacc : ¬hasAssignment (decide ¬p i = true) acc.fst[i.val]! = true
⊢ hasAssignment (decide (p i = false)) (acc.fst.modify l.val (addAssignment b))[i.val]! = false

State before:
case isFalse
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
plb : p ⊨ (l, b)
i : PosFin n
pacc : ¬hasAssignment (decide ¬p i = true) acc.fst[i.val]! = true
⊢ hasAssignment (decide (p i = false)) (acc.fst.modify l.val (addAssignment b))[i.val]! = false
Tactic:
simp only [Bool.not_eq_true] at pacc
State after:
case isFalse
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
plb : p ⊨ (l, b)
i : PosFin n
pacc : hasAssignment (decide (p i = false)) acc.fst[i.val]! = false
⊢ hasAssignment (decide (p i = false)) (acc.fst.modify l.val (addAssignment b))[i.val]! = false

State before:
case isFalse
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
plb : p ⊨ (l, b)
i : PosFin n
pacc : hasAssignment (decide (p i = false)) acc.fst[i.val]! = false
⊢ hasAssignment (decide (p i = false)) (acc.fst.modify l.val (addAssignment b))[i.val]! = false
Tactic:
have i_in_bounds : i.1 < acc.1.size := by rw [hsize]; exact i.2.2
State after:
case isFalse
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
plb : p ⊨ (l, b)
i : PosFin n
pacc : hasAssignment (decide (p i = false)) acc.fst[i.val]! = false
i_in_bounds : i.val < acc.fst.size
⊢ hasAssignment (decide (p i = false)) (acc.fst.modify l.val (addAssignment b))[i.val]! = false

State before:
case isFalse
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
plb : p ⊨ (l, b)
i : PosFin n
pacc : hasAssignment (decide (p i = false)) acc.fst[i.val]! = false
i_in_bounds : i.val < acc.fst.size
⊢ hasAssignment (decide (p i = false)) (acc.fst.modify l.val (addAssignment b))[i.val]! = false
Tactic:
have l_in_bounds : l.1 < acc.1.size := by rw [hsize]; exact l.2.2
State after:
case isFalse
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
plb : p ⊨ (l, b)
i : PosFin n
pacc : hasAssignment (decide (p i = false)) acc.fst[i.val]! = false
i_in_bounds : i.val < acc.fst.size
l_in_bounds : l.val < acc.fst.size
⊢ hasAssignment (decide (p i = false)) (acc.fst.modify l.val (addAssignment b))[i.val]! = false

State before:
case isFalse
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
plb : p ⊨ (l, b)
i : PosFin n
pacc : hasAssignment (decide (p i = false)) acc.fst[i.val]! = false
i_in_bounds : i.val < acc.fst.size
l_in_bounds : l.val < acc.fst.size
⊢ hasAssignment (decide (p i = false)) (acc.fst.modify l.val (addAssignment b))[i.val]! = false
Tactic:
by_cases l.1 = i.1
State after:
case pos
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝¹ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
plb : p ⊨ (l, b)
i : PosFin n
pacc : hasAssignment (decide (p i = false)) acc.fst[i.val]! = false
i_in_bounds : i.val < acc.fst.size
l_in_bounds : l.val < acc.fst.size
h✝ : l.val = i.val
⊢ hasAssignment (decide (p i = false)) (acc.fst.modify l.val (addAssignment b))[i.val]! = false

case neg
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝¹ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
plb : p ⊨ (l, b)
i : PosFin n
pacc : hasAssignment (decide (p i = false)) acc.fst[i.val]! = false
i_in_bounds : i.val < acc.fst.size
l_in_bounds : l.val < acc.fst.size
h✝ : ¬l.val = i.val
⊢ hasAssignment (decide (p i = false)) (acc.fst.modify l.val (addAssignment b))[i.val]! = false

State before:
case neg
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝¹ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
plb : p ⊨ (l, b)
i : PosFin n
pacc : hasAssignment (decide (p i = false)) acc.fst[i.val]! = false
i_in_bounds : i.val < acc.fst.size
l_in_bounds : l.val < acc.fst.size
h✝ : ¬l.val = i.val
⊢ hasAssignment (decide (p i = false)) (acc.fst.modify l.val (addAssignment b))[i.val]! = false
Tactic:
. next l_ne_i =>
  simp only [getElem!, Array.modify_preserves_size, i_in_bounds,
    Array.get_modify_unchanged l_in_bounds i_in_bounds _ l_ne_i, dite_true,
    Array.get_eq_getElem]
  simp only [getElem!, i_in_bounds, dite_true] at pacc
  exact pacc
State after:
no goals

State before:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pacc : p ⊨ acc.fst
pf :
  ∀ (x : DefaultClause n),
    x ∈ f.toList → decide (((Clause.toList x).any fun l => decide (p l.fst = l.snd)) = true) = true
⊢ p ⊨ c
Tactic:
exact of_decide_eq_true $ pf c c_in_f
State after:
no goals

State before:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
plb : p ⊨ (l, b)
i : PosFin n
pacc : hasAssignment (decide (p i = false)) acc.fst[i.val]! = false
⊢ i.val < acc.fst.size
Tactic:
rw [hsize]
State after:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
plb : p ⊨ (l, b)
i : PosFin n
pacc : hasAssignment (decide (p i = false)) acc.fst[i.val]! = false
⊢ i.val < n

State before:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
plb : p ⊨ (l, b)
i : PosFin n
pacc : hasAssignment (decide (p i = false)) acc.fst[i.val]! = false
⊢ i.val < n
Tactic:
exact i.2.2
State after:
no goals

State before:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
plb : p ⊨ (l, b)
i : PosFin n
pacc : hasAssignment (decide (p i = false)) acc.fst[i.val]! = false
i_in_bounds : i.val < acc.fst.size
⊢ l.val < acc.fst.size
Tactic:
rw [hsize]
State after:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
plb : p ⊨ (l, b)
i : PosFin n
pacc : hasAssignment (decide (p i = false)) acc.fst[i.val]! = false
i_in_bounds : i.val < acc.fst.size
⊢ l.val < n

State before:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
plb : p ⊨ (l, b)
i : PosFin n
pacc : hasAssignment (decide (p i = false)) acc.fst[i.val]! = false
i_in_bounds : i.val < acc.fst.size
⊢ l.val < n
Tactic:
exact l.2.2
State after:
no goals

State before:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
plb : p ⊨ (l, b)
i : PosFin n
pacc : hasAssignment (decide (p i = false)) acc.fst[i.val]! = false
i_in_bounds : i.val < acc.fst.size
l_in_bounds : l.val < acc.fst.size
l_eq_i : l.val = i.val
⊢ hasAssignment (decide (p i = false)) (acc.fst.modify l.val (addAssignment b))[i.val]! = false
Tactic:
simp only [getElem!, Array.modify_preserves_size, i_in_bounds, ↓ reduceDite,
  Array.get_eq_getElem, l_eq_i, Array.get_modify_at_idx i_in_bounds (addAssignment b)]
State after:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
plb : p ⊨ (l, b)
i : PosFin n
pacc : hasAssignment (decide (p i = false)) acc.fst[i.val]! = false
i_in_bounds : i.val < acc.fst.size
l_in_bounds : l.val < acc.fst.size
l_eq_i : l.val = i.val
⊢ hasAssignment (decide (p i = false)) (addAssignment b acc.fst[i.val]) = false

State before:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
plb : p ⊨ (l, b)
i : PosFin n
pacc : hasAssignment (decide (p i = false)) acc.fst[i.val]! = false
i_in_bounds : i.val < acc.fst.size
l_in_bounds : l.val < acc.fst.size
l_eq_i : l.val = i.val
⊢ hasAssignment (decide (p i = false)) (addAssignment b acc.fst[i.val]) = false
Tactic:
simp only [getElem!, i_in_bounds, dite_true, Array.get_eq_getElem] at pacc
State after:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
plb : p ⊨ (l, b)
i : PosFin n
i_in_bounds : i.val < acc.fst.size
l_in_bounds : l.val < acc.fst.size
l_eq_i : l.val = i.val
pacc : hasAssignment (decide (p i = false)) acc.fst[i.val] = false
⊢ hasAssignment (decide (p i = false)) (addAssignment b acc.fst[i.val]) = false

State before:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
plb : p ⊨ (l, b)
i : PosFin n
i_in_bounds : i.val < acc.fst.size
l_in_bounds : l.val < acc.fst.size
l_eq_i : l.val = i.val
pacc : hasAssignment (decide (p i = false)) acc.fst[i.val] = false
⊢ hasAssignment (decide (p i = false)) (addAssignment b acc.fst[i.val]) = false
Tactic:
by_cases pi : p i
State after:
case pos
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
plb : p ⊨ (l, b)
i : PosFin n
i_in_bounds : i.val < acc.fst.size
l_in_bounds : l.val < acc.fst.size
l_eq_i : l.val = i.val
pacc : hasAssignment (decide (p i = false)) acc.fst[i.val] = false
pi : p i = true
⊢ hasAssignment (decide (p i = false)) (addAssignment b acc.fst[i.val]) = false

case neg
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
plb : p ⊨ (l, b)
i : PosFin n
i_in_bounds : i.val < acc.fst.size
l_in_bounds : l.val < acc.fst.size
l_eq_i : l.val = i.val
pacc : hasAssignment (decide (p i = false)) acc.fst[i.val] = false
pi : ¬p i = true
⊢ hasAssignment (decide (p i = false)) (addAssignment b acc.fst[i.val]) = false

State before:
case pos
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
plb : p ⊨ (l, b)
i : PosFin n
i_in_bounds : i.val < acc.fst.size
l_in_bounds : l.val < acc.fst.size
l_eq_i : l.val = i.val
pacc : hasAssignment (decide (p i = false)) acc.fst[i.val] = false
pi : p i = true
⊢ hasAssignment (decide (p i = false)) (addAssignment b acc.fst[i.val]) = false
Tactic:
simp only [pi, decide_False]
State after:
case pos
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
plb : p ⊨ (l, b)
i : PosFin n
i_in_bounds : i.val < acc.fst.size
l_in_bounds : l.val < acc.fst.size
l_eq_i : l.val = i.val
pacc : hasAssignment (decide (p i = false)) acc.fst[i.val] = false
pi : p i = true
⊢ hasAssignment false (addAssignment b acc.fst[i.val]) = false

State before:
case pos
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
plb : p ⊨ (l, b)
i : PosFin n
i_in_bounds : i.val < acc.fst.size
l_in_bounds : l.val < acc.fst.size
l_eq_i : l.val = i.val
pacc : hasAssignment (decide (p i = false)) acc.fst[i.val] = false
pi : p i = true
⊢ hasAssignment false (addAssignment b acc.fst[i.val]) = false
Tactic:
simp only [hasAssignment, pi, decide_False, ite_false] at pacc
State after:
case pos
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
plb : p ⊨ (l, b)
i : PosFin n
i_in_bounds : i.val < acc.fst.size
l_in_bounds : l.val < acc.fst.size
l_eq_i : l.val = i.val
pi : p i = true
pacc : acc.fst[i.val].hasNegAssignment = false
⊢ hasAssignment false (addAssignment b acc.fst[i.val]) = false

State before:
case pos
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
plb : p ⊨ (l, b)
i : PosFin n
i_in_bounds : i.val < acc.fst.size
l_in_bounds : l.val < acc.fst.size
l_eq_i : l.val = i.val
pi : p i = true
pacc : acc.fst[i.val].hasNegAssignment = false
⊢ hasAssignment false (addAssignment b acc.fst[i.val]) = false
Tactic:
by_cases hb : b
State after:
case pos
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
plb : p ⊨ (l, b)
i : PosFin n
i_in_bounds : i.val < acc.fst.size
l_in_bounds : l.val < acc.fst.size
l_eq_i : l.val = i.val
pi : p i = true
pacc : acc.fst[i.val].hasNegAssignment = false
hb : b = true
⊢ hasAssignment false (addAssignment b acc.fst[i.val]) = false

case neg
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
plb : p ⊨ (l, b)
i : PosFin n
i_in_bounds : i.val < acc.fst.size
l_in_bounds : l.val < acc.fst.size
l_eq_i : l.val = i.val
pi : p i = true
pacc : acc.fst[i.val].hasNegAssignment = false
hb : ¬b = true
⊢ hasAssignment false (addAssignment b acc.fst[i.val]) = false

State before:
case pos
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
plb : p ⊨ (l, b)
i : PosFin n
i_in_bounds : i.val < acc.fst.size
l_in_bounds : l.val < acc.fst.size
l_eq_i : l.val = i.val
pi : p i = true
pacc : acc.fst[i.val].hasNegAssignment = false
hb : b = true
⊢ hasAssignment false (addAssignment b acc.fst[i.val]) = false

case neg
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
plb : p ⊨ (l, b)
i : PosFin n
i_in_bounds : i.val < acc.fst.size
l_in_bounds : l.val < acc.fst.size
l_eq_i : l.val = i.val
pi : p i = true
pacc : acc.fst[i.val].hasNegAssignment = false
hb : ¬b = true
⊢ hasAssignment false (addAssignment b acc.fst[i.val]) = false
Tactic:
. simp only [hasAssignment, ↓reduceIte, addAssignment]
  simp only [hb]
  simp only [hasAssignment, addAssignment, hb, ite_true, ite_false, hasNeg_of_addPos]
  exact pacc
State after:
case neg
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
plb : p ⊨ (l, b)
i : PosFin n
i_in_bounds : i.val < acc.fst.size
l_in_bounds : l.val < acc.fst.size
l_eq_i : l.val = i.val
pi : p i = true
pacc : acc.fst[i.val].hasNegAssignment = false
hb : ¬b = true
⊢ hasAssignment false (addAssignment b acc.fst[i.val]) = false

State before:
case pos
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
plb : p ⊨ (l, b)
i : PosFin n
i_in_bounds : i.val < acc.fst.size
l_in_bounds : l.val < acc.fst.size
l_eq_i : l.val = i.val
pi : p i = true
pacc : acc.fst[i.val].hasNegAssignment = false
hb : b = true
⊢ hasAssignment false (addAssignment b acc.fst[i.val]) = false
Tactic:
simp only [hasAssignment, ↓reduceIte, addAssignment]
State after:
case pos
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
plb : p ⊨ (l, b)
i : PosFin n
i_in_bounds : i.val < acc.fst.size
l_in_bounds : l.val < acc.fst.size
l_eq_i : l.val = i.val
pi : p i = true
pacc : acc.fst[i.val].hasNegAssignment = false
hb : b = true
⊢ ((if b = true then addPosAssignment else addNegAssignment) acc.fst[i.val]).hasNegAssignment = false

State before:
case pos
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
plb : p ⊨ (l, b)
i : PosFin n
i_in_bounds : i.val < acc.fst.size
l_in_bounds : l.val < acc.fst.size
l_eq_i : l.val = i.val
pi : p i = true
pacc : acc.fst[i.val].hasNegAssignment = false
hb : b = true
⊢ ((if b = true then addPosAssignment else addNegAssignment) acc.fst[i.val]).hasNegAssignment = false
Tactic:
simp only [hb]
State after:
case pos
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
plb : p ⊨ (l, b)
i : PosFin n
i_in_bounds : i.val < acc.fst.size
l_in_bounds : l.val < acc.fst.size
l_eq_i : l.val = i.val
pi : p i = true
pacc : acc.fst[i.val].hasNegAssignment = false
hb : b = true
⊢ ((if True then addPosAssignment else addNegAssignment) acc.fst[i.val]).hasNegAssignment = false

State before:
case pos
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
plb : p ⊨ (l, b)
i : PosFin n
i_in_bounds : i.val < acc.fst.size
l_in_bounds : l.val < acc.fst.size
l_eq_i : l.val = i.val
pi : p i = true
pacc : acc.fst[i.val].hasNegAssignment = false
hb : b = true
⊢ ((if True then addPosAssignment else addNegAssignment) acc.fst[i.val]).hasNegAssignment = false
Tactic:
simp only [hasAssignment, addAssignment, hb, ite_true, ite_false, hasNeg_of_addPos]
State after:
case pos
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
plb : p ⊨ (l, b)
i : PosFin n
i_in_bounds : i.val < acc.fst.size
l_in_bounds : l.val < acc.fst.size
l_eq_i : l.val = i.val
pi : p i = true
pacc : acc.fst[i.val].hasNegAssignment = false
hb : b = true
⊢ acc.fst[i.val].hasNegAssignment = false

State before:
case pos
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
plb : p ⊨ (l, b)
i : PosFin n
i_in_bounds : i.val < acc.fst.size
l_in_bounds : l.val < acc.fst.size
l_eq_i : l.val = i.val
pi : p i = true
pacc : acc.fst[i.val].hasNegAssignment = false
hb : b = true
⊢ acc.fst[i.val].hasNegAssignment = false
Tactic:
exact pacc
State after:
no goals

State before:
case neg
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
plb : p ⊨ (l, b)
i : PosFin n
i_in_bounds : i.val < acc.fst.size
l_in_bounds : l.val < acc.fst.size
l_eq_i : l.val = i.val
pi : p i = true
pacc : acc.fst[i.val].hasNegAssignment = false
hb : ¬b = true
⊢ hasAssignment false (addAssignment b acc.fst[i.val]) = false
Tactic:
exfalso
State after:
case neg
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
plb : p ⊨ (l, b)
i : PosFin n
i_in_bounds : i.val < acc.fst.size
l_in_bounds : l.val < acc.fst.size
l_eq_i : l.val = i.val
pi : p i = true
pacc : acc.fst[i.val].hasNegAssignment = false
hb : ¬b = true
⊢ False

State before:
case neg
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
plb : p ⊨ (l, b)
i : PosFin n
i_in_bounds : i.val < acc.fst.size
l_in_bounds : l.val < acc.fst.size
l_eq_i : l.val = i.val
pi : p i = true
pacc : acc.fst[i.val].hasNegAssignment = false
hb : ¬b = true
⊢ False
Tactic:
simp only [Bool.not_eq_true] at hb
State after:
case neg
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
plb : p ⊨ (l, b)
i : PosFin n
i_in_bounds : i.val < acc.fst.size
l_in_bounds : l.val < acc.fst.size
l_eq_i : l.val = i.val
pi : p i = true
pacc : acc.fst[i.val].hasNegAssignment = false
hb : b = false
⊢ False

State before:
case neg
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
plb : p ⊨ (l, b)
i : PosFin n
i_in_bounds : i.val < acc.fst.size
l_in_bounds : l.val < acc.fst.size
l_eq_i : l.val = i.val
pacc : hasAssignment (decide (p i = false)) acc.fst[i.val] = false
pi : ¬p i = true
⊢ hasAssignment (decide (p i = false)) (addAssignment b acc.fst[i.val]) = false
Tactic:
simp only [Bool.not_eq_true] at pi
State after:
case neg
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
plb : p ⊨ (l, b)
i : PosFin n
i_in_bounds : i.val < acc.fst.size
l_in_bounds : l.val < acc.fst.size
l_eq_i : l.val = i.val
pacc : hasAssignment (decide (p i = false)) acc.fst[i.val] = false
pi : p i = false
⊢ hasAssignment (decide (p i = false)) (addAssignment b acc.fst[i.val]) = false

State before:
case neg
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
plb : p ⊨ (l, b)
i : PosFin n
i_in_bounds : i.val < acc.fst.size
l_in_bounds : l.val < acc.fst.size
l_eq_i : l.val = i.val
pacc : hasAssignment (decide (p i = false)) acc.fst[i.val] = false
pi : p i = false
⊢ hasAssignment (decide (p i = false)) (addAssignment b acc.fst[i.val]) = false
Tactic:
simp only [pi, decide_True]
State after:
case neg
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
plb : p ⊨ (l, b)
i : PosFin n
i_in_bounds : i.val < acc.fst.size
l_in_bounds : l.val < acc.fst.size
l_eq_i : l.val = i.val
pacc : hasAssignment (decide (p i = false)) acc.fst[i.val] = false
pi : p i = false
⊢ hasAssignment true (addAssignment b acc.fst[i.val]) = false

State before:
case neg
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
plb : p ⊨ (l, b)
i : PosFin n
i_in_bounds : i.val < acc.fst.size
l_in_bounds : l.val < acc.fst.size
l_eq_i : l.val = i.val
pacc : hasAssignment (decide (p i = false)) acc.fst[i.val] = false
pi : p i = false
⊢ hasAssignment true (addAssignment b acc.fst[i.val]) = false
Tactic:
simp only [pi, decide_True] at pacc
State after:
case neg
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
plb : p ⊨ (l, b)
i : PosFin n
i_in_bounds : i.val < acc.fst.size
l_in_bounds : l.val < acc.fst.size
l_eq_i : l.val = i.val
pi : p i = false
pacc : hasAssignment true acc.fst[i.val] = false
⊢ hasAssignment true (addAssignment b acc.fst[i.val]) = false

State before:
case neg
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
plb : p ⊨ (l, b)
i : PosFin n
i_in_bounds : i.val < acc.fst.size
l_in_bounds : l.val < acc.fst.size
l_eq_i : l.val = i.val
pi : p i = false
pacc : hasAssignment true acc.fst[i.val] = false
⊢ hasAssignment true (addAssignment b acc.fst[i.val]) = false
Tactic:
by_cases hb : b
State after:
case pos
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
plb : p ⊨ (l, b)
i : PosFin n
i_in_bounds : i.val < acc.fst.size
l_in_bounds : l.val < acc.fst.size
l_eq_i : l.val = i.val
pi : p i = false
pacc : hasAssignment true acc.fst[i.val] = false
hb : b = true
⊢ hasAssignment true (addAssignment b acc.fst[i.val]) = false

case neg
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
plb : p ⊨ (l, b)
i : PosFin n
i_in_bounds : i.val < acc.fst.size
l_in_bounds : l.val < acc.fst.size
l_eq_i : l.val = i.val
pi : p i = false
pacc : hasAssignment true acc.fst[i.val] = false
hb : ¬b = true
⊢ hasAssignment true (addAssignment b acc.fst[i.val]) = false

State before:
case neg
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
plb : p ⊨ (l, b)
i : PosFin n
i_in_bounds : i.val < acc.fst.size
l_in_bounds : l.val < acc.fst.size
l_eq_i : l.val = i.val
pi : p i = false
pacc : hasAssignment true acc.fst[i.val] = false
hb : ¬b = true
⊢ hasAssignment true (addAssignment b acc.fst[i.val]) = false
Tactic:
. simp only [Bool.not_eq_true] at hb
  simp only [hasAssignment, addAssignment, hb, ite_false, ite_true, hasPos_of_addNeg]
  simp only [hasAssignment, ite_true] at pacc
  exact pacc
State after:
no goals

State before:
case neg
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
plb : p ⊨ (l, b)
i : PosFin n
i_in_bounds : i.val < acc.fst.size
l_in_bounds : l.val < acc.fst.size
l_eq_i : l.val = i.val
pi : p i = false
pacc : hasAssignment true acc.fst[i.val] = false
hb : ¬b = true
⊢ hasAssignment true (addAssignment b acc.fst[i.val]) = false
Tactic:
simp only [Bool.not_eq_true] at hb
State after:
case neg
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
plb : p ⊨ (l, b)
i : PosFin n
i_in_bounds : i.val < acc.fst.size
l_in_bounds : l.val < acc.fst.size
l_eq_i : l.val = i.val
pi : p i = false
pacc : hasAssignment true acc.fst[i.val] = false
hb : b = false
⊢ hasAssignment true (addAssignment b acc.fst[i.val]) = false

State before:
case neg
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
plb : p ⊨ (l, b)
i : PosFin n
i_in_bounds : i.val < acc.fst.size
l_in_bounds : l.val < acc.fst.size
l_eq_i : l.val = i.val
pi : p i = false
pacc : hasAssignment true acc.fst[i.val] = false
hb : b = false
⊢ hasAssignment true (addAssignment b acc.fst[i.val]) = false
Tactic:
simp only [hasAssignment, addAssignment, hb, ite_false, ite_true, hasPos_of_addNeg]
State after:
case neg
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
plb : p ⊨ (l, b)
i : PosFin n
i_in_bounds : i.val < acc.fst.size
l_in_bounds : l.val < acc.fst.size
l_eq_i : l.val = i.val
pi : p i = false
pacc : hasAssignment true acc.fst[i.val] = false
hb : b = false
⊢ acc.fst[i.val].hasPosAssignment = false

State before:
case neg
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
plb : p ⊨ (l, b)
i : PosFin n
i_in_bounds : i.val < acc.fst.size
l_in_bounds : l.val < acc.fst.size
l_eq_i : l.val = i.val
pi : p i = false
pacc : hasAssignment true acc.fst[i.val] = false
hb : b = false
⊢ acc.fst[i.val].hasPosAssignment = false
Tactic:
simp only [hasAssignment, ite_true] at pacc
State after:
case neg
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
plb : p ⊨ (l, b)
i : PosFin n
i_in_bounds : i.val < acc.fst.size
l_in_bounds : l.val < acc.fst.size
l_eq_i : l.val = i.val
pi : p i = false
hb : b = false
pacc : acc.fst[i.val].hasPosAssignment = false
⊢ acc.fst[i.val].hasPosAssignment = false

State before:
case neg
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
plb : p ⊨ (l, b)
i : PosFin n
i_in_bounds : i.val < acc.fst.size
l_in_bounds : l.val < acc.fst.size
l_eq_i : l.val = i.val
pi : p i = false
hb : b = false
pacc : acc.fst[i.val].hasPosAssignment = false
⊢ acc.fst[i.val].hasPosAssignment = false
Tactic:
exact pacc
State after:
no goals

State before:
case neg
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝¹ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
plb : p ⊨ (l, b)
i : PosFin n
pacc : hasAssignment (decide (p i = false)) acc.fst[i.val]! = false
i_in_bounds : i.val < acc.fst.size
l_in_bounds : l.val < acc.fst.size
h✝ : ¬l.val = i.val
⊢ hasAssignment (decide (p i = false)) (acc.fst.modify l.val (addAssignment b))[i.val]! = false
Tactic:
next l_ne_i =>
simp only [getElem!, Array.modify_preserves_size, i_in_bounds,
  Array.get_modify_unchanged l_in_bounds i_in_bounds _ l_ne_i, dite_true,
  Array.get_eq_getElem]
simp only [getElem!, i_in_bounds, dite_true] at pacc
exact pacc
State after:
no goals

State before:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
plb : p ⊨ (l, b)
i : PosFin n
pacc : hasAssignment (decide (p i = false)) acc.fst[i.val]! = false
i_in_bounds : i.val < acc.fst.size
l_in_bounds : l.val < acc.fst.size
l_ne_i : ¬l.val = i.val
⊢ hasAssignment (decide (p i = false)) (acc.fst.modify l.val (addAssignment b))[i.val]! = false
Tactic:
simp only [getElem!, Array.modify_preserves_size, i_in_bounds,
  Array.get_modify_unchanged l_in_bounds i_in_bounds _ l_ne_i, dite_true,
  Array.get_eq_getElem]
State after:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
plb : p ⊨ (l, b)
i : PosFin n
pacc : hasAssignment (decide (p i = false)) acc.fst[i.val]! = false
i_in_bounds : i.val < acc.fst.size
l_in_bounds : l.val < acc.fst.size
l_ne_i : ¬l.val = i.val
⊢ hasAssignment (decide (p i = false)) acc.fst[i.val] = false

State before:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
plb : p ⊨ (l, b)
i : PosFin n
pacc : hasAssignment (decide (p i = false)) acc.fst[i.val]! = false
i_in_bounds : i.val < acc.fst.size
l_in_bounds : l.val < acc.fst.size
l_ne_i : ¬l.val = i.val
⊢ hasAssignment (decide (p i = false)) acc.fst[i.val] = false
Tactic:
simp only [getElem!, i_in_bounds, dite_true] at pacc
State after:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
plb : p ⊨ (l, b)
i : PosFin n
i_in_bounds : i.val < acc.fst.size
l_in_bounds : l.val < acc.fst.size
l_ne_i : ¬l.val = i.val
pacc : hasAssignment (decide (p i = false)) (acc.fst.get ⟨i.val, ⋯⟩) = false
⊢ hasAssignment (decide (p i = false)) acc.fst[i.val] = false

State before:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
plb : p ⊨ (l, b)
i : PosFin n
i_in_bounds : i.val < acc.fst.size
l_in_bounds : l.val < acc.fst.size
l_ne_i : ¬l.val = i.val
pacc : hasAssignment (decide (p i = false)) (acc.fst.get ⟨i.val, ⋯⟩) = false
⊢ hasAssignment (decide (p i = false)) acc.fst[i.val] = false
Tactic:
exact pacc
State after:
no goals

State before:
case h_4
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
heq✝ : c.reduce acc.fst = reducedToNonunit
⊢ f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1) (acc.fst, acc.2.fst, false, true)
Tactic:
apply And.intro hsize ∘ And.intro h1
State after:
case h_4
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
heq✝ : c.reduce acc.fst = reducedToNonunit
⊢ (acc.fst, acc.2.fst, false, true).snd.snd.fst = true → incompatible (PosFin n) (acc.fst, acc.2.fst, false, true).fst f

State before:
case h_4
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
heq✝ : c.reduce acc.fst = reducedToNonunit
⊢ (acc.fst, acc.2.fst, false, true).snd.snd.fst = true → incompatible (PosFin n) (acc.fst, acc.2.fst, false, true).fst f
Tactic:
simp only [false_implies]
State after:
no goals

State before:
case h_2
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝ : Option (Option (DefaultClause n))
heq✝ : f.clauses[rupHints[↑idx]]? = some none
⊢ f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1) (acc.fst, acc.2.fst, false, true)
Tactic:
apply And.intro hsize ∘ And.intro h1
State after:
case h_2
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝ : Option (Option (DefaultClause n))
heq✝ : f.clauses[rupHints[↑idx]]? = some none
⊢ (acc.fst, acc.2.fst, false, true).snd.snd.fst = true → incompatible (PosFin n) (acc.fst, acc.2.fst, false, true).fst f

State before:
case h_2
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝ : Option (Option (DefaultClause n))
heq✝ : f.clauses[rupHints[↑idx]]? = some none
⊢ (acc.fst, acc.2.fst, false, true).snd.snd.fst = true → incompatible (PosFin n) (acc.fst, acc.2.fst, false, true).fst f
Tactic:
simp only [false_implies]
State after:
no goals

State before:
case h_3
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝ : Option (Option (DefaultClause n))
heq✝ : f.clauses[rupHints[↑idx]]? = none
⊢ f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1) (acc.fst, acc.2.fst, false, true)
Tactic:
apply And.intro hsize ∘ And.intro h1
State after:
case h_3
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝ : Option (Option (DefaultClause n))
heq✝ : f.clauses[rupHints[↑idx]]? = none
⊢ (acc.fst, acc.2.fst, false, true).snd.snd.fst = true → incompatible (PosFin n) (acc.fst, acc.2.fst, false, true).fst f

State before:
case h_3
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝ : Option (Option (DefaultClause n))
heq✝ : f.clauses[rupHints[↑idx]]? = none
⊢ (acc.fst, acc.2.fst, false, true).snd.snd.fst = true → incompatible (PosFin n) (acc.fst, acc.2.fst, false, true).fst f
Tactic:
simp only [false_implies]
State after:
no goals