[Agda] forced arguments in EqReasoning

guillaume allais guillaume.allais at ens-lyon.org
Sat Nov 28 00:19:13 CET 2020


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 
>



More information about the Agda mailing list