[Agda] cong with wildcard

[Matthew Daggitt]

Also might be worth having a look at Bradley's Agda holes library (
https://github.com/bch29/agda-holes).

On Tue, Jul 10, 2018 at 6:11 PM Arseniy Alekseyev <rotsor at gmail.com> wrote:

> 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
>>
> _______________________________________________
> 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/9a8d98a1/attachment.html>