[Agda] forced arguments in EqReasoning

[mechvel at scico.botik.ru]

On 2020-11-28 19:17, James Wood wrote:
> On 28/11/2020 16:03, mechvel at scico.botik.ru wrote:
>> Also James Wood writes that the definition of =fr (and thus =fr' too) 
>> ignore certain
>> parts of the Fraction record (the two remaining fields), and so the 
>> unification will
>> not work in  =fr
>> (if so, then probably for =fr' too).
>> ?
> In reply to the parenthetical remark, precisely not. With `record` or
> `data`, it is fine, because those definitions do not compute
> automatically. This is the key part of Sandro's _≃_ example. I think,
> in fact, exactly the same thing is happening in that example (fields
> being missed).
> 
>> The point of the record is for Agda to remember the two parameters f
>> and g, which it 'forgets' when you provide a value of the defined
>> equality type directly.


I have an impression that these implicits in EqReasoning can be solved
automatically for any design of _=fr_.
Consider

   *fr-cong : Congruent₂ _=fr_ _*fr_
   *fr-cong {f} {f'} {g} {g'} f=fr=f' g=fr=g' =
     begin
       ...
       f' *₁ g'    ≈⟨ =fr-sym {f' *fr g'} {f' *₁ g'} (*fr≗*₁ f' g') ⟩
       f' *fr g'
     ∎
     where open Fr-Reasoning

Let us write this as
   begin
     ...
     f' *₁ g'    ≈⟨ =fr-sym {X} {Y} (*fr≗*₁ f' g') ⟩
     f' *fr g'
   ∎

Let us abstract it further to
   begin
     ...
     I     ≈⟨ =fr-sym {X} {Y} (*fr≗*₁ f' g') ⟩
     II
   ∎,
where X and Y are unknown terms.
Normalization does not happen at this stage, no computation.
The goal of the last step is
                              I =fr II.

=fr-sym  has type (Symmetric _=fr_).
So, the solution
          X := II = f' *fr g';   Y := I = f' *₁ g'

is always satisfactory.
So, in the step of
     f' *₁ g'    ≈⟨ =fr-sym (*fr≗*₁ f' g') ⟩
     f' *fr g'

the implicits are found automatically.
Normalization does not happen at this stage, no computation.
After the terms for X and Y are substituted,
it (may be) applies normalization
(I do not know, I currently do not think of when normalization is 
applied),
and all the type checker work, and this will form a proof for the goal.

Suppose I write a program, and see  =fr-sym  on the top of RHS,
and see I and II in the left hand column,
and unsolved things are reported for this line.
Then I automatically, without thinking, copy the expressions I and II to
{II} and {I} to the arguments of =fr-sym in RHS.
And this is always satisfactory.
Why cannot this be done by the type checker or may be by a library 
function
near EqReasoning ?
Or is it for the Reflection tool? At what stage can this be done?

Am I missing something?

The next question will be: what if  =fr-sym  is not on the top?
For example,
     f +fr g    ≈⟨ +fr-cong =fr-refl (=fr-sym g'=g) ⟩
     f +fr g'

One has to discover that "{g'} {g}" need to be inserted after "=fr-sym".
As normalization is not applied at this step, it is evident that
these expressions are found in a similar way.
?

Regards,

--
SM



The expressions are