[Agda] extending equality

[Sergei Meshveliani]

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