[Agda] Decidable _\~~_ of Semiring

[Andreas Abel]

There are two different definitions of Decidable:

1) The one in Relation.Unary is for predicates (unary relations).
2) The one in Relation.Binary is for binary relations.

Just import the right one and the type error goes away.

open import Relation.Binary using ( Decidable; IsDecEquivalence; module 
IsDecEquivalence )

Cheers,
Andreas

On 09.11.2012 12:42, Serge D. Mechveliani wrote:
> Please, what is wrong in the following program?
>
> (for  Agda-2.3.0.1, MAlonzo, lib-0.6,  lib-0.6 used heavily)
>
> ------------------------------------------------------------------------
> ...
> open import Relation.Unary using ( Decidable )
> open import Algebra using ( Semiring; module Semiring; ...
>                            )
> open import Relation.Binary using
>                             ( IsDecEquivalence; module IsDecEquivalence )
>
> test : {c l : Level} -> {R : Semiring c l} ->
>         let open Semiring {{...}}
>             C  = Carrier
>         in
>         C ->
>         IsDecEquivalence {A = C} _~~_ ->    -- (1)
>         -- Decidable {A = C} _~~_ ->        -- (2)
>         C
>
> test x
>         isDE =   -- (1)
>         -- eq =  -- (2)
>
>                 case eq x 0# of н╩ { (yes _) -> 0# ;  _ -> 1# }
>                 where
> 	       open Semiring {{...}}
>                 eq = IsDecEquivalence._?=_ isDE   -- (1)
> ------------------------------------------------------------------------
>
> -- here I replace the math symbols as  \~~  ->  ~~,  \?=  ->  ?=
>
> Now I need to simplify this varant (1) to variant (2).
> Because
> 1) IsDecEquivalence {A : Set A} _~~_
>     has the fields               isEquivalence : IsEquivalence _~~_
>                                  _?=_          : Decidable _~~_,
>
> 2) `test'  uses only the  field  ?=,
>     it does not need checking   isEquivalence,  because it takes  _~~_
>     from  R : Semiring _ _,
>     and there  _~~_  is declared as an equivalence,
> 3) so, instead of  isDE,  `test'  needs only
>     eq : Decidable {A = C} _~~_,  where _~~_ is of R.
>
> Right?
> So I comment out the three lines marked by  (1)
> and un-comment the two lines marked by      (2).
> The checker reports
>
>    (Semiring.Carrier R -> Set l) !=< (Set _540) of type
>    (Set (L-suc l L-max c))
>    when checking that the expression _~~_ has type (Carrier -> Set _540)
>
> for the line of   " Decidable {A = C} _~~_ ->  "
>
> Skipping here {A = C} does not change this.
>
> So, for  _~~_  taken from  R  we have that
> 1) _?=_ : Decidable _~~_   is accepted in  IsDecEquivalence
> 2) Decidable _~~_          is rejected in the signature of `test'.
>
> This looks like a contradiction. How to fix the variant (2) ?
> Thank you in advance for explanation,
>
> ------
> 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/