bluescreen303 · February 13, 2013 19:46
diff --git a/hello2.agda b/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 ▸ ε)!}
	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 ▸ ε)!}