[Agda] Sized Natural Numbers

[Andrea Vezzosi]

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
>