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

[Jon Sterling]

Sergei,

On Wed, Dec 17, 2014, at 01:28 AM, Sergei Meshveliani 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_.
> 

With regard to this comment:

> 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.

It may be a digression from the point of this thread, but I'll note that
this is not an "essential" property of type theory. Type theories based
on Martin-Löf's 1986 logical framework presentation, such as the theory
underlying Agda, typically do not have a judgement "M in A" which means
"M is a member of domain A" but rather they have a proofhood judgement,
"M is a proof of A". In order for it to be meaningful, this judgement
must be analytic, so it cannot be proved, it can only be "known".

But other type theories, such as Computational Type Theory (Nuprl) which
expands on Martin-Löf's polymorphic type theory from the early 80s, do
not internally have a judgement like Agda's but instead have a judgement
"A ext M" which means "M is a witness for A" or "M is a realizer for A".
And this judgement behaves more like the domain membership relation
you're talking about, and it can be proved in the logical framework.

Common practice in the modern intensional LF presentation of type theory
(see Nordström for some examples, also Sambin, though their approaches
differ) is to overlay a "subset theory" on top of the theory.

> 
> 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

Kind regards,
Jon

> 
> 
> 
> 
>   
> 
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda