<div dir="auto"><div>As Guillaume has already hinted at, the problem isn't with equality reasoning per se, it is, I believe, to do with unification. I have seen this problem whenever an equivalence _≈A_ on some type A is defined not as a separate data-type, but via a definition of the form</div><div dir="auto"><br></div><div dir="auto"> a <span style="font-family:sans-serif">≈A</span> b = f a ≈B f b</div><div dir="auto"><br></div><div dir="auto"><span style="font-family:sans-serif">where _≈B_ is an equivalence over some type B and f is a function/expression from B's to A's. Typical examples are where f is a projection or some computation involving B's. The definition of </span><span style="font-family:sans-serif">_</span><span style="font-family:sans-serif">≈A_ could also involve some pattern matching -- it doesn't matter, as long as it's not a data-type definition.</span><span style="font-family:sans-serif"> This is what Guillaume meant by defining _</span><span style="font-family:sans-serif">≈A_ via recursion (I think). Your explanation about =fr indicates that this is the case for you.</span></div><div dir="auto"><span style="font-family:sans-serif"><br></span></div><div dir="auto"><span style="font-family:sans-serif">I think what happens is that during unification/type checking, the definition of a ≈A b gets expanded and the original terms a and b are "computed away" so the unifier cannot use them any longer to instantiate the hidden/implicit arguments of _</span><span style="font-family:sans-serif">≈A_ or those of the equational reasoning combinators. Someone with more insight into Agda's unification machinery, please correct me if I am wrong.</span></div><div dir="auto"><br></div><div dir="auto">The workaround is to wrap the direct definition in a data-type or record. That requires some extra constructors/projections to convert between direct proofs of equality and the wrapped ones, but the problem with implicit arguments seems to disappear.</div><div dir="auto"><br></div><div dir="auto">Here's an example from the agda-categories library:</div><div dir="auto"><br></div><div dir="auto"><a href="https://github.com/agda/agda-categories/blob/master/src/Categories/Morphism/IsoEquiv.agda">https://github.com/agda/agda-categories/blob/master/src/Categories/Morphism/IsoEquiv.agda</a><br></div><div dir="auto"><br></div><div dir="auto">I hope that helps.</div><div dir="auto"><br></div><div dir="auto">Cheers</div><div dir="auto">/Sandro</div><div dir="auto"> <br><br><div class="gmail_quote" dir="auto"><div dir="ltr" class="gmail_attr">On Sat, Nov 28, 2020, 11:33 <<a href="mailto:mechvel@scico.botik.ru">mechvel@scico.botik.ru</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">On 2020-11-28 02:19, guillaume allais wrote:<br>
> Hi Sergei,<br>
> <br>
> Is your notion of equivalence by any change defined by recursion on its <br>
> inputs?<br>
> That would explain why you're getting really bad inference despite the<br>
> equational<br>
> reasoning combinators being designed to make inference as strong as <br>
> possible.<br>
> <br>
<br>
<br>
In the last example as below ("begin⟨ fooSetoid ⟩")<br>
it is of polSetoid - of setoid of polynomials. And its equivalence <br>
_=ₚ_is<br>
the _pointwise equality_ of certain ordered lists of pairs. The first <br>
component<br>
in a pair belongs to the specified CommutativeRing R, the second is of <br>
Nat.<br>
The first components are compared by _≈_ of R, the second components <br>
compared<br>
by _≡_.<br>
The pointwise equality of lists is taken from lib-1.4, I expect it is <br>
implemented<br>
by a certain recursion on input that you write about.<br>
Is it?<br>
<br>
But earlier I dealt with the same difficulty with the equality reasoning <br>
which does<br>
not apply recursion: generic arithmetic of fractions over a GCDRing R.<br>
The equality =fr on fractions is defined by applying once the equality <br>
_≈_<br>
on R:<br>
(Fr num denom denom≉0) =fr (Fr num' denom' denom'≉0) =<br>
num * denom' ≈ num' * denom,<br>
where _≈_ and _*_ re of R.<br>
Still there was the same problem with implicits in EqReasoning for <br>
_=fr_.<br>
<br>
I wrote<br>
<br>
>> eq = =ₚsym {Y} {Z} eq'<br>
>> where<br>
>> eq' : largeExpression2 =ₚ largeExpr1 *ₚ x<br>
>> eq' = lemma largeExpr1 x,<br>
>> <br>
>> where Y and Z are new variables. What terms to substitute for Y and Z<br>
>> in order for eq to have the needed type?<br>
>> If the type checker is able to solve this, then it would not require<br>
>> these large implicit arguments.<br>
<br>
But the left hand column<br>
begin⟨ fooSetoid ⟩<br>
fT + 0ₚ<br>
fT + ((- largeExpression) + largeExpression)<br>
...<br>
<br>
already has these terms. They only need to be substituted for X and Y.<br>
Why EqReasoning cannot do this?<br>
<br>
--<br>
SM<br>
<br>
<br>
> <br>
> <br>
> On 27/11/2020 21:50, <a href="mailto:mechvel@scico.botik.ru" target="_blank" rel="noreferrer">mechvel@scico.botik.ru</a> wrote:<br>
>> On 2020-11-27 22:22, <a href="mailto:mechvel@scico.botik.ru" target="_blank" rel="noreferrer">mechvel@scico.botik.ru</a> wrote:<br>
>>> [..]<br>
>>> <br>
>>> For more complex types, Agda forces me to write this:<br>
>>> begin⟨ fooSetoid ⟩<br>
>>> fT + 0ₚ<br>
>>> ≈⟨ +ₚcongˡ {fT} {0ₚ} {(- largeExpression) + <br>
>>> largeExpression} $<br>
>>> =ₚsym {(- largeExpression) + largeExpression} {0ₚ} $<br>
>>> -f+f largeExpression<br>
>>> ⟩<br>
>>> fT + ((- largeExpression) + largeExpression)<br>
>>> ...<br>
>>> ∎<br>
>>> <br>
>>> It this source code, largeExpression is written 7 times instead of <br>
>>> 3.<br>
>>> And real proofs often contain 5-10 versions of largeExpression that<br>
>>> are forced to be copied this way and pollute the source.<br>
>> <br>
>> The most nasty is the "sym" combinator.<br>
>> For example, its step in Reasoining can represented as<br>
>> <br>
>> eq : largeExpr1 *ₚ x =ₚ largeExpression2<br>
>> eq = =ₚsym {largeExpression2} {largeExpresssion1}<br>
>> (lemma largeExpr1 x)<br>
>> <br>
>> I am not an expert in this are. But here is a naive consideration.<br>
>> Suppose the type checker rewrites the implementation for eq as<br>
>> <br>
>> eq = =ₚsym {Y} {Z} eq'<br>
>> where<br>
>> eq' : largeExpression2 =ₚ largeExpr1 *ₚ x<br>
>> eq' = lemma largeExpr1 x,<br>
>> <br>
>> where Y and Z are new variables. What terms to substitute for Y and Z<br>
>> in order for eq to have the needed type?<br>
>> If the type checker is able to solve this, then it would not require<br>
>> these large implicit arguments.<br>
>> ?<br>
>> <br>
>> -- SM<br>
>> _______________________________________________<br>
>> Agda mailing list<br>
>> <a href="mailto:Agda@lists.chalmers.se" target="_blank" rel="noreferrer">Agda@lists.chalmers.se</a><br>
>> <a href="https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Flists.chalmers.se%2Fmailman%2Flistinfo%2Fagda&data=04%7C01%7Cguillaume.allais%40strath.ac.uk%7C0206289743574a9be04408d8931e736b%7C631e0763153347eba5cd0457bee5944e%7C0%7C0%7C637421106314023035%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=CUrWBN2ydEe8xllykjX2gSI3m4xkdSfw9xwQzEAVgUA%3D&reserved=0" rel="noreferrer noreferrer" target="_blank">https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Flists.chalmers.se%2Fmailman%2Flistinfo%2Fagda&data=04%7C01%7Cguillaume.allais%40strath.ac.uk%7C0206289743574a9be04408d8931e736b%7C631e0763153347eba5cd0457bee5944e%7C0%7C0%7C637421106314023035%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=CUrWBN2ydEe8xllykjX2gSI3m4xkdSfw9xwQzEAVgUA%3D&reserved=0</a><br>
> <br>
> _______________________________________________<br>
> Agda mailing list<br>
> <a href="mailto:Agda@lists.chalmers.se" target="_blank" rel="noreferrer">Agda@lists.chalmers.se</a><br>
> <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank" rel="noreferrer">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div></div></div>