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

[Sergei Meshveliani]

On Wed, 2014-12-17 at 16:19 +0100, Andrea Vezzosi wrote:
> The isomorphism you're talking about can be defined with "subst Vec p"
> where p : m + n == n + m.
> 
> it's not something very pleasing to have to do, but that's the state
> of the art in intensional type theory afaik.
> 
> the reduction behaviour of subst could be less "all or nothing" than
> what it is now though.


We need to replace        v +1 v'
with                      v +1 (iso v')

So, an isomorphism (call it `iso') needs to have signature

                         iso : Vec (n + m) -> Vec (m + n)

And if you mean   subst = Relation.Binary.PropositionalEquality.subst,

then `subst' just transmits the equality relation, and 

                  (subst Vec p)  

has not the needed signature. Has it?

This must be simple, but so far, I fail to implement  iso.

Can you, please, demonstrate?
 
I have never dealt with Vec. If is was defined as 
 
  Vec' : Set → ℕ → Set
  Vec' A n =  Σ (List A) (_≡_ n ∘ length),

this would be easier for me, I expect.

Regards,

------
Sergei




> On Wed, Dec 17, 2014 at 10:28 AM, Sergei Meshveliani <mechvel at botik.ru> wrote:
> > 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
> >
> >
> >
> >
> >
> >
> >
> >
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda
>