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

[Andrea Vezzosi]

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)

IsIso1 : ∀ {x} → from (to x) ≡ x
IsIso1 rewrite x=y = refl

IsIso2 : ∀ {x} → to (from x) ≡ x
IsIso2 rewrite x=y = refl



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