[Agda] Sized Natural Numbers

[Bruno Bianchi]

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)
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20150602/aeb399c1/attachment.html