[Agda] termination by contradiction

[Sergei Meshveliani]

On 01/07/2014 16:19, Altenkirch Thorsten wrote:

> However, it is not clear how to do symbolic evaluation with MP. That
> is if we have a hypothetical classical proof of termination this
> doesn’t tell us wether we can partially execute our program. In the
> case of a constructive proof this is the case.
>
> We could say that we can run the program if the proof is closed but
> this seems a bit weird.

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

Assuming Markov's rule, we consider the type  
                                ¬ (∀ n → ¬ P n) → (\exist \n → P n)
as inhabited,
and this proves that  findFrom  is terminating.
Right?

> if we have a hypothetical classical proof of termination this
> doesn’t tell us wether we can partially execute our program. In the
> case of a constructive proof this is the case.

Do you consider the termination proof by 
                                    ¬ (∀ n → ¬ P n) → (\exist \n → P n)
as constructive?
Can we partially execute the program  findFrom ?
(why do you add `partially' ?).

Thanks,

------
Sergei