<div dir="ltr">Have you tried to use irrelevance?<div>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.</div><div>I haven’t tried, so I don’t know if it interacts well with instance arguments.</div><div><br></div><div>Guillaume</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Jan 11, 2018 at 11:00 AM, Apostolis Xekoukoulotakis <span dir="ltr"><<a href="mailto:apostolis.xekoukoulotakis@gmail.com" target="_blank">apostolis.xekoukoulotakis@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div>I think I understand what you mean. <br><br></div>Let me see if I can prune my context then.<br></div><div class="HOEnZb"><div class="h5"><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Jan 11, 2018 at 11:37 AM, Ulf Norell <span dir="ltr"><<a href="mailto:ulf.norell@gmail.com" target="_blank">ulf.norell@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div><div><div><div>The more fundamental problem here is that it does actually matter which solution we<br></div>pick when they aren't definitionally equal, even in the case when they are provable equal.<br></div>It might well be the case that picking `q` is the right choice and picking `z≤s` is wrong and<br></div>doing so would result in a type error further down in the code.<span class="m_5801853662012490868HOEnZb"><font color="#888888"><br><br></font></span></div><span class="m_5801853662012490868HOEnZb"><font color="#888888">/ Ulf<br></font></span></div><div class="m_5801853662012490868HOEnZb"><div class="m_5801853662012490868h5"><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Jan 11, 2018 at 10:28 AM, Apostolis Xekoukoulotakis <span dir="ltr"><<a href="mailto:apostolis.xekoukoulotakis@gmail.com" target="_blank">apostolis.xekoukoulotakis@gma<wbr>il.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div><div>I do not know. <br><br></div>From a use case point of view, I would like to provide a proof that all construction of a type are equal.<br><br>"∀ x y → (a : x ≤ y) → (b : x ≤ y) → a ≡ b" , and then use this proof to merge all solutions into one.<br><br></div>Is this possible today ?<br><div><br></div></div><div class="m_5801853662012490868m_-6928079499170528997HOEnZb"><div class="m_5801853662012490868m_-6928079499170528997h5"><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Jan 11, 2018 at 11:20 AM, Ulf Norell <span dir="ltr"><<a href="mailto:ulf.norell@gmail.com" target="_blank">ulf.norell@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div><div>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.<br><br></div>Did you have a particular suggestion for what kind of smartness improvement would make this work?<br><br></div>/ Ulf<br></div><div class="gmail_extra"><br><div class="gmail_quote"><div><div class="m_5801853662012490868m_-6928079499170528997m_8922789605119647212h5">On Thu, Jan 11, 2018 at 10:03 AM, Apostolis Xekoukoulotakis <span dir="ltr"><<a href="mailto:apostolis.xekoukoulotakis@gmail.com" target="_blank">apostolis.xekoukoulotakis@gma<wbr>il.com</a>></span> wrote:<br></div></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div><div class="m_5801853662012490868m_-6928079499170528997m_8922789605119647212h5"><div dir="ltr"><div><div><div><div><div><div><div>Currently, instance resolution tries all possible ways to construct an instance argument.<br><br></div>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.<br><br></div>example :</div><div><br></div><div> Assuming we have defined "less than" as instance.<br><br></div>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.<br></div><br></div>But q is  in fact z≤n.<br><br><br></div>We can prove that there is only one possible construction of the type, thus any variables with the same type are the same.<br></div><div><br></div><div>At the moment, I am trying to prune my context but it would be nice if instance resolution was a bit smarter.<br></div></div>
<br></div></div>______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mail<wbr>man/listinfo/agda</a><br>
<br></blockquote></div><br></div>
</blockquote></div><br></div>
</div></div></blockquote></div><br></div>
</div></div></blockquote></div><br></div>
</div></div><br>______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
<br></blockquote></div><br></div>