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

[Apostolis Xekoukoulotakis]

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/8060b0a7/attachment-0001.html>