# [Agda] Proving m + (1 + n) == 1 + (m + n)

Jan Stolarek jan.stolarek at p.lodz.pl
Thu Oct 31 13:59:27 CET 2013

```Hi *,

I'm trying to figure out how to prove things like m + (1 + n) == 1 + (m + n) so that I can write
reverse-append function for vectors. I found materials for Computer Aided Formal Reasoning
(http://www.cs.nott.ac.uk/~txa/g53cfr/) to be quite accessible, but there are some things I don't
understand. Lecture 9 gives a proof of correctness for reverse-append:

_++'_ : {X : Set} {n m : ℕ} → Vec X n → Vec X m → Vec X (n + m)
_++'_ {X} {zero } {m} []       ys = ys
_++'_ {X} {suc n} {m} (x :: xs) ys =
subst (Vec X) (sym (+suc n  m)) (xs ++' (x :: ys))

where

+suc : (m n : ℕ) → suc (m + n) ≡ m + (suc n)
+suc zero n = refl
+suc (suc m) n = cong suc (+suc m n)

and cong, subst, refl and sym are imported from Relation.Binary.PropositionalEquality, Nat is from
Data.Nat and Vec is from Data.Vec. However, if remove import of PropositionalEquality and use
definitions of cong, subst, refl and sym that were given earlier in the course (lecture 7):

Prp : Set1
Prp = Set

data _==_ {A : Set} : A → A → Prp where
refl : {a : A} → a == a

sym : {A : Set} → {a b : A} → a == b → b == a
sym refl = refl

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

subst : {A : Set}{P : A → Prp} → {a b : A} → a == b → P a → P b
subst refl p = p

I get error when typechecking second case of _++'_. Typechecker higlights Vec X (first argument to
subst) and produces an error:

ℕ → Set !=< _a_55 n x xs ys ≡ _b_56 n x xs ys of type Set₁
when checking that the expression Vec X has type
_a_55 n x xs ys ≡ _b_56 n x xs ys

I can't figure out goes wrong here. I looked at the definitions of refl, sym and other functions
in standard library to see how they differ. I see that refl in std lib operates on other levels
than just Set. As for other functions thier definition in the library is too difficult for me to
understand. I would appreciate if someone could explain why the typechecker complains and how to
fix definitions of refl & friends so that it works.

Janek
```