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

[Sergei Meshveliani]

On Wed, 2014-12-17 at 21:32 +0400, Sergei Meshveliani wrote:
> 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 tried this:

  aux : {k : ℕ} → Vec ℕ (k + 0) → Vec ℕ k
  aux {0}     v        = v
  aux {suc k} (x ∷ xs) = u  where  u : Vec ℕ (suc k)
       	       	       	       	   u = x ∷ (aux {k} xs)

  iso : Vec2 → Vec1
  iso = go n m
    where
    go : (k : ℕ) → (l : ℕ) → Vec ℕ (k + l) → Vec ℕ (l + k)
    go k 0       v        =  aux {k} v
   
This works!
But the next pattern

    go k (suc l) (x ∷ xs) =  

needs some further invention. Really, is this so complex?

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
> > 
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>