internlm/Lean-Github huggingface dataset:
Theorem: LRAT.DefaultFormula.deleteOne_preserves_strong_assignments_invariant
Proof state before:
case neg.h_3.inl.h.isTrue.intro
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
hl :
  ∀ (x : PosFin n),
    ¬c = { clause := [(x, false)], nodupkey := ⋯, nodup := ⋯ } ∧
      ¬c = { clause := [(x, true)], nodupkey := ⋯, nodup := ⋯ }
x✝¹ : Option (DefaultClause n)
val✝ : DefaultClause n
x✝ :
  ∀ (l : Literal (PosFin n)) (nodupkey : ∀ (l_1 : PosFin n), ¬(l_1, true) ∈ [l] ∨ ¬(l_1, false) ∈ [l])
    (nodup : [l].Nodup), val✝ = { clause := [l], nodupkey := nodupkey, nodup := nodup } → False
heq✝ : some c = some val✝
deleteOne_f_rw :
  f.deleteOne id =
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
⊢ some (unit (i, b)) ∈ (f.clauses.set ⟨id, h✝⟩ none).data
Tactic:
simp only [← hidx, Array.data_set]
Proof state after:
case neg.h_3.inl.h.isTrue.intro
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
hl :
  ∀ (x : PosFin n),
    ¬c = { clause := [(x, false)], nodupkey := ⋯, nodup := ⋯ } ∧
      ¬c = { clause := [(x, true)], nodupkey := ⋯, nodup := ⋯ }
x✝¹ : Option (DefaultClause n)
val✝ : DefaultClause n
x✝ :
  ∀ (l : Literal (PosFin n)) (nodupkey : ∀ (l_1 : PosFin n), ¬(l_1, true) ∈ [l] ∨ ¬(l_1, false) ∈ [l])
    (nodup : [l].Nodup), val✝ = { clause := [l], nodupkey := nodupkey, nodup := nodup } → False
heq✝ : some c = some val✝
deleteOne_f_rw :
  f.deleteOne id =
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
⊢ f.clauses.data.get idx ∈ f.clauses.data.set id none
Theorem: LRAT.DefaultFormula.deleteOne_preserves_strong_assignments_invariant
Proof state before:
case neg.h_3.inl.h.isTrue.intro
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
hl :
  ∀ (x : PosFin n),
    ¬c = { clause := [(x, false)], nodupkey := ⋯, nodup := ⋯ } ∧
      ¬c = { clause := [(x, true)], nodupkey := ⋯, nodup := ⋯ }
x✝¹ : Option (DefaultClause n)
val✝ : DefaultClause n
x✝ :
  ∀ (l : Literal (PosFin n)) (nodupkey : ∀ (l_1 : PosFin n), ¬(l_1, true) ∈ [l] ∨ ¬(l_1, false) ∈ [l])
    (nodup : [l].Nodup), val✝ = { clause := [l], nodupkey := nodupkey, nodup := nodup } → False
heq✝ : some c = some val✝
deleteOne_f_rw :
  f.deleteOne id =
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
⊢ f.clauses.data.get idx ∈ f.clauses.data.set id none
Tactic:
rw [List.mem_iff_get]
Proof state after:
case neg.h_3.inl.h.isTrue.intro
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
hl :
  ∀ (x : PosFin n),
    ¬c = { clause := [(x, false)], nodupkey := ⋯, nodup := ⋯ } ∧
      ¬c = { clause := [(x, true)], nodupkey := ⋯, nodup := ⋯ }
x✝¹ : Option (DefaultClause n)
val✝ : DefaultClause n
x✝ :
  ∀ (l : Literal (PosFin n)) (nodupkey : ∀ (l_1 : PosFin n), ¬(l_1, true) ∈ [l] ∨ ¬(l_1, false) ∈ [l])
    (nodup : [l].Nodup), val✝ = { clause := [l], nodupkey := nodupkey, nodup := nodup } → False
