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

[Guillaume Brunerie]

Have you tried to use irrelevance?
As far as I understand, it does basically what you want, by somehow making
all elements of the type x ≤ y definitionally equal to each other.
I haven’t tried, so I don’t know if it interacts well with instance
arguments.

Guillaume

On Thu, Jan 11, 2018 at 11:00 AM, Apostolis Xekoukoulotakis <
apostolis.xekoukoulotakis at gmail.com> wrote:

> 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
>>>>>
>>>>>
>>>>
>>>
>>
>
> _______________________________________________
> 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/f7693a55/attachment.html>