<div dir="ltr"><div class="gmail_extra"><br><div class="gmail_quote">On Mon, Jul 7, 2014 at 2: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>I have installed Agda of July 7, 2014<br>
(in which the checker loop is fixed), and tried this program version:<br>
<br>
----------------------------------------------------------------<br>
{-# NO_TERMINATION_CHECK #-}<br>
<div class="">findNatByContra :<br>
           (P : ℕ → Set) → (P? : Decidable P) → ¬ (∀ n → ¬ P n) → Σ ℕ P<br>
findNatByContra P P? _ =  findFrom 0<br>
  where<br>
  findFrom : ℕ → Σ ℕ P<br>
  findFrom n = case P? n of \ { (yes Pn) → (n , Pn)<br>
                              ; (no _)   → findFrom (suc n) }<br>
<br>
</div>eq3 : ℕ → Set<br>
eq3 = _≡_ 3<br>
<br>
eq3? : Decidable eq3<br>
eq3? = _≟_ 3<br>
<br>
find3 :  ¬ (∀ n → 3 ≢ n) → Σ ℕ (_≡_ 3)<br>
find3 H =  findNatByContra eq3 eq3? H<br>
<br>
thm&#39; : (H : ¬ (∀ n → 3 ≢ n)) → proj₁ (find3 H) ≡ 3<br>
thm&#39; _ = refl<br>
-----------------------------------------------------------------<br>
<br>
Ulf wrote that there will be difficulties in proving the properties<br>
of the results of  findNatByContra<br>
(right?).<br>
<br>
find3  means finding the first n equal to 3.<br>
And the programmer pretends that he has not a proof for<br>
``exists n equal to 3&#39;&#39; other than termination by contradiction.<br>
<br>
thm&#39;  is an attempt for such a proof.<br>
<br>
1) The type checker does not loop.<br>
2) It reports that  refl  does not have the needed type.<br>
<br>
Is this because it does not try to normalize  (find3 H)  in the type of<br>
thm&#39; ?<br>
<br>
I am trying to provide the feature ``classic termination proof&#39;&#39; with<br>
some possibilities in Agda.<br>
<br>
Suppose the pragma  {-# NORMALIZE_UP m #-}<br>
means to do only  m  loops (`steps&#39; ?) of normalization when<br>
type-checking.<br>
In this case,  m = 4  will, probably, accept this  refl  as a proof.<br>
<br>
Will it?<br></blockquote><div><br></div><div>First of all, I got overruled on the behaviour of NO_TERMINATION_CHECK. I&#39;ve implemented a new pragma NON_TERMINATING with the non-looping behaviour.</div><div><br></div><div>

The reason you get a type error in thm&#39; is as you suspect because the type checker does not reduce find3 H (or rather it does reduce find3, but not findNatByContra).</div><div><br></div><div>Probably m = 4 would not be enough since each iteration of findFrom requires several reductions. Fortunately you can program this yourself without the need of a special pragma. Here&#39;s my version:</div>

<div><br></div><div><div><font face="courier new, monospace">private</font></div><div><font face="courier new, monospace">  {-# NON_TERMINATING #-}</font></div><div><font face="courier new, monospace">  -- This won&#39;t be reduced by the type checker</font></div>

<div><font face="courier new, monospace">  findFromUnsafe : {P : ℕ → Set} (P? : Decidable P) → ℕ → Σ ℕ P</font></div><div><font face="courier new, monospace">  findFromUnsafe P? n =</font></div><div><font face="courier new, monospace">    case P? n of</font></div>

<div><font face="courier new, monospace">    λ { (yes Pn) → (n , Pn)</font></div><div><font face="courier new, monospace">      ; (no _)   → findFromUnsafe P? (suc n) }</font></div><div><font face="courier new, monospace"><br>

</font></div><div><font face="courier new, monospace">  -- This will be reduced</font></div><div><font face="courier new, monospace">  findFromSafeish : {P : ℕ → Set} (P? : Decidable P) → ℕ → ℕ → Σ ℕ P</font></div><div><font face="courier new, monospace">  findFromSafeish P? zero n = findFromUnsafe P? n</font></div>

<div><font face="courier new, monospace">  findFromSafeish P? (suc steps) n =</font></div><div><font face="courier new, monospace">    case P? n of</font></div><div><font face="courier new, monospace">    λ { (yes Pn) → (n , Pn)</font></div>

<div><font face="courier new, monospace">      ; (no _)   → findFromSafeish P? steps (suc n) }</font></div><div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace">findNatByContra :</font></div>

<div><font face="courier new, monospace">         ℕ → (P : ℕ → Set) → (P? : Decidable P) → ¬ (∀ n → ¬ P n) → Σ ℕ P</font></div><div><font face="courier new, monospace">findNatByContra steps P P? _ = findFromSafeish P? steps 0</font></div>

<div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace">eq3 : ℕ → Set</font></div><div><font face="courier new, monospace">eq3 = _≡_ 3</font></div><div><font face="courier new, monospace"><br>

</font></div><div><font face="courier new, monospace">eq3? : Decidable eq3</font></div><div><font face="courier new, monospace">eq3? = _≟_ 3</font></div><div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace">find3 :  ¬ (∀ n → 3 ≢ n) → Σ ℕ (_≡_ 3)</font></div>

<div><font face="courier new, monospace">find3 H =  findNatByContra 4 eq3 eq3? H</font></div><div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace">-- Checks</font></div><div><font face="courier new, monospace">thm&#39; : (H : ¬ (∀ n → 3 ≢ n)) → proj₁ (find3 H) ≡ 3</font></div>

<div><font face="courier new, monospace">thm&#39; _ = refl</font></div></div><div><br></div><div>The trick here is that for the first &#39;steps&#39; iterations you run the safe findFrom that does reduce, and</div><div>when you run out of steps you fall back to the unsafe one which doesn&#39;t.<br>

</div><div><br></div><div>/ Ulf</div></div></div></div>