Skip to content

Commit

Permalink
feat: improve Array GetElem lemmas (#5465)
Browse files Browse the repository at this point in the history
This should be tested against Mathlib, but there are conflicts with the
`nightly-with-mathlib` branch right now, so I'll wait until tomorrow.
  • Loading branch information
kim-em authored Sep 25, 2024
1 parent 7845a05 commit e4f2de0
Show file tree
Hide file tree
Showing 7 changed files with 65 additions and 46 deletions.
59 changes: 39 additions & 20 deletions src/Init/Data/Array/Lemmas.lean
Original file line number Diff line number Diff line change
Expand Up @@ -23,11 +23,33 @@ namespace Array

@[simp] theorem getElem_mk {xs : List α} {i : Nat} (h : i < xs.length) : (Array.mk xs)[i] = xs[i] := rfl

theorem getElem_eq_toList_getElem (a : Array α) (h : i < a.size) : a[i] = a.toList[i] := by
theorem getElem_eq_getElem_toList {a : Array α} (h : i < a.size) : a[i] = a.toList[i] := by
by_cases i < a.size <;> (try simp [*]) <;> rfl

theorem getElem?_eq_getElem {a : Array α} {i : Nat} (h : i < a.size) : a[i]? = some a[i] :=
getElem?_pos ..

@[simp] theorem getElem?_eq_none_iff {a : Array α} : a[i]? = none ↔ a.size ≤ i := by
by_cases h : i < a.size
· simp [getElem?_eq_getElem, h]
· rw [getElem?_neg a i h]
simp_all

theorem getElem?_eq {a : Array α} {i : Nat} :
a[i]? = if h : i < a.size then some a[i] else none := by
split
· simp_all [getElem?_eq_getElem]
· simp_all

theorem getElem?_eq_getElem?_toList (a : Array α) (i : Nat) : a[i]? = a.toList[i]? := by
rw [getElem?_eq]
split <;> simp_all

@[deprecated getElem_eq_getElem_toList (since := "2024-09-25")]
abbrev getElem_eq_toList_getElem := @getElem_eq_getElem_toList

@[deprecated getElem_eq_toList_getElem (since := "2024-09-09")]
abbrev getElem_eq_data_getElem := @getElem_eq_toList_getElem
abbrev getElem_eq_data_getElem := @getElem_eq_getElem_toList

@[deprecated getElem_eq_toList_getElem (since := "2024-06-12")]
theorem getElem_eq_toList_get (a : Array α) (h : i < a.size) : a[i] = a.toList.get ⟨i, h⟩ := by
Expand All @@ -36,11 +58,11 @@ theorem getElem_eq_toList_get (a : Array α) (h : i < a.size) : a[i] = a.toList.
theorem get_push_lt (a : Array α) (x : α) (i : Nat) (h : i < a.size) :
have : i < (a.push x).size := by simp [*, Nat.lt_succ_of_le, Nat.le_of_lt]
(a.push x)[i] = a[i] := by
simp only [push, getElem_eq_toList_getElem, List.concat_eq_append, List.getElem_append_left, h]
simp only [push, getElem_eq_getElem_toList, List.concat_eq_append, List.getElem_append_left, h]

@[simp] theorem get_push_eq (a : Array α) (x : α) : (a.push x)[a.size] = x := by
simp only [push, getElem_eq_toList_getElem, List.concat_eq_append]
rw [List.getElem_append_right] <;> simp [getElem_eq_toList_getElem, Nat.zero_lt_one]
simp only [push, getElem_eq_getElem_toList, List.concat_eq_append]
rw [List.getElem_append_right] <;> simp [getElem_eq_getElem_toList, Nat.zero_lt_one]

theorem get_push (a : Array α) (x : α) (i : Nat) (h : i < (a.push x).size) :
(a.push x)[i] = if h : i < a.size then a[i] else x := by
Expand Down Expand Up @@ -220,11 +242,11 @@ theorem get!_eq_getD [Inhabited α] (a : Array α) : a.get! n = a.getD n default
@[simp] theorem getElem_set_eq (a : Array α) (i : Fin a.size) (v : α) {j : Nat}
(eq : i.val = j) (p : j < (a.set i v).size) :
(a.set i v)[j]'p = v := by
simp [set, getElem_eq_toList_getElem, ←eq]
simp [set, getElem_eq_getElem_toList, ←eq]

@[simp] theorem getElem_set_ne (a : Array α) (i : Fin a.size) (v : α) {j : Nat} (pj : j < (a.set i v).size)
(h : i.val ≠ j) : (a.set i v)[j]'pj = a[j]'(size_set a i v ▸ pj) := by
simp only [set, getElem_eq_toList_getElem, List.getElem_set_ne h]
simp only [set, getElem_eq_getElem_toList, List.getElem_set_ne h]

theorem getElem_set (a : Array α) (i : Fin a.size) (v : α) (j : Nat)
(h : j < (a.set i v).size) :
Expand Down Expand Up @@ -314,7 +336,7 @@ termination_by n - i
abbrev mkArray_data := @toList_mkArray

@[simp] theorem getElem_mkArray (n : Nat) (v : α) (h : i < (mkArray n v).size) :
(mkArray n v)[i] = v := by simp [Array.getElem_eq_toList_getElem]
(mkArray n v)[i] = v := by simp [Array.getElem_eq_getElem_toList]

/-- # mem -/

Expand Down Expand Up @@ -355,7 +377,7 @@ theorem lt_of_getElem {x : α} {a : Array α} {idx : Nat} {hidx : idx < a.size}
hidx

theorem getElem?_mem {l : Array α} {i : Fin l.size} : l[i] ∈ l := by
erw [Array.mem_def, getElem_eq_toList_getElem]
erw [Array.mem_def, getElem_eq_getElem_toList]
apply List.get_mem

theorem getElem_fin_eq_toList_get (a : Array α) (i : Fin _) : a[i] = a.toList.get i := rfl
Expand All @@ -366,14 +388,11 @@ abbrev getElem_fin_eq_data_get := @getElem_fin_eq_toList_get
@[simp] theorem ugetElem_eq_getElem (a : Array α) {i : USize} (h : i.toNat < a.size) :
a[i] = a[i.toNat] := rfl

theorem getElem?_eq_getElem (a : Array α) (i : Nat) (h : i < a.size) : a[i]? = some a[i] :=
getElem?_pos ..

theorem get?_len_le (a : Array α) (i : Nat) (h : a.size ≤ i) : a[i]? = none := by
simp [getElem?_neg, h]

theorem getElem_mem_toList (a : Array α) (h : i < a.size) : a[i] ∈ a.toList := by
simp only [getElem_eq_toList_getElem, List.getElem_mem]
simp only [getElem_eq_getElem_toList, List.getElem_mem]

@[deprecated getElem_mem_toList (since := "2024-09-09")]
abbrev getElem_mem_data := @getElem_mem_toList
Expand Down Expand Up @@ -433,7 +452,7 @@ abbrev data_set := @toList_set

theorem get_set_eq (a : Array α) (i : Fin a.size) (v : α) :
(a.set i v)[i.1] = v := by
simp only [set, getElem_eq_toList_getElem, List.getElem_set_self]
simp only [set, getElem_eq_getElem_toList, List.getElem_set_self]

theorem get?_set_eq (a : Array α) (i : Fin a.size) (v : α) :
(a.set i v)[i.1]? = v := by simp [getElem?_pos, i.2]
Expand All @@ -452,7 +471,7 @@ theorem get_set (a : Array α) (i : Fin a.size) (j : Nat) (hj : j < a.size) (v :

@[simp] theorem get_set_ne (a : Array α) (i : Fin a.size) {j : Nat} (v : α) (hj : j < a.size)
(h : i.1 ≠ j) : (a.set i v)[j]'(by simp [*]) = a[j] := by
simp only [set, getElem_eq_toList_getElem, List.getElem_set_ne h]
simp only [set, getElem_eq_getElem_toList, List.getElem_set_ne h]

theorem getElem_setD (a : Array α) (i : Nat) (v : α) (h : i < (setD a i v).size) :
(setD a i v)[i] = v := by
Expand Down Expand Up @@ -554,7 +573,7 @@ abbrev data_range := @toList_range

@[simp]
theorem getElem_range {n : Nat} {x : Nat} (h : x < (Array.range n).size) : (Array.range n)[x] = x := by
simp [getElem_eq_toList_getElem]
simp [getElem_eq_getElem_toList]

set_option linter.deprecated false in
@[simp] theorem reverse_toList (a : Array α) : a.reverse.toList = a.toList.reverse := by
Expand Down Expand Up @@ -853,15 +872,15 @@ theorem size_append (as bs : Array α) : (as ++ bs).size = as.size + bs.size :=

theorem get_append_left {as bs : Array α} {h : i < (as ++ bs).size} (hlt : i < as.size) :
(as ++ bs)[i] = as[i] := by
simp only [getElem_eq_toList_getElem]
simp only [getElem_eq_getElem_toList]
have h' : i < (as.toList ++ bs.toList).length := by rwa [← toList_length, append_toList] at h
conv => rhs; rw [← List.getElem_append_left (bs := bs.toList) (h' := h')]
apply List.get_of_eq; rw [append_toList]

theorem get_append_right {as bs : Array α} {h : i < (as ++ bs).size} (hle : as.size ≤ i)
(hlt : i - as.size < bs.size := Nat.sub_lt_left_of_lt_add hle (size_append .. ▸ h)) :
(as ++ bs)[i] = bs[i - as.size] := by
simp only [getElem_eq_toList_getElem]
simp only [getElem_eq_getElem_toList]
have h' : i < (as.toList ++ bs.toList).length := by rwa [← toList_length, append_toList] at h
conv => rhs; rw [← List.getElem_append_right (h₁ := hle) (h₂ := h')]
apply List.get_of_eq; rw [append_toList]
Expand Down Expand Up @@ -1074,10 +1093,10 @@ theorem all_def {p : α → Bool} (as : Array α) : as.all p = as.toList.all p :
rw [Bool.eq_iff_iff, all_eq_true, List.all_eq_true]; simp only [List.mem_iff_getElem]
constructor
· rintro w x ⟨r, h, rfl⟩
rw [← getElem_eq_toList_getElem]
rw [← getElem_eq_getElem_toList]
exact w ⟨r, h⟩
· intro w i
exact w as[i] ⟨i, i.2, (getElem_eq_toList_getElem as i.2).symm⟩
exact w as[i] ⟨i, i.2, (getElem_eq_getElem_toList i.2).symm⟩

theorem all_eq_true_iff_forall_mem {l : Array α} : l.all p ↔ ∀ x, x ∈ l → p x := by
simp only [all_def, List.all_eq_true, mem_def]
Expand Down
2 changes: 1 addition & 1 deletion src/Init/Data/Array/TakeDrop.lean
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ namespace Array
theorem exists_of_uset (self : Array α) (i d h) :
∃ l₁ l₂, self.toList = l₁ ++ self[i] :: l₂ ∧ List.length l₁ = i.toNat ∧
(self.uset i d h).toList = l₁ ++ d :: l₂ := by
simpa only [ugetElem_eq_getElem, getElem_eq_toList_getElem, uset, toList_set] using
simpa only [ugetElem_eq_getElem, getElem_eq_getElem_toList, uset, toList_set] using
List.exists_of_set _

end Array
2 changes: 1 addition & 1 deletion src/Std/Data/DHashMap/Internal/WF.lean
Original file line number Diff line number Diff line change
Expand Up @@ -140,7 +140,7 @@ theorem expand.go_eq [BEq α] [Hashable α] [PartialEquivBEq α] (source : Array
refine ih.trans ?_
simp only [Array.get_eq_getElem, AssocList.foldl_eq, Array.toList_set]
rw [List.drop_eq_getElem_cons hi, List.bind_cons, List.foldl_append,
List.drop_set_of_lt _ _ (by omega), Array.getElem_eq_toList_getElem]
List.drop_set_of_lt _ _ (by omega), Array.getElem_eq_getElem_toList]
· next i source target hi =>
rw [expand.go_neg hi, List.drop_eq_nil_of_le, bind_nil, foldl_nil]
rwa [Array.size_eq_length_toList, Nat.not_lt] at hi
Expand Down
2 changes: 1 addition & 1 deletion src/Std/Tactic/BVDecide/LRAT/Internal/Clause.lean
Original file line number Diff line number Diff line change
Expand Up @@ -297,7 +297,7 @@ theorem ofArray_eq (arr : Array (Literal (PosFin n)))
dsimp; omega
rw [List.getElem?_eq_getElem i_in_bounds, List.getElem?_eq_getElem i_in_bounds']
simp only [List.get_eq_getElem, Nat.zero_add] at h
rw [← Array.getElem_eq_toList_getElem]
rw [← Array.getElem_eq_getElem_toList]
simp [h]
· have arr_data_length_le_i : arr.toList.length ≤ i := by
dsimp; omega
Expand Down
6 changes: 3 additions & 3 deletions src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean
Original file line number Diff line number Diff line change
Expand Up @@ -503,7 +503,7 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
conv => rhs; rw [Array.size_mk]
exact hbound
simp only [getElem!, id_eq_idx, Array.toList_length, idx_in_bounds2, ↓reduceDIte,
Fin.eta, Array.get_eq_getElem, Array.getElem_eq_toList_getElem, decidableGetElem?] at heq
Fin.eta, Array.get_eq_getElem, Array.getElem_eq_getElem_toList, decidableGetElem?] at heq
rw [hidx, hl] at heq
simp only [unit, Option.some.injEq, DefaultClause.mk.injEq, List.cons.injEq, and_true] at heq
simp only [← heq] at l_ne_b
Expand Down Expand Up @@ -536,7 +536,7 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
conv => rhs; rw [Array.size_mk]
exact hbound
simp only [getElem!, id_eq_idx, Array.toList_length, idx_in_bounds2, ↓reduceDIte,
Fin.eta, Array.get_eq_getElem, Array.getElem_eq_toList_getElem, decidableGetElem?] at heq
Fin.eta, Array.get_eq_getElem, Array.getElem_eq_getElem_toList, decidableGetElem?] at heq
rw [hidx, hl] at heq
simp only [unit, Option.some.injEq, DefaultClause.mk.injEq, List.cons.injEq, and_true] at heq
have i_eq_l : i = l.1 := by rw [← heq]
Expand Down Expand Up @@ -596,7 +596,7 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
conv => rhs; rw [Array.size_mk]
exact hbound
simp only [getElem!, id_eq_idx, Array.toList_length, idx_in_bounds2, ↓reduceDIte,
Fin.eta, Array.get_eq_getElem, Array.getElem_eq_toList_getElem, decidableGetElem?] at heq
Fin.eta, Array.get_eq_getElem, Array.getElem_eq_getElem_toList, decidableGetElem?] at heq
rw [hidx] at heq
simp only [Option.some.injEq] at heq
rw [← heq] at hl
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -461,7 +461,7 @@ theorem existsRatHint_of_ratHintsExhaustive {n : Nat} (f : DefaultFormula n)
constructor
· rw [← Array.mem_toList]
apply Array.getElem_mem_toList
· rw [← Array.getElem_eq_toList_getElem] at c'_in_f
· rw [← Array.getElem_eq_getElem_toList] at c'_in_f
simp only [getElem!, Array.getElem_range, i_lt_f_clauses_size, dite_true,
c'_in_f, DefaultClause.contains_iff, Array.get_eq_getElem, decidableGetElem?]
simpa [Clause.toList] using negPivot_in_c'
Expand All @@ -472,8 +472,8 @@ theorem existsRatHint_of_ratHintsExhaustive {n : Nat} (f : DefaultFormula n)
dsimp at *
omega
simp only [List.get_eq_getElem, Array.map_toList, Array.toList_length, List.getElem_map] at h'
rw [← Array.getElem_eq_toList_getElem] at h'
rw [← Array.getElem_eq_toList_getElem] at c'_in_f
rw [← Array.getElem_eq_getElem_toList] at h'
rw [← Array.getElem_eq_getElem_toList] at c'_in_f
exists ⟨j.1, j_in_bounds⟩
simp [getElem!, h', i_lt_f_clauses_size, dite_true, c'_in_f, decidableGetElem?]

Expand Down
34 changes: 17 additions & 17 deletions src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean
Original file line number Diff line number Diff line change
Expand Up @@ -1140,25 +1140,25 @@ theorem nodup_derivedLits {n : Nat} (f : DefaultFormula n)
specialize h3 ⟨j.1, j_in_bounds⟩ j_ne_k
simp only [derivedLits_arr_def, Fin.getElem_fin] at li_eq_lj
simp only [Fin.getElem_fin, derivedLits_arr_def, ne_eq, li, li_eq_lj] at h3
simp only [List.get_eq_getElem, Array.getElem_eq_toList_getElem, not_true_eq_false] at h3
simp only [List.get_eq_getElem, Array.getElem_eq_getElem_toList, not_true_eq_false] at h3
· next k_ne_i =>
have i_ne_k : ⟨i.1, i_in_bounds⟩ ≠ k := by intro i_eq_k; simp only [← i_eq_k, not_true] at k_ne_i
specialize h3 ⟨i.1, i_in_bounds⟩ i_ne_k
simp (config := { decide := true }) [Fin.getElem_fin, derivedLits_arr_def, ne_eq,
Array.getElem_eq_toList_getElem, li] at h3
Array.getElem_eq_getElem_toList, li] at h3
· by_cases li.2 = true
· next li_eq_true =>
have i_ne_k2 : ⟨i.1, i_in_bounds⟩ ≠ k2 := by
intro i_eq_k2
rw [← i_eq_k2] at k2_eq_false
simp only [List.get_eq_getElem] at k2_eq_false
simp [derivedLits_arr_def, Array.getElem_eq_toList_getElem, k2_eq_false, li] at li_eq_true
simp [derivedLits_arr_def, Array.getElem_eq_getElem_toList, k2_eq_false, li] at li_eq_true
have j_ne_k2 : ⟨j.1, j_in_bounds⟩ ≠ k2 := by
intro j_eq_k2
rw [← j_eq_k2] at k2_eq_false
simp only [List.get_eq_getElem] at k2_eq_false
simp only [derivedLits_arr_def, Fin.getElem_fin, Array.getElem_eq_toList_getElem] at li_eq_lj
simp [derivedLits_arr_def, Array.getElem_eq_toList_getElem, k2_eq_false, li_eq_lj, li] at li_eq_true
simp only [derivedLits_arr_def, Fin.getElem_fin, Array.getElem_eq_getElem_toList] at li_eq_lj
simp [derivedLits_arr_def, Array.getElem_eq_getElem_toList, k2_eq_false, li_eq_lj, li] at li_eq_true
by_cases ⟨i.1, i_in_bounds⟩ = k1
· next i_eq_k1 =>
have j_ne_k1 : ⟨j.1, j_in_bounds⟩ ≠ k1 := by
Expand All @@ -1167,11 +1167,11 @@ theorem nodup_derivedLits {n : Nat} (f : DefaultFormula n)
simp only [Fin.mk.injEq] at i_eq_k1
exact i_ne_j (Fin.eq_of_val_eq i_eq_k1)
specialize h3 ⟨j.1, j_in_bounds⟩ j_ne_k1 j_ne_k2
simp [li, li_eq_lj, derivedLits_arr_def, Array.getElem_eq_toList_getElem] at h3
simp [li, li_eq_lj, derivedLits_arr_def, Array.getElem_eq_getElem_toList] at h3
· next i_ne_k1 =>
specialize h3 ⟨i.1, i_in_bounds⟩ i_ne_k1 i_ne_k2
apply h3
simp (config := { decide := true }) only [Fin.getElem_fin, Array.getElem_eq_toList_getElem,
simp (config := { decide := true }) only [Fin.getElem_fin, Array.getElem_eq_getElem_toList,
ne_eq, derivedLits_arr_def, li]
rfl
· next li_eq_false =>
Expand All @@ -1180,13 +1180,13 @@ theorem nodup_derivedLits {n : Nat} (f : DefaultFormula n)
intro i_eq_k1
rw [← i_eq_k1] at k1_eq_true
simp only [List.get_eq_getElem] at k1_eq_true
simp [derivedLits_arr_def, Array.getElem_eq_toList_getElem, k1_eq_true, li] at li_eq_false
simp [derivedLits_arr_def, Array.getElem_eq_getElem_toList, k1_eq_true, li] at li_eq_false
have j_ne_k1 : ⟨j.1, j_in_bounds⟩ ≠ k1 := by
intro j_eq_k1
rw [← j_eq_k1] at k1_eq_true
simp only [List.get_eq_getElem] at k1_eq_true
simp only [derivedLits_arr_def, Fin.getElem_fin, Array.getElem_eq_toList_getElem] at li_eq_lj
simp [derivedLits_arr_def, Array.getElem_eq_toList_getElem, k1_eq_true, li_eq_lj, li] at li_eq_false
simp only [derivedLits_arr_def, Fin.getElem_fin, Array.getElem_eq_getElem_toList] at li_eq_lj
simp [derivedLits_arr_def, Array.getElem_eq_getElem_toList, k1_eq_true, li_eq_lj, li] at li_eq_false
by_cases ⟨i.1, i_in_bounds⟩ = k2
· next i_eq_k2 =>
have j_ne_k2 : ⟨j.1, j_in_bounds⟩ ≠ k2 := by
Expand All @@ -1195,10 +1195,10 @@ theorem nodup_derivedLits {n : Nat} (f : DefaultFormula n)
simp only [Fin.mk.injEq] at i_eq_k2
exact i_ne_j (Fin.eq_of_val_eq i_eq_k2)
specialize h3 ⟨j.1, j_in_bounds⟩ j_ne_k1 j_ne_k2
simp [li, li_eq_lj, derivedLits_arr_def, Array.getElem_eq_toList_getElem] at h3
simp [li, li_eq_lj, derivedLits_arr_def, Array.getElem_eq_getElem_toList] at h3
· next i_ne_k2 =>
specialize h3 ⟨i.1, i_in_bounds⟩ i_ne_k1 i_ne_k2
simp (config := { decide := true }) [Array.getElem_eq_toList_getElem, derivedLits_arr_def, li] at h3
simp (config := { decide := true }) [Array.getElem_eq_getElem_toList, derivedLits_arr_def, li] at h3

theorem restoreAssignments_performRupCheck_base_case {n : Nat} (f : DefaultFormula n)
(f_assignments_size : f.assignments.size = n)
Expand Down Expand Up @@ -1232,7 +1232,7 @@ theorem restoreAssignments_performRupCheck_base_case {n : Nat} (f : DefaultFormu
constructor
· apply Nat.zero_le
· constructor
· simp only [derivedLits_arr_def, Fin.getElem_fin, Array.getElem_eq_toList_getElem, ← j_eq_i]
· simp only [derivedLits_arr_def, Fin.getElem_fin, Array.getElem_eq_getElem_toList, ← j_eq_i]
rfl
· apply And.intro h1 ∘ And.intro h2
intro k _ k_ne_j
Expand All @@ -1244,7 +1244,7 @@ theorem restoreAssignments_performRupCheck_base_case {n : Nat} (f : DefaultFormu
apply Fin.ne_of_val_ne
simp only
exact Fin.val_ne_of_ne k_ne_j
simp only [Fin.getElem_fin, Array.getElem_eq_toList_getElem, ne_eq, derivedLits_arr_def]
simp only [Fin.getElem_fin, Array.getElem_eq_getElem_toList, ne_eq, derivedLits_arr_def]
exact h3 ⟨k.1, k_in_bounds⟩ k_ne_j
· apply Or.inr ∘ Or.inr
have j1_lt_derivedLits_arr_size : j1.1 < derivedLits_arr.size := by
Expand All @@ -1258,11 +1258,11 @@ theorem restoreAssignments_performRupCheck_base_case {n : Nat} (f : DefaultFormu
⟨j2.1, j2_lt_derivedLits_arr_size⟩,
i_gt_zero, Nat.zero_le j1.1, Nat.zero_le j2.1, ?_⟩
constructor
· simp only [derivedLits_arr_def, Fin.getElem_fin, Array.getElem_eq_toList_getElem, ← j1_eq_i]
· simp only [derivedLits_arr_def, Fin.getElem_fin, Array.getElem_eq_getElem_toList, ← j1_eq_i]
rw [← j1_eq_true]
rfl
· constructor
· simp only [derivedLits_arr_def, Fin.getElem_fin, Array.getElem_eq_toList_getElem, ← j2_eq_i]
· simp only [derivedLits_arr_def, Fin.getElem_fin, Array.getElem_eq_getElem_toList, ← j2_eq_i]
rw [← j2_eq_false]
rfl
· apply And.intro h1 ∘ And.intro h2
Expand All @@ -1279,7 +1279,7 @@ theorem restoreAssignments_performRupCheck_base_case {n : Nat} (f : DefaultFormu
apply Fin.ne_of_val_ne
simp only
exact Fin.val_ne_of_ne k_ne_j2
simp only [Fin.getElem_fin, Array.getElem_eq_toList_getElem, ne_eq, derivedLits_arr_def]
simp only [Fin.getElem_fin, Array.getElem_eq_getElem_toList, ne_eq, derivedLits_arr_def]
exact h3 ⟨k.1, k_in_bounds⟩ k_ne_j1 k_ne_j2

theorem restoreAssignments_performRupCheck {n : Nat} (f : DefaultFormula n) (f_assignments_size : f.assignments.size = n)
Expand Down

0 comments on commit e4f2de0

Please sign in to comment.