module Padova2025.ProvingBasics.Equality.Lists where

Results on lists

open import Padova2025.ProgrammingBasics.Naturals.Base
open import Padova2025.ProgrammingBasics.Naturals.Arithmetic
open import Padova2025.ProgrammingBasics.Lists
open import Padova2025.ProvingBasics.Equality.Base
open import Padova2025.ProvingBasics.Equality.General

Exercise: Double reverse

For the following exercise, note that reverse (x ∷ xs) is defined as reverse xs ∷ʳ x.

reverse-∷ʳ : {A : Set} (ys : List A) (x : A) → reverse (ys ∷ʳ x) ≡ (x ∷ reverse ys)
reverse-∷ʳ = {!!}

reverse-reverse : {A : Set} (xs : List A) → reverse (reverse xs) ≡ xs
reverse-reverse = {!!}

Exercise: Associativity of concatenation

++-assoc : {A : Set} (xs ys zs : List A) → (xs ++ ys) ++ zs ≡ xs ++ (ys ++ zs)
++-assoc = {!!}

Exercise: Length as a homomorphism

length-homo : {A : Set} (xs ys : List A) → length (xs ++ ys) ≡ length xs + length ys
length-homo = {!!}

Exercise: Replication as a natural transformation

replicate-natural
  : {A B : Set} (f : A → B) (n : ℕ) (x : A)
  → map f (replicate n x) ≡ replicate n (f x)
replicate-natural = {!!}

Exercise: Snocking and concatenation

snoc-++ : {A : Set} (a : A) (xs ys : List A) → (xs ∷ʳ a) ++ ys ≡ xs ++ (a ∷ ys)
snoc-++ = {!!}

Exercise: Empty list neutral for concatenation

++-[] : {A : Set} (xs : List A) → xs ++ [] ≡ xs
++-[] = {!!}