internlm/Lean-Github huggingface dataset:
Theorem: LRAT.DefaultFormula.insert_readyForRupAdd
Proof state before:
n : Nat
f : DefaultFormula n
c : DefaultClause n
f_readyForRupAdd : f.readyForRupAdd
x✝ : Option (Literal (PosFin n))
l : PosFin n
hc : c.isUnit = some (l, false)
hsize : (f.assignments.modify l.val addNegAssignment).size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.assignments.modify l.val addNegAssignment)[i.val] = true
hf : hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
i_in_bounds : i.val < f.assignments.size
l_in_bounds : l.val < f.assignments.size
ib_ne_c : ¬(i, b) = (l, false)
⊢ unit (i, b) ∈
    { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments.modify l.val addNegAssignment }.toList
Tactic:
have hb' : hasAssignment b (f.assignments[i.1]'i_in_bounds) := by
  by_cases l.1 = i.1
  . next l_eq_i =>
    have b_eq_false : b = true := by
      by_cases b = true
      . assumption
      . next b_eq_false =>
        simp only [b_eq_false, Subtype.ext l_eq_i, not_true] at ib_ne_c
    simp only [hasAssignment, b_eq_false, l_eq_i, Array.get_modify_at_idx i_in_bounds, ite_true, hasPos_of_addNeg] at hb
    simp only [hasAssignment, b_eq_false, ite_true, hb]
  . next l_ne_i =>
    simp only [Array.get_modify_unchanged l_in_bounds i_in_bounds _ l_ne_i] at hb
    exact hb
Proof state after:
n : Nat
f : DefaultFormula n
c : DefaultClause n
f_readyForRupAdd : f.readyForRupAdd
x✝ : Option (Literal (PosFin n))
l : PosFin n
hc : c.isUnit = some (l, false)
hsize : (f.assignments.modify l.val addNegAssignment).size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.assignments.modify l.val addNegAssignment)[i.val] = true
hf : hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
i_in_bounds : i.val < f.assignments.size
l_in_bounds : l.val < f.assignments.size
ib_ne_c : ¬(i, b) = (l, false)
hb' : hasAssignment b f.assignments[i.val] = true
⊢ unit (i, b) ∈
    { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments.modify l.val addNegAssignment }.toList
Theorem: LRAT.DefaultFormula.insert_readyForRupAdd
Proof state before:
n : Nat
f : DefaultFormula n
c : DefaultClause n
f_readyForRupAdd : f.readyForRupAdd
x✝ : Option (Literal (PosFin n))
l : PosFin n
hc : c.isUnit = some (l, false)
hsize : (f.assignments.modify l.val addNegAssignment).size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.assignments.modify l.val addNegAssignment)[i.val] = true
hf : hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
i_in_bounds : i.val < f.assignments.size
l_in_bounds : l.val < f.assignments.size
ib_ne_c : ¬(i, b) = (l, false)
hb' : hasAssignment b f.assignments[i.val] = true
⊢ unit (i, b) ∈
    { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments.modify l.val addNegAssignment }.toList
Tactic:
specialize hf hb'
Proof state after:
n : Nat
f : DefaultFormula n
c : DefaultClause n
f_readyForRupAdd : f.readyForRupAdd
x✝ : Option (Literal (PosFin n))
l : PosFin n
hc : c.isUnit = some (l, false)
hsize : (f.assignments.modify l.val addNegAssignment).size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.assignments.modify l.val addNegAssignment)[i.val] = true
i_in_bounds : i.val < f.assignments.size
l_in_bounds : l.val < f.assignments.size
ib_ne_c : ¬(i, b) = (l, false)
hb' : hasAssignment b f.assignments[i.val] = true
hf : unit (i, b) ∈ f.toList
⊢ unit (i, b) ∈
    { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments.modify l.val addNegAssignment }.toList
Theorem: LRAT.DefaultFormula.insert_readyForRupAdd
Proof state before:
n : Nat
f : DefaultFormula n
c : DefaultClause n
f_readyForRupAdd : f.readyForRupAdd
x✝ : Option (Literal (PosFin n))
l : PosFin n
hc : c.isUnit = some (l, false)
hsize : (f.assignments.modify l.val addNegAssignment).size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.assignments.modify l.val addNegAssignment)[i.val] = true
i_in_bounds : i.val < f.assignments.size
l_in_bounds : l.val < f.assignments.size
ib_ne_c : ¬(i, b) = (l, false)
hb' : hasAssignment b f.assignments[i.val] = true
hf : unit (i, b) ∈ f.toList
⊢ unit (i, b) ∈
    { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments.modify l.val addNegAssignment }.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] at hf
Proof state after:
n : Nat
f : DefaultFormula n
c : DefaultClause n
f_readyForRupAdd : f.readyForRupAdd
x✝ : Option (Literal (PosFin n))
l : PosFin n
hc : c.isUnit = some (l, false)
hsize : (f.assignments.modify l.val addNegAssignment).size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.assignments.modify l.val addNegAssignment)[i.val] = true
i_in_bounds : i.val < f.assignments.size
l_in_bounds : l.val < f.assignments.size
ib_ne_c : ¬(i, b) = (l, false)
hb' : hasAssignment b f.assignments[i.val] = true
hf :
  some (unit (i, b)) ∈ f.clauses.data ∨
    (∃ a,
        (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = unit (i, b)) ∨
      ∃ a,
        (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = unit (i, b)
⊢ unit (i, b) ∈
    { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments.modify l.val addNegAssignment }.toList
Theorem: LRAT.DefaultFormula.insert_readyForRupAdd
Proof state before:
n : Nat
f : DefaultFormula n
c : DefaultClause n
f_readyForRupAdd : f.readyForRupAdd
x✝ : Option (Literal (PosFin n))
l : PosFin n
hc : c.isUnit = some (l, false)
hsize : (f.assignments.modify l.val addNegAssignment).size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.assignments.modify l.val addNegAssignment)[i.val] = true
i_in_bounds : i.val < f.assignments.size
l_in_bounds : l.val < f.assignments.size
ib_ne_c : ¬(i, b) = (l, false)
hb' : hasAssignment b f.assignments[i.val] = true
hf :
  some (unit (i, b)) ∈ f.clauses.data ∨
    (∃ a,
        (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = unit (i, b)) ∨
      ∃ a,
        (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = unit (i, b)
⊢ unit (i, b) ∈
    { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments.modify l.val addNegAssignment }.toList
Tactic:
simp only [toList, Array.toList_eq, Array.push_data, List.append_assoc, List.mem_append, List.mem_filterMap,
  List.mem_singleton, id_eq, exists_eq_right, Option.some.injEq, List.mem_map, Prod.exists, Bool.exists_bool]
Proof state after:
n : Nat
f : DefaultFormula n
c : DefaultClause n
f_readyForRupAdd : f.readyForRupAdd
x✝ : Option (Literal (PosFin n))
l : PosFin n
hc : c.isUnit = some (l, false)
hsize : (f.assignments.modify l.val addNegAssignment).size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.assignments.modify l.val addNegAssignment)[i.val] = true
i_in_bounds : i.val < f.assignments.size
l_in_bounds : l.val < f.assignments.size
ib_ne_c : ¬(i, b) = (l, false)
hb' : hasAssignment b f.assignments[i.val] = true
hf :
  some (unit (i, b)) ∈ f.clauses.data ∨
    (∃ a,
        (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = unit (i, b)) ∨
      ∃ a,
        (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = unit (i, b)
⊢ (some (unit (i, b)) ∈ f.clauses.data ∨ unit (i, b) = c) ∨
    (∃ a,
        (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = unit (i, b)) ∨
      ∃ a,
        (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = unit (i, b)
Theorem: LRAT.DefaultFormula.insert_readyForRupAdd
Proof state before:
case inr
n : Nat
f : DefaultFormula n
c : DefaultClause n
f_readyForRupAdd : f.readyForRupAdd
x✝ : Option (Literal (PosFin n))
l : PosFin n
hc : c.isUnit = some (l, false)
hsize : (f.assignments.modify l.val addNegAssignment).size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.assignments.modify l.val addNegAssignment)[i.val] = true
i_in_bounds : i.val < f.assignments.size
l_in_bounds : l.val < f.assignments.size
ib_ne_c : ¬(i, b) = (l, false)
hb' : hasAssignment b f.assignments[i.val] = true
hf :
  (∃ a,
      (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = unit (i, b) ∨
        (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = unit (i, b)) ∨
    ∃ a,
      (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = unit (i, b) ∨
        (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = unit (i, b)
⊢ (some (unit (i, b)) ∈ f.clauses.data ∨ unit (i, b) = c) ∨
    (∃ a,
        (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = unit (i, b)) ∨
      ∃ a,
        (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = unit (i, b)
Tactic:
. exact Or.inr hf
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insert_readyForRupAdd
Proof state before:
n : Nat
f : DefaultFormula n
c : DefaultClause n
f_readyForRupAdd : f.readyForRupAdd
x✝ : Option (Literal (PosFin n))
l : PosFin n
hc : c.isUnit = some (l, false)
hsize : (f.assignments.modify l.val addNegAssignment).size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.assignments.modify l.val addNegAssignment)[i.val] = true
hf : hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
i_in_bounds : i.val < f.assignments.size
l_in_bounds : l.val < f.assignments.size
ib_ne_c : ¬(i, b) = (l, false)
⊢ hasAssignment b f.assignments[i.val] = true
Tactic:
by_cases l.1 = i.1
Proof state after:
case pos
n : Nat
f : DefaultFormula n
c : DefaultClause n
f_readyForRupAdd : f.readyForRupAdd
x✝ : Option (Literal (PosFin n))
l : PosFin n
hc : c.isUnit = some (l, false)
hsize : (f.assignments.modify l.val addNegAssignment).size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.assignments.modify l.val addNegAssignment)[i.val] = true
hf : hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
i_in_bounds : i.val < f.assignments.size
l_in_bounds : l.val < f.assignments.size
ib_ne_c : ¬(i, b) = (l, false)
h✝ : l.val = i.val
⊢ hasAssignment b f.assignments[i.val] = true

case neg
n : Nat
f : DefaultFormula n
c : DefaultClause n
f_readyForRupAdd : f.readyForRupAdd
x✝ : Option (Literal (PosFin n))
l : PosFin n
hc : c.isUnit = some (l, false)
hsize : (f.assignments.modify l.val addNegAssignment).size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.assignments.modify l.val addNegAssignment)[i.val] = true
hf : hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
i_in_bounds : i.val < f.assignments.size
l_in_bounds : l.val < f.assignments.size
ib_ne_c : ¬(i, b) = (l, false)
h✝ : ¬l.val = i.val
⊢ hasAssignment b f.assignments[i.val] = true
Theorem: LRAT.DefaultFormula.insert_readyForRupAdd
Proof state before:
case pos
n : Nat
f : DefaultFormula n
c : DefaultClause n
f_readyForRupAdd : f.readyForRupAdd
x✝ : Option (Literal (PosFin n))
l : PosFin n
hc : c.isUnit = some (l, false)
hsize : (f.assignments.modify l.val addNegAssignment).size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.assignments.modify l.val addNegAssignment)[i.val] = true
hf : hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
i_in_bounds : i.val < f.assignments.size
l_in_bounds : l.val < f.assignments.size
ib_ne_c : ¬(i, b) = (l, false)
h✝ : l.val = i.val
⊢ hasAssignment b f.assignments[i.val] = true

case neg
n : Nat
f : DefaultFormula n
c : DefaultClause n
f_readyForRupAdd : f.readyForRupAdd
x✝ : Option (Literal (PosFin n))
l : PosFin n
hc : c.isUnit = some (l, false)
hsize : (f.assignments.modify l.val addNegAssignment).size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.assignments.modify l.val addNegAssignment)[i.val] = true
hf : hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
i_in_bounds : i.val < f.assignments.size
l_in_bounds : l.val < f.assignments.size
ib_ne_c : ¬(i, b) = (l, false)
h✝ : ¬l.val = i.val
⊢ hasAssignment b f.assignments[i.val] = true
Tactic:
. next l_eq_i =>
  have b_eq_false : b = true := by
    by_cases b = true
    . assumption
    . next b_eq_false =>
      simp only [b_eq_false, Subtype.ext l_eq_i, not_true] at ib_ne_c
  simp only [hasAssignment, b_eq_false, l_eq_i, Array.get_modify_at_idx i_in_bounds, ite_true, hasPos_of_addNeg] at hb
  simp only [hasAssignment, b_eq_false, ite_true, hb]
Proof state after:
case neg
n : Nat
f : DefaultFormula n
c : DefaultClause n
f_readyForRupAdd : f.readyForRupAdd
x✝ : Option (Literal (PosFin n))
l : PosFin n
hc : c.isUnit = some (l, false)
hsize : (f.assignments.modify l.val addNegAssignment).size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.assignments.modify l.val addNegAssignment)[i.val] = true
hf : hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
i_in_bounds : i.val < f.assignments.size
l_in_bounds : l.val < f.assignments.size
ib_ne_c : ¬(i, b) = (l, false)
h✝ : ¬l.val = i.val
⊢ hasAssignment b f.assignments[i.val] = true
Theorem: LRAT.DefaultFormula.insert_readyForRupAdd
Proof state before:
case neg
n : Nat
f : DefaultFormula n
c : DefaultClause n
f_readyForRupAdd : f.readyForRupAdd
x✝ : Option (Literal (PosFin n))
l : PosFin n
hc : c.isUnit = some (l, false)
hsize : (f.assignments.modify l.val addNegAssignment).size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.assignments.modify l.val addNegAssignment)[i.val] = true
hf : hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
i_in_bounds : i.val < f.assignments.size
l_in_bounds : l.val < f.assignments.size
ib_ne_c : ¬(i, b) = (l, false)
h✝ : ¬l.val = i.val
⊢ hasAssignment b f.assignments[i.val] = true
Tactic:
. next l_ne_i =>
  simp only [Array.get_modify_unchanged l_in_bounds i_in_bounds _ l_ne_i] at hb
  exact hb
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insert_readyForRupAdd
Proof state before:
case pos
n : Nat
f : DefaultFormula n
c : DefaultClause n
f_readyForRupAdd : f.readyForRupAdd
x✝ : Option (Literal (PosFin n))
l : PosFin n
hc : c.isUnit = some (l, false)
hsize : (f.assignments.modify l.val addNegAssignment).size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.assignments.modify l.val addNegAssignment)[i.val] = true
hf : hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
i_in_bounds : i.val < f.assignments.size
l_in_bounds : l.val < f.assignments.size
ib_ne_c : ¬(i, b) = (l, false)
h✝ : l.val = i.val
⊢ hasAssignment b f.assignments[i.val] = true
Tactic:
next l_eq_i =>
have b_eq_false : b = true := by
  by_cases b = true
  . assumption
  . next b_eq_false =>
    simp only [b_eq_false, Subtype.ext l_eq_i, not_true] at ib_ne_c
simp only [hasAssignment, b_eq_false, l_eq_i, Array.get_modify_at_idx i_in_bounds, ite_true, hasPos_of_addNeg] at hb
simp only [hasAssignment, b_eq_false, ite_true, hb]
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insert_readyForRupAdd
Proof state before:
n : Nat
f : DefaultFormula n
c : DefaultClause n
f_readyForRupAdd : f.readyForRupAdd
x✝ : Option (Literal (PosFin n))
l : PosFin n
hc : c.isUnit = some (l, false)
hsize : (f.assignments.modify l.val addNegAssignment).size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.assignments.modify l.val addNegAssignment)[i.val] = true
hf : hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
i_in_bounds : i.val < f.assignments.size
l_in_bounds : l.val < f.assignments.size
ib_ne_c : ¬(i, b) = (l, false)
l_eq_i : l.val = i.val
⊢ hasAssignment b f.assignments[i.val] = true
Tactic:
have b_eq_false : b = true := by
  by_cases b = true
  . assumption
  . next b_eq_false =>
    simp only [b_eq_false, Subtype.ext l_eq_i, not_true] at ib_ne_c
Proof state after:
n : Nat
f : DefaultFormula n
c : DefaultClause n
f_readyForRupAdd : f.readyForRupAdd
x✝ : Option (Literal (PosFin n))
l : PosFin n
hc : c.isUnit = some (l, false)
hsize : (f.assignments.modify l.val addNegAssignment).size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.assignments.modify l.val addNegAssignment)[i.val] = true
hf : hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
i_in_bounds : i.val < f.assignments.size
l_in_bounds : l.val < f.assignments.size
ib_ne_c : ¬(i, b) = (l, false)
l_eq_i : l.val = i.val
b_eq_false : b = true
⊢ hasAssignment b f.assignments[i.val] = true
Theorem: LRAT.DefaultFormula.insert_readyForRupAdd
Proof state before:
n : Nat
f : DefaultFormula n
c : DefaultClause n
f_readyForRupAdd : f.readyForRupAdd
x✝ : Option (Literal (PosFin n))
l : PosFin n
hc : c.isUnit = some (l, false)
hsize : (f.assignments.modify l.val addNegAssignment).size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.assignments.modify l.val addNegAssignment)[i.val] = true
hf : hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
i_in_bounds : i.val < f.assignments.size
l_in_bounds : l.val < f.assignments.size
ib_ne_c : ¬(i, b) = (l, false)
l_eq_i : l.val = i.val
b_eq_false : b = true
⊢ hasAssignment b f.assignments[i.val] = true
Tactic:
simp only [hasAssignment, b_eq_false, l_eq_i, Array.get_modify_at_idx i_in_bounds, ite_true, hasPos_of_addNeg] at hb
Proof state after:
n : Nat
f : DefaultFormula n
c : DefaultClause n
f_readyForRupAdd : f.readyForRupAdd
x✝ : Option (Literal (PosFin n))
l : PosFin n
hc : c.isUnit = some (l, false)
hsize : (f.assignments.modify l.val addNegAssignment).size = n
i : PosFin n
b : Bool
hf : hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
i_in_bounds : i.val < f.assignments.size
l_in_bounds : l.val < f.assignments.size
ib_ne_c : ¬(i, b) = (l, false)
l_eq_i : l.val = i.val
b_eq_false : b = true
hb : f.assignments[i.val].hasPosAssignment = true
⊢ hasAssignment b f.assignments[i.val] = true
Theorem: LRAT.DefaultFormula.insert_readyForRupAdd
Proof state before:
n : Nat
f : DefaultFormula n
c : DefaultClause n
f_readyForRupAdd : f.readyForRupAdd
x✝ : Option (Literal (PosFin n))
l : PosFin n
hc : c.isUnit = some (l, false)
hsize : (f.assignments.modify l.val addNegAssignment).size = n
i : PosFin n
b : Bool
hf : hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
i_in_bounds : i.val < f.assignments.size
l_in_bounds : l.val < f.assignments.size
ib_ne_c : ¬(i, b) = (l, false)
l_eq_i : l.val = i.val
b_eq_false : b = true
hb : f.assignments[i.val].hasPosAssignment = true
⊢ hasAssignment b f.assignments[i.val] = true
Tactic:
simp only [hasAssignment, b_eq_false, ite_true, hb]
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insert_readyForRupAdd
Proof state before:
n : Nat
f : DefaultFormula n
c : DefaultClause n
f_readyForRupAdd : f.readyForRupAdd
x✝ : Option (Literal (PosFin n))
l : PosFin n
hc : c.isUnit = some (l, false)
hsize : (f.assignments.modify l.val addNegAssignment).size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.assignments.modify l.val addNegAssignment)[i.val] = true
hf : hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
i_in_bounds : i.val < f.assignments.size
l_in_bounds : l.val < f.assignments.size
ib_ne_c : ¬(i, b) = (l, false)
l_eq_i : l.val = i.val
⊢ b = true
Tactic:
by_cases b = true
Proof state after:
case pos
n : Nat
f : DefaultFormula n
c : DefaultClause n
f_readyForRupAdd : f.readyForRupAdd
x✝ : Option (Literal (PosFin n))
l : PosFin n
hc : c.isUnit = some (l, false)
hsize : (f.assignments.modify l.val addNegAssignment).size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.assignments.modify l.val addNegAssignment)[i.val] = true
hf : hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
i_in_bounds : i.val < f.assignments.size
l_in_bounds : l.val < f.assignments.size
ib_ne_c : ¬(i, b) = (l, false)
l_eq_i : l.val = i.val
h✝ : b = true
⊢ b = true

