[Agda] termination by contradiction

[Sergei Meshveliani]

On Wed, 2014-07-02 at 11:12 +0200, Ulf Norell wrote:
> 
> 
> 
> On Tue, Jul 1, 2014 at 10:04 PM, Altenkirch Thorsten
> <psztxa at exmail.nottingham.ac.uk> wrote:
>         
>         
>         On 01/07/2014 20:40, "Sergei Meshveliani" <mechvel at botik.ru>
>         wrote:
>         
>         >
>         >Consider the example:
>         >
>         >  findNatByContra :
>         >     (P : ℕ → Set) → (P? : Decidable P) → ¬ (∀ n → ¬ P n) → Σ
>         ℕ P
>         >
>         >  findNatByContra P P? _ =  findFrom 0
>         >    where
>         >    findFrom : ℕ → Σ ℕ P
>         >    findFrom n = case P? n of \ { (yes Pn) → (n , Pn)
>         >                                ; (no _)   → findFrom (suc
>         n) }
>         >
> [..]


> The problem is that findNatByContra never looks at the proof, so there
> is no guarantee that it's a closed proof (which Thorsten mentioned 
> above). 

Please, what is a  closed proof?


> For instance,
>
> False : ℕ → Set
> False _ = ⊥
>
> decFalse : Decidable False
> decFalse _ = no (λ x → x)
>
> loopy : ¬ (∀ n → ¬ False n) → Σ ℕ False
> loopy H = findNatByContra False decFalse H
> 
> 
> Here, loopy will happily evaluate forever with the hypothetical
> (classical) proof that there is a number satisfying False. There is no
> need to evaluate under the case since decFalse comes back 'no' for any
> number.


Can you, please, explain further?

To apply  (loopy H),  one needs to provide  
                                   H : (∀ n → ¬ False n) → ⊥. 

And this is not possible, because its type normalizes to 

((n : ℕ) → (False n → ⊥)) → ⊥,  and to  ((n : ℕ) → (⊥ → ⊥)) → ⊥,

and the type  (n : ℕ) → (⊥ → ⊥)  has a value  (\n → id)  in it.


As one cannot provide any argument value to `loopy',  how can it
evaluate forever?

I understand the whole story as follows.
If we assume the Markov's rule, then  findNatByContra  is terminating.
Agda does not find this termination.
So, in order to try Markov's approach in Agda, I set  
                                      {-# NO_TERMINATION_CHECK #-} 

for the function  findNatByContra  only
--- is this possible in Agda-2.4.0.1 ?
(anyway, one can place it into a separate file).

Then all the program is type-checked.

But  `loopy'  is still strange:  it can be applied only to an absurd
value.
So `loopy' is useless, it can appear only by a programmer mistake.
Hence what bad may happen from introducing   findNatByContra,
and even by occasionally adding `loopy' 
?
(I am about confused).

Regards,

------
Sergei