Is there an element-wise instance of Preorder (List α)?

Stream: Is there code for X?

[Albus Dompeldorius]

Is there an instance [Preorder α] : Preorder (List α) where xs ≤ ys iff xs.length = ys.length and where xs[i] ≤ ys[i] for all 0 ≤ i < xs.length?

I have found List.Forall₂, which can be used to define ≤ for this preorder, as follows:

instance [LE α] : LE (List α) where
  le := Forall₂ LE.le

In order to extend this to a preorder on List α, we need to show reflexivity and transitivity. Reflexivity can be obtained by List.forall₂_refl, but I can't seem to find a corresponding result List.forall₂_trans for transitivity. Should this be added to Mathlib?

It should be noted that this preorder on List α is a very natural one, since it it makes List α exactly the free monoid generated by α in the category of preorders and monotone functions.

[A.]

The appropriate preorder already exists on Fin n → α. If xs : List α then xs.get has type Fin xs.length → α so I guess some rewriting would be required to compare xs.get to ys.get. On the other hand if you work with xs : Vector α n then xs.get : Fin n → α and you don't have the problem.
.

[A.]

It looks like Lean is going to default to lexicographic order on List itself. https://github.com/leanprover/lean4/blob/1248a55d32f5fc64c7a26cd606fdf4c2908ce09c/src/Init/Data/List/Basic.lean#L163

[Albus Dompeldorius]

Thanks! That seems like what I'm looking for. I have an idea, it should be possible to define an isomorphism between List α and the disjoint sum of Fin n → α for all n ∈ ℕ. (A sigma type, I think). Then we can use Sigma.preorder, to give the latter a preorder structure, which can be pulled back to List α. Does that make sense?

[Albus Dompeldorius]

Oh, I found this: List.equivSigmaTuple. This seems promising!

[Albus Dompeldorius]

Update: I managed to define the preorder as follows:

import Mathlib.Data.List.OfFn
import Mathlib.Data.Sigma.Order

instance PointwisePreorder [Preorder α] : Preorder (List α)
  := Preorder.lift List.equivSigmaTuple.toFun

[Eric Wieser]

Albus Dompeldorius said:

but I can't seem to find a corresponding result List.forall₂_trans for transitivity. Should this be added to Mathlib?

Yes, I think this ought to exist

[Albus Dompeldorius]

Eric Wieser said:

Yes, I think this ought to exist

Here is my attempt. It seems to work.

theorem forall₂_trans [IsTrans α R]: ∀ {a b c : List α}, Forall₂ R a b → Forall₂ R b c → Forall₂ R a c
  | _, _, _, Forall₂.nil, Forall₂.nil => by simp
  | _, _, _, Forall₂.cons ha0 h0, Forall₂.cons ha1 h1 => by
    constructor
    . exact IsTrans.trans _ _ _ ha0 ha1
    . exact forall₂_trans h0 h1