<div dir="ltr"><div class="gmail_extra"><div class="gmail_quote">On Fri, Jul 28, 2017 at 12:13 PM, Sergei Meshveliani <span dir="ltr"><<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">People,<br>
<br>
I try to accompany divmod-unique of Agda prelude with a certain<br>
congruence:<br>
<br>
  DivMod-cong :  ∀ {a a' b b'} → a ≡ a' → b ≡ b' → (d  : DivMod a  b ) →<br>
                                                   (d' : DivMod a' b') →<br>
                                       quot d ≡ quot d' × rem d ≡ rem d'<br>
<br>
<br>
1) Has Agda prelude something close to it?<br></blockquote><div><br></div><div>Yes, divmod-unique (which you are actually using in your proof). Simply match on the equality proofs and you can apply it:</div><div><br></div><div><div>DivMod-cong' :  ∀ {a a' b b'} → a ≡ a' → b ≡ b' → (d  : DivMod a  b ) →</div><div>                                                 (d' : DivMod a' b') →</div><div>                                     quot d ≡ quot d' × rem d ≡ rem d'</div><div>DivMod-cong' refl refl d d' = divmod-unique d d'</div></div><div><br></div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
2) I wonder: how to fix the below implementation?<br>
   Agda reports that  eq  is not of the declared type<br>
   (and I think that it is).<br></blockquote><div><br></div><div>The problem is that the type of eq is using the product from agda-prelude and you are expecting the one from the standard library. You should have no trouble converting between them.<br></div><div><br></div><div>/ Ulf</div><div><br></div></div></div></div>