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, true)
hsize : (f.assignments.modify l.val addPosAssignment).size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.assignments.modify l.val addPosAssignment)[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_eq_c : (i, b) = (l, true)
⊢ unit (i, b) = c
Tactic:
rw [isUnit_iff, DefaultClause.toList, ← ib_eq_c] at hc
Proof state after:
n : Nat
f : DefaultFormula n
c : DefaultClause n
f_readyForRupAdd : f.readyForRupAdd
x✝ : Option (Literal (PosFin n))
l : PosFin n
hsize : (f.assignments.modify l.val addPosAssignment).size = n
i : PosFin n
b : Bool
hc : c.clause = [(i, b)]
hb : hasAssignment b (f.assignments.modify l.val addPosAssignment)[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_eq_c : (i, b) = (l, true)
⊢ unit (i, b) = c
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
hsize : (f.assignments.modify l.val addPosAssignment).size = n
i : PosFin n
b : Bool
hc : c.clause = [(i, b)]
hb : hasAssignment b (f.assignments.modify l.val addPosAssignment)[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_eq_c : (i, b) = (l, true)
⊢ unit (i, b) = c
Tactic:
apply DefaultClause.ext
Proof state after:
case clause
n : Nat
f : DefaultFormula n
c : DefaultClause n
f_readyForRupAdd : f.readyForRupAdd
x✝ : Option (Literal (PosFin n))
l : PosFin n
hsize : (f.assignments.modify l.val addPosAssignment).size = n
i : PosFin n
b : Bool
hc : c.clause = [(i, b)]
hb : hasAssignment b (f.assignments.modify l.val addPosAssignment)[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_eq_c : (i, b) = (l, true)
⊢ (unit (i, b)).clause = c.clause
Theorem: LRAT.DefaultFormula.insert_readyForRupAdd
Proof state before:
case clause
n : Nat
f : DefaultFormula n
c : DefaultClause n
f_readyForRupAdd : f.readyForRupAdd
x✝ : Option (Literal (PosFin n))
l : PosFin n
hsize : (f.assignments.modify l.val addPosAssignment).size = n
i : PosFin n
b : Bool
hc : c.clause = [(i, b)]
hb : hasAssignment b (f.assignments.modify l.val addPosAssignment)[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_eq_c : (i, b) = (l, true)
⊢ (unit (i, b)).clause = c.clause
Tactic:
simp only [unit, hc]
Proof state after:
no goals
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, true)
hsize : (f.assignments.modify l.val addPosAssignment).size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.assignments.modify l.val addPosAssignment)[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
h✝ : ¬(i, b) = (l, true)
⊢ unit (i, b) ∈
    { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments.modify l.val addPosAssignment }.toList
Tactic:
next ib_ne_c =>
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 = false := by
      by_cases b = true
      . next b_eq_true =>
        simp only [b_eq_true, Subtype.ext l_eq_i, not_true] at ib_ne_c
      . next b_eq_false =>
        simp only [Bool.not_eq_true] at b_eq_false
        exact b_eq_false
    simp only [hasAssignment, b_eq_false, l_eq_i, Array.get_modify_at_idx i_in_bounds, ite_false, hasNeg_of_addPos] at hb
    simp only [hasAssignment, b_eq_false, ite_false, hb]
  . next l_ne_i =>
    simp only [Array.get_modify_unchanged l_in_bounds i_in_bounds _ l_ne_i] at hb
    exact hb
specialize hf hb'
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
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]
rcases hf with hf | hf
. exact Or.inl $ Or.inl hf
. 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, true)
hsize : (f.assignments.modify l.val addPosAssignment).size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.assignments.modify l.val addPosAssignment)[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, true)
⊢ unit (i, b) ∈
    { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments.modify l.val addPosAssignment }.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 = false := by
      by_cases b = true
      . next b_eq_true =>
        simp only [b_eq_true, Subtype.ext l_eq_i, not_true] at ib_ne_c
      . next b_eq_false =>
        simp only [Bool.not_eq_true] at b_eq_false
        exact b_eq_false
    simp only [hasAssignment, b_eq_false, l_eq_i, Array.get_modify_at_idx i_in_bounds, ite_false, hasNeg_of_addPos] at hb
    simp only [hasAssignment, b_eq_false, ite_false, 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, true)
hsize : (f.assignments.modify l.val addPosAssignment).size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.assignments.modify l.val addPosAssignment)[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, true)
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 addPosAssignment }.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, true)
hsize : (f.assignments.modify l.val addPosAssignment).size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.assignments.modify l.val addPosAssignment)[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, true)
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 addPosAssignment }.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, true)
hsize : (f.assignments.modify l.val addPosAssignment).size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.assignments.modify l.val addPosAssignment)[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, true)
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 addPosAssignment }.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, true)
hsize : (f.assignments.modify l.val addPosAssignment).size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.assignments.modify l.val addPosAssignment)[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, true)
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 addPosAssignment }.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, true)
hsize : (f.assignments.modify l.val addPosAssignment).size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.assignments.modify l.val addPosAssignment)[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, true)
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 addPosAssignment }.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, true)
hsize : (f.assignments.modify l.val addPosAssignment).size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.assignments.modify l.val addPosAssignment)[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, true)
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 addPosAssignment }.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, true)
hsize : (f.assignments.modify l.val addPosAssignment).size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.assignments.modify l.val addPosAssignment)[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, true)
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, true)
hsize : (f.assignments.modify l.val addPosAssignment).size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.assignments.modify l.val addPosAssignment)[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, true)
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, true)
hsize : (f.assignments.modify l.val addPosAssignment).size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.assignments.modify l.val addPosAssignment)[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, true)
⊢ 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, true)
hsize : (f.assignments.modify l.val addPosAssignment).size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.assignments.modify l.val addPosAssignment)[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, true)
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, true)
hsize : (f.assignments.modify l.val addPosAssignment).size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.assignments.modify l.val addPosAssignment)[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, true)
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, true)
hsize : (f.assignments.modify l.val addPosAssignment).size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.assignments.modify l.val addPosAssignment)[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, true)
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, true)
hsize : (f.assignments.modify l.val addPosAssignment).size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.assignments.modify l.val addPosAssignment)[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, true)
h✝ : ¬l.val = i.val
⊢ hasAssignment b f.assignments[i.val] = true
Tactic:
. next l_eq_i =>
  have b_eq_false : b = false := by
    by_cases b = true
    . next b_eq_true =>
      simp only [b_eq_true, Subtype.ext l_eq_i, not_true] at ib_ne_c
    . next b_eq_false =>
      simp only [Bool.not_eq_true] at b_eq_false
      exact b_eq_false
  simp only [hasAssignment, b_eq_false, l_eq_i, Array.get_modify_at_idx i_in_bounds, ite_false, hasNeg_of_addPos] at hb
  simp only [hasAssignment, b_eq_false, ite_false, 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, true)
