max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: fix Array.modify lemmas (#5536)

Browse source 
Generally works best to pick up the proofs by unification with the lhs.

pinging @hargoniX as this goes by, as it changes some proofs in
bv_decide (nothing interesting, just a bit simpler)
This commit is contained in:
Kim Morrison 2024-09-30 16:31:10 +10:00 • committed by GitHub
parent 4f2c4c7bd1
commit 5e8718dff9
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
4 changed files with 51 additions and 65 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

24
src/Init/Data/Array/Lemmas.lean
View file

@ -871,26 +871,26 @@ theorem mapIdx_spec (as : Array α) (f : Fin as.size → α → β)
unfold modify modifyM Id.run
split <;> simp
theorem getElem_modify {as : Array α} {x i} (h : i < as.size) :
(as.modify x f)[i]'(by simp [h]) = if x = i then f as[i] else as[i] := by
theorem getElem_modify {as : Array α} {x i} (h : i < (as.modify x f).size) :
(as.modify x f)[i] = if x = i then f (as[i]'(by simpa using h)) else as[i]'(by simpa using h) := by
simp only [modify, modifyM, get_eq_getElem, Id.run, Id.pure_eq]
split
· simp only [Id.bind_eq, get_set _ _ _ h]; split <;> simp [*]
· rw [if_neg (mt (by rintro rfl; exact h) ‹_›)]
· simp only [Id.bind_eq, get_set _ _ _ (by simpa using h)]; split <;> simp [*]
· rw [if_neg (mt (by rintro rfl; exact h) (by simp_all))]
theorem getElem_modify_self {as : Array α} {i : Nat} (h : i < as.size) (f : α → α) :
(as.modify i f)[i]'(by simp [h]) = f as[i] := by
theorem getElem_modify_self {as : Array α} {i : Nat} (f : α → α) (h : i < (as.modify i f).size) :
(as.modify i f)[i] = f (as[i]'(by simpa using h)) := by
simp [getElem_modify h]
theorem getElem_modify_of_ne {as : Array α} {i : Nat} (hj : j < as.size)
(f : α → α) (h : i ≠ j) :
(as.modify i f)[j]'(by rwa [size_modify]) = as[j] := by
theorem getElem_modify_of_ne {as : Array α} {i : Nat} (h : i ≠ j)
(f : α → α) (hj : j < (as.modify i f).size) :
(as.modify i f)[j] = as[j]'(by simpa using hj) := by
simp [getElem_modify hj, h]
@[deprecated getElem_modify (since := "2024-08-08")]
theorem get_modify {arr : Array α} {x i} (h : i < arr.size) :
(arr.modify x f).get ⟨i, by simp [h]⟩ =
if x = i then f (arr.get ⟨i, h⟩) else arr.get ⟨i, h⟩ := by
theorem get_modify {arr : Array α} {x i} (h : i < (arr.modify x f).size) :
(arr.modify x f).get ⟨i, h⟩ =
if x = i then f (arr.get ⟨i, by simpa using h⟩) else arr.get ⟨i, by simpa using h⟩ := by
simp [getElem_modify h]
/-! ### filter -/

32
src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean
View file

@ -136,12 +136,10 @@ theorem readyForRupAdd_ofArray {n : Nat} (arr : Array (Option (DefaultClause n))
exact ih.2 i b h
| some (l, true) =>
simp only [heq] at h
have i_in_bounds : i.1 < acc.size := by simp only [ih.1, i.2.2]
have l_in_bounds : l.1 < acc.size := by simp only [ih.1, l.2.2]
rcases ih with ⟨hsize, ih⟩
by_cases i = l.1
· next i_eq_l =>
simp only [i_eq_l, Array.getElem_modify_self l_in_bounds] at h
simp only [i_eq_l, Array.getElem_modify_self] at h
by_cases b
· next b_eq_true =>
rw [isUnit_iff, DefaultClause.toList] at heq
@ -160,16 +158,14 @@ theorem readyForRupAdd_ofArray {n : Nat} (arr : Array (Option (DefaultClause n))
rw [b_eq_false, Subtype.ext i_eq_l]
exact ih h
· next i_ne_l =>
simp only [Array.getElem_modify_of_ne i_in_bounds _ (Ne.symm i_ne_l)] at h
simp only [Array.getElem_modify_of_ne (Ne.symm i_ne_l)] at h
exact ih i b h
| some (l, false) =>
simp only [heq] at h
have i_in_bounds : i.1 < acc.size := by simp only [ih.1, i.2.2]
have l_in_bounds : l.1 < acc.size := by simp only [ih.1, l.2.2]
rcases ih with ⟨hsize, ih⟩
by_cases i = l.1
· next i_eq_l =>
simp only [i_eq_l, Array.getElem_modify_self l_in_bounds] at h
simp only [i_eq_l, Array.getElem_modify_self] at h
by_cases b
· next b_eq_true =>
simp only [hasAssignment, b_eq_true, ite_true, hasPos_addNeg] at h
@ -187,7 +183,7 @@ theorem readyForRupAdd_ofArray {n : Nat} (arr : Array (Option (DefaultClause n))
rw [c_def] at cOpt_in_arr
exact cOpt_in_arr
· next i_ne_l =>
simp only [Array.getElem_modify_of_ne i_in_bounds _ (Ne.symm i_ne_l)] at h
simp only [Array.getElem_modify_of_ne (Ne.symm i_ne_l)] at h
exact ih i b h
rcases List.foldlRecOn arr.toList ofArray_fold_fn (mkArray n unassigned) hb hl with ⟨_h_size, h'⟩
intro i b h
@ -281,7 +277,6 @@ theorem readyForRupAdd_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClaus
intro i b hb
have hf := f_readyForRupAdd.2.2 i b
have i_in_bounds : i.1 < f.assignments.size := by rw [f_readyForRupAdd.2.1]; exact i.2.2
have l_in_bounds : l.1 < f.assignments.size := by rw [f_readyForRupAdd.2.1]; exact l.2.2
simp only at hb
by_cases (i, b) = (l, true)
· next ib_eq_c =>
@ -292,7 +287,7 @@ theorem readyForRupAdd_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClaus
apply DefaultClause.ext
simp only [unit, hc]
· next ib_ne_c =>
have hb' : hasAssignment b (f.assignments[i.1]'i_in_bounds) := by
have hb' : hasAssignment b f.assignments[i.1] := by
by_cases l.1 = i.1
· next l_eq_i =>
have b_eq_false : b = false := by
@ -302,10 +297,10 @@ theorem readyForRupAdd_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClaus
· 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.getElem_modify_self i_in_bounds, ite_false, hasNeg_addPos, reduceCtorEq] at hb
simp only [hasAssignment, b_eq_false, l_eq_i, Array.getElem_modify_self, ite_false, hasNeg_addPos, reduceCtorEq] at hb
simp only [hasAssignment, b_eq_false, ite_false, hb, reduceCtorEq]
· next l_ne_i =>
simp only [Array.getElem_modify_of_ne i_in_bounds _ l_ne_i] at hb
simp only [Array.getElem_modify_of_ne l_ne_i] at hb
exact hb
specialize hf hb'
simp only [toList, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
@ -322,7 +317,6 @@ theorem readyForRupAdd_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClaus
intro i b hb
have hf := f_readyForRupAdd.2.2 i b
have i_in_bounds : i.1 < f.assignments.size := by rw [f_readyForRupAdd.2.1]; exact i.2.2
have l_in_bounds : l.1 < f.assignments.size := by rw [f_readyForRupAdd.2.1]; exact l.2.2
simp only at hb
by_cases (i, b) = (l, false)
· next ib_eq_c =>
@ -333,7 +327,7 @@ theorem readyForRupAdd_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClaus
apply DefaultClause.ext
simp only [unit, hc]
· next ib_ne_c =>
have hb' : hasAssignment b (f.assignments[i.1]'i_in_bounds) := by
have hb' : hasAssignment b f.assignments[i.1] := by
by_cases l.1 = i.1
· next l_eq_i =>
have b_eq_false : b = true := by
@ -341,10 +335,10 @@ theorem readyForRupAdd_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClaus
· 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.getElem_modify_self i_in_bounds, ite_true, hasPos_addNeg] at hb
simp only [hasAssignment, b_eq_false, l_eq_i, Array.getElem_modify_self, ite_true, hasPos_addNeg] at hb
simp only [hasAssignment, b_eq_false, ite_true, hb]
· next l_ne_i =>
simp only [Array.getElem_modify_of_ne i_in_bounds _ l_ne_i] at hb
simp only [Array.getElem_modify_of_ne l_ne_i] at hb
exact hb
specialize hf hb'
simp only [toList, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
@ -471,14 +465,14 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
simp only [deleteOne, heq, hl] at hb
by_cases l.1.1 = i.1
· next l_eq_i =>
simp only [l_eq_i, Array.getElem_modify_self i_in_bounds] at hb
simp only [l_eq_i, Array.getElem_modify_self] at hb
have l_ne_b : l.2 ≠ b := by
intro l_eq_b
rw [← l_eq_b] at hb
have hb' := not_has_remove f.assignments[i.1] l.2
simp [hb] at hb'
replace l_ne_b := Bool.eq_not_of_ne l_ne_b
rw [l_ne_b] at hb
simp only [l_ne_b] at hb
have hb := has_remove_irrelevant f.assignments[i.1] b hb
specialize hf i b hb
simp only [toList, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
@ -512,7 +506,7 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
· exact hf
· exact Or.inr hf
· next l_ne_i =>
simp only [Array.getElem_modify_of_ne i_in_bounds _ l_ne_i] at hb
simp only [Array.getElem_modify_of_ne l_ne_i] at hb
specialize hf i b hb
simp only [toList, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool] at hf

45
src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean
View file

@ -115,7 +115,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
constructor
· rfl
· constructor
· rw [Array.getElem_modify_self l_in_bounds]
· rw [Array.getElem_modify_self]
simp only [← i_eq_l, h1]
· constructor
· simp only [getElem!, l_in_bounds, ↓reduceDIte, Array.get_eq_getElem,
@ -138,7 +138,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
· next i_ne_l =>
apply Or.inl
simp only [insertUnit, h3, ite_false, reduceCtorEq]
rw [Array.getElem_modify_of_ne i_in_bounds _ (Ne.symm i_ne_l)]
rw [Array.getElem_modify_of_ne (Ne.symm i_ne_l)]
constructor
· exact h1
· intro j
@ -197,7 +197,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
rfl
· constructor
· simp only [i_eq_l]
rw [Array.getElem_modify_self l_in_bounds]
rw [Array.getElem_modify_self]
simp only [addAssignment, hl, ← i_eq_l, h2, ite_true, ite_false]
apply addNeg_addPos_eq_both
· constructor
@ -234,7 +234,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
· rw [Array.get_push_lt units l j.1 j.2, h1]
· constructor
· simp only [i_eq_l]
rw [Array.getElem_modify_self l_in_bounds]
rw [Array.getElem_modify_self]
simp only [addAssignment, hl, ← i_eq_l, h2, ite_true, ite_false]
apply addPos_addNeg_eq_both
· constructor
@ -277,7 +277,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
constructor
· rw [Array.get_push_lt units l j.1 j.2, h1]
· constructor
· rw [Array.getElem_modify_of_ne i_in_bounds _ (Ne.symm i_ne_l), h2]
· rw [Array.getElem_modify_of_ne (Ne.symm i_ne_l), h2]
· constructor
· exact h3
· intro k k_ne_j
@ -319,9 +319,9 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
by_cases i.1 = l.1.1
· next i_eq_l =>
simp only [i_eq_l]
rw [Array.getElem_modify_self l_in_bounds]
rw [Array.getElem_modify_self]
simp only [← i_eq_l, h3, add_both_eq_both]
· next i_ne_l => rw [Array.getElem_modify_of_ne i_in_bounds _ (Ne.symm i_ne_l), h3]
· next i_ne_l => rw [Array.getElem_modify_of_ne (Ne.symm i_ne_l), h3]
· constructor
· exact h4
· intro k k_ne_j1 k_ne_j2
@ -535,7 +535,7 @@ theorem clear_insert_inductive_case {n : Nat} (f : DefaultFormula n) (f_assignme
have i_in_bounds : i.1 < assignments.size := by
rw [hsize]
exact i.2
have h := Array.getElem_modify_of_ne i_in_bounds (removeAssignment units[idx.val].2) ih2
have h := Array.getElem_modify_of_ne ih2 (removeAssignment units[idx.val].2) (by simpa using i_in_bounds)
simp only [Fin.getElem_fin] at h
rw [h]
exact ih1
@ -546,8 +546,7 @@ theorem clear_insert_inductive_case {n : Nat} (f : DefaultFormula n) (f_assignme
apply Or.inl
constructor
· simp only [clearUnit, idx_eq_j, Array.get_eq_getElem, ih1]
have i_in_bounds : i.1 < assignments.size := by rw [hsize]; exact i.2
rw [Array.getElem_modify_self i_in_bounds, ih2, remove_add_cancel]
rw [Array.getElem_modify_self, ih2, remove_add_cancel]
exact ih3
· intro k k_ge_idx_add_one
have k_ge_idx : k.val ≥ idx.val := Nat.le_of_succ_le k_ge_idx_add_one
@ -568,8 +567,7 @@ theorem clear_insert_inductive_case {n : Nat} (f : DefaultFormula n) (f_assignme
· constructor
· simp only [clearUnit, Array.get_eq_getElem]
specialize ih4 idx (Nat.le_refl idx.1) idx_ne_j
have i_in_bounds : i.1 < assignments.size := by rw [hsize]; exact i.2
rw [Array.getElem_modify_of_ne i_in_bounds _ ih4]
rw [Array.getElem_modify_of_ne ih4]
exact ih2
· constructor
· exact ih3
@ -593,8 +591,7 @@ theorem clear_insert_inductive_case {n : Nat} (f : DefaultFormula n) (f_assignme
exact ih2
· constructor
· simp only [clearUnit, idx_eq_j1, Array.get_eq_getElem, ih1]
have i_in_bounds : i.1 < assignments.size := hsize ▸ i.2
rw [Array.getElem_modify_self i_in_bounds, ih3, ih4]
rw [Array.getElem_modify_self, ih3, ih4]
decide
· constructor
· simp [hasAssignment, hasNegAssignment, ih4]
@ -630,8 +627,7 @@ theorem clear_insert_inductive_case {n : Nat} (f : DefaultFormula n) (f_assignme
exact ih1
· constructor
· simp only [clearUnit, idx_eq_j2, Array.get_eq_getElem, ih2]
have i_in_bounds : i.1 < assignments.size := hsize ▸ i.2
rw [Array.getElem_modify_self i_in_bounds, ih3, ih4]
rw [Array.getElem_modify_self, ih3, ih4]
decide
· constructor
· simp only [hasAssignment, hasNegAssignment, ih4, ite_false, not_false_eq_true]
@ -687,10 +683,7 @@ theorem clear_insert_inductive_case {n : Nat} (f : DefaultFormula n) (f_assignme
simp only [Bool.not_eq_true] at h2
simp only [Fin.getElem_fin, ih2, ← h1, ← h2, ne_eq] at h3
exact h3 rfl
have idx_unit_in_bounds : units[idx.1].1.1 < assignments.size := by
rw [hsize]; exact units[idx.1].1.2.2
have i_in_bounds : i.1 < assignments.size := hsize ▸ i.2
rw [Array.getElem_modify_of_ne i_in_bounds _ idx_res_ne_i]
rw [Array.getElem_modify_of_ne idx_res_ne_i]
exact ih3
· constructor
· exact ih4
@ -796,7 +789,7 @@ theorem confirmRupHint_preserves_invariant_helper {n : Nat} (f : DefaultFormula
constructor
· simp only [List.get, l_eq_i]
· constructor
· simp only [l_eq_i, Array.getElem_modify_self i_in_bounds, List.get, h1]
· simp only [l_eq_i, Array.getElem_modify_self, List.get, h1]
· constructor
· simp only [List.get, Bool.not_eq_true]
simp only [getElem!, l_in_bounds, ↓reduceDIte, Array.get_eq_getElem,
@ -826,7 +819,7 @@ theorem confirmRupHint_preserves_invariant_helper {n : Nat} (f : DefaultFormula
· next l_ne_i =>
apply Or.inl
constructor
· rw [Array.getElem_modify_of_ne i_in_bounds (addAssignment l.2) l_ne_i]
· rw [Array.getElem_modify_of_ne l_ne_i]
exact h1
· intro l' l'_in_list
simp only [List.find?, List.mem_cons] at l'_in_list
@ -865,7 +858,7 @@ theorem confirmRupHint_preserves_invariant_helper {n : Nat} (f : DefaultFormula
apply And.intro l_eq_true ∘ And.intro l'_eq_false
constructor
· simp only [l'] at l'_eq_false
simp only [l_eq_i, addAssignment, l_eq_true, ite_true, Array.getElem_modify_self i_in_bounds, h1,
simp only [l_eq_i, addAssignment, l_eq_true, ite_true, Array.getElem_modify_self, h1,
l'_eq_false, ite_false]
apply addPos_addNeg_eq_both
· constructor
@ -914,7 +907,7 @@ theorem confirmRupHint_preserves_invariant_helper {n : Nat} (f : DefaultFormula
apply And.intro l'_eq_true ∘ And.intro l_eq_false
constructor
· simp only [l'] at l'_eq_true
simp only [l_eq_i, addAssignment, l'_eq_true, ite_true, Array.getElem_modify_self i_in_bounds, h1,
simp only [l_eq_i, addAssignment, l'_eq_true, ite_true, Array.getElem_modify_self, h1,
l_eq_false, ite_false]
apply addNeg_addPos_eq_both
· constructor
@ -950,7 +943,7 @@ theorem confirmRupHint_preserves_invariant_helper {n : Nat} (f : DefaultFormula
constructor
· exact j_eq_i
· constructor
· rw [Array.getElem_modify_of_ne i_in_bounds _ l_ne_i]
· rw [Array.getElem_modify_of_ne l_ne_i]
exact h1
· apply And.intro h2
intro k k_ne_j_succ
@ -1002,7 +995,7 @@ theorem confirmRupHint_preserves_invariant_helper {n : Nat} (f : DefaultFormula
all_goals
simp (config := {decide := true}) [getElem!, l_eq_i, i_in_bounds, h1, decidableGetElem?] at h
constructor
· rw [Array.getElem_modify_of_ne i_in_bounds _ l_ne_i]
· rw [Array.getElem_modify_of_ne l_ne_i]
exact h1
· constructor
· exact h2

15
src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean
View file

@ -39,27 +39,26 @@ theorem contradiction_of_insertUnit_success {n : Nat} (assignments : Array Assig
rcases insertUnit_success with foundContradiction_eq_true | assignments_l_ne_unassigned
· simp only [insertUnit, hl, ite_false]
rcases h foundContradiction_eq_true with ⟨i, h⟩
have i_in_bounds : i.1 < assignments.size := by rw [assignments_size]; exact i.2.2
apply Exists.intro i
by_cases l.1.1 = i.1
· next l_eq_i =>
simp [l_eq_i, Array.getElem_modify_self i_in_bounds, h]
simp [l_eq_i, Array.getElem_modify_self, h]
exact add_both_eq_both l.2
· next l_ne_i =>
simp [Array.getElem_modify_of_ne i_in_bounds _ l_ne_i]
simp [Array.getElem_modify_of_ne l_ne_i]
exact h
· apply Exists.intro l.1
simp only [insertUnit, hl, ite_false, Array.getElem_modify_self l_in_bounds, reduceCtorEq]
simp only [insertUnit, hl, ite_false, Array.getElem_modify_self, reduceCtorEq]
simp only [getElem!, l_in_bounds, dite_true, decidableGetElem?] at assignments_l_ne_unassigned
by_cases l.2
· next l_eq_true =>
rw [l_eq_true]
simp only [l_eq_true]
simp only [hasAssignment, l_eq_true, hasPosAssignment, getElem!, l_in_bounds, dite_true, ite_true,
Bool.not_eq_true, decidableGetElem?] at hl
split at hl <;> simp_all (config := { decide := true })
· next l_eq_false =>
simp only [Bool.not_eq_true] at l_eq_false
rw [l_eq_false]
simp only [l_eq_false]
simp [hasAssignment, l_eq_false, hasNegAssignment, getElem!, l_in_bounds, decidableGetElem?] at hl
split at hl <;> simp_all (config := { decide := true })
@ -681,7 +680,7 @@ theorem confirmRupHint_preserves_motive {n : Nat} (f : DefaultFormula n) (rupHin
by_cases l.1 = i.1
· next l_eq_i =>
simp only [getElem!, Array.size_modify, i_in_bounds, ↓ reduceDIte,
Array.get_eq_getElem, l_eq_i, Array.getElem_modify_self i_in_bounds (addAssignment b), decidableGetElem?]
Array.get_eq_getElem, l_eq_i, Array.getElem_modify_self (addAssignment b), decidableGetElem?]
simp only [getElem!, i_in_bounds, dite_true, Array.get_eq_getElem, decidableGetElem?] at pacc
by_cases pi : p i
· simp only [pi, decide_False]
@ -705,7 +704,7 @@ theorem confirmRupHint_preserves_motive {n : Nat} (f : DefaultFormula n) (rupHin
exact pacc
· next l_ne_i =>
simp only [getElem!, Array.size_modify, i_in_bounds,
Array.getElem_modify_of_ne i_in_bounds _ l_ne_i, dite_true,
Array.getElem_modify_of_ne l_ne_i, dite_true,
Array.get_eq_getElem, decidableGetElem?]
simp only [getElem!, i_in_bounds, dite_true, decidableGetElem?] at pacc
exact pacc