Inductive definition of an ordered list

Stream: lean4

[Marc Masdeu]

In a learning seminar on Lean the question arose as possible ways to define an inductive type for ordered lists, where the constructors already guarantee the ordering. Here is what we tried without success:

import Mathlib.Data.Real.Basic

open Real

inductive MyList : Type :=
| nil (x : ℝ) : MyList
| cons (y : ℝ) (nil x) (h : y ≤ x) : MyList -- faisl with: invalid universe level in constructor 'MyList.cons',...
| cons' (y : ℝ) (cons x h) (h : y ≤ x) : MyList

I know how to do this using a structure that hold the list and with some helper functions, but the question is how to make it directly using an inductive definition. Thanks for the help!

[Kevin Buzzard]

set_option autoImplicit false is always a good first step here. Does this change the error?

[Kevin Buzzard]

Many people asking questions about inductive types seem to be victims of this footgun.

[Marc Masdeu]

No, it doesn't... Here's the full error:

invalid universe level in constructor 'MyList.cons', parameter 'nil' has type
  ?m.24 y
at universe level
  ?u.9
it must be smaller than or equal to the inductive datatype universe level
  1

[Kevin Buzzard]

I have no idea what (nil x) is supposed to mean. It's a random term in a bracket, not a variable name or anything

[Kevin Buzzard]

Do you mean (x : \R)?

[Marc Masdeu]

I understand that by "I" you mean "Lean". I would like to match against the previous constructor, and this is precisely what I don't know hot to do. That is, you can construct an ordered list by either:

1. Pass one real.
2. Pass one real, a list created using the previous constructor, and a proof that this new real is smaller than the x used in the first instance.
3. Pass one real, a list created the second constructor, and a proof that this new real is smaller than the term used in the other constructor.

This would make sense, right? It's similar to creating a list in the usual inductive definition, but at each step you ensure that your new element is sorted relative to the others.

[Kevin Buzzard]

But a list is called (L : MyList) not (nil x)

[Marc Masdeu]

Kevin Buzzard said:

Do you mean (x : \R)?

Yes, and I would want to write MyList.nil (x : R) but this does not work either...

[Kevin Buzzard]

I don't understand why you want to pass the list and not just x

[Marc Masdeu]

Kevin Buzzard said:

But a list is called (L : MyList) not (nil x)

Yes, I want this constructor to only take mylists created using the first constructor, not any mylist.

[Marc Masdeu]

In the usual inductive definition of a list, the cons constructor you pass an element and a list to it, too.

[Ruben Van de Velde]

Do you want to disallow empty lists?

[Marc Masdeu]

Yes, this proposal would not allow empty lists. I guess if I wanted an empty list then I would add one empty constructor.

[Kevin Buzzard]

Do you want to allow lists of length bigger than 3? Because you're not getting those either, right?

[Marc Masdeu]

That's a worse problem, I am trying to work out a solution for that. But the first problem will still be there: Lean does not take my definition...

[Kevin Buzzard]

Do you even know that it's possible to express the idea using a bare inductive type (as opposed to using inbuilt List, which your structure solution presumably does)?

[Marc Masdeu]

If you mean from a type theoretical point of view, the answer is: I have no clue. If you mean "intuitively", then my idea is that what I am constructing has a "last added value" and I should be able to access that value and compare it with my new value...

[François G. Dorais]

Record the last inserted object as a type parameter:

inductive MyList : ℝ → Type
| one (x : ℝ) : MyList x
| cons (x : ℝ) {y : ℝ} (h : x ≤ y) : MyList y → MyList x

[Marc Masdeu]

That's exactly what I was trying to accomplish, thank you all for looking into this!

[François G. Dorais]

If the type parameter is bothersome, you can wrap it in a sigma type

def MyActualList := (x : ℝ) × MyList x

or an equivalent custom structure type.

[James Gallicchio]

I think(?) this would also be a nice place for induction-recursion, something like

inductive MyList
| nil : MyList
| cons (hd : ℝ) (tl : MyList) (h : ltList tl hd) : MyList

def ltList : MyList -> ℝ -> Prop
| nil          => fun _ => True
| cons hd tl _ => fun x => x < hd

I don't think lean can do induction-recursion at the moment, and I don't think it's on the roadmap, but this is a nice simple example of induction-recursion in the wild

[Henrik Böving]

It cannot, It is not on the immediate roadmap but we are definitely not opposed to having this feature and it might be added eventually (eventually is an unknown far away moment in the future here)

[Max Nowak 🐉]

How would you expect ind-rec to be added to Lean? It would require modifying the kernel, as it’s not reducible to lean’s current type theory

[Henrik Böving]

We have not thought about it at all (to my knowledge). It is just something that we want to have eventually