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

[Andrea Vezzosi]

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.

Cheers,
Andrea

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