Add NonemptyList

[JamesGallicchio]

Sort of a stub at the moment, but a useful type to have rather than inlining the head/tail at use site.

I suspect we'd want to replicate many (most?) functions on List to have equivalents here, but my current use case just pattern matches the head/tail out so I don't know yet what functions will be useful.

[digama0]

What's the application? I'm basically neutral on adding this, but it would be nice to have some examples of code that already depends on it, in keeping with std4's trend of taking data structures from other libraries that have already been using the type in practice.

Regarding ofList, I think we should not try to be too fancy here. I'm not sure there is any tactic that is appropriate to use there because we don't know why the list is supposed to be nonempty. (intro. comes to mind, but if the input is a cons then you may as well just use the constructor.) If you really want an auto param there, you can make it user configurable by using an extensible tactic made for the occasion.

[JamesGallicchio]

I'm using it in my SML formalization; the syntax has a couple places with syntactic non-empty restrictions (for instance, fun declarations must have at least one pattern), and this makes that code clean.

RE: the ofList stuff, I just wanted to be able to write 5::L somewhere expecting a NonemptyList and have it automatically coerce to nonempty. I know the more canonical way would be to have an autoparam at that use site, but then I'm back to inlining the nonempty type which is what I was trying to avoid.

[urkud]

A similar type in Mathlib 3: https://leanprover-community.github.io/mathlib_docs/find/free_semigroup/

[fgdorais]

I've used this under the friendlier(?) name List1 in my personal code.

Have you considered making the type an abbreviation for α × List α instead? That would make the type a bit more versatile. Here is a (pointless but illustrative) example:

abbrev List1 (α : Type _) := α × List α

def List1.toList {α} : List1 α → List α
| (x, xs) => x :: xs

example (x : Nat) (xs : List Nat) : List1.toList (x, xs) = x :: xs := rfl

[urkud]

I'm not sure about programming but abbreviations are bad for reasoning: e.g., you can't have custom instances. If you use a semireducible def, then you can have custom instances but you have to make sure that the definitional equality doesn't leak through API because otherwise, e.g., simp won't be able to apply a lemma like

@[simp]
theorem Prod.map_fst (f : α → β) (g : γ → δ) (x : α × γ) :
    (Prod.map f g x).fst = f x.fst :=
  rfl

to x : List1 Nat.

BTW, your example can be written with a custom structure without loss of readability:

structure List1 (α : Type _) where
  hd : α
  tl : List α

def List1.toList {α} : List1 α → List α
| ⟨x, xs⟩ => x :: xs

example (x : Nat) (xs : List Nat) : List1.toList ⟨x, xs⟩ = x :: xs := rfl

[fgdorais]

Yes, absolutely. Named structures are often better.

The basic issue is that there are two different ways to view this type

• As a subtype of List with positive length (could be a structure instead of a subtype)
• As a pair with head and tail (could be a structure instead of a pair)

I think it's worth looking back at @leodemoura's idea to implement "type views" as briefly illustrated at: https://github.com/leanprover/lean4/blob/1a6663a41baf95cb995b79cd8a466ab81e230b35/tests/lean/run/posView.lean

Since forward and backward translations are O(1) this is probably worth while!

[kim-em]

I lean towards not including this in Std for now, but I'll note that I recently found myself using the 0 < L.length variant in Mathlib.

[joehendrix]

Closing since there wasn't activity and this is currently more of a stub.

Please reopen if needed.