[Agda] forced arguments in EqReasoning
Sandro Stucki
sandro.stucki at gmail.com
Sat Nov 28 12:45:20 CET 2020
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
a ≈A b = f a ≈B f b
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 _≈A_ could
also involve some pattern matching -- it doesn't matter, as long as it's
not a data-type definition. This is what Guillaume meant by defining _≈A_
via recursion (I think). Your explanation about =fr indicates that this is
the case for you.
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 _≈A_ or those of the equational reasoning
combinators. Someone with more insight into Agda's unification machinery,
please correct me if I am wrong.
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.
Here's an example from the agda-categories library:
https://github.com/agda/agda-categories/blob/master/src/Categories/Morphism/IsoEquiv.agda
I hope that helps.
Cheers
/Sandro
On Sat, Nov 28, 2020, 11:33 <mechvel at scico.botik.ru> wrote:
> On 2020-11-28 02:19, guillaume allais wrote:
> > Hi Sergei,
> >
> > Is your notion of equivalence by any change defined by recursion on its
> > inputs?
> > That would explain why you're getting really bad inference despite the
> > equational
> > reasoning combinators being designed to make inference as strong as
> > possible.
> >
>
>
> In the last example as below ("begin⟨ fooSetoid ⟩")
> it is of polSetoid - of setoid of polynomials. And its equivalence
> _=ₚ_is
> the _pointwise equality_ of certain ordered lists of pairs. The first
> component
> in a pair belongs to the specified CommutativeRing R, the second is of
> Nat.
> The first components are compared by _≈_ of R, the second components
> compared
> by _≡_.
> The pointwise equality of lists is taken from lib-1.4, I expect it is
> implemented
> by a certain recursion on input that you write about.
> Is it?
>
> But earlier I dealt with the same difficulty with the equality reasoning
> which does
> not apply recursion: generic arithmetic of fractions over a GCDRing R.
> The equality =fr on fractions is defined by applying once the equality
> _≈_
> on R:
> (Fr num denom denom≉0) =fr (Fr num' denom' denom'≉0) =
> num * denom' ≈ num' * denom,
> where _≈_ and _*_ re of R.
> Still there was the same problem with implicits in EqReasoning for
> _=fr_.
>
> I wrote
>
> >> eq = =ₚsym {Y} {Z} eq'
> >> where
> >> eq' : largeExpression2 =ₚ largeExpr1 *ₚ x
> >> eq' = lemma largeExpr1 x,
> >>
> >> where Y and Z are new variables. What terms to substitute for Y and Z
> >> in order for eq to have the needed type?
> >> If the type checker is able to solve this, then it would not require
> >> these large implicit arguments.
>
> But the left hand column
> begin⟨ fooSetoid ⟩
> fT + 0ₚ
> fT + ((- largeExpression) + largeExpression)
> ...
>
> already has these terms. They only need to be substituted for X and Y.
> Why EqReasoning cannot do this?
>
> --
> SM
>
>
> >
> >
> > On 27/11/2020 21:50, mechvel at scico.botik.ru wrote:
> >> On 2020-11-27 22:22, mechvel at scico.botik.ru wrote:
> >>> [..]
> >>>
> >>> For more complex types, Agda forces me to write this:
> >>> begin⟨ fooSetoid ⟩
> >>> fT + 0ₚ
> >>> ≈⟨ +ₚcongˡ {fT} {0ₚ} {(- largeExpression) +
> >>> largeExpression} $
> >>> =ₚsym {(- largeExpression) + largeExpression} {0ₚ} $
> >>> -f+f largeExpression
> >>> ⟩
> >>> fT + ((- largeExpression) + largeExpression)
> >>> ...
> >>> ∎
> >>>
> >>> It this source code, largeExpression is written 7 times instead of
> >>> 3.
> >>> And real proofs often contain 5-10 versions of largeExpression that
> >>> are forced to be copied this way and pollute the source.
> >>
> >> The most nasty is the "sym" combinator.
> >> For example, its step in Reasoining can represented as
> >>
> >> eq : largeExpr1 *ₚ x =ₚ largeExpression2
> >> eq = =ₚsym {largeExpression2} {largeExpresssion1}
> >> (lemma largeExpr1 x)
> >>
> >> I am not an expert in this are. But here is a naive consideration.
> >> Suppose the type checker rewrites the implementation for eq as
> >>
> >> eq = =ₚsym {Y} {Z} eq'
> >> where
> >> eq' : largeExpression2 =ₚ largeExpr1 *ₚ x
> >> eq' = lemma largeExpr1 x,
> >>
> >> where Y and Z are new variables. What terms to substitute for Y and Z
> >> in order for eq to have the needed type?
> >> If the type checker is able to solve this, then it would not require
> >> these large implicit arguments.
> >> ?
> >>
> >> -- SM
> >> _______________________________________________
> >> Agda mailing list
> >> Agda at lists.chalmers.se
> >>
> 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
> >
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda
> _______________________________________________
> 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/20201128/12f27f77/attachment.html>
More information about the Agda
mailing list