[Agda] difficult termination

[Nils Anders Danielsson]

On 2017-11-20 18:03, Sergei Meshveliani wrote:
> This can be finding by  searching through  of any  n : ℕ  satisfying
> some subtle property  P.
> It needs to be known a non-constructive proof for  ∃ \(n : ℕ) → P n,
> but a bound for such  x  to be not known.
> I wonder what might be this example.

It should not be possible to implement something with the following type
in Agda (if it is, then that is a bug):

   (P : ℕ → Set) → (∀ n → Dec (P n)) → ¬ ¬ ∃ P → ∃ P

This is (one form of) Markov's principle.

Here is one implementation that Agda rejects:

   markov : (P : ℕ → Set) → (∀ n → Dec (P n)) → ¬ ¬ ∃ P → ∃ P
   markov P dec _ = search 0
     where
     search : ℕ → ∃ P
     search n with dec n
     ... | yes p = n , p
     ... | no _  = search (suc n)

-- 
/NAD