<div dir="ltr"><div><div>If you define a function with a {-# NON_TERMINATING #-} pragma then it's generally not possible to prove things about it because Agda will refuse to evaluate it. This is also the problem in your example: even though in this case evaluation is terminating, Agda will play it safe and block *all* evaluation of the NON_TERMINATING function. So I don't think what you're trying to do is currently possible in Agda.</div><div><br></div><div>A workaround is to postulate the clauses of the non-terminating function as propositional equalities (i.e. elements of the ≡ type). This allows you to prove properties of the non-terminating function without breaking the Agda typechecker (as you risk doing when using TERMINATING). In your example:</div><div><br></div><div>
------------------------------<wbr>------------------------------<wbr>--------</div><div>open import Relation.Nullary using (yes; no; ¬_)<br>open import Relation.Binary  using (Decidable)<br>open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; inspect; [_])<br>open import Data.Empty   using (⊥-elim)<br>open import Data.Product using (_,_; proj₁; proj₂; ∃)<br>open import Data.Nat     using (ℕ; suc)<br><br>postulate  P  : ℕ → ℕ → Set<br>           p? : Decidable P<br><br>{-# NON_TERMINATING #-}<br>find : (m : ℕ) → ℕ → ∃ (\k → P m k)<br>find m n<br>       with p? m n<br>...    | yes pmn = (n , pmn)       -- found<br>...    | no _    = find m (suc n)  -- try next<br><br>postulate<br>  find-yes : (m n : ℕ) ( pmn :   P m n) → p? m n ≡ yes pmn → find m n ≡ (n , pmn)<br>  find-no  : (m n : ℕ) (¬pmn : ¬ P m n) → p? m n ≡ no ¬pmn → find m n ≡ find m (suc n)<br><br>lemma :  ∀ m → P m 0 → proj₁ (find m 0) ≡ 0<br>lemma m pm0<br>    with p? m 0 | inspect (λ m → p? m 0) m<br>... | yes pm0'  | [ proof ] = cong proj₁ (find-yes m 0 pm0' proof)<br>... | no  ¬pm0  | _         = ⊥-elim (¬pm0 pm0)<br></div><div>
------------------------------<wbr>------------------------------<wbr>--------<br>

</div><div><br></div>Something we could consider adding to Agda is some facility to get hold of the clauses of a non-terminating function automatically, so you wouldn't have to postulate them.<br><br></div>-- Jesper<br></div><div class="gmail_extra"><br><div class="gmail_quote">On Tue, Jan 23, 2018 at 2:14 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:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Can somebody, please, explain how to express/prove the following lemma?<br>
<br>
------------------------------<wbr>------------------------------<wbr>-------<br>
open import Relation.Nullary using (yes; no)<br>
open import Relation.Binary  using (Decidable)<br>
open import Relation.Binary.<wbr>PropositionalEquality using (_≡_; refl)<br>
open import Data.Empty   using (⊥-elim)<br>
open import Data.Product using (_,_; proj₁; ∃)<br>
open import Data.Nat     using (ℕ; suc)<br>
<br>
postulate  P  : ℕ → ℕ → Set<br>
           p? : Decidable P<br>
<br>
{-# NON_TERMINATING #-}<br>
find : (m : ℕ) → ℕ → ∃ (\k → P m k)<br>
find m n<br>
       with p? m n<br>
...    | yes pmn = (n , pmn)       -- found<br>
...    | no _    = find m (suc n)  -- try next<br>
<br>
lemma :  ∀ m → P m 0 → proj₁ (find m 0) ≡ 0<br>
lemma m pm0<br>
        with p? m 0<br>
...     | yes _   =  refl<br>
...     | no ¬pm0 =  ⊥-elim (¬pm0 pm0)<br>
------------------------------<wbr>------------------------------<wbr>--------<br>
<br>
For some P above the algorithm `find' is not terminating.<br>
So that this program would not type-check without pragma.<br>
The TERMINATING pragma is wrong to set.<br>
So, NON_TERMINATING is needed (?).<br>
<br>
Then, it occurs that `lemma' is not type-checked.<br>
This contradicts to the fact that  (find m 0)  terminates when  (P m 0)<br>
is satisfied.<br>
<br>
Is it possible to express and prove in Agda the above lemma?<br>
<br>
Thanks,<br>
<br>
------<br>
Sergei<br>
<br>
______________________________<wbr>_________________<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" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
</blockquote></div><br></div>