[Agda] forced arguments in EqReasoning

[mechvel at scico.botik.ru]

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