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

[Andrea Vezzosi]

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