internlm/Lean-Github huggingface dataset:
Theorem: LRAT.DefaultFormula.performRupCheck_preserves_assignments_invariant
Proof state before:
case intro.intro
n : Nat
f : DefaultFormula n
f_assignments_invariant : f.assignments_invariant
rupHints : Array Nat
motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  f.confirmRupHint_fold_entails_hsat_motive
h_base : motive 0 (f.assignments, [], false, false)
h_inductive :
  ∀ (idx : Fin rupHints.size) (acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool),
    motive (↑idx) acc →
      f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1) (confirmRupHint f.clauses acc rupHints[idx])
hsize : (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).fst.size = n
right✝ :
  (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).snd.snd.fst = true →
    incompatible (PosFin n)
      (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).fst f
i : PosFin n
b : Bool
h :
  hasAssignment b (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints 0).fst[i.val] =
    true
p : PosFin n → Bool
pf :
  p ⊨
    { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
      assignments := (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints 0).fst }
h1 :
  ∀ (i : PosFin n),
    hasAssignment (decide (p i = false))
        (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).fst[i.val]! =
      false
⊢ p ⊨ (i, b)
Tactic:
specialize h1 i
Proof state after:
case intro.intro
n : Nat
f : DefaultFormula n
f_assignments_invariant : f.assignments_invariant
rupHints : Array Nat
motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  f.confirmRupHint_fold_entails_hsat_motive
h_base : motive 0 (f.assignments, [], false, false)
h_inductive :
  ∀ (idx : Fin rupHints.size) (acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool),
    motive (↑idx) acc →
      f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1) (confirmRupHint f.clauses acc rupHints[idx])
hsize : (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).fst.size = n
right✝ :
  (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).snd.snd.fst = true →
    incompatible (PosFin n)
      (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).fst f
i : PosFin n
b : Bool
h :
  hasAssignment b (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints 0).fst[i.val] =
    true
p : PosFin n → Bool
pf :
  p ⊨
    { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
      assignments := (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints 0).fst }
h1 :
  hasAssignment (decide (p i = false))
      (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).fst[i.val]! =
    false
⊢ p ⊨ (i, b)
Theorem: LRAT.DefaultFormula.performRupCheck_preserves_assignments_invariant
Proof state before:
case neg
n : Nat
f : DefaultFormula n
f_assignments_invariant : f.assignments_invariant
rupHints : Array Nat
motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  f.confirmRupHint_fold_entails_hsat_motive
h_base : motive 0 (f.assignments, [], false, false)
h_inductive :
  ∀ (idx : Fin rupHints.size) (acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool),
    motive (↑idx) acc →
      f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1) (confirmRupHint f.clauses acc rupHints[idx])
hsize : (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).fst.size = n
right✝ :
  (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).snd.snd.fst = true →
    incompatible (PosFin n)
      (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).fst f
i : PosFin n
b : Bool
h :
  hasAssignment b (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints 0).fst[i.val] =
    true
p : PosFin n → Bool
pf :
  p ⊨
    { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
      assignments := (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints 0).fst }
i_in_bounds :
  i.val < (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).fst.size
h1 :
  hasAssignment (decide (p i = false))
      (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).fst[i.val] =
    false
hb : ¬b = true
⊢ p i = b
Tactic:
. simp only [Bool.not_eq_true] at hb
  rw [hb]
  rw [hb] at h
  by_cases pi : p i
  . simp only [pi, decide_False, h] at h1
  . simp only [Bool.not_eq_true] at pi
    exact pi
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.performRupCheck_preserves_assignments_invariant
Proof state before:
n : Nat
f : DefaultFormula n
f_assignments_invariant : f.assignments_invariant
rupHints : Array Nat
motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  f.confirmRupHint_fold_entails_hsat_motive
⊢ motive 0 (f.assignments, [], false, false)
Tactic:
simp only [confirmRupHint_fold_entails_hsat_motive, f_assignments_invariant.1, false_implies, and_true, true_and,
  assignments_invariant_entails_limplies f f_assignments_invariant, motive]
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.performRupCheck_preserves_assignments_invariant
Proof state before:
n : Nat
f : DefaultFormula n
f_assignments_invariant : f.assignments_invariant
rupHints : Array Nat
motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  f.confirmRupHint_fold_entails_hsat_motive
h_base : motive 0 (f.assignments, [], false, false)
h_inductive :
  ∀ (idx : Fin rupHints.size) (acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool),
    motive (↑idx) acc →
      f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1) (confirmRupHint f.clauses acc rupHints[idx])
hsize : (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).fst.size = n
right✝ :
  (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).snd.snd.fst = true →
    incompatible (PosFin n)
      (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).fst f
i : PosFin n
b : Bool
h :
  hasAssignment b (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints 0).fst[i.val] =
    true
p : PosFin n → Bool
pf :
  p ⊨
    { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
      assignments := (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints 0).fst }
h1 :
  hasAssignment (decide (p i = false))
      (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).fst[i.val]! =
    false
in_bounds_motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  fun _idx acc => acc.fst.size = n
in_bounds_base : in_bounds_motive 0 (f.assignments, [], false, false)
in_bounds_inductive :
  ∀ (idx : Fin rupHints.size) (acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool),
    in_bounds_motive (↑idx) acc → in_bounds_motive (↑idx + 1) (confirmRupHint f.clauses acc rupHints[idx])
⊢ i.val < n
Tactic:
exact i.2.2
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.performRupCheck_preserves_assignments_invariant
Proof state before:
n : Nat
f : DefaultFormula n
f_assignments_invariant : f.assignments_invariant
rupHints : Array Nat
motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  f.confirmRupHint_fold_entails_hsat_motive
h_base : motive 0 (f.assignments, [], false, false)
h_inductive :
  ∀ (idx : Fin rupHints.size) (acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool),
    motive (↑idx) acc →
      f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1) (confirmRupHint f.clauses acc rupHints[idx])
hsize : (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).fst.size = n
right✝ :
  (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).snd.snd.fst = true →
    incompatible (PosFin n)
      (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).fst f
i : PosFin n
b : Bool
h :
  hasAssignment b (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints 0).fst[i.val] =
    true
p : PosFin n → Bool
pf :
  p ⊨
    { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
      assignments := (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints 0).fst }
h1 :
  hasAssignment (decide (p i = false))
      (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).fst[i.val]! =
    false
in_bounds_motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  fun _idx acc => acc.fst.size = n
⊢ in_bounds_motive 0 (f.assignments, [], false, false)
Tactic:
simp only [f_assignments_invariant.1, in_bounds_motive]
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.performRupCheck_preserves_assignments_invariant
Proof state before:
n : Nat
f : DefaultFormula n
f_assignments_invariant : f.assignments_invariant
rupHints : Array Nat
motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  f.confirmRupHint_fold_entails_hsat_motive
h_base : motive 0 (f.assignments, [], false, false)
hsize : (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).fst.size = n
right✝ :
  (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).snd.snd.fst = true →
    incompatible (PosFin n)
      (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).fst f
i : PosFin n
b : Bool
h✝ :
  hasAssignment b (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints 0).fst[i.val] =
    true
p : PosFin n → Bool
pf :
  p ⊨
    { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
      assignments := (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints 0).fst }
in_bounds_motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  fun _idx acc => acc.fst.size = n
in_bounds_base : in_bounds_motive 0 (f.assignments, [], false, false)
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
ih : in_bounds_motive (↑idx) acc
h_inductive :
  ∀ (idx : Fin rupHints.size) (a : Array Assignment) (a_1 : List (Literal (PosFin n))) (a_2 b : Bool),
    motive ↑idx (a, a_1, a_2, b) →
      f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1) (confirmRupHint f.clauses (a, a_1, a_2, b) rupHints[↑idx])
h1 :
  hasAssignment (!p i)
      (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).fst[i.val]! =
    false
h : (confirmRupHint f.clauses acc rupHints[↑idx]).fst.size = acc.fst.size
⊢ in_bounds_motive (↑idx + 1) (confirmRupHint f.clauses acc rupHints[↑idx])
Tactic:
omega
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.performRupCheck_preserves_assignments_invariant
Proof state before:
case neg
n : Nat
f : DefaultFormula n
f_assignments_invariant : f.assignments_invariant
rupHints : Array Nat
motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  f.confirmRupHint_fold_entails_hsat_motive
h_base : motive 0 (f.assignments, [], false, false)
h_inductive :
  ∀ (idx : Fin rupHints.size) (acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool),
    motive (↑idx) acc →
      f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1) (confirmRupHint f.clauses acc rupHints[idx])
