symmetric induction

Stream: Is there code for X?

[Aaron Liu]

How can I do induction on a product that gives me access to all the symmetries of the induction hypothesis?
Something like this:

import Mathlib

example {ι α : Type*} [Finite ι] [Preorder α] [WellFoundedLT α] {motive : (ι → α) → Prop}
    (ind : ∀ i, (∀ j < i, ∀ e : ι ≃ ι, motive (j ∘ e)) → motive i) (i : ι → α) : motive i :=
  sorry

I would also want this be made easy to use when I have instead of (i : ι → α) an explicit collection of (x y z : α) for some small finite number of x y z

[Violeta Hernández]

This sounds like you're reinventing docs#Relation.CutExpand

[Violeta Hernández]

Specifically, this should be provable by inducting on the image of i as a multiset

[Violeta Hernández]

We also have the specific case of two-element multisets as docs#Sym2.GameAdd.induction

[Aaron Liu]

I'd like to avoid depending on multisets..

[Aaron Liu]

I guess most of the Finite stuff depends on them indirectly

[Violeta Hernández]

I think you could add this specialization in the same file that CutExpand is defined in. And then you don't need to think about multisets anymore.

[Violeta Hernández]

(I guess your work would still depend on them, but yeah, that's technically true of anything involving Finite)

[Aaron Liu]

well I generalize the finiteness out of it

import Mathlib

example {ι α : Type*} {r : (ι → α) → (ι → α) → Prop} (hr : WellFounded r)
    -- there are very many ways to state this condition
    (perm : ∀ i j, ∀ e : ι ≃ ι, r i (j ∘ e) → r i j)
    {motive : (ι → α) → Prop} (ind : ∀ i, (∀ j, r j i → ∀ e : ι ≃ ι, motive (j ∘ e)) → motive i)
    (i : ι → α) : motive i := by
  change motive (i ∘ Equiv.refl ι)
  generalize Equiv.refl ι = e
  induction i using hr.induction generalizing e with | _ i ih
  exact ind (i ∘ e) fun j hj => ih j (perm j i e hj)

[Aaron Liu]

finite is only necessary to show the well founded lt