module Data.List.NonEmpty where

Nonempty lists🔗

A list is nonempty if it can be written as for some

We can encode this neatly in Agda by using an indexed inductive type, which makes it more amenable to proof automation.

data is-nonempty {ℓ} {A : Type ℓ} : (xs : List A) → Type ℓ where
  instance nonempty : ∀ {x xs} → is-nonempty (x ∷ xs)

Being nonempty is a proposition.

is-nonempty-is-prop
  : ∀ {xs : List A}
  → is-prop (is-nonempty xs)
is-nonempty-is-prop {xs = x ∷ xs} nonempty nonempty = refl

A list is non-empty if and only if it is not equal to the empty list.

is-nonempty→not-empty
  : is-nonempty xs
  → xs ≠ []
is-nonempty→not-empty nonempty = ∷≠[]

not-empty→is-nonempty
  : xs ≠ []
  → is-nonempty xs
not-empty→is-nonempty {xs = []} xs≠[] = absurd (xs≠[] refl)
not-empty→is-nonempty {xs = x ∷ xs} xs≠[] = nonempty

is-nonempty≃not-empty : is-nonempty xs ≃ (xs ≠ [])
is-nonempty≃not-empty = prop-ext! is-nonempty→not-empty not-empty→is-nonempty

A list is nonempty if and only if there is some and such that

is-nonempty≃∷
  : ∀ {xs : List A}
  → is-nonempty xs ≃ (Σ[ u ∈ A ] Σ[ us ∈ List A ] xs ≡ u ∷ us)
is-nonempty≃∷ {xs = []} =
  is-empty→≃
    (λ ())
    (λ (u , us , []=u∷us) → absurd ([]≠∷ []=u∷us))
is-nonempty≃∷ {xs = x ∷ xs} =
  is-contr→≃
    is-nonempty-is-contr
    (∷-singleton-is-contr x xs)

Properties🔗

We can decide if a list is nonempty by just checking if it is empty.

instance
  Dec-nonempty : ∀ {xs : List A} → Dec (is-nonempty xs)
  Dec-nonempty {xs = []} = no (λ ())
  Dec-nonempty {xs = x ∷ xs} = yes nonempty

Closure properties🔗

A list is nonempty if and only if one of or is nonempty.

++-nonemptyl
  : ∀ (xs ys : List A)
  → is-nonempty xs
  → is-nonempty (xs ++ ys)
++-nonemptyl (x ∷ xs) ys ne = nonempty

++-nonemptyr
  : ∀ (xs ys : List A)
  → is-nonempty ys
  → is-nonempty (xs ++ ys)
++-nonemptyr [] ys ne = ne
++-nonemptyr (x ∷ xs) ys ne = nonempty

++-nonempty-split
  : ∀ (xs ys : List A)
  → is-nonempty (xs ++ ys)
  → is-nonempty xs ⊎ is-nonempty ys
++-nonempty-split [] ys ne = inr ne
++-nonempty-split (x ∷ xs) ys ne = inl nonempty

++-nonempty≃
  : ∀ (xs ys : List A)
  → is-nonempty (xs ++ ys) ≃ ∥ (is-nonempty xs ⊎ is-nonempty ys) ∥
++-nonempty≃ xs ys =
  prop-ext!
    (λ ne → inc (++-nonempty-split xs ys ne))
    (rec! [ ++-nonemptyl xs ys , ++-nonemptyr xs ys ])