```
{-# OPTIONS --cubical-compatible #-}
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: Replication and snocking

The following lemma will prove useful in verifying that [Markov's
principle fails in some mathematical
universes](Padova2025.Explorations.Forcing.Cohen.html#markovs-principle).

```
replicate-snoc : {A : Set} (n : ℕ) (x : A) → x ∷ replicate n x ≡ replicate n x ∷ʳ x
replicate-snoc = {!!}
```


## Exercise: Snocking and concatenation

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

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

## Exercise: Length after snocking

```
length-snoc : {A : Set} (xs : List A) (y : A) → length (xs ∷ʳ y) ≡ succ (length xs)
length-snoc = {!!}
```


## Exercise: Empty list neutral for concatenation

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