On Tue, 2018-01-23 at 15:21 +0100, Jesper Cockx wrote:

JC: -------------------------------------------------------------------

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:

[..]

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)

[..]

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.

-------------------------------------------------------------------------

Thank you. This is interesting.

My goal is to find a simple way to express in Agda proofs about an

algorithm which termination domain is not known.

Is there a simpler approach than applying coinductive types and `delay'

monad?

I try your approach of "postulate-clauses" on the following simple

example.

f (m : ℕ) searches for n ≥ m such that P n, and when finds,

returns n + n.

It is needed to represent and prove the statement

"if (f 0) terminates, then Even (f 0)" (I).

--------------------------------------------------------------------

open import Function using (_∘_)

open import Relation.Nullary using (Dec; yes; no; ¬_)

open import Relation.Unary using (Decidable)

open import Relation.Binary.PropositionalEquality as PE using

(_≡_; refl; sym; trans; cong; subst)

open import Data.Product using (_×_; _,_; ∃)

open import Data.Nat using (ℕ; suc; _+_; _<_; _>_; _≤_)

open import Data.Nat.Properties using

(≤-refl; ≤-reflexive; ≤-trans; m+n∸m≡n; +-comm; +-assoc;

m≤m+n; <⇒≱; ≰⇒>; module ≤-Reasoning)

postulate P : ℕ → Set

p? : Decidable P

{-# NON_TERMINATING #-}

f : ℕ → ℕ -- find n satisfying (P n) and return n + n

f n

with p? n

... | yes _ = n + n -- found

... | no _ = f (suc n) -- try next

postulate f-yes : ∀ n → P n → f n ≡ n + n

f-no : ∀ n → ¬ P n → f n ≡ f (suc n)

data Even : ℕ → Set

where

even0 : Even 0

even+2 : {n : ℕ} → Even n → Even (suc (suc n))

postulate

even-n+n : ∀ n → Even (n + n) -- the proof skipped for brevity

postulate

minimizeSolution : ∀ m → P m → ∃ (\n → P n × f 0 ≡ f n)

--

-- Can be proved by moving from m to minimal i such that (P i),

-- and by applying f-yes, f-no.

theorem : ∀ m → P m → Even (f 0)

theorem m pm =

let

(n , pn , f0≡fn) = minimizeSolution m pm

fn≡n+n = f-yes n pn

even-fn = subst Even (sym fn≡n+n) (even-n+n n)

in

subst Even (sym f0≡fn) even-fn

------------------------------------------------------------------

First, I think that (Even (f 0)) cannot be proved. Right?

Further, the condition "if (f 0) terminates" is replaced with

"∀ m → P m".

I have an impression that `theorem' represents (I), in a certain sense,

and proves it.

Am I missing something?

In general:

this approach works when the programmer is able to formulate the

statement

"(g x1 ... xn) terminates"

as some Agda predicate in x1 ... xn.

For example, this is possible for any semidecision procedure g

(?)

I wonder: how generic is this approach.

What people think?

Thanks,

------

Sergei