case neg
n : Nat
f : DefaultFormula n
c : DefaultClause n
f_readyForRupAdd : f.readyForRupAdd
x✝ : Option (Literal (PosFin n))
l : PosFin n
hc : c.isUnit = some (l, false)
hsize : (f.assignments.modify l.val addNegAssignment).size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.assignments.modify l.val addNegAssignment)[i.val] = true
hf : hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
i_in_bounds : i.val < f.assignments.size
l_in_bounds : l.val < f.assignments.size
ib_ne_c : ¬(i, b) = (l, false)
l_eq_i : l.val = i.val
h✝ : ¬b = true
⊢ b = true
Theorem: LRAT.DefaultFormula.insert_readyForRupAdd
Proof state before:
case pos
n : Nat
f : DefaultFormula n
c : DefaultClause n
f_readyForRupAdd : f.readyForRupAdd
x✝ : Option (Literal (PosFin n))
l : PosFin n
hc : c.isUnit = some (l, false)
hsize : (f.assignments.modify l.val addNegAssignment).size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.assignments.modify l.val addNegAssignment)[i.val] = true
hf : hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
i_in_bounds : i.val < f.assignments.size
l_in_bounds : l.val < f.assignments.size
ib_ne_c : ¬(i, b) = (l, false)
l_eq_i : l.val = i.val
h✝ : b = true
⊢ b = true

