[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, there is recursion in _=ₚ_.
The simplest ready example does not apply recursion for equality.
Probably the matter is in a nontrivial equality on records expressed in
the record fields.
May be you mean a composition of equality definitions?
Consider this:

module Fraction.I {α α=} (R : GCDDomain α α=)
   where
   open GCDDomain R
        using (_≈_; _≟_; _≉_; ≈refl; ≈sym; ≈trans; ≉respˡ; ...)
        renaming (Carrier to C)
   ...
   record Fraction : Set (α ⊔ α=) where
     constructor frᶜ
     field  num     : C
            denom   : C
            denom≉0 : denom ≉ 0#
            coprime : Coprime num denom

   open Fraction

   _=fr_ :  Rel Fraction α=
   f =fr g =  (num f * denom g) ≈ (num g * denom f)
   ...

   _*fr_ : Op₂ Fraction
   (frᶜ n₁  d₁ d₁≉0 co-n₁d₁) *fr (frᶜ n₂ d₂ d₂≉0 co-n₂d₂) =
                               frᶜ n₁'n₂' d₁'d₂' d₁'d₂'≉0 
coprime-n₁'n₂'-d₁'d₂'
     where
     n₁' = ...
     ...
     -- There is not any recursion here, only several arithmetic 
operations in R,
     -- and non-recursive proofs with _≈_ in R.

   *fr-cong : Congruent₂ _=fr_ _*fr_
   *fr-cong {f} {f'} {g} {g'} f=fr=f' g=fr=g' =
     begin
       f *fr g     ≈⟨ *fr≗*₁ f g ⟩
       f *₁ g      ≈⟨ *₁cong {f} {f'} {g} {g'} f=fr=f' g=fr=g' ⟩
       f' *₁ g'    ≈⟨ =fr-sym {f' *fr g'} {f' *₁ g'} (*fr≗*₁ f' g') ⟩
       f' *fr g'
     ∎
     where open Fr-Reasoning  -- equational reasoning of lib-1.4 for 
fractionSetoid
------------------------------------------------

Consider this _sym_ (=fr-sym)  in the last step.
Agda 2.6.1 does not allow to skip any implicit argument in it.
But their terms are exactly neighbors in the left hand column.
Can  EqReasoning  observe the left hand columns, compare the terms and
substitute them automatically as needed?

Further, this proof uses *fr≗*₁ and *₁cong.
This uses a certain pair of maps  Fraction R  <-->  Prefraction R.
The  Prefraction  record is similar to Fraction, but the _coprime_
condition is skipped.
And the proofs for Prefraction arithmetic do not suffer of this problem
of forced implicit arguments in EqReasoning.

So: there are records over R:  Prefraction  and  Fraction.
Arithmetic and equality on Fraction uses the ones of Prefraction,
(do you consider this as recursion in equality?).
Prefraction does not force writing unneeded implicits in EqReasoning,
and Fraction does force such.

So, there are equality _=1_ and EqReasoning of record (I)
which call for equality _=2_ and EqReasoning of record (II).
I do not know, may be, the effect is due to this composition.

And with polynomial, the equality on the record of Pol
calls for the equality on the record on Mon,
the equality on the record on Mon calls for basic _≈_ on R and for _≡_ 
on Nat,
also here is the pointwise equality on lists.

Regards,

--
SM