[Agda] divmod-unique of Agda prelude

[Ulf Norell]

On Fri, Jul 28, 2017 at 12:13 PM, Sergei Meshveliani <mechvel at botik.ru>
wrote:

> People,
>
> I try to accompany divmod-unique of Agda prelude with a certain
> congruence:
>
>   DivMod-cong :  ∀ {a a' b b'} → a ≡ a' → b ≡ b' → (d  : DivMod a  b ) →
>                                                    (d' : DivMod a' b') →
>                                        quot d ≡ quot d' × rem d ≡ rem d'
>
>
> 1) Has Agda prelude something close to it?
>

Yes, divmod-unique (which you are actually using in your proof). Simply
match on the equality proofs and you can apply it:

DivMod-cong' :  ∀ {a a' b b'} → a ≡ a' → b ≡ b' → (d  : DivMod a  b ) →
                                                 (d' : DivMod a' b') →
                                     quot d ≡ quot d' × rem d ≡ rem d'
DivMod-cong' refl refl d d' = divmod-unique d d'



> 2) I wonder: how to fix the below implementation?
>    Agda reports that  eq  is not of the declared type
>    (and I think that it is).
>

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.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170728/de821415/attachment.html>