<div dir="ltr"><div>Thank you Andrea. I wasn&#39;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">&lt;<a href="mailto:sanzhiyan@gmail.com" target="_blank">sanzhiyan@gmail.com</a>&gt;</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 &quot;_&lt;=_ {up (up i)} e1 e2&quot; but you only have &quot;_&lt;=_ {up<br>
i} e1 e2&quot; 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>
_&lt;=_, 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 &lt;<a href="mailto:bgbianchi@gmail.com">bgbianchi@gmail.com</a>&gt; wrote:<br>
&gt; Hi,<br>
&gt;<br>
&gt; This time I&#39;m writing to ask you for some help to understand what&#39;s going on<br>
&gt; with the following code. I&#39;m using a sized definition of natural numbers as<br>
&gt; part of a more general proof about logarithms. In particular, I don&#39;t<br>
&gt; understand why the last sentence is failing. I&#39;ve noticed that if I define a<br>
&gt; &quot;subtype : {i : Size} -&gt; SNat {i} -&gt; SNat {up i}&quot; function and then I<br>
&gt; replace the last sentence in function &quot;/2&quot; by &quot;(suc (suc n)) /2 = suc<br>
&gt; (subtype (n /2))&quot; then I&#39;m able to prove &quot;m/2&lt;=n/2&quot; using an auxiliary lemma<br>
&gt; &quot;subtype&lt;= : {i : Size}{m : SNat {i}}{n : SNat} -&gt; m &lt;= n -&gt; subtype m &lt;=<br>
&gt; subtype n&quot;.<br>
&gt;<br>
&gt; Thanks in advance,<br>
&gt;<br>
&gt; Bruno<br>
&gt;<br>
&gt;<br>
&gt; module SNat where<br>
&gt;<br>
&gt; open import Size<br>
&gt;<br>
&gt; data SNat : {i : Size} -&gt; Set where<br>
&gt;   zero : {i : Size} -&gt; SNat {up i}<br>
&gt;   suc  : {i : Size} -&gt; SNat {i} -&gt; SNat {up i}<br>
&gt;<br>
&gt; data _&lt;=_ : {i : Size} -&gt; SNat {i} -&gt; SNat -&gt; Set where<br>
&gt;   z&lt;=n : {i : Size}(n : SNat) -&gt; _&lt;=_ {up i} zero n<br>
&gt;   s&lt;=s : {i : Size}{m : SNat {i}}{n : SNat} -&gt; m &lt;= n -&gt; suc m &lt;= suc n<br>
&gt;<br>
&gt; _/2 : {i : Size} -&gt; SNat {i} -&gt; SNat {i}<br>
&gt; zero /2 = zero<br>
&gt; (suc zero) /2 = zero<br>
&gt; (suc (suc n)) /2 = suc (n /2)<br>
&gt;<br>
&gt; m/2&lt;=n/2 : {i : Size}{m : SNat {i}}{n : SNat} -&gt; m &lt;= n -&gt; (m /2) &lt;= (n /2)<br>
&gt; m/2&lt;=n/2 (z&lt;=n n) = z&lt;=n (n /2)<br>
&gt; m/2&lt;=n/2 (s&lt;=s (z&lt;=n n)) = z&lt;=n (suc n /2)<br>
&gt; m/2&lt;=n/2 (s&lt;=s (s&lt;=s m&lt;=n)) = s&lt;=s (m/2&lt;=n/2 m&lt;=n)<br>
&gt;<br>
</div></div>&gt; _______________________________________________<br>
&gt; Agda mailing list<br>
&gt; <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
&gt; <a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
&gt;<br>
</blockquote></div><br></div>