heq✝ : some c = some val✝
deleteOne_f_rw :
  f.deleteOne id =
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
⊢ ∃ n_1, (f.clauses.data.set id none).get n_1 = f.clauses.data.get idx
Theorem: LRAT.DefaultFormula.deleteOne_preserves_strong_assignments_invariant
Proof state before:
case neg.h_3.inl.h.isTrue.intro
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
hl :
  ∀ (x : PosFin n),
    ¬c = { clause := [(x, false)], nodupkey := ⋯, nodup := ⋯ } ∧
      ¬c = { clause := [(x, true)], nodupkey := ⋯, nodup := ⋯ }
x✝¹ : Option (DefaultClause n)
val✝ : DefaultClause n
x✝ :
  ∀ (l : Literal (PosFin n)) (nodupkey : ∀ (l_1 : PosFin n), ¬(l_1, true) ∈ [l] ∨ ¬(l_1, false) ∈ [l])
    (nodup : [l].Nodup), val✝ = { clause := [l], nodupkey := nodupkey, nodup := nodup } → False
heq✝ : some c = some val✝
deleteOne_f_rw :
  f.deleteOne id =
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
⊢ ∃ n_1, (f.clauses.data.set id none).get n_1 = f.clauses.data.get idx
Tactic:
have idx_in_bounds : idx.1 < List.length (List.set f.clauses.data id none) := by
  simp only [List.length_set]
  exact idx.2
Proof state after:
case neg.h_3.inl.h.isTrue.intro
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
hl :
  ∀ (x : PosFin n),
    ¬c = { clause := [(x, false)], nodupkey := ⋯, nodup := ⋯ } ∧
      ¬c = { clause := [(x, true)], nodupkey := ⋯, nodup := ⋯ }
x✝¹ : Option (DefaultClause n)
val✝ : DefaultClause n
x✝ :
  ∀ (l : Literal (PosFin n)) (nodupkey : ∀ (l_1 : PosFin n), ¬(l_1, true) ∈ [l] ∨ ¬(l_1, false) ∈ [l])
    (nodup : [l].Nodup), val✝ = { clause := [l], nodupkey := nodupkey, nodup := nodup } → False
heq✝ : some c = some val✝
deleteOne_f_rw :
  f.deleteOne id =
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
⊢ ∃ n_1, (f.clauses.data.set id none).get n_1 = f.clauses.data.get idx
Theorem: LRAT.DefaultFormula.deleteOne_preserves_strong_assignments_invariant
Proof state before:
case neg.h_3.inl.h.isTrue.intro
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
hl :
  ∀ (x : PosFin n),
    ¬c = { clause := [(x, false)], nodupkey := ⋯, nodup := ⋯ } ∧
      ¬c = { clause := [(x, true)], nodupkey := ⋯, nodup := ⋯ }
x✝¹ : Option (DefaultClause n)
val✝ : DefaultClause n
x✝ :
  ∀ (l : Literal (PosFin n)) (nodupkey : ∀ (l_1 : PosFin n), ¬(l_1, true) ∈ [l] ∨ ¬(l_1, false) ∈ [l])
    (nodup : [l].Nodup), val✝ = { clause := [l], nodupkey := nodupkey, nodup := nodup } → False
heq✝ : some c = some val✝
deleteOne_f_rw :
  f.deleteOne id =
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
⊢ ∃ n_1, (f.clauses.data.set id none).get n_1 = f.clauses.data.get idx
Tactic:
apply Exists.intro ⟨idx.1, idx_in_bounds⟩
Proof state after:
case neg.h_3.inl.h.isTrue.intro
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
hl :
  ∀ (x : PosFin n),
    ¬c = { clause := [(x, false)], nodupkey := ⋯, nodup := ⋯ } ∧
      ¬c = { clause := [(x, true)], nodupkey := ⋯, nodup := ⋯ }
x✝¹ : Option (DefaultClause n)
val✝ : DefaultClause n
x✝ :
  ∀ (l : Literal (PosFin n)) (nodupkey : ∀ (l_1 : PosFin n), ¬(l_1, true) ∈ [l] ∨ ¬(l_1, false) ∈ [l])
    (nodup : [l].Nodup), val✝ = { clause := [l], nodupkey := nodupkey, nodup := nodup } → False
