{-# 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.

Exercise 1reverse-∷ʳ

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

The reference solution uses: [] refl cong

Your solution

Reference solution

reverse-∷ʳ : {A : Set} (ys : List A) (x : A) → reverse (ys ∷ʳ x) ≡ (x ∷ reverse ys)
reverse-∷ʳ []       x = refl
reverse-∷ʳ (y ∷ ys) x = cong (λ zs → zs ∷ʳ y) (reverse-∷ʳ ys x)

Exercise 2reverse-reverse

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

The reference solution uses: [] refl _∷_ trans reverse-∷ʳ cong

Your solution

Reference solution

reverse-reverse : {A : Set} (xs : List A) → reverse (reverse xs) ≡ xs
reverse-reverse [] = refl
reverse-reverse (x ∷ xs) =
  trans (reverse-∷ʳ (reverse xs) x) (cong (x ∷_) (reverse-reverse xs))

Exercise: Associativity of concatenation#

Exercise 3++-assoc

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

The reference solution uses: [] refl _∷_ cong

Your solution

Reference solution

++-assoc : {A : Set} (xs ys zs : List A) → (xs ++ ys) ++ zs ≡ xs ++ (ys ++ zs)
++-assoc []       ys zs = refl
++-assoc (x ∷ xs) ys zs = cong (x ∷_) (++-assoc xs ys zs)

Exercise: Length as a homomorphism#

Exercise 4length-homo

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

The reference solution uses: [] refl _∷_ cong succ

Your solution

Reference solution

length-homo : {A : Set} (xs ys : List A) → length (xs ++ ys) ≡ length xs + length ys
length-homo []       ys = refl
length-homo (x ∷ xs) ys = cong succ (length-homo xs ys)

Exercise: Replication as a natural transformation#

Exercise 5replicate-natural

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

The reference solution uses: zero refl succ cong

Your solution

Reference solution

replicate-natural
  : {A B : Set} (f : A → B) (n : ℕ) (x : A)
  → map f (replicate n x) ≡ replicate n (f x)
replicate-natural f zero     x = refl
replicate-natural f (succ n) x = cong (f x ∷_) (replicate-natural f n x)

Exercise: Replication and snocking#

The following lemma will prove useful in verifying that Markov’s principle fails in some mathematical universes.

Exercise 6replicate-snoc

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

The reference solution uses: zero refl succ cong

Your solution

Reference solution

replicate-snoc : {A : Set} (n : ℕ) (x : A) → x ∷ replicate n x ≡ replicate n x ∷ʳ x
replicate-snoc zero     x = refl
replicate-snoc (succ n) x = cong (x ∷_) (replicate-snoc n x)

Exercise: Snocking and concatenation#

Exercise 7snoc-++

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

The reference solution uses: [] refl cong

Your solution

Reference solution

snoc-++ : {A : Set} (a : A) (xs ys : List A) → (xs ∷ʳ a) ++ ys ≡ xs ++ (a ∷ ys)
snoc-++ a []       ys = refl
snoc-++ a (x ∷ xs) ys = cong (x ∷_) (snoc-++ a xs ys)

Exercise 8++-snoc

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

The reference solution uses: [] refl _∷_ cong

Your solution

Reference solution

++-snoc : {A : Set} (a : A) (xs ys : List A) → xs ++ (ys ∷ʳ a) ≡ (xs ++ ys) ∷ʳ a
++-snoc a []       ys = refl
++-snoc a (x ∷ xs) ys = cong (x ∷_) (++-snoc a xs ys)

Exercise: Length after snocking#

Exercise 9length-snoc

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

The reference solution uses: [] refl _∷_ cong

Your solution

Reference solution

length-snoc : {A : Set} (xs : List A) (y : A) → length (xs ∷ʳ y) ≡ succ (length xs)
length-snoc []       y = refl
length-snoc (x ∷ xs) y = cong succ (length-snoc xs y)

Exercise: Empty list neutral for concatenation#

Exercise 10++-[]

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

The reference solution uses: refl _∷_ cong

Your solution

Reference solution

++-[] : {A : Set} (xs : List A) → xs ++ [] ≡ xs
++-[] []       = refl
++-[] (x ∷ xs) = cong (x ∷_) (++-[] xs)