Lists of elements in discrete types

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-04-08.
Last modified on 2023-06-10.

module lists.lists-discrete-types where
open import foundation.booleans
open import foundation.cartesian-product-types
open import foundation.coproduct-types
open import foundation.decidable-equality
open import foundation.decidable-types
open import foundation.dependent-pair-types
open import foundation.empty-types
open import foundation.function-types
open import foundation.identity-types
open import foundation.raising-universe-levels
open import foundation.unit-type
open import foundation.universe-levels

open import lists.lists


In this file we study lists of elements in discrete types.


The type of lists of a discrete type is discrete

has-decidable-equality-list :
  {l1 : Level} {A : UU l1} 
  has-decidable-equality A  has-decidable-equality (list A)
has-decidable-equality-list d nil nil = inl refl
has-decidable-equality-list d nil (cons x l) =
  inr (map-inv-raise  Eq-eq-list nil (cons x l))
has-decidable-equality-list d (cons x l) nil =
  inr (map-inv-raise  Eq-eq-list (cons x l) nil)
has-decidable-equality-list d (cons x l) (cons x' l') =
    ( eq-Eq-list (cons x l) (cons x' l'))
    ( Eq-eq-list (cons x l) (cons x' l'))
    ( is-decidable-prod
      ( d x x')
      ( is-decidable-iff
        ( Eq-eq-list l l')
        ( eq-Eq-list l l')
        ( has-decidable-equality-list d l l')))

has-decidable-equality-has-decidable-equality-list :
  {l1 : Level} {A : UU l1} 
  has-decidable-equality (list A)  has-decidable-equality A
has-decidable-equality-has-decidable-equality-list d x y =
    ( is-decidable-iff
      ( Eq-eq-list (cons x nil) (cons y nil))
      ( eq-Eq-list (cons x nil) (cons y nil))
      ( d (cons x nil) (cons y nil)))
    ( raise-star)

Testing whether an element of a discrete type is in a list

elem-list :
  {l1 : Level} {A : UU l1} 
  has-decidable-equality A 
  A  list A  bool
elem-list d x nil = false
elem-list d x (cons x' l) with (d x x')
... | inl _ = true
... | inr _ = elem-list d x l

Removing duplicates in lists

union-list :
  {l1 : Level} {A : UU l1} 
  has-decidable-equality A 
  list A  list A  list A
union-list d nil l' = l'
union-list d (cons x l) l' with (elem-list d x l')
... | true = l'
... | false = cons x l'


If a list has an element then it is non empty

is-nonnil-elem-list :
  {l : Level} {A : UU l} 
  (d : has-decidable-equality A) 
  (a : A) 
  (l : list A) 
  elem-list d a l  true 
  is-nonnil-list l
is-nonnil-elem-list d a nil ()
is-nonnil-elem-list d a (cons x l) p ()

If the union of two lists is empty, then these two lists are empty

is-nil-union-is-nil-list :
  {l : Level} {A : UU l} 
  (d : has-decidable-equality A) 
  (l l' : list A) 
  union-list d l l'  nil 
  is-nil-list l × is-nil-list l'
is-nil-union-is-nil-list d nil l' p = (refl , p)
is-nil-union-is-nil-list d (cons x l) l' p with (elem-list d x l') in q
... | true =
  ex-falso (is-nonnil-elem-list d x l' q p)
    -- ( is-nonnil-elem-list d x l' q
    --   (pr2 (is-nil-union-is-nil-list d l l' p)))
... | false = ex-falso (is-nonnil-cons-list x l' p)
    -- (is-nonnil-cons-list x (union-list d l l') p)

Recent changes