From fa11076d2d771a94e8619dca09831073606ae091 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 26 Aug 2024 10:08:54 -0700 Subject: [PATCH 1/3] chore: remore staging workarounds --- .../BVDecide/LRAT/Internal/Formula/RatAddSound.lean | 5 +---- .../BVDecide/LRAT/Internal/Formula/RupAddResult.lean | 7 ++----- .../BVDecide/LRAT/Internal/Formula/RupAddSound.lean | 9 +++------ 3 files changed, 6 insertions(+), 15 deletions(-) diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean index a678dbd8c6dd..02ee8a38ed98 100644 --- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean +++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean @@ -17,9 +17,6 @@ namespace Internal namespace DefaultFormula --- TODO: remove aux lemma after update-stage0 -private theorem false_ne_true : (false = true) = False := by simp - open Std.Sat open DefaultClause DefaultFormula Assignment ReduceResult @@ -318,7 +315,7 @@ theorem sat_of_insertRat {n : Nat} (f : DefaultFormula n) · apply Or.inr rw [i'_eq_i] at i_true_in_c apply And.intro i_true_in_c - simp only [addAssignment, ← b_eq_false, addNegAssignment, ite_false, false_ne_true] at h2 + simp only [addAssignment, ← b_eq_false, addNegAssignment, ite_false, reduceCtorEq] at h2 split at h2 · next heq => have hasPosAssignment_fi : hasAssignment true (f.assignments[i.1]'i_in_bounds) := by diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean index 8b847b5193fe..8118d1850fcb 100644 --- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean +++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean @@ -20,9 +20,6 @@ namespace DefaultFormula open Std.Sat open DefaultClause DefaultFormula Assignment --- TODO: remove aux lemma after update-stage0 -private theorem false_ne_true : (false = true) = False := by simp - theorem size_insertUnit {n : Nat} (units : Array (Literal (PosFin n))) (assignments : Array Assignment) (b : Bool) (l : Literal (PosFin n)) : (insertUnit (units, assignments, b) l).2.1.size = assignments.size := by @@ -876,7 +873,7 @@ theorem confirmRupHint_preserves_invariant_helper {n : Nat} (f : DefaultFormula simp only [l'_eq_false, hasAssignment, ite_false] at h2 simp only [hasAssignment, l_eq_true, getElem!, l_eq_i, i_in_bounds, Array.get_eq_getElem, ↓reduceIte, ↓reduceDIte, h1, addAssignment, l'_eq_false, - hasPos_addNeg, decidableGetElem?, false_ne_true] at h + hasPos_addNeg, decidableGetElem?, reduceCtorEq] at h exact unassigned_of_has_neither _ h h2 · intro k k_ne_zero k_ne_j_succ have k_eq_succ : ∃ k' : Nat, ∃ k'_succ_in_bounds : k' + 1 < (l :: acc.2.1).length, k = ⟨k' + 1, k'_succ_in_bounds⟩ := by @@ -924,7 +921,7 @@ theorem confirmRupHint_preserves_invariant_helper {n : Nat} (f : DefaultFormula · simp only [l'] at l'_eq_true simp only [hasAssignment, l'_eq_true, ite_true] at h2 simp only [hasAssignment, l_eq_false, ↓reduceIte, getElem!, l_eq_i, i_in_bounds, - Array.get_eq_getElem, h1, addAssignment, l'_eq_true, hasNeg_addPos, decidableGetElem?, false_ne_true] at h + Array.get_eq_getElem, h1, addAssignment, l'_eq_true, hasNeg_addPos, decidableGetElem?, reduceCtorEq] at h exact unassigned_of_has_neither _ h2 h · intro k k_ne_j_succ k_ne_zero have k_eq_succ : ∃ k' : Nat, ∃ k'_succ_in_bounds : k' + 1 < (l :: acc.2.1).length, k = ⟨k' + 1, k'_succ_in_bounds⟩ := by diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean index b3c73982a78e..e628e12347f9 100644 --- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean +++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean @@ -17,9 +17,6 @@ namespace Internal namespace DefaultFormula --- TODO: remove aux lemma after update-stage0 -private theorem false_ne_true : (false = true) = False := by simp - open Std.Sat open DefaultClause DefaultFormula Assignment ReduceResult @@ -52,7 +49,7 @@ theorem contradiction_of_insertUnit_success {n : Nat} (assignments : Array Assig simp [Array.getElem_modify_of_ne i_in_bounds _ l_ne_i] exact h · apply Exists.intro l.1 - simp only [insertUnit, hl, ite_false, Array.getElem_modify_self l_in_bounds, false_ne_true] + simp only [insertUnit, hl, ite_false, Array.getElem_modify_self l_in_bounds, reduceCtorEq] simp only [getElem!, l_in_bounds, dite_true, decidableGetElem?] at assignments_l_ne_unassigned by_cases l.2 · next l_eq_true => @@ -184,7 +181,7 @@ theorem sat_of_insertRup {n : Nat} (f : DefaultFormula n) (f_readyForRupAdd : Re · apply Or.inr rw [i'_eq_i] at i_true_in_c apply And.intro i_true_in_c - simp only [addAssignment, ← b_eq_false, addNegAssignment, ite_false, false_ne_true] at h2 + simp only [addAssignment, ← b_eq_false, addNegAssignment, ite_false, reduceCtorEq] at h2 split at h2 · next heq => have hasPosAssignment_fi : hasAssignment true (f.assignments[i.1]'i_in_bounds) := by @@ -703,7 +700,7 @@ theorem confirmRupHint_preserves_motive {n : Nat} (f : DefaultFormula n) (rupHin by_cases hb : b · simp [(· ⊨ ·), hb, Subtype.ext l_eq_i, pi] at plb · simp only [Bool.not_eq_true] at hb - simp only [hasAssignment, addAssignment, hb, ite_false, ite_true, hasPos_addNeg, false_ne_true] + simp only [hasAssignment, addAssignment, hb, ite_false, ite_true, hasPos_addNeg, reduceCtorEq] simp only [hasAssignment, ite_true] at pacc exact pacc · next l_ne_i => From 9ba468cfe3cc45c0df33c6ade2b42812ccc2c384 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 26 Aug 2024 10:23:44 -0700 Subject: [PATCH 2/3] chore: staging issues --- src/Init/WFTactics.lean | 2 +- .../Tactic/BVDecide/LRAT/Internal/Clause.lean | 2 +- .../LRAT/Internal/Formula/Lemmas.lean | 8 +++---- .../LRAT/Internal/Formula/RatAddSound.lean | 4 ++-- .../LRAT/Internal/Formula/RupAddResult.lean | 22 +++++++++---------- .../LRAT/Internal/Formula/RupAddSound.lean | 2 +- tests/lean/mutwf1.lean | 4 ++-- 7 files changed, 22 insertions(+), 22 deletions(-) diff --git a/src/Init/WFTactics.lean b/src/Init/WFTactics.lean index 88f0dab18c60..b30f3e43dcff 100644 --- a/src/Init/WFTactics.lean +++ b/src/Init/WFTactics.lean @@ -26,7 +26,7 @@ macro "clean_wf" : tactic => `(tactic| simp (config := { unfoldPartialApp := true, zetaDelta := true, failIfUnchanged := false }) only [invImage, InvImage, Prod.lex, sizeOfWFRel, measure, Nat.lt_wfRel, - WellFoundedRelation.rel, sizeOf_nat]) + WellFoundedRelation.rel, sizeOf_nat, reduceCtorEq]) /-- Extensible helper tactic for `decreasing_tactic`. This handles the "base case" reasoning after applying lexicographic order lemmas. diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Clause.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Clause.lean index ca968b86cef0..e5d7be1745f4 100644 --- a/src/Std/Tactic/BVDecide/LRAT/Internal/Clause.lean +++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Clause.lean @@ -155,7 +155,7 @@ theorem isUnit_iff (c : DefaultClause n) (l : Literal (PosFin n)) : split · next l' heq => simp [heq] · next hne => - simp [false_iff] + simp apply hne def negate (c : DefaultClause n) : CNF.Clause (PosFin n) := c.clause.map Literal.negate diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean index 4b7d1d1b3a17..a9146eed96d3 100644 --- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean +++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean @@ -154,9 +154,9 @@ theorem readyForRupAdd_ofArray {n : Nat} (arr : Array (Option (DefaultClause n)) exact cOpt_in_arr · next b_eq_false => simp only [Bool.not_eq_true] at b_eq_false - simp [hasAssignment, b_eq_false, ite_false, hasNeg_addPos] at h + simp only [hasAssignment, b_eq_false, ite_false, hasNeg_addPos, reduceCtorEq] at h specialize ih l false - simp [hasAssignment, ite_false] at ih + simp only [hasAssignment, ite_false] at ih rw [b_eq_false, Subtype.ext i_eq_l] exact ih h · next i_ne_l => @@ -302,8 +302,8 @@ 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 [hasAssignment, b_eq_false, l_eq_i, Array.getElem_modify_self i_in_bounds, ite_false, hasNeg_addPos] at hb - simp [hasAssignment, b_eq_false, ite_false, hb] + 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, ite_false, hb, reduceCtorEq] · next l_ne_i => simp only [Array.getElem_modify_of_ne i_in_bounds _ l_ne_i] at hb exact hb diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean index 02ee8a38ed98..87813f9d5baa 100644 --- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean +++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean @@ -405,8 +405,8 @@ theorem assignmentsInvariant_performRupCheck_of_assignmentsInvariant {n : Nat} ( rw [hb] at h by_cases pi : p i · exact pi - · simp at pi - simp [pi, decide_True, h] at h1 + · simp only at pi + simp [pi, h] at h1 · simp only [Bool.not_eq_true] at hb rw [hb] rw [hb] at h diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean index 8118d1850fcb..797fa177144c 100644 --- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean +++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean @@ -111,7 +111,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen ⟨units.size, units_size_lt_updatedUnits_size⟩ have i_gt_zero : i.1 > 0 := by rw [i_eq_l]; exact l.1.2.1 refine ⟨mostRecentUnitIdx, l.2, i_gt_zero, ?_⟩ - simp [insertUnit, h3, ite_false, Array.get_push_eq, i_eq_l] + simp only [insertUnit, h3, ite_false, Array.get_push_eq, i_eq_l, reduceCtorEq] constructor · rfl · constructor @@ -127,7 +127,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen apply Nat.lt_of_le_of_ne · apply Nat.le_of_lt_succ have k_property := k.2 - simp [insertUnit, h3, ite_false, Array.size_push] at k_property + simp only [insertUnit, h3, ite_false, Array.size_push, reduceCtorEq] at k_property exact k_property · intro h simp only [← h, not_true, mostRecentUnitIdx] at hk @@ -137,7 +137,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen exact h2 ⟨k.1, k_in_bounds⟩ · next i_ne_l => apply Or.inl - simp [insertUnit, h3, ite_false] + simp only [insertUnit, h3, ite_false, reduceCtorEq] rw [Array.getElem_modify_of_ne i_in_bounds _ (Ne.symm i_ne_l)] constructor · exact h1 @@ -189,7 +189,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen exact h5 (has_add _ true) | true, false => refine ⟨⟨j.1, j_lt_updatedUnits_size⟩, mostRecentUnitIdx, i_gt_zero, ?_⟩ - simp [insertUnit, h5, ite_false, Array.get_push_eq, ne_eq] + simp only [insertUnit, h5, ite_false, Array.get_push_eq, ne_eq, reduceCtorEq] constructor · rw [Array.get_push_lt units l j.1 j.2, h1] · constructor @@ -219,7 +219,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen exact h4 ⟨k.1, h⟩ k_ne_j · exfalso have k_property := k.2 - simp [insertUnit, h5, ite_false, Array.size_push] at k_property + simp only [insertUnit, h5, ite_false, Array.size_push, reduceCtorEq] at k_property rcases Nat.lt_or_eq_of_le <| Nat.le_of_lt_succ k_property with k_lt_units_size | k_eq_units_size · exact h k_lt_units_size · simp only [← k_eq_units_size, not_true, mostRecentUnitIdx] at k_ne_l @@ -241,8 +241,8 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen · match h : assignments0[i.val]'_ with | unassigned => rfl | pos => - simp [addAssignment, h, ite_false, addNegAssignment] at h2 - simp [i_eq_l] at h2 + simp only [addAssignment, h, ite_false, addNegAssignment, reduceCtorEq] at h2 + simp only [i_eq_l] at h2 simp [hasAssignment, hl, getElem!, l_in_bounds, h2, hasPosAssignment, decidableGetElem?] at h5 | neg => simp (config := {decide := true}) only [h] at h3 | both => simp (config := {decide := true}) only [h] at h3 @@ -256,7 +256,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen exact h4 ⟨k.1, h⟩ k_ne_j · exfalso have k_property := k.2 - simp [insertUnit, h5, ite_false, Array.size_push] at k_property + simp only [insertUnit, h5, ite_false, Array.size_push, reduceCtorEq] at k_property rcases Nat.lt_or_eq_of_le <| Nat.le_of_lt_succ k_property with k_lt_units_size | k_eq_units_size · exact h k_lt_units_size · simp only [← k_eq_units_size, not_true, mostRecentUnitIdx] at k_ne_l @@ -270,10 +270,10 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen · next i_ne_l => apply Or.inr ∘ Or.inl have j_lt_updatedUnits_size : j.1 < (insertUnit (units, assignments, foundContradiction) l).1.size := by - simp [insertUnit, h5, ite_false, Array.size_push] + simp only [insertUnit, h5, ite_false, Array.size_push, reduceCtorEq] exact Nat.lt_trans j.2 (Nat.lt_succ_self units.size) refine ⟨⟨j.1, j_lt_updatedUnits_size⟩, b,i_gt_zero, ?_⟩ - simp [insertUnit, h5, ite_false] + simp only [insertUnit, h5, ite_false, reduceCtorEq] constructor · rw [Array.get_push_lt units l j.1 j.2, h1] · constructor @@ -350,7 +350,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen simp only have k_eq_units_size : k.1 = units.size := by have k_property := k.2 - simp [insertUnit, h, ite_false, Array.size_push] at k_property + simp only [insertUnit, h, ite_false, Array.size_push, reduceCtorEq] at k_property rcases Nat.lt_or_eq_of_le <| Nat.le_of_lt_succ k_property with k_lt_units_size | k_eq_units_size · exfalso; exact k_not_lt_units_size k_lt_units_size · exact k_eq_units_size diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean index e628e12347f9..2c2a864a57a8 100644 --- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean +++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean @@ -666,7 +666,7 @@ theorem confirmRupHint_preserves_motive {n : Nat} (f : DefaultFormula n) (rupHin simp only [ConfirmRupHintFoldEntailsMotive] split · simp [h1, hsize] - · simp [Array.size_modify, hsize] + · simp only [Array.size_modify, hsize, Bool.false_eq_true, false_implies, and_true, true_and] intro p pf have pacc := h1 p pf have pc : p ⊨ c := by diff --git a/tests/lean/mutwf1.lean b/tests/lean/mutwf1.lean index 432833b9f049..7050a119e62d 100644 --- a/tests/lean/mutwf1.lean +++ b/tests/lean/mutwf1.lean @@ -6,8 +6,8 @@ mutual | n, false => n + g n termination_by n b => (n, if b then 2 else 1) decreasing_by - · apply Prod.Lex.right; simp -- decide TODO: add `reduceCtorEq` at `clean_wf` after update-stage0 - · apply Prod.Lex.right; simp -- decide + · apply Prod.Lex.right; decide + · apply Prod.Lex.right; decide def g (n : Nat) : Nat := if h : n ≠ 0 then From 10be846b18f93ba607d5e3ffcc068ab4ef63adea Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 26 Aug 2024 10:34:10 -0700 Subject: [PATCH 3/3] chore: cleanup --- src/Init/ByCases.lean | 3 +-- src/Init/Data/BitVec/Lemmas.lean | 5 ++--- src/Init/Data/List/Count.lean | 6 +++--- src/Init/Data/List/Erase.lean | 4 ++-- src/Init/Data/List/Find.lean | 4 ++-- src/Init/Data/List/Nat/Range.lean | 2 +- src/Init/Data/List/Pairwise.lean | 2 +- src/Init/Data/List/Sort/Lemmas.lean | 2 +- src/Init/Data/Nat/Bitwise/Lemmas.lean | 2 +- 9 files changed, 14 insertions(+), 16 deletions(-) diff --git a/src/Init/ByCases.lean b/src/Init/ByCases.lean index a6174aa50507..cb205829a918 100644 --- a/src/Init/ByCases.lean +++ b/src/Init/ByCases.lean @@ -57,8 +57,7 @@ theorem apply_ite (f : α → β) (P : Prop) [Decidable P] (x y : α) : -- We don't mark this as `simp` as it is already handled by `ite_eq_right_iff`. theorem ite_some_none_eq_none [Decidable P] : (if P then some x else none) = none ↔ ¬ P := by - have : some x ≠ none := Option.noConfusion - simp only [ite_eq_right_iff, this] + simp only [ite_eq_right_iff, reduceCtorEq] rfl @[simp] theorem ite_some_none_eq_some [Decidable P] : diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index a105f486cffe..bd3f5ecd9564 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -993,9 +993,8 @@ theorem signExtend_eq_not_zeroExtend_not_of_msb_false {x : BitVec w} {v : Nat} ( x.signExtend v = x.zeroExtend v := by ext i by_cases hv : i < v - · have : (false = true) = False := by simp - simp only [signExtend, getLsb, getLsb_zeroExtend, hv, decide_True, Bool.true_and, toNat_ofInt, - BitVec.toInt_eq_msb_cond, hmsb, ↓reduceIte, this] + · simp only [signExtend, getLsb, getLsb_zeroExtend, hv, decide_True, Bool.true_and, toNat_ofInt, + BitVec.toInt_eq_msb_cond, hmsb, ↓reduceIte, reduceCtorEq] rw [Int.ofNat_mod_ofNat, Int.toNat_ofNat, Nat.testBit_mod_two_pow] simp [BitVec.testBit_toNat] · simp only [getLsb_zeroExtend, hv, decide_False, Bool.false_and] diff --git a/src/Init/Data/List/Count.lean b/src/Init/Data/List/Count.lean index 1ebf8a0b9ce1..c938468c4797 100644 --- a/src/Init/Data/List/Count.lean +++ b/src/Init/Data/List/Count.lean @@ -47,11 +47,11 @@ theorem length_eq_countP_add_countP (l) : length l = countP p l + countP (fun a if h : p x then rw [countP_cons_of_pos _ _ h, countP_cons_of_neg _ _ _, length, ih] · rw [Nat.add_assoc, Nat.add_comm _ 1, Nat.add_assoc] - · simp [h, not_true_eq_false, decide_False, not_false_eq_true] + · simp [h] else rw [countP_cons_of_pos (fun a => ¬p a) _ _, countP_cons_of_neg _ _ h, length, ih] · rfl - · simp [h, not_false_eq_true, decide_True] + · simp [h] theorem countP_eq_length_filter (l) : countP p l = length (filter p l) := by induction l with @@ -234,7 +234,7 @@ theorem count_erase (a b : α) : rw [if_pos hc_beq, hc, count_cons, Nat.add_sub_cancel] else have hc_beq := beq_false_of_ne hc - simp [hc_beq, if_false, count_cons, count_cons, count_erase a b l] + simp only [hc_beq, if_false, count_cons, count_cons, count_erase a b l, reduceCtorEq] if ha : b = a then rw [ha, eq_comm] at hc rw [if_pos ((beq_iff_eq _ _).2 ha), if_neg (by simpa using Ne.symm hc), Nat.add_zero, Nat.add_zero] diff --git a/src/Init/Data/List/Erase.lean b/src/Init/Data/List/Erase.lean index 07b8f8f91871..7bb0b2b17f69 100644 --- a/src/Init/Data/List/Erase.lean +++ b/src/Init/Data/List/Erase.lean @@ -39,13 +39,13 @@ theorem eraseP_of_forall_not {l : List α} (h : ∀ a, a ∈ l → ¬p a) : l.er | cons x xs ih => simp only [eraseP_cons, cond_eq_if] split <;> rename_i h - · simp + · simp only [reduceCtorEq, cons.injEq, false_or] constructor · rintro rfl simpa · rintro ⟨_, _, rfl, rfl⟩ rfl - · simp + · simp only [reduceCtorEq, cons.injEq, false_or, false_iff, not_exists, not_and] rintro x h' rfl simp_all diff --git a/src/Init/Data/List/Find.lean b/src/Init/Data/List/Find.lean index a5cefcdf9c14..361ad7022d76 100644 --- a/src/Init/Data/List/Find.lean +++ b/src/Init/Data/List/Find.lean @@ -737,10 +737,10 @@ theorem findIdx?_eq_enum_findSome? {xs : List α} {p : α → Bool} : induction xs with | nil => simp | cons x xs ih => - simp [findIdx?_cons, Nat.zero_add, findIdx?_succ, enum] + simp only [findIdx?_cons, Nat.zero_add, findIdx?_succ, enum] split · simp_all - · simp_all [enumFrom_cons, ite_false, Option.isNone_none, findSome?_cons_of_isNone] + · simp_all only [enumFrom_cons, ite_false, Option.isNone_none, findSome?_cons_of_isNone, reduceCtorEq] simp [Function.comp_def, ← map_fst_add_enum_eq_enumFrom, findSome?_map] theorem Sublist.findIdx?_isSome {l₁ l₂ : List α} (h : l₁ <+ l₂) : diff --git a/src/Init/Data/List/Nat/Range.lean b/src/Init/Data/List/Nat/Range.lean index aec8583b22a4..becacb274175 100644 --- a/src/Init/Data/List/Nat/Range.lean +++ b/src/Init/Data/List/Nat/Range.lean @@ -200,7 +200,7 @@ theorem range'_eq_append_iff : range' s n = xs ++ ys ↔ ∃ k, k ≤ n ∧ xs = cases k with | zero => simp [range'_succ] | succ k => - simp [range'_succ, ih, exists_eq_left'] + simp only [range'_succ, reduceCtorEq, false_and, cons.injEq, true_and, ih, range'_inj, exists_eq_left', or_true, and_true, false_or] refine ⟨k, ?_⟩ simp_all omega diff --git a/src/Init/Data/List/Pairwise.lean b/src/Init/Data/List/Pairwise.lean index fae5c995a490..fc0768806906 100644 --- a/src/Init/Data/List/Pairwise.lean +++ b/src/Init/Data/List/Pairwise.lean @@ -123,7 +123,7 @@ theorem pairwise_filterMap (f : β → Option α) {l : List β} : match e : f a with | none => rw [filterMap_cons_none e, pairwise_cons] - simp [e, false_implies, implies_true, true_and, IH] + simp only [e, false_implies, implies_true, true_and, IH, reduceCtorEq] | some b => rw [filterMap_cons_some e] simpa [IH, e] using fun _ => diff --git a/src/Init/Data/List/Sort/Lemmas.lean b/src/Init/Data/List/Sort/Lemmas.lean index 3b0e50029298..88a5ae153f2d 100644 --- a/src/Init/Data/List/Sort/Lemmas.lean +++ b/src/Init/Data/List/Sort/Lemmas.lean @@ -136,7 +136,7 @@ theorem merge_stable : ∀ (xs ys) (_ : ∀ x y, x ∈ xs → y ∈ ys → x.1 simp only [map_cons, cons.injEq, true_and] rw [merge_stable, map_cons] exact fun x' y' mx my => h x' y' (mem_cons_of_mem (i, x) mx) my - · simp [↓reduceIte, map_cons, cons.injEq, true_and] + · simp only [↓reduceIte, map_cons, cons.injEq, true_and, reduceCtorEq] rw [merge_stable, map_cons] exact fun x' y' mx my => h x' y' mx (mem_cons_of_mem (j, y) my) diff --git a/src/Init/Data/Nat/Bitwise/Lemmas.lean b/src/Init/Data/Nat/Bitwise/Lemmas.lean index 372217093391..1fa7253543ed 100644 --- a/src/Init/Data/Nat/Bitwise/Lemmas.lean +++ b/src/Init/Data/Nat/Bitwise/Lemmas.lean @@ -123,7 +123,7 @@ theorem ne_zero_implies_bit_true {x : Nat} (xnz : x ≠ 0) : ∃ i, testBit x i match mod_two_eq_zero_or_one x with | Or.inl mod2_eq => rw [←div_add_mod x 2] at xnz - simp [mod2_eq, ne_eq, Nat.mul_eq_zero, Nat.add_zero, false_or] at xnz + simp only [mod2_eq, ne_eq, Nat.mul_eq_zero, Nat.add_zero, false_or, reduceCtorEq] at xnz have ⟨d, dif⟩ := hyp x_pos xnz apply Exists.intro (d+1) simp_all