[Agda] Instance arguments and types who have a unique construction.

[Apostolis Xekoukoulotakis]

I think I understand what you mean.

Let me see if I can prune my context then.

On Thu, Jan 11, 2018 at 11:37 AM, Ulf Norell <ulf.norell at gmail.com> wrote:

> The more fundamental problem here is that it does actually matter which
> solution we
> pick when they aren't definitionally equal, even in the case when they are
> provable equal.
> It might well be the case that picking `q` is the right choice and picking
> `z≤s` is wrong and
> doing so would result in a type error further down in the code.
>
> / Ulf
>
> On Thu, Jan 11, 2018 at 10:28 AM, Apostolis Xekoukoulotakis <
> apostolis.xekoukoulotakis at gmail.com> wrote:
>
>> I do not know.
>>
>> From a use case point of view, I would like to provide a proof that all
>> construction of a type are equal.
>>
>> "∀ x y → (a : x ≤ y) → (b : x ≤ y) → a ≡ b" , and then use this proof to
>> merge all solutions into one.
>>
>> Is this possible today ?
>>
>>
>> On Thu, Jan 11, 2018 at 11:20 AM, Ulf Norell <ulf.norell at gmail.com>
>> wrote:
>>
>>> Instance search does check solutions for *definitional* equality. The
>>> problem in your case is that `q` is only propositionally (provably) equal
>>> to `z≤n`. I think it's a bit too much to ask of instance search that it
>>> would look for proofs that two candidate solutions are equal.
>>>
>>> Did you have a particular suggestion for what kind of smartness
>>> improvement would make this work?
>>>
>>> / Ulf
>>>
>>> On Thu, Jan 11, 2018 at 10:03 AM, Apostolis Xekoukoulotakis <
>>> apostolis.xekoukoulotakis at gmail.com> wrote:
>>>
>>>> Currently, instance resolution tries all possible ways to construct an
>>>> instance argument.
>>>>
>>>> It will look for arguments in the environment and it will use instance
>>>> functions to create new ones. If there are multiple solutions, instance
>>>> resolution will fail.
>>>>
>>>> example :
>>>>
>>>> Assuming we have defined "less than" as instance.
>>>>
>>>> if we have in the context, a variable q with type zero ≤ (suc zero) ,
>>>> instance resolution will fail because there are two solutions, q and z≤n.
>>>>
>>>> But q is in fact z≤n.
>>>>
>>>>
>>>> We can prove that there is only one possible construction of the type,
>>>> thus any variables with the same type are the same.
>>>>
>>>> At the moment, I am trying to prune my context but it would be nice if
>>>> instance resolution was a bit smarter.
>>>>
>>>> _______________________________________________
>>>> Agda mailing list
>>>> Agda at lists.chalmers.se
>>>> https://lists.chalmers.se/mailman/listinfo/agda
>>>>
>>>>
>>>
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180111/017c53be/attachment.html>