[Agda] extending equality

[Matus Tejiscak]

Ah, sorry, I edited the function to fit your names, making a mistake.

The nRefl should be changed to the constructor of _≡_, whatever it is  
called in your code (usually it's refl).

Matus

Quoting Sergei Meshveliani <mechvel at botik.ru>:

> On Mon, 2013-07-29 at 17:00 +0200, Matus Tejiscak wrote:
>> Hello, you could shorten it as, for example,
>>
>>    cSym : Symmetric _=c_
>>    cSym {infinity} {infinity} tt    = tt
>>    cSym {fin m}    {fin .m}   nRefl = nRefl
>>    cSym {infinity} {fin _}    ()
>>    cSym {fin _}    {infinity} ()
>>
>> which does not omit the two impossible cases but is a bit simpler overall.
>>
>> In this variant, you need to match on the nRefl (instead of putting an
>> underscore there) in order to unify m and n in the typechecker.
>
> Agda-2.3.2.1 reports to this:
> "
> Failed to infer the value of dotted pattern
> when checking that the pattern .m has type ℕ
> "
>
> Regards,
>
> ------
> Sergei
>
>
>> Quoting Sergei Meshveliani <mechvel at botik.ru>:
>>
>> > How do you think, please,
>> > is there possible a simpler expression for  cSym  below?
>> >
>> > -------------------------------------------------------------
>> > data Cardinality : Set where  fin      : ℕ → Cardinality
>> >                               infinity : Cardinality
>> > _=c_ : Rel Cardinality _
>> > (fin m)  =c (fin n)  =  m ≡ n
>> > infinity =c infinity =  ⊤
>> > _        =c _        =  ⊥
>> >
>> > natDecSetoid = DecTotalOrder.Eq.decSetoid natDTO    -- for ℕ
>> > natSetoid    = DecSetoid.setoid natDecSetoid
>> > natEquiv     = Setoid.isEquivalence natSetoid
>> >
>> > open IsEquivalence natEquiv renaming
>> >                           (refl to nRefl; sym to nSym; trans to nTrans)
>> > _≟_ = DecSetoid._≟_ natDecSetoid
>> >
>> > cSym : Symmetric _=c_
>> > cSym {infinity} {infinity} _    =  ⊤.tt
>> > cSym {infinity} {fin _}    x='y =  ⊥-elim x='y
>> > cSym {fin _}    {infinity} x='y =  ⊥-elim x='y
>> > cSym {fin m}    {fin n}    x='y  with m ≟ n
>> > ...                            | yes m=n = nSym m=n
>> > ...                            | no m/=n = ⊥-elim $ m/=n x='y
>> > ---------------------------------------------------------------
>> >
>> > I hoped for   cSym {fin m}  {.(fin m)} _  =  nRefl
>> >               cSym infinity .infinity  _  =  ⊤.tt
>> >
>> > to work - due to the type of the third argument.
>> > Buth all my `dot' variants are not type-checked.
>> >
>> > Thanks,
>> >
>> > ------
>> > Sergei
>> >
>> > _______________________________________________
>> > Agda mailing list
>> > Agda at lists.chalmers.se
>> > https://lists.chalmers.se/mailman/listinfo/agda
>>
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda


-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 490 bytes
Desc: PGP Digital Signature
Url : http://lists.chalmers.se/pipermail/agda/attachments/20130729/92b7aee2/attachment.bin