case neg
n : Nat
f : DefaultFormula n
c : DefaultClause n
f_readyForRupAdd : f.readyForRupAdd
x✝ : Option (Literal (PosFin n))
l : PosFin n
hc : c.isUnit = some (l, false)
hsize : (f.assignments.modify l.val addNegAssignment).size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.assignments.modify l.val addNegAssignment)[i.val] = true
hf : hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
i_in_bounds : i.val < f.assignments.size
l_in_bounds : l.val < f.assignments.size
ib_ne_c : ¬(i, b) = (l, false)
l_eq_i : l.val = i.val
h✝ : ¬b = true
⊢ b = true
Tactic:
. assumption
Proof state after:
case neg
n : Nat
f : DefaultFormula n
c : DefaultClause n
f_readyForRupAdd : f.readyForRupAdd
x✝ : Option (Literal (PosFin n))
l : PosFin n
hc : c.isUnit = some (l, false)
hsize : (f.assignments.modify l.val addNegAssignment).size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.assignments.modify l.val addNegAssignment)[i.val] = true
hf : hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
i_in_bounds : i.val < f.assignments.size
l_in_bounds : l.val < f.assignments.size
ib_ne_c : ¬(i, b) = (l, false)
l_eq_i : l.val = i.val
h✝ : ¬b = true
⊢ b = true
Theorem: LRAT.DefaultFormula.insert_readyForRupAdd
Proof state before:
case neg
n : Nat
f : DefaultFormula n
c : DefaultClause n
f_readyForRupAdd : f.readyForRupAdd
x✝ : Option (Literal (PosFin n))
l : PosFin n
hc : c.isUnit = some (l, false)
hsize : (f.assignments.modify l.val addNegAssignment).size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.assignments.modify l.val addNegAssignment)[i.val] = true
hf : hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
i_in_bounds : i.val < f.assignments.size
l_in_bounds : l.val < f.assignments.size
ib_ne_c : ¬(i, b) = (l, false)
l_eq_i : l.val = i.val
h✝ : ¬b = true
⊢ b = true
Tactic:
. next b_eq_false =>
  simp only [b_eq_false, Subtype.ext l_eq_i, not_true] at ib_ne_c
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insert_readyForRupAdd
Proof state before:
case pos
n : Nat
f : DefaultFormula n
c : DefaultClause n
f_readyForRupAdd : f.readyForRupAdd
x✝ : Option (Literal (PosFin n))
l : PosFin n
hc : c.isUnit = some (l, false)
hsize : (f.assignments.modify l.val addNegAssignment).size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.assignments.modify l.val addNegAssignment)[i.val] = true
hf : hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
i_in_bounds : i.val < f.assignments.size
l_in_bounds : l.val < f.assignments.size
ib_ne_c : ¬(i, b) = (l, false)
l_eq_i : l.val = i.val
h✝ : b = true
⊢ b = true
Tactic:
assumption
Proof state after:
no goals