<div dir="ltr"><div>Thank you Andrea. I wasn't sure if the automatic subtyping should solve it, but now it became clear.</div><div> </div><div>Regards,</div><div> </div><div>Bruno</div></div><div class="gmail_extra"><br><div class="gmail_quote">2015-06-02 18:33 GMT+08:00 Andrea Vezzosi <span dir="ltr"><<a href="mailto:sanzhiyan@gmail.com" target="_blank">sanzhiyan@gmail.com</a>></span>:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">If you make Agda display hidden arguments then you can see you are<br>
trying to prove "_<=_ {up (up i)} e1 e2" but you only have "_<=_ {up<br>
i} e1 e2" and the automatic subtyping is not upcasting the latter to<br>
the former.<br>
<br>
An alternative could be to remove the sizes from the definition of<br>
_<=_, unless you need them somewhere else.<br>
<br>
Best,<br>
Andrea<br>
<div><div class="h5"><br>
On Tue, Jun 2, 2015 at 12:13 PM, Bruno Bianchi <<a href="mailto:bgbianchi@gmail.com">bgbianchi@gmail.com</a>> wrote:<br>
> Hi,<br>
><br>
> This time I'm writing to ask you for some help to understand what's going on<br>
> with the following code. I'm using a sized definition of natural numbers as<br>
> part of a more general proof about logarithms. In particular, I don't<br>
> understand why the last sentence is failing. I've noticed that if I define a<br>
> "subtype : {i : Size} -> SNat {i} -> SNat {up i}" function and then I<br>
> replace the last sentence in function "/2" by "(suc (suc n)) /2 = suc<br>
> (subtype (n /2))" then I'm able to prove "m/2<=n/2" using an auxiliary lemma<br>
> "subtype<= : {i : Size}{m : SNat {i}}{n : SNat} -> m <= n -> subtype m <=<br>
> subtype n".<br>
><br>
> Thanks in advance,<br>
><br>
> Bruno<br>
><br>
><br>
> module SNat where<br>
><br>
> open import Size<br>
><br>
> data SNat : {i : Size} -> Set where<br>
> zero : {i : Size} -> SNat {up i}<br>
> suc : {i : Size} -> SNat {i} -> SNat {up i}<br>
><br>
> data _<=_ : {i : Size} -> SNat {i} -> SNat -> Set where<br>
> z<=n : {i : Size}(n : SNat) -> _<=_ {up i} zero n<br>
> s<=s : {i : Size}{m : SNat {i}}{n : SNat} -> m <= n -> suc m <= suc n<br>
><br>
> _/2 : {i : Size} -> SNat {i} -> SNat {i}<br>
> zero /2 = zero<br>
> (suc zero) /2 = zero<br>
> (suc (suc n)) /2 = suc (n /2)<br>
><br>
> m/2<=n/2 : {i : Size}{m : SNat {i}}{n : SNat} -> m <= n -> (m /2) <= (n /2)<br>
> m/2<=n/2 (z<=n n) = z<=n (n /2)<br>
> m/2<=n/2 (s<=s (z<=n n)) = z<=n (suc n /2)<br>
> m/2<=n/2 (s<=s (s<=s m<=n)) = s<=s (m/2<=n/2 m<=n)<br>
><br>
</div></div>> _______________________________________________<br>
> Agda mailing list<br>
> <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
> <a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
><br>
</blockquote></div><br></div>