[Agda] forced arguments in EqReasoning

[guillaume allais]

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.

Best,


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 
>