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

[Frédéric Blanqui]

Hello.

Another alternative is to extend the congruence on types while keeping 
it decidable. For instance, it is possible to extend it with the 
equation (x+y)+z = x+(y+z) on ℕ, which is an inductive consequence of 
the definition of +. This is done for instance in:

- http://dedukti.gforge.inria.fr/ is a proof-checker for LF where the 
congruence on types includes non only beta-reduction but also 
user-defined rewrite rules, of which (x+y)+z -> x+(y+z) on ℕ is a 
particular case. Type-level rewriting is very powerful since it allows 
to encode any functional pure type systems (PTS) in LF + user-defined 
rewrite rules.

- http://pierre-yves.strub.nu/coqmt/ is an extension of Coq where the 
congruence on types in some context Gamma is extended with all the 
propositional consequences one can deduce from Gamma modulo some 
decidable theory like linear arithmetic, of which (x+y)+z = x+(y+z) on ℕ 
is a particular case.

Best regards,

Frédéric.

Le 17/12/2014 16:00, Jon Sterling a écrit :
> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda