[Agda] EqReasoning example

[Andreas Abel]

Hello Sergei,

you are simply using the wrong identifier for the equality chaining. 
The correct one is

   \equiv\<      \>

and you used s.th. like

   \approx( ... )

First, parentheses () cannot be part of an identifier, since they are 
special symbols in Agda (and any language I know).

Secondly, the chaining is nothing magic.  If you want to use a different 
chaining symbol, you have to rename

   _\equiv\<_\>_

to something suitable, e.g.

   _\approx\<_\>_

This works:

open module EqR-ns = EqR natSetoid public hiding (_≈⟨_⟩_) renaming 
(_≡⟨_⟩_ to _≈⟨_⟩_)


f : (n : ℕ) -> (n + zero) ≈ (zero + n)
f n = begin
            n    + zero     ≈⟨ +comm n zero ⟩
            zero + n
       ∎

Cheers,
Andreas

On 04.03.13 3:20 PM, Serge D. Mechveliani wrote:
> Please,
> how to fix the below program using  EqReasoning ?
> I am trying  "begin ...",  and it does not type-check.
>
> This short program is attached here as  Main.agda.zip.
>
> The example is only for  n + 0 ~~ 0 + n   for n : Nat,
> and the report is
> ------------------------------------------------------------
> (n + 0 .Relation.Binary.Core.Dummy... 0 + n)
>
> when checking that 0 are valid arguments to a function of type
> (n + 0 .Relation.Binary.Core.Dummy.... 0 + n)
> ------------------------------------------------------------
>
> Thanks,
>
> ------
> Sergei
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/
-------------- next part --------------
module EqR where
open import Foreign.Haskell
open import IO.Primitive
open import Data.String as String using (String; toCostring)

open import Relation.Binary using (Setoid; module Setoid)
open import Data.Nat as Nat using (ℕ; _+_; zero)
open import Data.Nat.Properties as NatProp renaming
                     (commutativeSemiring   to natCommSemiring;
                      isCommutativeSemiring to natIsCommSemiring)
open import Algebra using
                    (CommutativeSemiring; module CommutativeSemiring)
open import Algebra.Structures using
            (IsCommutativeSemiring; module IsCommutativeSemiring;
             IsCommutativeMonoid;   module IsCommutativeMonoid)

import Relation.Binary.EqReasoning as EqR


------------------------------------------------------------------------
natSetoid = CommutativeSemiring.setoid natCommSemiring
_≈_       = Setoid._≈_ natSetoid
+isComMon = IsCommutativeSemiring.+-isCommutativeMonoid
                                                 natIsCommSemiring
+comm = IsCommutativeMonoid.comm +isComMon

open module EqR-ns = EqR natSetoid public hiding (_≈⟨_⟩_) renaming (_≡⟨_⟩_ to _≈⟨_⟩_)


f : (n : ℕ) -> (n + zero) ≈ (zero + n)
                            -- I need an example with  ≈( )  reasoning
                            -- rather than with  ≡( )
f n = begin
           n    + zero     ≈⟨ +comm n zero ⟩ -- ≡⟨ +comm n zero ⟩
           zero + n
      ∎
      -- this works:  +comm n zero


main : IO Foreign.Haskell.Unit
main = putStrLn (toCostring "done")