[Agda] proofs for (NON)TERMINATING

[Sergei Meshveliani]

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

[Nils Anders Danielsson]

Post by Sergei Meshveliani
Is it possible to express and prove in Agda the above lemma?

If you want to prove properties of possibly non-terminating code in
Agda, then I suggest that you avoid using TERMINATING/NON_TERMINATING
and instead use one of several methods to represent non-terminating
computations as total values. One possibility is to use the delay monad.

[Sergei Meshveliani]

Post by Nils Anders Danielsson

Post by Sergei Meshveliani
Is it possible to express and prove in Agda the above lemma?

If you want to prove properties of possibly non-terminating code in
Agda, then I suggest that you avoid using TERMINATING/NON_TERMINATING
and instead use one of several methods to represent non-terminating
computations as total values. One possibility is to use the delay monad.

Please, where it is described the delay monad ?
(I see a certain Monad.agda in Standard library, but do not find the
`delay' word).

------
Sergei

[Nils Anders Danielsson]

Post by Sergei Meshveliani
Please, where it is described the delay monad ?

Venanzio Capretta
General Recursion via Coinductive Types
https://doi.org/10.2168/LMCS-1(2:1)2005

The standard library contains an implementation in
Category.Monad.Partiality. I would not recommend that you use this
implementation. I have another implementation that uses sized types, and
which is therefore in my opinion easier to use (the delay-monad library,
available from http://www.cse.chalmers.se/~nad/software.html). However,
this implementation depends on a different library, which is set up in a
somewhat roundabout way in order to cater to a certain experiment. I
believe others have also implemented the delay monad using sized types.

Here's an example of how one can implement an interpreter for the
untyped λ-calculus using the delay monad:

http://www.cse.chalmers.se/~nad/listings/partiality-monad/Lambda.Simplified.Delay-monad.Interpreter.html

[Jesper Cockx]

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

Post by Sergei Meshveliani
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
https://lists.chalmers.se/mailman/listinfo/agda

[Sergei Meshveliani]

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

[Jesper Cockx]

It is needed to represent and prove the statement
"if (f 0) terminates, then Even (f 0)" (I).

I don't think it's possible to formulate inside Agda what it means for a
function with a {-# NON_TERMINATING #-} pragma to terminate. So I also
don't think it's possible to represent the statement you want. If you want
to reason in Agda about termination of functions, I'd recommend to use the
Delay monad as Nils suggested.

-- Jesper

Post by Sergei Meshveliani
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
[..]
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?
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

[Martin Escardo]

Post by Sergei Meshveliani
It is needed to represent and prove the statement
                "if (f 0) terminates, then  Even (f 0)"     (I).
I don't think it's possible to formulate inside Agda what it means for a
function with a {-# NON_TERMINATING #-} pragma to terminate. So I also
don't think it's possible to represent the statement you want. If you
want to reason in Agda about termination of functions, I'd recommend to
use the Delay monad as Nils suggested.

Or you can define a relation R, and show that if R 0 y then y is even.

M.

Post by Sergei Meshveliani
-- Jesper
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
[..]
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?
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
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

[Sergei Meshveliani]

Post by Sergei Meshveliani
It is needed to represent and prove the statement
"if (f 0) terminates, then Even (f 0)"
(I).
I don't think it's possible to formulate inside Agda what it means for
a function with a {-# NON_TERMINATING #-} pragma to terminate. So I
also don't think it's possible to represent the statement you want. If
you want to reason in Agda about termination of functions, I'd
recommend to use the Delay monad as Nils suggested.

Can anybody, please, demonstrate the usage of the Delay monad on the
below example of f : ℕ → ℕ and expressing the statement

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



-------------------------------------------------------------------
open import Relation.Nullary using (yes; no)
open import Relation.Unary using (Decidable)
open import Data.Nat using (ℕ; suc; _+_)

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


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
----------------------------------------------------------------------


Thanks,

------
Sergei

[Nils Anders Danielsson]

Post by Sergei Meshveliani
Can anybody, please, demonstrate the usage of the Delay monad on the
below example of f : ℕ → ℕ and expressing the statement
"if (f 0) terminates, then Even (f 0)" (I)

.agda-lib file:

depend: equality delay-monad

.agda file:

module _ where

open import Delay-monad
open import Delay-monad.Always
open import Delay-monad.Monad
open import Equality.Propositional
open import Prelude

open import Monad equality-with-J

Even : ℕ → Set
Even n = ∃ λ k → n ≡ k + k

module _
(P : ℕ → Set)
(p? : ∀ n → Dec (P n))
where

f : ∀ {i} → ℕ → Delay ℕ i
f n with p? n
... | yes _ = return (n + n)
... | no _ = later λ { .force → f (suc n) }

f-even : ∀ {i} n → □ i Even (f n)
f-even n with p? n
... | yes _ = now (n , refl)
... | no _ = later λ { .force → f-even (suc n) }

[Sergei Meshveliani]

Post by Nils Anders Danielsson

Post by Sergei Meshveliani
Can anybody, please, demonstrate the usage of the Delay monad on the
below example of f : ℕ → ℕ and expressing the statement
"if (f 0) terminates, then Even (f 0)" (I)

depend: equality delay-monad
module _ where
open import Delay-monad
open import Delay-monad.Always
open import Delay-monad.Monad
open import Equality.Propositional
open import Prelude
open import Monad equality-with-J
Even : ℕ → Set
Even n = ∃ λ k → n ≡ k + k
module _
(P : ℕ → Set)
(p? : ∀ n → Dec (P n))
where
f : ∀ {i} → ℕ → Delay ℕ i
f n with p? n
... | yes _ = return (n + n)
... | no _ = later λ { .force → f (suc n) }
f-even : ∀ {i} n → □ i Even (f n)
f-even n with p? n
... | yes _ = now (n , refl)
... | no _ = later λ { .force → f-even (suc n) }

Thank you. I shall keep this in mind.
One day the DoCon-A library may need to prove something about a function
with unsolved termination domain.

------
Sergei