[Agda] forced arguments in EqReasoning

[mechvel at scico.botik.ru]

On 2020-11-27 22:22, mechvel at scico.botik.ru wrote:
> [..]
> The reasoning step of the the kind
>               foo + 0  ==  foo + ((- largeExpression) + 
> largeExpression)
> is normally coded as
>                   +congˡ (=sym (-x+x largeExpression)),
> [..]
> 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.
> [..]

As Agda does not allow to skip such large implicits,
we could replace them with the denotation {I}, {II}, {III}, {IV} ....
The proof remains clear, due to the expressions in the left hand column 
and
due to the function names, such as "+ₚcongˡ, =ₚsym, -f+f".
But this needs to write separately an array of the formulae with a 
certain comment:
"
-- ignore this garbage ----
I = largeExpression-1
...
IV = largeExpression-4
---------------------------
"

--
SM