Martin Escardo, January 2021. It is possible to work with lists *defined* from the ingredients of our Spartan MLTT (see the module Fin.lagda). For the moment we are Athenian in this respect. \begin{code} {-# OPTIONS --safe --without-K #-} -- --exact-split module MLTT.List where open import MLTT.Spartan open import MLTT.Bool open import Naturals.Properties data List {𝓤} (X : 𝓤 ̇ ) : 𝓤 ̇ where [] : List X _∷_ : X → List X → List X infixr 3 _∷_ {-# BUILTIN LIST List #-} length : {X : 𝓤 ̇ } → List X → ℕ length [] = 0 length (x ∷ xs) = succ (length xs) Vector' : 𝓤 ̇ → ℕ → 𝓤 ̇ Vector' X n = (Σ xs ꞉ List X , length xs ＝ n) _∷'_ : {X : 𝓤 ̇ } {n : ℕ} → X → Vector' X n → Vector' X (succ n) x ∷' (xs , p) = (x ∷ xs) , ap succ p equal-heads : {X : 𝓤 ̇ } {x y : X} {s t : List X} → x ∷ s ＝ y ∷ t → x ＝ y equal-heads refl = refl equal-tails : {X : 𝓤 ̇ } {x y : X} {s t : List X} → x ∷ s ＝ y ∷ t → s ＝ t equal-tails {𝓤} {X} refl = refl [_] : {X : 𝓤 ̇ } → X → List X [ x ] = x ∷ [] []-is-not-cons : {X : 𝓤 ̇ } (x : X) (xs : List X) → [] ≠ x ∷ xs []-is-not-cons x [] () []-is-not-cons x (x₀ ∷ xs) () _++_ : {X : 𝓤 ̇ } → List X → List X → List X [] ++ t = t (x ∷ s) ++ t = x ∷ (s ++ t) infixr 4 _++_ []-right-neutral : {X : 𝓤 ̇ } (s : List X) → s ＝ s ++ [] []-right-neutral [] = refl []-right-neutral (x ∷ s) = ap (x ∷_) ([]-right-neutral s) ++-assoc : {X : 𝓤 ̇ } → associative (_++_ {𝓤} {X}) ++-assoc [] t u = refl ++-assoc (x ∷ s) t u = ap (x ∷_) (++-assoc s t u) foldr : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } → (X → Y → Y) → Y → List X → Y foldr _·_ ε [] = ε foldr _·_ ε (x ∷ xs) = x · foldr _·_ ε xs map : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } → (X → Y) → List X → List Y map f [] = [] map f (x ∷ xs) = f x ∷ map f xs _<$>_ = map empty : {𝓤 : Universe} {X : 𝓤 ̇ } → List X → Bool empty [] = true empty (x ∷ xs) = false data member {X : 𝓤 ̇ } : X → List X → 𝓤 ̇ where in-head : {x : X} {xs : List X} → member x (x ∷ xs) in-tail : {x y : X} {xs : List X} → member x xs → member x (y ∷ xs) member-map : {X Y : Type} (f : X → Y) (x : X) (xs : List X) → member x xs → member (f x) (map f xs) member-map f x' (_ ∷ _) in-head = in-head member-map f x' (_ ∷ xs) (in-tail m) = in-tail (member-map f x' xs m) member' : {X : Type} → X → List X → Type member' y [] = 𝟘 member' y (x ∷ xs) = (x ＝ y) + member y xs member'-map : {X Y : Type} (f : X → Y) (x : X) (xs : List X) → member' x xs → member' (f x) (map f xs) member'-map f x' (x ∷ xs) (inl p) = inl (ap f p) member'-map f x' (x ∷ xs) (inr m) = inr (member-map f x' xs m) listed : Type → Type listed X = Σ xs ꞉ List X , ((x : X) → member x xs) listed⁺ : Type → Type listed⁺ X = X × listed X type-from-list : {X : Type} → List X → Type type-from-list {X} xs = Σ x ꞉ X , member x xs type-from-list-is-listed : {X : Type} (xs : List X) → listed (type-from-list xs) type-from-list-is-listed {X} [] = [] , g where g : (σ : type-from-list []) → member σ [] g (x , ()) type-from-list-is-listed {X} (x ∷ xs) = g where h : (x : X) → type-from-list (x ∷ xs) h x = x , in-head t : type-from-list xs → type-from-list (x ∷ xs) t (x , m) = x , in-tail m α : List (type-from-list xs) → List (type-from-list (x ∷ xs)) α σs = h x ∷ map t σs β : ((σs , μ) : listed (type-from-list xs)) → (τ : type-from-list (x ∷ xs)) → member τ (α σs) β (σs , μ) (y , in-head) = in-head β (σs , μ) (y , in-tail m) = in-tail (member-map t (y , m) σs (μ (y , m))) f : listed (type-from-list xs) → listed (type-from-list (x ∷ xs)) f (σs , μ) = α σs , β (σs , μ) g : listed (type-from-list (x ∷ xs)) g = f (type-from-list-is-listed xs) module _ {X : 𝓤 ̇ } where delete : {n : ℕ} {y : X} ((xs , _) : Vector' X (succ n)) → member y xs → Vector' X n delete {0} _ in-head = [] , refl delete {0} _ (in-tail _) = [] , refl delete {succ _} ((_ ∷ xs) , p) in-head = xs , succ-lc p delete {succ n} ((x ∷ xs) , p) (in-tail m) = x ∷' delete {n} (xs , succ-lc p) m module list-util {𝓤 : Universe} {X : 𝓤 ̇ } {{_ : Eq X}} where _is-in_ : X → List X → Bool x is-in [] = false x is-in (y ∷ ys) = (x == y) || (x is-in ys) insert : X → List X → List X insert x xs = x ∷ xs _contained-in_ : List X → List X → Bool [] contained-in ys = true (x ∷ xs) contained-in ys = (x is-in ys) && (xs contained-in ys) contained-lemma₀ : (x z : X) (xs ys : List X) → ys contained-in (x ∷ xs) ＝ true → ys contained-in (x ∷ z ∷ xs) ＝ true contained-lemma₀ x z xs [] e = e contained-lemma₀ x z xs (y ∷ ys) e = γ where IH : ys contained-in (x ∷ xs) ＝ true → ys contained-in (x ∷ z ∷ xs) ＝ true IH = contained-lemma₀ x z xs ys e₁ : (y == x) || (y is-in xs) ＝ true e₁ = pr₁ (&&-gives-× e) e₂ : ys contained-in (x ∷ xs) ＝ true e₂ = pr₂ (&&-gives-× e) a : (y == x) || ((y == z) || (y is-in xs)) ＝ true a = Cases (||-gives-+ e₁) (λ (e : (y == x) ＝ true) → ||-left-intro ((y == z) || (y is-in xs)) e) (λ (e : y is-in xs ＝ true) → ||-right-intro {y == x} ((y == z) || (y is-in xs)) (||-right-intro (y is-in xs) e)) b : ys contained-in (x ∷ z ∷ xs) ＝ true b = IH e₂ γ : ((y == x) || ((y == z) || (y is-in xs))) && (ys contained-in (x ∷ z ∷ xs)) ＝ true γ = &&-intro a b contained-lemma₁ : (x : X) (ys : List X) → ys contained-in (x ∷ ys) ＝ true contained-lemma₁ x [] = refl contained-lemma₁ x (y ∷ ys) = γ where IH : ys contained-in (x ∷ ys) ＝ true IH = contained-lemma₁ x ys a : y == x || (y == y || (y is-in ys)) ＝ true a = ||-right-intro {y == x} ((y == y) || (y is-in ys)) (||-left-intro (y is-in ys) (==-refl y)) b : ys contained-in (x ∷ y ∷ ys) ＝ true b = contained-lemma₀ x y ys ys IH γ : (y == x || (y == y || (y is-in ys))) && (ys contained-in (x ∷ y ∷ ys)) ＝ true γ = &&-intro a b some-contained : List (List X) → List X → Bool some-contained [] ys = false some-contained (xs ∷ xss) ys = xs contained-in ys || some-contained xss ys remove-first : X → List X → List X remove-first x [] = [] remove-first x (y ∷ ys) = if x == y then ys else (y ∷ remove-first x ys) remove-all : X → List X → List X remove-all x [] = [] remove-all x (y ∷ ys) = if x == y then remove-all x ys else (y ∷ remove-all x ys) _minus_ : List X → List X → List X xs minus [] = xs xs minus (y ∷ ys) = (remove-all y xs) minus ys \end{code} Remove first occurrence: \begin{code} remove : X → List X → List X remove x [] = [] remove x (y ∷ ys) = if x == y then ys else (y ∷ remove x ys) remove-head : (x y : X) (ys : List X) → (x == y) ＝ true → remove x (y ∷ ys) ＝ ys remove-head x y ys q = remove x (y ∷ ys) ＝⟨ refl ⟩ (if x == y then ys else (y ∷ remove x ys)) ＝⟨ I ⟩ (if true then ys else (y ∷ remove x ys)) ＝⟨ refl ⟩ ys ∎ where I = ap (λ - → if - then ys else (y ∷ remove x ys)) q remove-tail : (x y : X) (ys : List X) → (x == y) ＝ false → remove x (y ∷ ys) ＝ y ∷ remove x ys remove-tail x y ys q = remove x (y ∷ ys) ＝⟨ refl ⟩ if x == y then ys else (y ∷ remove x ys) ＝⟨ I ⟩ if false then ys else (y ∷ remove x ys) ＝⟨ refl ⟩ y ∷ remove x ys ∎ where I = ap (λ - → if - then ys else (y ∷ remove x ys)) q remove-length : (x : X) (ys : List X) → member x ys → (n : ℕ) → length ys ＝ succ n → length (remove x ys) ＝ n remove-length x ys@(z ∷ zs) m n p = h m n p (x == z) refl where h : member x ys → (n : ℕ) → length ys ＝ succ n → (b : Bool) → (x == z) ＝ b → length (remove x ys) ＝ n h _ n p true q = length (remove x (z ∷ zs)) ＝⟨ ap length (remove-head x z zs q) ⟩ length zs ＝⟨ succ-lc p ⟩ n ∎ h in-head n p false q = 𝟘-elim (true-is-not-false (true ＝⟨ (==-refl x)⁻¹ ⟩ (x == x) ＝⟨ q ⟩ false ∎)) h (in-tail in-head) 0 () false q h (in-tail (in-tail m)) 0 () false q h (in-tail m) (succ n) p false q = length (remove x (z ∷ zs)) ＝⟨ I ⟩ length (z ∷ remove x zs) ＝⟨ refl ⟩ succ (length (remove x zs)) ＝⟨ II ⟩ succ n ∎ where I = ap length (remove-tail x z zs q) II = ap succ (remove-length x zs m n (succ-lc p)) delete' : {n : ℕ} (x : X) ((xs , _) : Vector' X (succ n)) → member x xs → Vector' X n delete' {n} x (xs , p) m = remove x xs , remove-length x xs m n p \end{code}