[Agda] termination by contradiction

[Ulf Norell]

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 reason you get a type error in thm' is as you suspect because the type
checker does not reduce find3 H (or rather it does reduce find3, but not
findNatByContra).

Probably m = 4 would not be enough since each iteration of findFrom
requires several reductions. 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

The trick here is that for the first 'steps' iterations you run the safe
findFrom that does reduce, and
when you run out of steps you fall back to the unsafe one which doesn't.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140707/d8a9fc4b/attachment.html