[Agda] termination by contradiction

[Sergei Meshveliani]

On Thu, 2014-07-03 at 15:06 +0200, Ulf Norell wrote:
> Using NO_TERMINATION_CHECK is not going to cause the type
> checker to loop. What happens is that the type checker simply won't
> evaluate functions that haven't been termination checked. 


How does the below program correspond to these your two assertions? 

----------------------------------------------------------------------
open import Foreign.Haskell
open import IO.Primitive
open import Data.String as String using (toCostring)
open import Function         using (case_of_)
open import Relation.Nullary using (yes; no; ¬_)
open import Relation.Unary   using (Decidable)
open import Relation.Binary.PropositionalEquality as PE using 
                                                     (_≡_; refl)
open import Data.Empty   using (⊥)
open import Data.Product using (_,_; proj₁; Σ)
open import Data.Nat     using (ℕ; suc)

{-# 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) }
False : ℕ → Set
False _ = ⊥

decFalse : Decidable False
decFalse _ = no (λ x → x)

loopy : ¬ (∀ n → ¬ False n) → Σ ℕ False
loopy H =  findNatByContra False decFalse H

thm : (H : ¬ (∀ n → ¬ False n)) → proj₁ (loopy H) ≡ 42
thm _ = refl

main : IO Unit
main = putStrLn (toCostring "done")
----------------------------------------------------------------------

1) The checker loops at it  (Agda 2.4.0).
2) If  thm  is removed, than it is checked and compiled.
3) In expect that this NO_TERMINATION_CHECK applies only to the 
   function  findNatByContra.  Right?


> So it's
> perfectly safe for you to use findNatByContra in your programs. At
> run-time it will run fine, but you won't be able to prove any theorems
> about it since it doesn't reduce at type checking time.
> 


Regards,

------
Sergei