test: for simp configuration plumbing

tests/lean/run/simpConfigPropagationIssue1.lean

@@ -0,0 +1,13 @@
+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

tests/lean/run/simpConfigPropagationIssue2.lean

@@ -0,0 +1,63 @@
+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]

tests/lean/run/simpConfigPropagationIssue3.lean

@@ -0,0 +1,36 @@
+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₁