list with at least one element

Stream: Is there code for X?

[Jared green]

so i can do this:

def theFun (c : ilist a) : v a :=
  match c with
  | [b]  => f b
  | (b :: as )  => g b (theFun as)

that would give "missing cases"if it were list

[Eric Wieser]

You could use a docs#Subtype:

abbrev IList (α) := {l : List α // l ≠ []}

def theFun (c : IList Nat) : Nat :=
  match c with
  | ⟨[b], _⟩ => 0
  | ⟨b :: as, _⟩ => 1

edit: though this doesn't help for the recursive case

[Jared green]

is this not already in mathlib or the builtins?

[Eric Wieser]

I'm pretty sure it's not

[Eric Wieser]

Probably you will have a better time using a custom inductive than what I do above

[Jared green]

can that be done while also getting the already implemented functionality of list?

[Eric Wieser]

That functionality isn't going to come for free whatever you do. If you care about compilation, then my approach above will be fastest, and you have to deal with not being able to use match syntax for recursion

[Eric Wieser]

If you don't care about compilation, you can write a pair ofIList.toList and IList.mk l hl functions and use the inductive APi

[Jared green]

what do you mean 'if you care about compilation'

[Eric Wieser]

I mean "if you are building executable code, and want conversion between IList and List to be free"

[Eric Wieser]

If you use the inductive spelling without some very clever FFI hacks, the cost of the conversion would be O(n)

[Jared green]

i need it to run, and i need recursion. i dont know how to use ffi at all, though there should ideally be optimization in the compiler so the conversion doesnt actually occur, which is the least of my worries.

[Jared green]

specifically i need something like fold, which would look like this if i was to build it:

def fold (l : IList a) (f : a -> b -> b) (g: a  ->  b) : b
  match l  with
  | [d] => g d
  | (d :: ds) => f  d (fold ds f g)

[Jared green]

i also need to take things that come in the form of lists and use them in that way

[Yury G. Kudryashov]

See also docs#FreeSemigroup

[Jared green]

i went with inductive. got stuck on ofList

import Init.Prelude
import Init.Coe
import Mathlib.Data.List.Basic
variable {a : Type}
inductive IList a
  where
  | single : a -> IList a
  | cons : a -> IList a -> IList

def IList.ofList (l : {l : List // l ≠ [] }) : IList a :=
  if h : List.length l.1 = 1
  then single (List.head l.1 l.2)
  else cons (List.head l.1 l.2) (IList.ofList ⟨List.tail l.1,
    by
    by_contra ha
    apply h
    have hi : List.length l.1.tail = 0 := by {
       rw [ha]
       simp
    }
    rw [List.length_tail] at hi
    apply Nat.eq_add_of_sub_eq at hi
    simp at hi
    exact hi
    simp
    by_contra hj
    simp at hj
    apply l.2
    exact hj  ⟩

i needed the if statement to complete the proof, but now i need a termination proof

[Eric Wieser]

Here's a simple version:

def IList.ofList (l : {l : List a // l ≠ [] }) : IList a :=
  match l with
  | ⟨[x], _⟩ => .single x
  | ⟨x :: xs@(y :: ys), h⟩ => .cons x (IList.ofList ⟨xs, fun h => by aesop⟩)

[Eric Wieser]

A slightly neater spelling might be

def IList.ofList? (l : List a) : Option (IList a) :=
  match l with
  | [] => none
  | x :: xs => some <|
    match IList.ofList? xs with
    | .none => .single x
    | .some ixs => .cons x ixs

[Jared green]

what other imports are needed for the first one?

[Kyle Miller]

Any reason not to do this?

def IList (α : Type*) := α × List α
def IList.toList {α : Type*} : IList α → List α := fun (x, xs) => x :: xs
def List.toIList {α : Type*} (l : List α) (h : l ≠ []) : IList α :=
  match l, h with
  | x :: xs, _ => (x, xs)

[Jared green]

i was making toList and ofList as coercions with {l : List a // l ≠ [] } so that i can treat them as the same.

[Eric Wieser]

Any reason not to do this?

You lose the ability to pattern match on a .cons constructor (you can make .single work with @[match_pattern])

[Kyle Miller]

I think this would take some concrete use cases to evaluate, but that's true.

A big benefit to my IList is that you don't have to rebuild the List to convert it.

[Eric Wieser]

Arguably {l : List a // l ≠ [] } also has that property, and is likely to make things like (IList.map l f).toList = l.toList.map f defeq

[Kyle Miller]

Yeah, the subtype is likely the best version

[Eric Wieser]

But as you say, there are tradeoffs to be made here, informed by the concrete use case we don't know!

[Eric Wieser]

(I think custom match patterns would remove the need for some tradeoffs, but that sounds like a massive design challenge; especially if such a scheme were to be compatible with ~q matching!)

[Jared green]

in fact i have not implemented IList.map, mainly because my application doesnt call for it.