[Agda] termination by contradiction

[Sergei Meshveliani]

On Mon, 2014-07-07 at 18:11 +0200, Ulf Norell wrote:
> 
> On Mon, Jul 7, 2014 at 2:36 PM, Sergei Meshveliani <mechvel at botik.ru>
> wrote:
>         
>         
>         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?
> 
> 
> First of all, I got overruled on the behaviour of
> NO_TERMINATION_CHECK. I've implemented a new pragma NON_TERMINATING
> with the non-looping behaviour.

The word  `non-terminating'  (algorithm Foo) already has a default
meaning:
``Foo does not terminate at each argument'', 
or may be,  ``Foo does not terminate at some argument''.
I wonder of whether the meaning of the NON_TERMINATING pragma 
can confuse with this meaning.

> [..]
>  Fortunately you can program this yourself without the need of a
> special pragma. Here's my version:
> 
> 
> private
>   {-# NON_TERMINATING #-}
>   -- This won't be reduced by the type checker
>   findFromUnsafe : {P : ℕ → Set} (P? : Decidable P) → ℕ → Σ ℕ P
>   findFromUnsafe P? n =
>     case P? n of
>     λ { (yes Pn) → (n , Pn)
>       ; (no _)   → findFromUnsafe P? (suc n) }
> 
> 
>   -- This will be reduced
>   findFromSafeish : {P : ℕ → Set} (P? : Decidable P) → ℕ → ℕ → Σ ℕ P
>   findFromSafeish P? zero n = findFromUnsafe P? n
>   findFromSafeish P? (suc steps) n =
>     case P? n of
>     λ { (yes Pn) → (n , Pn)
>       ; (no _)   → findFromSafeish P? steps (suc n) }
> 
> 
> findNatByContra :
>       ℕ → (P : ℕ → Set) → (P? : Decidable P) → ¬ (∀ n → ¬ P n) → Σ ℕ P
> findNatByContra steps P P? _ = findFromSafeish P? steps 0
> 
> eq3 : ℕ → Set
> eq3 = _≡_ 3

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

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

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

Great!
I have an impression that classical proofs for termination can work
under this approach.
 
Thank you.

------
Sergei