Questions about lists

Stream: new members

[Ching-Tsun Chou]

(1) Suppose I want to define isLast (x : α) (xl : List α) : Prop to mean that x is the last element of the list xl. What is the most natural way to do it?
(2) Is it possible to define a recursive function on lists by recursing from the tail end? That is, doing something like the following:

def foo : List α → ...
  | [] => ...
  | xl  ++ [x] => ...

[Damiano Testa]

I'm not sure if it is possible to match on the tail of a list. You can look at how docs#List.getLast and the other ones are defined though and maybe they are good for your purposes?

[Ruben Van de Velde]

You can use getLast directly, of course. Otherwise I would expect an implementation that checks if the list is a singleton and otherwise calls isLastagain on the tail

[Damiano Testa]

Depending on what you want to do, you may be better off either reversing the list, or converting to an array.

[Ching-Tsun Chou]

For (1), the most natural code I can think of is:

def isLast {X : Type*} (x : X) (xl : List X) : Prop :=
  match (xl.getLast?) with
  | none => false
  | some y => x = y

For (2), I ended up working with functions of type Fin n → X and convert them to lists using List.OfFn when necessary.

[Robin Arnez]

For (1): xl.getLast? = some x
For (2):
Define a helper recursing from the start and call it with the reversed list, e.g.:

def foo (l : List α) : ...
  go l.reverse
where
  go : List α → ...
  | [] => ...
  | x :: xl => ...