heq✝ : some c = some val✝
deleteOne_f_rw :
  f.deleteOne id =
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
⊢ (f.clauses.data.set id none).get ⟨↑idx, idx_in_bounds⟩ = f.clauses.data.get idx
Theorem: LRAT.DefaultFormula.deleteOne_preserves_strong_assignments_invariant
Proof state before:
case neg
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
hl :
  ∀ (x : PosFin n),
    ¬c = { clause := [(x, false)], nodupkey := ⋯, nodup := ⋯ } ∧
      ¬c = { clause := [(x, true)], nodupkey := ⋯, nodup := ⋯ }
x✝¹ : Option (DefaultClause n)
val✝ : DefaultClause n
x✝ :
  ∀ (l : Literal (PosFin n)) (nodupkey : ∀ (l_1 : PosFin n), ¬(l_1, true) ∈ [l] ∨ ¬(l_1, false) ∈ [l])
    (nodup : [l].Nodup), val✝ = { clause := [l], nodupkey := nodupkey, nodup := nodup } → False
heq✝ : some c = some val✝
deleteOne_f_rw :
  f.deleteOne id =
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝¹ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
h✝ : ¬id = ↑idx
⊢ (f.clauses.data.set id none).get ⟨↑idx, idx_in_bounds⟩ = f.clauses.data.get idx
Tactic:
. next id_ne_idx =>
  simp only [ne_eq, id_ne_idx, not_false_eq_true, List.get_set_ne]
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.deleteOne_preserves_strong_assignments_invariant
Proof state before:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
hl :
  ∀ (x : PosFin n),
    ¬c = { clause := [(x, false)], nodupkey := ⋯, nodup := ⋯ } ∧
      ¬c = { clause := [(x, true)], nodupkey := ⋯, nodup := ⋯ }
x✝¹ : Option (DefaultClause n)
val✝ : DefaultClause n
x✝ :
  ∀ (l : Literal (PosFin n)) (nodupkey : ∀ (l_1 : PosFin n), ¬(l_1, true) ∈ [l] ∨ ¬(l_1, false) ∈ [l])
    (nodup : [l].Nodup), val✝ = { clause := [l], nodupkey := nodupkey, nodup := nodup } → False
heq✝ : some c = some val✝
deleteOne_f_rw :
  f.deleteOne id =
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
⊢ ↑idx < (f.clauses.data.set id none).length
Tactic:
simp only [List.length_set]
Proof state after:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
hl :
  ∀ (x : PosFin n),
    ¬c = { clause := [(x, false)], nodupkey := ⋯, nodup := ⋯ } ∧
      ¬c = { clause := [(x, true)], nodupkey := ⋯, nodup := ⋯ }
x✝¹ : Option (DefaultClause n)
val✝ : DefaultClause n
x✝ :
  ∀ (l : Literal (PosFin n)) (nodupkey : ∀ (l_1 : PosFin n), ¬(l_1, true) ∈ [l] ∨ ¬(l_1, false) ∈ [l])
    (nodup : [l].Nodup), val✝ = { clause := [l], nodupkey := nodupkey, nodup := nodup } → False
heq✝ : some c = some val✝
deleteOne_f_rw :
  f.deleteOne id =
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
⊢ ↑idx < f.clauses.data.length
Theorem: LRAT.DefaultFormula.deleteOne_preserves_strong_assignments_invariant
Proof state before:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
hl :
  ∀ (x : PosFin n),
    ¬c = { clause := [(x, false)], nodupkey := ⋯, nodup := ⋯ } ∧
      ¬c = { clause := [(x, true)], nodupkey := ⋯, nodup := ⋯ }
x✝¹ : Option (DefaultClause n)
val✝ : DefaultClause n
x✝ :
  ∀ (l : Literal (PosFin n)) (nodupkey : ∀ (l_1 : PosFin n), ¬(l_1, true) ∈ [l] ∨ ¬(l_1, false) ∈ [l])
    (nodup : [l].Nodup), val✝ = { clause := [l], nodupkey := nodupkey, nodup := nodup } → False