hsize : (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).fst.size = n
right✝ :
  (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).snd.snd.fst = true →
    incompatible (PosFin n)
      (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).fst f
i : PosFin n
b : Bool
h :
  hasAssignment true (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints 0).fst[i.val] =
    true
p : PosFin n → Bool
pf :
  p ⊨
    { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
      assignments := (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints 0).fst }
i_in_bounds :
  i.val < (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).fst.size
h1 :
  hasAssignment (decide (p i = false))
      (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).fst[i.val] =
    false
hb : b = true
pi : ¬p i = true
⊢ p i = true
Tactic:
. simp only [Bool.not_eq_true] at pi
  simp only [pi, decide_True, h] at h1
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.performRupCheck_preserves_assignments_invariant
Proof state before:
case pos
n : Nat
f : DefaultFormula n
f_assignments_invariant : f.assignments_invariant
rupHints : Array Nat
motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  f.confirmRupHint_fold_entails_hsat_motive
h_base : motive 0 (f.assignments, [], false, false)
h_inductive :
  ∀ (idx : Fin rupHints.size) (acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool),
    motive (↑idx) acc →
      f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1) (confirmRupHint f.clauses acc rupHints[idx])
hsize : (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).fst.size = n
right✝ :
  (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).snd.snd.fst = true →
    incompatible (PosFin n)
      (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).fst f
i : PosFin n
b : Bool
h :
  hasAssignment true (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints 0).fst[i.val] =
    true
p : PosFin n → Bool
pf :
  p ⊨
    { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
      assignments := (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints 0).fst }
i_in_bounds :
  i.val < (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).fst.size
h1 :
  hasAssignment (decide (p i = false))
      (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).fst[i.val] =
    false
hb : b = true
pi : p i = true
⊢ p i = true
Tactic:
exact pi
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.performRupCheck_preserves_assignments_invariant
Proof state before:
case neg
n : Nat
f : DefaultFormula n
f_assignments_invariant : f.assignments_invariant
rupHints : Array Nat
motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  f.confirmRupHint_fold_entails_hsat_motive
h_base : motive 0 (f.assignments, [], false, false)
h_inductive :
  ∀ (idx : Fin rupHints.size) (acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool),
    motive (↑idx) acc →
      f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1) (confirmRupHint f.clauses acc rupHints[idx])
hsize : (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).fst.size = n
right✝ :
  (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).snd.snd.fst = true →
    incompatible (PosFin n)
      (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).fst f
i : PosFin n
b : Bool
h :
  hasAssignment true (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints 0).fst[i.val] =
    true
p : PosFin n → Bool
pf :
  p ⊨
    { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
      assignments := (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints 0).fst }
i_in_bounds :
  i.val < (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).fst.size
h1 :
  hasAssignment (decide (p i = false))
      (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).fst[i.val] =
    false
hb : b = true
pi : p i = false
⊢ p i = true
Tactic:
simp only [pi, decide_True, h] at h1
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.performRupCheck_preserves_assignments_invariant
Proof state before:
case neg
n : Nat
f : DefaultFormula n
f_assignments_invariant : f.assignments_invariant
rupHints : Array Nat
motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  f.confirmRupHint_fold_entails_hsat_motive
h_base : motive 0 (f.assignments, [], false, false)
h_inductive :
  ∀ (idx : Fin rupHints.size) (acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool),
    motive (↑idx) acc →
      f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1) (confirmRupHint f.clauses acc rupHints[idx])
hsize : (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).fst.size = n
right✝ :
  (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).snd.snd.fst = true →
    incompatible (PosFin n)
      (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).fst f
i : PosFin n
b : Bool
h :
  hasAssignment false (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints 0).fst[i.val] =
    true
p : PosFin n → Bool
pf :
  p ⊨
    { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
      assignments := (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints 0).fst }
