[Agda] Q: Equational Reasoning

[Liang-Ting Chen]

On Wed, May 27, 2009 at 8:12 AM, ch <ch at cs.st-andrews.ac.uk> wrote:

> Hi,
>
> I am new to Agda and confused by all the library modules.
>
> Is there an easy way to make the properties of the
> operations on built-in natural numbers available for equational
> reasoning without copying larger parts of library code
> (especially those in private sections) into own Agda scripts
> and without a tedious top-down refinement of the algebraic
> definitions?
>
> Basically, I would like something like this:
>
>   begin
>     ...
>     m * n
>     =< Data.Nat.\nb.commutativity-* {m} {n} >
>     n * m
>     ...
>
> Could you please tell me, what has to be written inside the  =< ... >
>  brackets
> to achieve that? And what is the preferred library module to use for
> equational reasoning (=,  not <=) on the built-in Data.Nat.\nb type?

Hi,

You could check the README of the standard library and there is an
explanation in section Record hierarchies.

First, algebraic properties are record types, so you could extract the
desired properties by
the projection function of the record type. If you want to use algebraic
properties, you should import "Algebra" first.
Second, the preferred library for equational reasoning could be
"Relation.Binary.EqReasoning".
Note that, it's a parameterized module, and you should give a setoid.

For example, Data.Nat.Properties.commutativeSemiring is an element of the
record type, Algebra.CommutativeSemiring,
and you want to use the commutativity of adding. The function
"Algebra.CommutativeSemring.+-comm" is the projection function,
and "Algebra.CommutativeSemring.+-comm
Data.Nat.Properties.commutativeSemring" is the desired proof.

To use the equational reasoning, you have to import
Relation.Binary.EqReasoning, and open it with Data.Nat.setoid, that is,
open Relation.Binary.EqReasoning Data.Nat.setoid.Data.Nat.Properties.

There are more examples in Data.Nat.Properties.


>
> If there is a specific tutorial on how to do equational reasoning in Agda
> or on the
> concept of how to deal with the libraries (when to use using, hiding,
> renaming),
> please give me the pointer.
>
> Many thanks in advance
> --
> Christoph
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>



-- 
sincerely,
Liang-Ting
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20090527/20a75e6f/attachment.html