fix: propagate Simp.Config when reducing terms and checking definitional equality in simp

[leodemoura]

This PR ensures that the configuration in Simp.Config is used when reducing terms and checking definitional equality in simp.

closes #5455

TODO: fix broken tests

[leanprover-community-bot]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-6123 build failed against this PR. (2024-11-19 02:14:53) View Log
• 💥 Mathlib branch lean-pr-testing-6123 build failed against this PR. (2024-11-20 23:30:46) View Log
• 🟡 Mathlib branch lean-pr-testing-6123 build this PR didn't complete normally. (2024-11-20 23:40:50) View Log
• 💥 Mathlib branch lean-pr-testing-6123 build failed against this PR. (2024-11-20 23:42:22) View Log
• 💥 Mathlib branch lean-pr-testing-6123 build failed against this PR. (2024-11-20 23:49:08) View Log
• 💥 Mathlib branch lean-pr-testing-6123 build failed against this PR. (2024-11-21 00:01:34) View Log
• 💥 Mathlib branch lean-pr-testing-6123 build failed against this PR. (2024-11-21 00:11:55) View Log
• 💥 Mathlib branch lean-pr-testing-6123 build failed against this PR. (2024-11-21 00:46:40) View Log
• 🟡 Mathlib branch lean-pr-testing-6123 build against this PR was cancelled. (2024-11-21 23:32:02) View Log
• 💥 Mathlib branch lean-pr-testing-6123 build failed against this PR. (2024-11-21 23:35:07) View Log
• 💥 Mathlib branch lean-pr-testing-6123 build failed against this PR. (2024-11-22 00:32:04) View Log
• 🟡 Mathlib branch lean-pr-testing-6123 build this PR didn't complete normally. (2024-11-22 03:14:30) View Log
• 💥 Mathlib branch lean-pr-testing-6123 build failed against this PR. (2024-11-22 20:23:52) View Log
• 💥 Mathlib branch lean-pr-testing-6123 build failed against this PR. (2024-11-25 03:30:00) View Log
• 💥 Mathlib branch lean-pr-testing-6123 build failed against this PR. (2024-11-25 05:59:14) View Log
• 💥 Mathlib branch lean-pr-testing-6123 build failed against this PR. (2024-11-25 22:48:29) View Log
• 💥 Mathlib branch lean-pr-testing-6123 build failed against this PR. (2024-11-26 01:18:36) View Log
• 💥 Mathlib branch lean-pr-testing-6123 build failed against this PR. (2024-11-26 05:04:32) View Log
• 💥 Mathlib branch lean-pr-testing-6123 build failed against this PR. (2024-11-26 07:43:23) View Log
• 💥 Mathlib branch lean-pr-testing-6123 build failed against this PR. (2024-11-27 00:36:26) View Log
• 💥 Mathlib branch lean-pr-testing-6123 build failed against this PR. (2024-11-27 00:47:37) View Log
• 💥 Mathlib branch lean-pr-testing-6123 build failed against this PR. (2024-11-29 22:56:24) View Log
• 💥 Mathlib branch lean-pr-testing-6123 build failed against this PR. (2024-11-30 00:52:23) View Log
• 💥 Mathlib branch lean-pr-testing-6123 build failed against this PR. (2024-11-30 01:49:55) View Log
• 💥 Mathlib branch lean-pr-testing-6123 build failed against this PR. (2024-12-01 00:17:47) View Log

[kim-em]

This is the first failure in Batteries:

namespace Ordering

@[simp] theorem swap_swap {o : Ordering} : o.swap.swap = o := by cases o <;> rfl

@[simp] theorem swap_inj {o₁ o₂ : Ordering} : o₁.swap = o₂.swap ↔ o₁ = o₂ :=
  ⟨fun h => by simpa using congrArg swap h, congrArg _⟩

end Ordering

/-- `OrientedCmp cmp` asserts that `cmp` is determined by the relation `cmp x y = .lt`. -/
class OrientedCmp (cmp : α → α → Ordering) : Prop where
  /-- The comparator operation is symmetric, in the sense that if `cmp x y` equals `.lt` then
  `cmp y x = .gt` and vice versa. -/
  symm (x y) : (cmp x y).swap = cmp y x

namespace OrientedCmp

theorem cmp_eq_gt [OrientedCmp cmp] : cmp x y = .gt ↔ cmp y x = .lt := by
  rw [← Ordering.swap_inj, symm]; exact .rfl

end OrientedCmp

/-- `TransCmp cmp` asserts that `cmp` induces a transitive relation. -/
class TransCmp (cmp : α → α → Ordering) extends OrientedCmp cmp : Prop where
  /-- The comparator operation is transitive. -/
  le_trans : cmp x y ≠ .gt → cmp y z ≠ .gt → cmp x z ≠ .gt

namespace TransCmp
variable [TransCmp cmp]
open OrientedCmp

theorem ge_trans (h₁ : cmp x y ≠ .lt) (h₂ : cmp y z ≠ .lt) : cmp x z ≠ .lt := by
  have := @TransCmp.le_trans _ cmp _ z y x
  simp [cmp_eq_gt] at *
  -- `simp` did not fire at `this`
  exact this h₂ h₁

[kim-em]

Another failure:

namespace Std.Range

/-- The number of elements contained in a `Std.Range`. -/
def numElems (r : Range) : Nat :=
  if r.step = 0 then
    -- This is a very weird choice, but it is chosen to coincide with the `forIn` impl
    if r.stop ≤ r.start then 0 else r.stop
  else
    (r.stop - r.start + r.step - 1) / r.step

theorem numElems_stop_le_start : ∀ r : Range, r.stop ≤ r.start → r.numElems = 0 := sorry

private theorem numElems_le_iff {start stop step i} (hstep : 0 < step) :
    (stop - start + step - 1) / step ≤ i ↔ stop ≤ start + step * i :=
  sorry

theorem mem_range'_elems (r : Range) (h : x ∈ List.range' r.start r.numElems r.step) : x ∈ r := by
  sorry

theorem forIn'_eq_forIn_range' [Monad m] (r : Std.Range)
    (init : β) (f : (a : Nat) → a ∈ r → β → m (ForInStep β)) :
    forIn' r init f =
    forIn
      ((List.range' r.start r.numElems r.step).pmap Subtype.mk fun _ => mem_range'_elems r)
      init (fun ⟨a, h⟩ => f a h) := by
  let ⟨start, stop, step⟩ := r
  let L := List.range' start (numElems ⟨start, stop, step⟩) step
  let f' : { a // start ≤ a ∧ a < stop } → _ := fun ⟨a, h⟩ => f a h
  suffices ∀ H, forIn' [start:stop:step] init f = forIn (L.pmap Subtype.mk H) init f' from this _
  intro H; dsimp only [forIn', Range.forIn']
  if h : start < stop then
    simp [numElems, Nat.not_le.2 h, L]; split
    · subst step
      suffices ∀ n H init,
          forIn'.loop start stop 0 f n start (Nat.le_refl _) init =
          forIn ((List.range' start n 0).pmap Subtype.mk H) init f' from this _ ..
      intro n; induction n with (intro H init; unfold forIn'.loop; simp [*]) -- fails here, can't unfold
      | succ n ih => simp [ih (List.forall_mem_cons.1 H).2]; rfl
    · next step0 =>
      have hstep := Nat.pos_of_ne_zero step0
      suffices ∀ fuel l i hle H, l ≤ fuel →
          (∀ j, stop ≤ i + step * j ↔ l ≤ j) → ∀ init,
          forIn'.loop start stop step f fuel i hle init =
          forIn ((List.range' i l step).pmap Subtype.mk H) init f' by
        refine this _ _ _ _ _
          ((numElems_le_iff hstep).2 (Nat.le_trans ?_ (Nat.le_add_left ..)))
          (fun _ => (numElems_le_iff hstep).symm) _
        conv => lhs; rw [← Nat.one_mul stop]
        exact Nat.mul_le_mul_right stop hstep
      intro fuel; induction fuel with intro l i hle H h1 h2 init
      | zero => simp [forIn'.loop, Nat.le_zero.1 h1]
      | succ fuel ih =>
        cases l with
        | zero => rw [forIn'.loop]; simp [Nat.not_lt.2 <| by simpa using (h2 0).2 (Nat.le_refl _)]
        | succ l =>
          have ih := ih _ _ (Nat.le_trans hle (Nat.le_add_right ..))
            (List.forall_mem_cons.1 H).2 (Nat.le_of_succ_le_succ h1) fun i => by
              rw [Nat.add_right_comm, Nat.add_assoc, ← Nat.mul_succ, h2, Nat.succ_le_succ_iff]
          have := h2 0; simp at this
          rw [forIn'.loop]; simp [this, ih]; rfl
  else
    simp [List.range', h, numElems_stop_le_start ⟨start, stop, step⟩ (Nat.not_lt.1 h), L]
    cases stop <;> unfold forIn'.loop <;> simp [List.forIn', h]

[kim-em]

And another, from Mathlib

namespace Option

variable {α : Type _}

instance liftOrGet_isCommutative (f : α → α → α) [Std.Commutative f] :
    Std.Commutative (liftOrGet f) :=
  ⟨fun a b ↦ by cases a <;> cases b <;> simp [liftOrGet, Std.Commutative.comm]⟩

instance liftOrGet_isAssociative (f : α → α → α) [Std.Associative f] :
    Std.Associative (liftOrGet f) :=
  ⟨fun a b c ↦ by cases a <;> cases b <;> cases c <;> simp [liftOrGet, Std.Associative.assoc]⟩

end Option