[Agda] Sized Natural Numbers

[Andrea Vezzosi]

Maybe it should!

On Tue, Jun 2, 2015 at 7:10 PM, Bruno Bianchi <bgbianchi at gmail.com> wrote:
> 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
>> >
>
>