heq✝ : some c = some val✝
deleteOne_f_rw :
  f.deleteOne id =
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
⊢ ↑idx < f.clauses.data.length
Tactic:
exact idx.2
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.deleteOne_preserves_strong_assignments_invariant
Proof state before:
case pos
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
hl :
  ∀ (x : PosFin n),
    ¬c = { clause := [(x, false)], nodupkey := ⋯, nodup := ⋯ } ∧
      ¬c = { clause := [(x, true)], nodupkey := ⋯, nodup := ⋯ }
x✝¹ : Option (DefaultClause n)
val✝ : DefaultClause n
x✝ :
  ∀ (l : Literal (PosFin n)) (nodupkey : ∀ (l_1 : PosFin n), ¬(l_1, true) ∈ [l] ∨ ¬(l_1, false) ∈ [l])
    (nodup : [l].Nodup), val✝ = { clause := [l], nodupkey := nodupkey, nodup := nodup } → False
heq✝ : some c = some val✝
deleteOne_f_rw :
  f.deleteOne id =
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝¹ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
h✝ : id = ↑idx
⊢ (f.clauses.data.set id none).get ⟨↑idx, idx_in_bounds⟩ = f.clauses.data.get idx
Tactic:
next id_eq_idx =>
exfalso
have idx_in_bounds2 : idx.1 < f.clauses.size := by
  have f_clauses_rw : f.clauses = { data := f.clauses.data } := rfl
  conv => rhs; rw [f_clauses_rw, Array.size_mk]
  exact idx.2
simp only [getElem!, id_eq_idx, Array.data_length, idx_in_bounds2, ↓reduceDite,
  Fin.eta, Array.get_eq_getElem, Array.getElem_eq_data_get] at heq
rw [hidx] at heq
simp only [Option.some.injEq] at heq
rw [← heq] at hl
specialize hl i
simp only [unit, DefaultClause.mk.injEq, List.cons.injEq, Prod.mk.injEq, true_and, and_true,
  Bool.not_eq_false, Bool.not_eq_true] at hl
by_cases b_val : b
. simp only [b_val, and_false] at hl
. simp only [b_val, false_and] at hl
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.deleteOne_preserves_strong_assignments_invariant
Proof state before:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
hl :
  ∀ (x : PosFin n),
    ¬c = { clause := [(x, false)], nodupkey := ⋯, nodup := ⋯ } ∧
      ¬c = { clause := [(x, true)], nodupkey := ⋯, nodup := ⋯ }
x✝¹ : Option (DefaultClause n)
val✝ : DefaultClause n
x✝ :
  ∀ (l : Literal (PosFin n)) (nodupkey : ∀ (l_1 : PosFin n), ¬(l_1, true) ∈ [l] ∨ ¬(l_1, false) ∈ [l])
    (nodup : [l].Nodup), val✝ = { clause := [l], nodupkey := nodupkey, nodup := nodup } → False
heq✝ : some c = some val✝
deleteOne_f_rw :
  f.deleteOne id =
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
id_eq_idx : id = ↑idx
⊢ (f.clauses.data.set id none).get ⟨↑idx, idx_in_bounds⟩ = f.clauses.data.get idx
Tactic:
exfalso
Proof state after:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
hl :
  ∀ (x : PosFin n),
    ¬c = { clause := [(x, false)], nodupkey := ⋯, nodup := ⋯ } ∧
      ¬c = { clause := [(x, true)], nodupkey := ⋯, nodup := ⋯ }
x✝¹ : Option (DefaultClause n)
val✝ : DefaultClause n
x✝ :
  ∀ (l : Literal (PosFin n)) (nodupkey : ∀ (l_1 : PosFin n), ¬(l_1, true) ∈ [l] ∨ ¬(l_1, false) ∈ [l])
    (nodup : [l].Nodup), val✝ = { clause := [l], nodupkey := nodupkey, nodup := nodup } → False
heq✝ : some c = some val✝
deleteOne_f_rw :
  f.deleteOne id =
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
id_eq_idx : id = ↑idx
⊢ False
Theorem: LRAT.DefaultFormula.deleteOne_preserves_strong_assignments_invariant
Proof state before:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
hl :
  ∀ (x : PosFin n),
    ¬c = { clause := [(x, false)], nodupkey := ⋯, nodup := ⋯ } ∧
      ¬c = { clause := [(x, true)], nodupkey := ⋯, nodup := ⋯ }
