First steps with agda

hello2.agda

module hello2 where

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

one : ℕ
one = suc zero



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

infixr 90 _∘∘_
_∘∘_ : {A : Set} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
refl ∘∘ refl = refl

-- dunno the mathemetical name for these
succed : ∀ {a b} → a ≡ b → suc a ≡ suc b
succed refl = refl

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



-- This is the opposite argument order compared to the standard agda definition
-- But I wanted to follow the wikipedia article as closely as possible
-- http://en.wikipedia.org/wiki/Proofs_involving_the_addition_of_natural_numbers
_+_ : ℕ → ℕ → ℕ
a + zero  = a             -- A1
a + suc b = suc (a + b)   -- A2

infixl 60 _+_

-- base observations (using A1 ∧ A2)
base-step1 : ∀ {a} → suc a ≡ suc (a + zero)
base-step1 = refl

base-step2 : ∀ {a} → suc (a + zero) ≡ a + suc zero
base-step2 = refl

base-step3 : ∀ {a} → a + suc zero ≡ a + one
base-step3 = refl

-- probably misnamed
prefixed : ∀ {x y b} → x ≡ y → b + x ≡ b + y
prefixed refl = refl

-- associativity
assoc : ∀ a b c → (a + b) + c ≡ a + (b + c)
assoc _ _ zero    = refl
assoc _ _ (suc d) = succed (assoc _ _ d)

-- identity element
identity : ∀ a → zero + a ≡ a
identity zero    = refl
identity (suc a) = succed (identity a)

-- commutativity
commutativity : ∀ n m → n + m ≡ m + n
commutativity n zero       = rev (identity n)
commutativity a (suc b)    = succed (commutativity a b) ∘∘ prefixed (1-commutes a) ∘∘ rev (assoc b one a)
  where 1-commutes : ∀ n → n + one ≡ one + n
        1-commutes zero = refl
        1-commutes (suc n) = succed (1-commutes n)

        commute-step1 : ∀ a b → a + suc b ≡ a + (b + one)
        commute-step1 a b = refl
        
        commute-step2 : ∀ a b → a + (b + one) ≡ (a + b) + one
        commute-step2 a b = refl
        
        commute-step3 : ∀ a b → (a + b) + one ≡ (b + a) + one
        commute-step3 a b = succed (commutativity a b)
        
        commute-step4 : ∀ a b → (b + a) + one ≡ b + (a + one)
        commute-step4 a b = refl

        commute-step5 : ∀ a b → b + (a + one) ≡ b + (one + a)
        commute-step5 a b = prefixed (1-commutes a)
        
        commute-step6 : ∀ a b → b + (one + a) ≡ (b + one) + a
        commute-step6 a b = rev (assoc b one a)
        
        commute-step7 : ∀ a b → (b + one) + a ≡ suc b + a
        commute-step7 a b = refl



data Vector (A : Set) : ℕ → Set where
  ε   : Vector A zero
  _▸_ : {n : ℕ} → A → Vector A n → Vector A (suc n)

infixr 50 _▸_

vLength : {A : Set} → {n : ℕ} → Vector A n → ℕ
vLength {_} {n} v = n

vMap : {A B : Set} → {n : ℕ} → (A → B) → Vector A n → Vector B n
vMap fn ε        = ε
vMap fn (x ▸ x₁) = fn x ▸ vMap fn x₁

-- Here the result says n + m
-- I understand this is because of the way my + definition deconstructs and constructs the number
-- However, as I've proven that ℕ is commutative under addition, there must be some way to "apply" this proof
-- to get n and m swapped here
vConcat : {A : Set} {m n : ℕ} → Vector A m → Vector A n → Vector A (n + m)
vConcat ε ys = ys
vConcat (x ▸ xs) ys = x ▸ vConcat xs ys

-- I know I can use a definition that does not use vConcat (and hence the +)
-- However, this definition should be able to work too I assume.
-- However, the whole wants me to prove (suc zero + n ≡ suc n) which I think I have all the ingredients for
-- but once again I can't figure out how to use these proofs
vReverse : {A : Set} → {n : ℕ} → Vector A n → Vector A n
vReverse ε = ε
vReverse (x ▸ x₁) = {!vConcat (vReverse x₁) (x ▸ ε)!}