[Agda] cong with wildcard

[Arseniy Alekseyev]

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.
Then Agda is much happier to infer things in general and I think it will
infer your example too.

On Tue, Jul 10, 2018, 12:57 Sergei Meshveliani <mechvel at botik.ru> wrote:

> Dear all,
>
> There is a problem of unnecessary large terms in proofs in a source
> program. For example, in an equality proof by EquationalReasoning of
>
>       begin T1  ≡⟨ cong foo1 eq1 ⟩
>             T2  ≡⟨ cong foo2 eq2 ⟩
>             T3
>             ...
>       ∎
>
> foo1, foo2 ...  often occur large terms which can be replaced with `_'.
> But Agda cannot solve this.
> For example, for the Nat arithmetic, the line
>
>    (a * 1 + 1+m * n)    ≡⟨ cong (_+ (1+m * n)) (Nat0.*1 a) ⟩
>
> means replacing  a * 1  with  a.
> And from the term triple
>
>    (a * 1 + 1+m * n)  ,  (cong (_+ _) (Nat0.*1 a)) ,
>    (a + 1+m * n)
>
> it is clear (to a human) which term  t  to substitute for `_' in order
> to obtain the third term
> -- provided that this  t  is a subterm in (a * 1 + 1+m * n).
>
> More general: the derivation is
>
>               E1   -- cong (op _) foo  -->
>               E2
>
> where op is an operator, and the prover needs to search in E1 all
> subterms to which (op X) matches, and which substitution derives E2.
>
> Does there exist a library for Agda that has tools for this?
> Can something easy be done towards such a tool?
>
> Regards,
>
> ------
> Sergei
>
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180710/a3432739/attachment.html>