[Agda] automatically instantiating rewrites

[Ramana Kumar]

My ulterior motives are actually to see how much tactic-based proving, as
you can do in Coq, it is feasible to accomplish somehow in Agda, and
whether its design as a programming language might reveal smarter ways to
do serious proofs.

On Sat, Jan 14, 2012 at 7:34 PM, <greenrd at greenrd.org> wrote:

> Of course Coq can do this already, but that's a completely different
> language.
>
> If you want to do full-blown dependently-typed programming in Coq, you may
> find the Program command, and the experimental Equations extension on
> github, useful. Equations tries to generate equations (and other things)
> from case distinctions. It can be a bit tricky to install though.
>
> --
> Robin Green
>
>
> On 2012-01-14 18:54, Ramana Kumar wrote:
>
>> Is there any plan to (or, more interestingly, never to) support this
>> kind of rewriting that automatically picks a matching term?
>> A middle ground could be to allow the interactive interface to
>> provide a list of probably matches.
>>  I'm asking because I just wrote some long rewrite terms by hand by
>> copying from my goal the appropriate arguments to a general rule...
>>
>> On Thu, Jan 12, 2012 at 6:46 PM, Nils Anders Danielsson
>> <nad at chalmers.se [2]> wrote:
>>
>>  On 2012-01-12 19:34, Ramana Kumar wrote:
>>>
>>>  If you have an equation of the form eqn : (x : t) → foo x ≡
>>>> bar x, is
>>>> it possible to use rewrite in such a way that it picks up all
>>>> instances of foo x and rewrites them, or do you always have to
>>>> manually apply eqn to the right terms before you can give it to
>>>> rewrite?
>>>>
>>>
>>> The latter. The rewrite construct is defined in terms of with:
>>>
>>>
>>>  http://wiki.portal.chalmers.**se/agda/agda.php?n=Main.**Version-2-2-6<http://wiki.portal.chalmers.se/agda/agda.php?n=Main.Version-2-2-6>
>>> [1]
>>>
>>> --
>>> /NAD
>>>
>>
>>
>>
>> Links:
>> ------
>> [1] http://wiki.portal.chalmers.**se/agda/agda.php?n=Main.**Version-2-2-6<http://wiki.portal.chalmers.se/agda/agda.php?n=Main.Version-2-2-6>
>> [2] mailto:nad at chalmers.se
>>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20120114/7a870150/attachment.html