[Agda] Q: Equational Reasoning

[Christoph Herrmann]

Hi Liang-Ting,

thank you very much. I already guessed that the right way is by using
the record hierarchy but how it has to be done is not so easy to
see, even with the content of the example files. I have attached a
working example based on your suggestions.

However, I'm still not sure whether it works just by accident or
whether it is methodically correct. It appears strange that the equality
symbol in the type consists of three parallel dashes and the one in
the derivation of two parallel tildes.

Cheers

Liang-Ting Chen wrote:
>
>
> On Wed, May 27, 2009 at 8:12 AM, ch <ch at cs.st-andrews.ac.uk 
> <mailto: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 <mailto:Agda at lists.chalmers.se>
>     https://lists.chalmers.se/mailman/listinfo/agda
>
>
>
>
> -- 
> sincerely,
> Liang-Ting


-- 
  Dr. Christoph Herrmann
  University of St Andrews, Scotland/UK
  phone: office: +44 1334 461629, home: +44 1334 478648
  email: ch at cs.st-andrews.ac.uk,  c.herrmann at virgin.net
  URL:   http://www.cs.st-andrews.ac.uk/~ch
 
  The University of St Andrews is a charity registered in Scotland: No SC013532
 

-------------- next part --------------
module Test where

open import Algebra
open import Data.Nat 
open import Data.Nat.Properties
import Relation.Binary.EqReasoning 
open Relation.Binary.EqReasoning (Data.Nat.setoid)
open import Relation.Binary.PropositionalEquality

foo : ∀ {a b : ℕ} → (a * b ≡ b * a)
foo {m} {n} =
  begin
    m * n
     ≈⟨ Algebra.CommutativeSemiring.*-comm Data.Nat.Properties.commutativeSemiring m n ⟩
    n * m
  ∎