Linked list const constructor on the right

Stream: new members

[C7X]

Hi! For a project I'm working on I would like to have a type that's like List Nat, but with a constructor for appending a natural on the right instead of the left. I guess I could make an inductive type myself, but I also want to use all of Mathlib's functions on lists and lemmas about lists. I'd like to have appending to the right as a constructor, so that proofs by cases will work. Is there a canonical way to do this?

[Aaron Liu]

Why can't you just use List Nat and read all the list right-to-left?

[C7X]

I currently have code that's based on the programmer writing all List literals in reverse and having to swap left and right in their head, but I think it might be more convenient to have code which doesn't require accounting for left-to-right reflection in the programmer's head

[Kevin Buzzard]

Why don't you write your own custom recursor for lists and instead of cases do induction x using List.myrecursor?

[Kevin Buzzard]

There might even be an option to change the default recursor for an inductive type but I can't remember whether you'd need a core change to access this functionality for List or whether it can be done locally in a file

[Aaron Liu]

I think it can be done locally with @[cases_eliminator] and @[induction_eliminator]

[Eric Wieser]

Or if this is really for programmers, you could use Array and push

[C7X]

Thanks, I can try this! I'm relatively new to Lean so I can't guarantee that I will be able to write a recursor yet, but I'll see what I can do!

[Kevin Buzzard]

You can practice by writing the induction principle first:

variable {α : Type u}

example
    (motive : List α → Prop)
    (hnil : motive [])
    (hsnoc : ∀ (init : List α) (last : α), motive init → motive (init ++ [last])) :
    ∀ l : List α, motive l := by
  sorry

[Eric Wieser]

It already exists as

docs#List.reverseRecOn