<div dir="auto"><div>What I found super-helpful to Agda is having the definitions of your operators abstract, e.g. working in an arbitrary semiring instead of with Nats directly.</div><div dir="auto">Then Agda is much happier to infer things in general and I think it will infer your example too.<br><br><div class="gmail_quote" dir="auto"><div dir="ltr">On Tue, Jul 10, 2018, 12:57 Sergei Meshveliani <<a href="mailto:mechvel@botik.ru" target="_blank" rel="noreferrer">mechvel@botik.ru</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Dear all,<br>
<br>
There is a problem of unnecessary large terms in proofs in a source<br>
program. For example, in an equality proof by EquationalReasoning of <br>
<br>
      begin T1  ≡⟨ cong foo1 eq1 ⟩ <br>
            T2  ≡⟨ cong foo2 eq2 ⟩<br>
            T3  <br>
            ...<br>
      ∎<br>
<br>
foo1, foo2 ...  often occur large terms which can be replaced with `_'.<br>
But Agda cannot solve this.<br>
For example, for the Nat arithmetic, the line<br>
<br>
   (a * 1 + 1+m * n)    ≡⟨ cong (_+ (1+m * n)) (Nat0.*1 a) ⟩<br>
<br>
means replacing  a * 1  with  a.<br>
And from the term triple<br>
<br>
   (a * 1 + 1+m * n)  ,  (cong (_+ _) (Nat0.*1 a)) ,<br>
   (a + 1+m * n)<br>
<br>
it is clear (to a human) which term  t  to substitute for `_' in order<br>
to obtain the third term  <br>
-- provided that this  t  is a subterm in (a * 1 + 1+m * n).<br>
<br>
More general: the derivation is <br>
<br>
              E1   -- cong (op _) foo  --><br>
              E2<br>
<br>
where op is an operator, and the prover needs to search in E1 all<br>
subterms to which (op X) matches, and which substitution derives E2.<br>
<br>
Does there exist a library for Agda that has tools for this? <br>
Can something easy be done towards such a tool?<br>
<br>
Regards,<br>
<br>
------<br>
Sergei<br>
<br>
<br>
<br>
<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" rel="noreferrer noreferrer" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer noreferrer noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div></div></div>