[Agda] list for termination counter

[Sergei Meshveliani]

I see now. Thank you.

------
Sergei


On Tue, 2016-08-23 at 13:59 +0200, G. Allais wrote:
> 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
> >
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>