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
is-nonempty-is-contr : ∀ {x : A} {xs : List A} → is-contr (is-nonempty (x ∷ xs)) is-nonempty-is-contr = is-prop∙→is-contr is-nonempty-is-prop nonempty instance H-Level-is-nonempty : ∀ {xs : List A} {n : Nat} → H-Level (is-nonempty xs) (suc n) H-Level-is-nonempty = prop-instance is-nonempty-is-prop
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 ])