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

[Frédéric Blanqui]

Termination and confluence.

Le 17/12/2014 16:34, Andrea Vezzosi a écrit :
> Hi,
>
> What kind of restrictions do these systems impose on the rewrite rules
> to keep equality checking decidable?
>
> Best,
> Andrea
>
> On Wed, Dec 17, 2014 at 4:21 PM, Frédéric Blanqui
> <frederic.blanqui at inria.fr> wrote:
>> 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
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda