inductionOn for List.groupBy

Stream: new members

[Stuart Geipel]

Hey, I followed the book's "Local recursive declarations" example to create a janky proof about List.groupBy. But what strikes me is, a) most of the proofs in the standard library are much shorter than mine, and b) when I prove my next thing about groupBy, I would be essentially copy-pasting the let rec aux. I think I want a reusable inductionOn-type construct but, what it would take as the inductive/base case parameters?

lemma groupby_loop_invariant (r : α → α → Bool) (ag' : List α) (g' : α) :
  (List.groupBy.loop r ag' g' [] []).Forall (. ≠ []) := by
  let rec aux (as : List α) (ag : α) (g : List α) (rem : List (List α)) :
      -- [really long proof here...]
      sorry
  exact aux ag' g' [] [] (by simp)

theorem groups_non_empty (r : α → α → Bool) (l : List α) : (l.groupBy r).Forall (. ≠ []) := by
  rw [List.groupBy]
  cases' l with a as <;> simp
  exact groupby_loop_invariant r as a

Or like, is my approach reasonable to begin with?

[ZHAO Jiecheng]

Where does Forall come from? Please follow #mwe when ask questions.

[Stuart Geipel]

Sorry - my mistake. Here is a MWE:

import Mathlib

universe u
variable {α : Type u}

lemma groupby_loop_invariant (r : α → α → Bool) (ag' : List α) (g' : α) :
  (List.groupBy.loop r ag' g' [] []).Forall (. ≠ []) := by
  let rec aux (as : List α) (ag : α) (g : List α) (rem : List (List α)) :
      rem.Forall (. ≠ []) → (List.groupBy.loop r as ag g rem).Forall (. ≠ []) :=
      -- [really long proof here...]
      sorry
  exact aux ag' g' [] [] (by simp)

theorem groups_non_empty (r : α → α → Bool) (l : List α) : (l.groupBy r).Forall (. ≠ []) := by
  rw [List.groupBy]
  cases' l with a as <;> simp
  exact groupby_loop_invariant r as a

I was able to delete universe u but the wiki included that so I left it in.

[Stuart Geipel]

I'm hoping that there's either a simpler way of proving this that doesn't require let rec aux, or a way to "box up" that recursion in a way to make future proofs simpler

[David Spies]

(deleted)