[Agda] termination by contradiction

[Sergei Meshveliani]

To my question about a termination proof by contradiction

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

Ulf Norell writes on 2 Jul 2014

>[..]
> 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). 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.

I have installed Agda of July 7, 2014 
(in which the checker loop is fixed), and tried this program version:

----------------------------------------------------------------
{-# NO_TERMINATION_CHECK #-}
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) }

eq3 : ℕ → Set
eq3 = _≡_ 3

eq3? : Decidable eq3
eq3? = _≟_ 3

find3 :  ¬ (∀ n → 3 ≢ n) → Σ ℕ (_≡_ 3)
find3 H =  findNatByContra eq3 eq3? H

thm' : (H : ¬ (∀ n → 3 ≢ n)) → proj₁ (find3 H) ≡ 3
thm' _ = refl
-----------------------------------------------------------------

Ulf wrote that there will be difficulties in proving the properties
of the results of  findNatByContra
(right?).

find3  means finding the first n equal to 3.
And the programmer pretends that he has not a proof for 
``exists n equal to 3'' other than termination by contradiction.
 
thm'  is an attempt for such a proof.

1) The type checker does not loop.
2) It reports that  refl  does not have the needed type.

Is this because it does not try to normalize  (find3 H)  in the type of
thm' ?

I am trying to provide the feature ``classic termination proof'' with
some possibilities in Agda.

Suppose the pragma  {-# NORMALIZE_UP m #-}
means to do only  m  loops (`steps' ?) of normalization when
type-checking.
In this case,  m = 4  will, probably, accept this  refl  as a proof.
 
Will it?

Regards,

------
Sergei