<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"><<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>></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' : (H : ¬ (∀ n → 3 ≢ n)) → proj₁ (find3 H) ≡ 3<br>
thm' _ = 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'' other than termination by contradiction.<br>
<br>
thm' 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' ?<br>
<br>
I am trying to provide the feature ``classic termination proof'' with<br>
some possibilities in Agda.<br>
<br>
Suppose the pragma {-# NORMALIZE_UP m #-}<br>
means to do only m loops (`steps' ?) 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'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' 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'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'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' : (H : ¬ (∀ n → 3 ≢ n)) → proj₁ (find3 H) ≡ 3</font></div>
<div><font face="courier new, monospace">thm' _ = refl</font></div></div><div><br></div><div>The trick here is that for the first 'steps' 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't.<br>
</div><div><br></div><div>/ Ulf</div></div></div></div>