[Agda] Sized Natural Numbers

[Bruno Bianchi]

Thank you Andrea. I wasn't sure if the automatic subtyping should solve it,
but now it became clear.

Regards,

Bruno

2015-06-02 18:33 GMT+08:00 Andrea Vezzosi <sanzhiyan at gmail.com>:

> If you make Agda display hidden arguments then you can see you are
> trying to prove "_<=_ {up (up i)} e1 e2" but you only have "_<=_ {up
> i} e1 e2" and the automatic subtyping is not upcasting the latter to
> the former.
>
> An alternative could be to remove the sizes from the definition of
> _<=_, unless you need them somewhere else.
>
> Best,
> Andrea
>
> On Tue, Jun 2, 2015 at 12:13 PM, Bruno Bianchi <bgbianchi at gmail.com>
> wrote:
> > Hi,
> >
> > This time I'm writing to ask you for some help to understand what's
> going on
> > with the following code. I'm using a sized definition of natural numbers
> as
> > part of a more general proof about logarithms. In particular, I don't
> > understand why the last sentence is failing. I've noticed that if I
> define a
> > "subtype : {i : Size} -> SNat {i} -> SNat {up i}" function and then I
> > replace the last sentence in function "/2" by "(suc (suc n)) /2 = suc
> > (subtype (n /2))" then I'm able to prove "m/2<=n/2" using an auxiliary
> lemma
> > "subtype<= : {i : Size}{m : SNat {i}}{n : SNat} -> m <= n -> subtype m <=
> > subtype n".
> >
> > Thanks in advance,
> >
> > Bruno
> >
> >
> > module SNat where
> >
> > open import Size
> >
> > data SNat : {i : Size} -> Set where
> >   zero : {i : Size} -> SNat {up i}
> >   suc  : {i : Size} -> SNat {i} -> SNat {up i}
> >
> > data _<=_ : {i : Size} -> SNat {i} -> SNat -> Set where
> >   z<=n : {i : Size}(n : SNat) -> _<=_ {up i} zero n
> >   s<=s : {i : Size}{m : SNat {i}}{n : SNat} -> m <= n -> suc m <= suc n
> >
> > _/2 : {i : Size} -> SNat {i} -> SNat {i}
> > zero /2 = zero
> > (suc zero) /2 = zero
> > (suc (suc n)) /2 = suc (n /2)
> >
> > m/2<=n/2 : {i : Size}{m : SNat {i}}{n : SNat} -> m <= n -> (m /2) <= (n
> /2)
> > m/2<=n/2 (z<=n n) = z<=n (n /2)
> > m/2<=n/2 (s<=s (z<=n n)) = z<=n (suc n /2)
> > m/2<=n/2 (s<=s (s<=s m<=n)) = s<=s (m/2<=n/2 m<=n)
> >
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda
> >
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20150603/c9f7d5b3/attachment.html