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

[Sergei Meshveliani]

On Wed, 2014-12-17 at 12:02 +0900, Kenichi Asai wrote:
> Thank you for the messages!  I could now implement it in two ways.
> 
> >  * Use Data.Vec.Equality rather than PropositionalEquality.
> [..]
> >  * Use Relation.Binary.HeterogeneousEquality rather than
> >    PropositionalEquality.
> [..]

> assoc : ∀ {l m n} → (l1 : Vec ℕ l) → (l2 : Vec ℕ m) → (l3 : Vec ℕ n) → 
>         (l1 ++ l2) ++ l3 ≅ l1 ++ (l2 ++ l3)
> assoc [] l2 l3 = refl
> assoc (x ∷ l1) l2 l3 = cong (λ l → x ∷ l) (assoc l1 l2 l3)
> 
> but it did not work, because cong appears to assume that two sides of
> ≅ has the same type.  Why is it so?  I think it is more natural that
> cong etc. in HeterogeneousEquality module are defined for heterogeneous
> types.
> [..]


People,
this whole feature looks like a point of disagreement of Agda to
mathematics.

In both areas, a domain can depend on a value, and can be treated as a
value (to a certain extent).

A mathematical computation and discourse can be as follows. 

  For all  k : Nat  define an additive semigroup on  (Vec Nat k)  
  with respect to the pointwise addition  _+l_  on vectors.

  Put      Vec1 = Vec Nat (m + n),   Vec2 = Vec Nat (m + n),
  and let  v  \in Vec1,              v' \in Vec2.

  Let us prove  m + n == n + m.
  ...
  All right, proved.

  Hence,  v and v'  belong to the _same_ domain  Vec1,  and to the same 
  additive semigroup H1. Hence it has sense the computation

    _+1_ = Semigroup._*_ H1;
    u    = v +1 v';

  and so on.

This discourse uses that _identity_ of domains respects the equality
_==_  on parameter values.     

And in a dependently typed language, one has:

  m + n == m + n  proved,  and still  v and v'  are of different 
  types (domains), and cannot be added by the semigroup operation _+1_.

In mathematics, the domain membership relation  v \in V(p)  can often be
proved or computed. And in a dependently typed language, the relation
v : V(p)  has somewhat a different nature, this is not of  (Rel _),  it
is a language construct.

I do not expect that this difference can be eliminated by some kind of
refining a language design.

And what a programmer has to do?

May be, one needs in each case to implement a certain appropriate
natural isomorpsims. In our example, this is  f : Vec2 -> Vec1,  
and to apply   v +1 (f v')  rather than  (v +1 v').
-- ?

Am I missing something?

Regards,

------
Sergei