Sergei Meshveliani

2018-01-23 13:14:03 UTC

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

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

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