[Agda] cong with wildcard

[Sergei Meshveliani]

On Tue, 2018-07-10 at 22:11 +0100, Matthew Daggitt wrote:
> Also might be worth having a look at Bradley's Agda holes library
> (https://github.com/bch29/agda-holes).
> 

Thank you. This may occur useful.

Of course, this can be done by developing/using a library based on
reflection. 

------
Sergei



> 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