Problem.agda

module Problem where

data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x

trans : {A : Set}{x y z : A} → x ≡ y → y ≡ z → x ≡ z
trans refl refl = refl

sym : {A : Set}{x y : A} → x ≡ y → y ≡ x
sym refl = refl

_~_ : {A : Set}{x y z : A} → x ≡ y → y ≡ z → x ≡ z
_~_ = trans
infixr 3 _~_

data Bool : Set where
  true : Bool
  false : Bool

data ℕ : Set where
  z : ℕ
  s : ℕ → ℕ

_+_ : ℕ → ℕ → ℕ
z + m = m
s n + m = s (n + m)

infixl 60 _*_
infixl 40 _+_

_*_ : ℕ → ℕ → ℕ
z * m = z
s n * m = m + n * m

data [_]₀ (A : Set) : ℕ → Set where
  [] : [ A ]₀ z
  _∷_ : {n : ℕ} → A → [ A ]₀ n → [ A ]₀ (s n)

cong : {A : Set}{B : Set}{x y : A} (f : A → B) → x ≡ y → f x ≡ f y
cong f refl = refl

lemma-succ : (n m : ℕ) → (s n) + m ≡ s (n + m)
lemma-succ n m = refl

n+0=n : (n : ℕ) → n + z ≡ n
n+0=n z = refl
n+0=n (s n) = lemma-succ n z ~ cong s (n+0=n n)

n+sm=sn+m : (n m : ℕ) → n + s m ≡ s n + m
n+sm=sn+m z m = refl
n+sm=sn+m (s n) m = lemma-succ n (s m) ~ cong s (n+sm=sn+m n m) ~ refl

n+sm=s[n+m] : (n m : ℕ) → n + s m ≡ s (n + m)
n+sm=s[n+m] z m = refl
n+sm=s[n+m] (s n) m = lemma-succ n (s m) ~ cong s (n+sm=s[n+m] n m)

reverse' : {A : Set}{n m : ℕ} → [ A ]₀ n → [ A ]₀ m → [ A ]₀ (n + m)
reverse' [] ys = ys
reverse' {n = s n}{m = m} (x ∷ xs) ys with reverse' xs (x ∷ ys)
... | result with n+sm=s[n+m] n m
... | refl = ?