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.
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:
--------------------------------------------------------------------
open import Relation.Nullary using (yes; no; ¬_)
open import Relation.Binary using (Decidable)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong;
inspect; [_])
open import Data.Empty using (⊥-elim)
open import Data.Product using (_,_; proj₁; proj₂; ∃)
open import Data.Nat using (ℕ; suc)
postulate P : ℕ → ℕ → Set
p? : Decidable P
{-# NON_TERMINATING #-}
find : (m : ℕ) → ℕ → ∃ (\k → P m k)
find m n
with p? m n
... | yes pmn = (n , pmn) -- found
... | no _ = find m (suc n) -- try next
postulate
find-yes : (m n : ℕ) ( pmn : P m n) → p? m n ≡ yes pmn → find m n ≡ (n
, pmn)
find-no : (m n : ℕ) (¬pmn : ¬ P m n) → p? m n ≡ no ¬pmn → find m n ≡
find m (suc n)
lemma : ∀ m → P m 0 → proj₁ (find m 0) ≡ 0
lemma m pm0
with p? m 0 | inspect (λ m → p? m 0) m
... | yes pm0' | [ proof ] = cong proj₁ (find-yes m 0 pm0' proof)
... | no ¬pm0 | _ = ⊥-elim (¬pm0 pm0)
--------------------------------------------------------------------
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.
-- Jesper
On Tue, Jan 23, 2018 at 2:14 PM, Sergei Meshveliani <mechvel at botik.ru>
wrote:
> Can somebody, please, explain how to express/prove the following lemma?
>
> -------------------------------------------------------------------
> open import Relation.Nullary using (yes; no)
> open import Relation.Binary using (Decidable)
> open import Relation.Binary.PropositionalEquality using (_≡_; refl)
> open import Data.Empty using (⊥-elim)
> open import Data.Product using (_,_; proj₁; ∃)
> open import Data.Nat using (ℕ; suc)
>
> postulate P : ℕ → ℕ → Set
> p? : Decidable P
>
> {-# NON_TERMINATING #-}
> find : (m : ℕ) → ℕ → ∃ (\k → P m k)
> find m n
> with p? m n
> ... | yes pmn = (n , pmn) -- found
> ... | no _ = find m (suc n) -- try next
>
> lemma : ∀ m → P m 0 → proj₁ (find m 0) ≡ 0
> lemma m pm0
> with p? m 0
> ... | yes _ = refl
> ... | no ¬pm0 = ⊥-elim (¬pm0 pm0)
> --------------------------------------------------------------------
>
> For some P above the algorithm `find' is not terminating.
> So that this program would not type-check without pragma.
> The TERMINATING pragma is wrong to set.
> So, NON_TERMINATING is needed (?).
>
> Then, it occurs that `lemma' is not type-checked.
> This contradicts to the fact that (find m 0) terminates when (P m 0)
> is satisfied.
>
> Is it possible to express and prove in Agda the above lemma?
>
> Thanks,
>
> ------
> Sergei
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180123/8813879b/attachment.html>