<div dir="ltr"><br><div class="gmail_extra"><br><br><div class="gmail_quote">On Wed, Jul 2, 2014 at 5:36 PM, Sergei Meshveliani <span dir="ltr">&lt;<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>&gt;</span> wrote:<br>

<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex"><div class=""><br></div><div class="">
&gt; The problem is that findNatByContra never looks at the proof, so there<br>
&gt; is no guarantee that it&#39;s a closed proof (which Thorsten mentioned<br>
&gt; above).<br>
<br>
</div>Please, what is a  closed proof?<br></blockquote><div><br></div><div>A closed proof is a proof that does not contain any free variables.</div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex">


<div class="">&gt; For instance,<br>
&gt;<br>
&gt; False : ℕ → Set<br>
&gt; False _ = ⊥<br>
&gt;<br>
&gt; decFalse : Decidable False<br>
&gt; decFalse _ = no (λ x → x)<br>
&gt;<br>
&gt; loopy : ¬ (∀ n → ¬ False n) → Σ ℕ False<br>
&gt; loopy H = findNatByContra False decFalse H<br>
&gt;<br>
&gt;<br>
&gt; Here, loopy will happily evaluate forever with the hypothetical<br>
&gt; (classical) proof that there is a number satisfying False. There is no<br>
&gt; need to evaluate under the case since decFalse comes back &#39;no&#39; for any<br>
&gt; number.<br><br>
</div>Can you, please, explain further?<br>
<br>
To apply  (loopy H),  one needs to provide<br>
                                   H : (∀ n → ¬ False n) → ⊥.<br>
<br>
And this is not possible, because its type normalizes to<br>
<br>
((n : ℕ) → (False n → ⊥)) → ⊥,  and to  ((n : ℕ) → (⊥ → ⊥)) → ⊥,<br>
<br>
and the type  (n : ℕ) → (⊥ → ⊥)  has a value  (\n → id)  in it.<br>
<br>
<br>
As one cannot provide any argument value to `loopy&#39;,  how can it<br>
evaluate forever?<br></blockquote><div><br></div><div>The problem is that in Agda programs need to terminate not only at run-time</div><div>when you apply them to actual arguments, but also at type checking-time when</div>

<div>the type checker runs programs to check for equality. For instance, suppose</div><div>you define loopy as above and then try to prove that loopy always returns 42</div><div><br></div><div>thm : (H : ¬ (∀ n → ¬ False n)) → proj₁ (loopy H) ≡ 42</div>

<div>thm _ = refl</div><div><br></div><div>In this case the type checker needs to evaluate loopy in the context of the</div><div>free variable H to check if it normalises to 42. This evaluation will not terminate</div><div>

with your definition of findNatByContra.</div><div><br></div><div>/ Ulf</div></div></div></div>