x✝¹ : Option (DefaultClause n)
val✝ : DefaultClause n
x✝ :
  ∀ (l : Literal (PosFin n)) (nodupkey : ∀ (l_1 : PosFin n), ¬(l_1, true) ∈ [l] ∨ ¬(l_1, false) ∈ [l])
    (nodup : [l].Nodup), val✝ = { clause := [l], nodupkey := nodupkey, nodup := nodup } → False
heq✝ : some c = some val✝
deleteOne_f_rw :
  f.deleteOne id =
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
id_eq_idx : id = ↑idx
⊢ False
Tactic:
have idx_in_bounds2 : idx.1 < f.clauses.size := by
  have f_clauses_rw : f.clauses = { data := f.clauses.data } := rfl
  conv => rhs; rw [f_clauses_rw, Array.size_mk]
  exact idx.2
Proof state after:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
hl :
  ∀ (x : PosFin n),
    ¬c = { clause := [(x, false)], nodupkey := ⋯, nodup := ⋯ } ∧
      ¬c = { clause := [(x, true)], nodupkey := ⋯, nodup := ⋯ }
x✝¹ : Option (DefaultClause n)
val✝ : DefaultClause n
x✝ :
  ∀ (l : Literal (PosFin n)) (nodupkey : ∀ (l_1 : PosFin n), ¬(l_1, true) ∈ [l] ∨ ¬(l_1, false) ∈ [l])
    (nodup : [l].Nodup), val✝ = { clause := [l], nodupkey := nodupkey, nodup := nodup } → False
heq✝ : some c = some val✝
deleteOne_f_rw :
  f.deleteOne id =
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
id_eq_idx : id = ↑idx
idx_in_bounds2 : ↑idx < f.clauses.size
⊢ False
Theorem: LRAT.DefaultFormula.deleteOne_preserves_strong_assignments_invariant
Proof state before:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
hl :
  ∀ (x : PosFin n),
    ¬c = { clause := [(x, false)], nodupkey := ⋯, nodup := ⋯ } ∧
      ¬c = { clause := [(x, true)], nodupkey := ⋯, nodup := ⋯ }
x✝¹ : Option (DefaultClause n)
val✝ : DefaultClause n
x✝ :
  ∀ (l : Literal (PosFin n)) (nodupkey : ∀ (l_1 : PosFin n), ¬(l_1, true) ∈ [l] ∨ ¬(l_1, false) ∈ [l])
    (nodup : [l].Nodup), val✝ = { clause := [l], nodupkey := nodupkey, nodup := nodup } → False
heq✝ : some c = some val✝
deleteOne_f_rw :
  f.deleteOne id =
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
id_eq_idx : id = ↑idx
idx_in_bounds2 : ↑idx < f.clauses.size
⊢ False
Tactic:
simp only [getElem!, id_eq_idx, Array.data_length, idx_in_bounds2, ↓reduceDite,
  Fin.eta, Array.get_eq_getElem, Array.getElem_eq_data_get] at heq
Proof state after:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
hl :
  ∀ (x : PosFin n),
    ¬c = { clause := [(x, false)], nodupkey := ⋯, nodup := ⋯ } ∧
      ¬c = { clause := [(x, true)], nodupkey := ⋯, nodup := ⋯ }
x✝¹ : Option (DefaultClause n)
val✝ : DefaultClause n
x✝ :
  ∀ (l : Literal (PosFin n)) (nodupkey : ∀ (l_1 : PosFin n), ¬(l_1, true) ∈ [l] ∨ ¬(l_1, false) ∈ [l])
    (nodup : [l].Nodup), val✝ = { clause := [l], nodupkey := nodupkey, nodup := nodup } → False
heq✝ : some c = some val✝
deleteOne_f_rw :
  f.deleteOne id =
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
id_eq_idx : id = ↑idx
idx_in_bounds2 : ↑idx < f.clauses.size
heq : f.clauses.data.get idx = some c
⊢ False