[Agda] Re: How can I prove associativity of vectors?

[Sergei Meshveliani]

On Wed, 2014-12-17 at 20:38 +0100, Andrea Vezzosi wrote:
> The following seems to work:
> 
> open import Data.Nat
> open import Data.Vec
> open import Relation.Binary.PropositionalEquality
> 
> postulate
>   x y : ℕ
>   x=y : x ≡ y
> 
> to : Vec ℕ x → Vec ℕ y
> to = subst (Vec ℕ) x=y
> 
> from = subst (Vec ℕ) (sym x=y)
> 
> [..]


Thank you for explanation. 
`subst' occurs more generic than I used to think of it.

I rewrite your code into this:

 vecCong-iso :  ∀ {A : Set} → ∀ {m n} → m ≡ n → Vec A m → Vec A n
 vecCong-iso {A} =  PE.subst (Vec A)

I think, this expresses that  (Vec A)  preserves _≡_ respectively to the
domain (type) identity.
Its usage for  Vec ℕ (m + n) and Vec ℕ (n + m)  is like this:

-------------------------------------
module _ (m n : ℕ)
  where
  Vec1 : Set _
  Vec1 = Vec ℕ (m + n)

  Vec2 : Set _
  Vec2 = Vec ℕ (n + m)

  v2-to-v1 : Vec2 → Vec1
  v2-to-v1 = vecCong-iso (+-comm n m)
--------------------------------------

And the whole situation is as follows.

1) There are many type expressions that rewrite nontrivially to  Vec1,  
   for example,  Vec ℕ ((m + n) + 0).

I think,  vecCong-iso  is a generic way to obtain the isomorphism needed
in each such case (it needs to combine with the corresponding equality
proof for the expressions in Nat).

2) In mathematics,  Vec A m  and  Vec A n  is the _same_ domain if  
   m ≡ n.
And in the current Agda, we need to 
a) pretend that they are different and mutually isomorphic,
b) to use  vecCong-iso  for the needed isomorphism.

3) People are talking of rewriting rule machine 
   (to incorporate into the type checker?) 
which will make Agda consider these two domains (type) as the same
domain. 
Right? 

4) On practice, the situation is usually more generic, it is as follows.
A programmer has  
a) a type constructor  Cons  taking a value parameter  p,
b) p usually comes from some Setoid S,
c) for any  p ≈ p'  (is this called a definitional equality?),
   (Cons p) and (Cons p')  need to be considered as the same domain.

Will incorporating rewriting rule machine help this?

Regards,

------
Sergei