hsize : (f.assignments.modify l.val addPosAssignment).size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.assignments.modify l.val addPosAssignment)[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, true)
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, true)
hsize : (f.assignments.modify l.val addPosAssignment).size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.assignments.modify l.val addPosAssignment)[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, true)
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, true)
hsize : (f.assignments.modify l.val addPosAssignment).size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.assignments.modify l.val addPosAssignment)[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, true)
h✝ : l.val = i.val
⊢ hasAssignment b f.assignments[i.val] = true
Tactic:
next l_eq_i =>
have b_eq_false : b = false := by
  by_cases b = true
  . next b_eq_true =>
    simp only [b_eq_true, Subtype.ext l_eq_i, not_true] at ib_ne_c
  . next b_eq_false =>
    simp only [Bool.not_eq_true] at b_eq_false
    exact b_eq_false
simp only [hasAssignment, b_eq_false, l_eq_i, Array.get_modify_at_idx i_in_bounds, ite_false, hasNeg_of_addPos] at hb
simp only [hasAssignment, b_eq_false, ite_false, 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, true)
hsize : (f.assignments.modify l.val addPosAssignment).size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.assignments.modify l.val addPosAssignment)[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, true)
l_eq_i : l.val = i.val
⊢ hasAssignment b f.assignments[i.val] = true
Tactic:
have b_eq_false : b = false := by
  by_cases b = true
  . next b_eq_true =>
    simp only [b_eq_true, Subtype.ext l_eq_i, not_true] at ib_ne_c
  . next b_eq_false =>
    simp only [Bool.not_eq_true] at b_eq_false
    exact b_eq_false
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, true)
hsize : (f.assignments.modify l.val addPosAssignment).size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.assignments.modify l.val addPosAssignment)[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, true)
l_eq_i : l.val = i.val
b_eq_false : b = false
⊢ 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, true)
hsize : (f.assignments.modify l.val addPosAssignment).size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.assignments.modify l.val addPosAssignment)[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, true)
l_eq_i : l.val = i.val
b_eq_false : b = false
⊢ 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_false, hasNeg_of_addPos] 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, true)
hsize : (f.assignments.modify l.val addPosAssignment).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, true)
l_eq_i : l.val = i.val
b_eq_false : b = false
hb : f.assignments[i.val].hasNegAssignment = 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, true)
hsize : (f.assignments.modify l.val addPosAssignment).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, true)
l_eq_i : l.val = i.val
b_eq_false : b = false
hb : f.assignments[i.val].hasNegAssignment = true
⊢ hasAssignment b f.assignments[i.val] = true
Tactic:
simp only [hasAssignment, b_eq_false, ite_false, hb]
Proof state after:
no goals