[Agda] difficult termination

[Sergei Meshveliani]

On Mon, 2017-11-20 at 18:47 +0300, Sergei Meshveliani wrote:
> Dear all,
> 
> I am thinking of the practical termination proof possibility in Agda.
> 
> In my current practice with computer algebra, all termination proofs are
> as follows.
> 
> 1) Syntactic:  the built-in rule of Agda when in each recursive call of
> the function some argument is syntactically smaller (in a certain
> "subterm" ordering) than in the current call. 
> 
> 2) By the counter.

> [..]

> Further, the Ackermann's function 
>  
>  ack : ℕ → ℕ → ℕ
>  ack 0       m       =  suc m
>  ack (suc n) 0       =  ack n 1
>  ack (suc n) (suc m) =  ack n (ack (suc n) m)
> 
> is not primitively recursive. But Agda sees its termination by the
> syntactic comparison rule.
> 
> Can anybody give a _simple_ example of a terminating algorithm which
> is difficult or impossible to write in Agda with providing termination
> proof for Agda ?


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.

Regards,

------
Sergei