[Agda] list for termination counter

[G. Allais]

Hi Sergei,

The issue comes from the pattern-matching lambda: it is quite often
the case that it hides a termination argument from Agda. Using an
equivalent `with` clause solves the issue:

---------------------------------------------------------------
add : Op₂ R
add (r [])       g            =  g
add f            (r [])       =  f
add (r (m ∷ ms)) (r (n ∷ ns)) with m ≤? n
... | yes _ = let (r hMems) = add (r (m ∷ ms)) (r ns)
               in  r (n ∷ hMems)
... | no _  = let (r hMems) = add (r ms) (r (n ∷ ns))
               in  r (m ∷ hMems)
---------------------------------------------------------------

Alternatively you can lift the recursive calls outside of the pattern
matching lambda (if your target language is lazy, the complexity should
be the same):

---------------------------------------------------------------
add' : Op₂ R
add' (r [])       g            =  g
add' f            (r [])       =  f
add' (r (m ∷ ms)) (r (n ∷ ns)) =
   let yesIH = add' (r ms) (r (n ∷ ns))
       noIH  = add' (r ms) (r (n ∷ ns))
   in case
         m ≤? n
     of \
     { (yes _) → let (r hMems) = yesIH
                 in  r (n ∷ hMems)

     ; (no _)  → let (r hMems) = noIH
                 in  r (m ∷ hMems)
     }	
---------------------------------------------------------------

Cheers,

On 22/08/16 14:48, Sergei Meshveliani wrote:
> Can somebody explain, please,
> what may be a simple way to prove termination in the following example?
>
>
> ---------------------------------------------------------------
> open import Function                   using (case_of_)
> open import Algebra.FunctionProperties using (Op₂)
> open import Relation.Nullary using (yes; no)
> open import Relation.Binary  using (DecTotalOrder)
> open import Relation.Binary.PropositionalEquality as PE using(_≡_)
> open import Data.Nat  using (ℕ; decTotalOrder)
> open import Data.List using (List; []; _∷_)
>
> open DecTotalOrder decTotalOrder using (_≤?_)
>
> record R : Set where
>                constructor r
>                field  members : List ℕ
>
> add : Op₂ R
>
> add (r [])       g            =  g
> add f            (r [])       =  f
> add (r (m ∷ ms)) (r (n ∷ ns)) =
>     case
>         m ≤? n
>     of \
>     { (yes _) → let (r hMems) = add (r (m ∷ ms)) (r ns)
>                 in  r (n ∷ hMems)
>
>     ; (no _)  → let (r hMems) = add (r ms) (r (n ∷ ns))
>                 in  r (m ∷ hMems)
>     }
> --------------------------------------------------------------------
>
> This is something similar to merging of ordered lists.
> Agda does not see termination. I think, this is due to that the lists
> are kept under the constructor r.
> So, I extract the two lists and use them as counters for termination:
>
> -------------------------------------------------------------------
> add f g =  aux f g (R.members f) (R.members g) PE.refl PE.refl
>   where
>   aux : (f g : R) → (ms ns : List ℕ) → ms ≡ R.members f →
>                                        ns ≡ R.members g → R
>
>   aux (r .[]) g        [] _  PE.refl _       =  g
>   aux f       (r .[])  _  [] _       PE.refl =  f
>
>   aux (r .(m ∷ ms)) (r .(n ∷ ns)) (m ∷ ms) (n ∷ ns) PE.refl PE.refl =
>     case
>         m ≤? n
>     of \
>     { (yes _) → let (r hMems) = aux (r (m ∷ ms)) (r ns) (m ∷ ms) ns
>                                                         PE.refl PE.refl
>                 in  r (n ∷ hMems)
>
>     ; (no _)  → let (r hMems) = aux (r ms) (r (n ∷ ns)) ms (n ∷ ns)
>                                                         PE.refl PE.refl
>                 in  r (m ∷ hMems)
>     }
> ------------------------------------------------------------------------
>
> The 'yes' pattern calls aux with  ns  -- which list expression is
> syntactically smaller than   n ∷ ns.
> The 'no' pattern calls aux with  ms  -- which list expression is
> syntactically smaller than   m ∷ ms.
>
> But Agda still reports : "Termination checking failed".
>
> Why?
> How to fix?
> What is a simple way to prove termination in this example?
>
> Thanks,
>
> ------
> Sergei
>
>
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>