From 050df5e0c3bacc25c2695678052b49b481164d69 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 11 Dec 2024 21:07:33 +1100 Subject: [PATCH] fix --- .../Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean index 069e2933d0cd..410e68e7b36a 100644 --- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean +++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean @@ -107,7 +107,7 @@ theorem readyForRupAdd_ofArray {n : Nat} (arr : Array (Option (DefaultClause n)) · simp only [ofArray] · have hsize : (ofArray arr).assignments.size = n := by simp only [ofArray, ← Array.foldl_toList] - have hb : (mkArray n unassigned).size = n := by simp only [Array.size_toArrayArray] + have hb : (mkArray n unassigned).size = n := by simp only [Array.size_mkArray] have hl (acc : Array Assignment) (ih : acc.size = n) (cOpt : Option (DefaultClause n)) (_cOpt_in_arr : cOpt ∈ arr.toList) : (ofArray_fold_fn acc cOpt).size = n := by rw [size_ofArray_fold_fn acc cOpt, ih] exact List.foldlRecOn arr.toList ofArray_fold_fn (mkArray n unassigned) hb hl @@ -117,7 +117,7 @@ theorem readyForRupAdd_ofArray {n : Nat} (arr : Array (Option (DefaultClause n)) ∀ i : PosFin n, ∀ b : Bool, hasAssignment b (assignments[i.1]'(by rw [hsize]; exact i.2.2)) → (unit (i, b)) ∈ toList (ofArray arr) have hb : ModifiedAssignmentsInvariant (mkArray n unassigned) := by - have hsize : (mkArray n unassigned).size = n := by simp only [Array.size_toArrayArray] + have hsize : (mkArray n unassigned).size = n := by simp only [Array.size_mkArray] apply Exists.intro hsize intro i b h by_cases hb : b <;> simp [hasAssignment, hb, hasPosAssignment, hasNegAssignment] at h @@ -494,7 +494,7 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor · next id_eq_idx => exfalso have idx_in_bounds2 : idx < f.clauses.size := by - conv => rhs; rw [Array.size_toArray] + conv => rhs; rw [Array.size_mk] exact hbound simp only [getElem!, id_eq_idx, Array.length_toList, idx_in_bounds2, ↓reduceDIte, Fin.eta, Array.get_eq_getElem, ← Array.getElem_toList, decidableGetElem?] at heq @@ -527,7 +527,7 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor · next id_eq_idx => exfalso have idx_in_bounds2 : idx < f.clauses.size := by - conv => rhs; rw [Array.size_toArray] + conv => rhs; rw [Array.size_mk] exact hbound simp only [getElem!, id_eq_idx, Array.length_toList, idx_in_bounds2, ↓reduceDIte, Fin.eta, Array.get_eq_getElem, ← Array.getElem_toList, decidableGetElem?] at heq @@ -587,7 +587,7 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor · next id_eq_idx => exfalso have idx_in_bounds2 : idx < f.clauses.size := by - conv => rhs; rw [Array.size_toArray] + conv => rhs; rw [Array.size_mk] exact hbound simp only [getElem!, id_eq_idx, Array.length_toList, idx_in_bounds2, ↓reduceDIte, Fin.eta, Array.get_eq_getElem, ← Array.getElem_toList, decidableGetElem?] at heq