[Agda] forced arguments in EqReasoning

[mechvel at scico.botik.ru]

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