relseries as inductive type

Stream: mathlib4

[Christian Merten]

docs#RelSeries is currently defined as

structure RelSeries where
  length : ℕ
  toFun : Fin (length + 1) → α
  step : ∀ (i : Fin length), r (toFun (Fin.castSucc i)) (toFun i.succ)

which I find rather hard to work with, because of the Fin.castSucc, Fin.succ etc. At first glance it seemed to me that this could instead be an inductive type on two constructors, but after trying some things, I am no longer convinced it is possible in a useful way. What is certainly possible is to define the type of RelSeries with fixed head as:

import Mathlib

inductive RelSeries' {α : Type} (r : Rel α α) : α → Type where
  | singleton (x : α) : RelSeries' r x
  | cons (x y : α) (hxy : r x y) (xs : RelSeries' r y) : RelSeries' r x

I can imagine that this simplifies things, docs#RelSeries would be a sigma type on top of that, where most of the api is developed for RelSeries'.

What do people think? Is it really not possible to give a direct definition of docs#RelSeries that gives useful induction principles?

[Christian Merten]

Alternatively, we can of course just add this

import Mathlib

lemma RelSeries.inductionOn {α : Type*} {r : Rel α α} (motive : RelSeries r → Prop)
    (singleton : (x : α) → motive (RelSeries.singleton r x))
    (cons : (p : RelSeries r) → (x : α) → (hx : r x p.head) → (hp : motive p) →
      motive (p.cons x hx)) (p : RelSeries r) :
    motive p := by
  sorry

[Edward van de Meent]

Surely using docs#List.Chain' works better here?

[Christian Merten]

We have docs#RelSeries.Equiv which is the equiv with the docs#List.Chain' definition.

[Edward van de Meent]

I think adding the recursive principle as a def (since afaict it should work for Sort too) would be best, for the same reason why Vector isn't an inductive type

[Christian Merten]

Christian Merten said:

We have docs#RelSeries.Equiv which is the equiv with the docs#List.Chain' definition.

But also that is rather painful, since you still don't get nice induction principles.

[Christian Merten]

Edward van de Meent said:

I think adding the recursive principle as a def (since afaict it should work for Sort too) would be best, for the same reason why Vector isn't an inductive type

What is that reason?

[Edward van de Meent]

I guess it's not quite the same reason, but in general I think it's better to reuse existing types and predicates rather than defining new ones, since recreating the API will be lots easier

[Christian Merten]

Edward van de Meent said:

I guess it's not quite the same reason, but in general I think it's better to reuse existing types and predicates rather than defining new ones, since recreating the API will be lots easier

I just found this #PR reviews > StrictSeries !4#3858, !4#3852, where there was some discussion on that.

[Christian Merten]

and where Kim suggested both your suggestion and my RelSeries' from above.