i_in_bounds :
  i.val < (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).fst.size
h1 :
  hasAssignment (decide (p i = false))
      (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).fst[i.val] =
    false
hb : b = false
pi : ¬p i = true
⊢ p i = false
Tactic:
. simp only [Bool.not_eq_true] at pi
  exact pi
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.performRupCheck_preserves_assignments_invariant
Proof state before:
case pos
n : Nat
f : DefaultFormula n
f_assignments_invariant : f.assignments_invariant
rupHints : Array Nat
motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  f.confirmRupHint_fold_entails_hsat_motive
h_base : motive 0 (f.assignments, [], false, false)
h_inductive :
  ∀ (idx : Fin rupHints.size) (acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool),
    motive (↑idx) acc →
      f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1) (confirmRupHint f.clauses acc rupHints[idx])
hsize : (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).fst.size = n
right✝ :
  (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).snd.snd.fst = true →
    incompatible (PosFin n)
      (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).fst f
i : PosFin n
b : Bool
h :
  hasAssignment false (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints 0).fst[i.val] =
    true
p : PosFin n → Bool
pf :
  p ⊨
    { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
      assignments := (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints 0).fst }
i_in_bounds :
  i.val < (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).fst.size
h1 :
  hasAssignment (decide (p i = false))
      (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).fst[i.val] =
    false
hb : b = false
pi : p i = true
⊢ p i = false
Tactic:
simp only [pi, decide_False, h] at h1
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.performRupCheck_preserves_assignments_invariant
Proof state before:
case neg
n : Nat
f : DefaultFormula n
f_assignments_invariant : f.assignments_invariant
rupHints : Array Nat
motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  f.confirmRupHint_fold_entails_hsat_motive
h_base : motive 0 (f.assignments, [], false, false)
h_inductive :
  ∀ (idx : Fin rupHints.size) (acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool),
    motive (↑idx) acc →
      f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1) (confirmRupHint f.clauses acc rupHints[idx])
hsize : (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).fst.size = n
right✝ :
  (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).snd.snd.fst = true →
    incompatible (PosFin n)
      (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).fst f
i : PosFin n
b : Bool
h :
  hasAssignment false (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints 0).fst[i.val] =
    true
p : PosFin n → Bool
pf :
  p ⊨
    { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
      assignments := (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints 0).fst }
i_in_bounds :
  i.val < (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).fst.size
h1 :
  hasAssignment (decide (p i = false))
      (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).fst[i.val] =
    false
hb : b = false
pi : p i = false
⊢ p i = false
Tactic:
exact pi
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.performRatCheck_success_entails_c_without_negPivot
Proof state before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
negPivot : Literal (PosFin n)
ratHint : Nat × Array Nat
performRatCheck_success : (f.performRatCheck negPivot ratHint).snd = true
c : DefaultClause n
⊢ f.clauses[ratHint.fst]! = some c → limplies (PosFin n) f (c.delete negPivot)
Tactic:
intro hc p pf
Proof state after:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
negPivot : Literal (PosFin n)
ratHint : Nat × Array Nat
performRatCheck_success : (f.performRatCheck negPivot ratHint).snd = true
c : DefaultClause n
hc : f.clauses[ratHint.fst]! = some c
p : PosFin n → Bool
pf : p ⊨ f
⊢ p ⊨ c.delete negPivot
Theorem: LRAT.DefaultFormula.performRatCheck_success_entails_c_without_negPivot
Proof state before:
case isTrue
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
negPivot : Literal (PosFin n)
ratHint : Nat × Array Nat
c : DefaultClause n
hc : f.clauses[ratHint.fst]! = some c
p : PosFin n → Bool
pf : p ⊨ f
h✝ :
  ({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }.insertRatUnits
        (c.delete negPivot).negate).snd =
    true
performRatCheck_success :
  (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                  assignments := f.assignments }.insertRatUnits
              (c.delete negPivot).negate).fst.clearRatUnits,
        true).snd =
    true
⊢ p ⊨ c.delete negPivot
Tactic:
next h =>
exact insertRat_entails_hsat f hf (DefaultClause.delete c negPivot) p pf h
Proof state after:
no goals