[Agda] Problem with reversing vector

[Lyndon Maydwell]

Thanks so much Dominique.

That's very helpful.

On Fri, Jun 15, 2012 at 6:24 PM, Dominique Devriese
<dominique.devriese at cs.kuleuven.be> wrote:
> Lyndon,
>
> Yes, one solution is to prove this fact about natural numbers. You can
> construct such a proof using the standard library:
>
> 2012/6/15 Lyndon Maydwell <maydwell at gmail.com>:
>> vrev (y ► ys) = vconcat (vrev ys) (y ► ε)
>
>  open import Data.Nat.Properties
>  open import Relation.Binary.PropositionalEquality
>  open import Algebra.Structures
>  open import Function
>
>  open IsCommutativeSemiring isCommutativeSemiring using (+-comm)
>
>  {- ... -}
>
>  vrev {A} {suc n} (y ► ys) = subst (Vec _) (+-comm _ 1) $ vconcat
> (vrev ys) (y ► ε)
>
> However, such casts are a bit unnice, and they typically get in your
> way when proving properties of vrev. There are sometimes better
> ways to organise your code that allow you to avoid casts. For
> example, if you look in the standard library in Data.Vec, you can find
> a cleaner way to make everything work (translated to your naming):
>
>  foldl : ∀ {b} {A : Set} (B : ℕ → Set b) {m} →
>          (∀ {n} → B n → A → B (suc n)) →
>          B zero →
>          Vec A m → B m
>  foldl b _⊕_ n ε       = n
>  foldl b _⊕_ n (x ► xs) = foldl (λ n → b (suc n)) _⊕_ (n ⊕ x) xs
>
>  reverse : {A : Set} → {n : ℕ} → Vec A n → Vec A n
>  reverse {A} = foldl (Vec A) (flip _►_) ε
>
> You might exploit the same strategy directly, by defining a version of
> Data.Nat._+_ that has a different recursion structure:
>
>  reverse : {A : Set} → {n : ℕ} → Vec A n → Vec A n
>  reverse {A} = go 0 (flip _►_) ε
>    where _+′_ : ℕ → ℕ → ℕ
>          x +′ zero = x
>          x +′ suc y = suc x +′ y
>
>          go : ∀ m {n} {A : Set} →
>               (∀ {n} → Vec A (n +′ m) → A → Vec A (n +′ suc m)) →
>               Vec A (0 +′ m) →
>               Vec A n → Vec A (n +′ m)
>          go m _⊕_ n ε       = n
>          go m _⊕_ n (x ► xs) = go (suc m) _⊕_ (n ⊕ x) xs
>
> A crucial point here is that while folding, the type of _⊕_ changes to
> keep track of the current length of the accumulator. I mean that after
> m iterations of foldl, _⊕_'s type will amount to something like
>  (∀ {n} → Vec A (m +′ n) → A → Vec A (m +′ suc n))
> where the type of _►_ would be hard to work with:
>  (∀ {n} → Vec A n → A → Vec A (suc n))
>
> Note also that the recursion structure of _+′_ that we had to define
> internally is the same as the recursion structure of the indices of
> the vectors in the recursion of go (i.e. we shift one element from the
> iteratee to the accumulator each time, so indices (m, suc b) are
> turned into indices (suc m, n)).
>
> Anyway, the point is that you can sometimes avoid casts like the subst
> call above by organizing your code in the best way. This best way may
> be hard to find though..
>
> Dominique