[Agda] strange Termination problem

[mechvel at scico.botik.ru]

On 2022-02-08 16:55, Jason Hu wrote:
> Is Patterns nonempty list? If so, that’s the reason. Two ∷ are  
> different constructors.
> 

In addition to my response:
in this program  _∷_  is of List and also of All.
When Agda cannot resolve, it reports. For example, I write
  lev tail : DimLevel

to help it to solve that _∷_ is of List there.


> From: mechvel at scico.botik.ru
> Sent: Tuesday, February 8, 2022 8:51 AM
> To: agda at lists.chalmers.se
> Subject: [Agda] strange Termination problem
> 
> Please, why does  Agda 2.6.2.1  reports "Termination checking failed"
> for the following program?
> (not a full code)
> 
> ------------------------------------------------------
> foo :  ∀ {e lev} → e ReducesLevel lev →
>                   sizeHead (reduceLevel e lev) <nn (lSize lev)
> 
> foo {e} {d , ps} (d≢0 , any-e-reduces-ps) =
>                          aux d ps d≢0 any-e-reduces-ps
>    where
>    aux : (d : ℕ) (ps : Patterns) → d ≢ 0 →
>          let lev = (d , ps)
>          in
>          Any (e Reduces_) ps →
>          sizeHead (reduceLevel e lev) <nn (lSize lev)
> 
>    aux 0       _             _     _                  =  anything
>    aux _       _             _     (there _)          =  anything
>    aux (suc d) (p ∷ [])      _     (here e-reduces-p) =  anything
>    aux (suc d) (p ∷ p' ∷ ps) 1+d≢0 (here e-reduces-p) =
> 
>      aux' (e reduces? p) (any? (e reduces?_) (p' ∷ ps))  -- line
> 1669
>      where
>      1+d = suc d
> 
>      lev tail : DimLevel
>      lev  = (1+d , p ∷ p' ∷ ps)
>      tail = (1+d , p' ∷ ps)
> 
>      |pp'ps|          = length (p ∷ p' ∷ ps)
>      redexes          = reduceLevel e lev
>      tail-redexes     = reduceLevel e tail
>      sh[tail-redexes] = sizeHead tail-redexes
>      d₂    = proj₁ sh[tail-redexes]
>      |ps₂| = proj₂ sh[tail-redexes]
> 
>      aux' :  Dec (e Reduces p) → Dec (Any (e Reduces_) (p' ∷ ps))
> →
>              sizeHead (reduceLevel e lev) <nn (1+d , |pp'ps|)
> 
>      aux' (no ¬reduces-p) _  = contradiction e-reduces-p ¬reduces-p
>      aux' (yes reduces-p) (no ¬e-reduces-any-p'ps) =  anything
>      aux' (yes reduces-p) (yes e-reduces-any-p'ps) =
> 
>        aux'' (d₂ <? 1+d) (aux 1+d (p' ∷ ps) 1+d≢0
> e-reduces-any-p'ps)  --
> line 1691
>        where
>        aux'' : Dec (d₂ < 1+d) → sh[tail-redexes] <nn (lSize tail)
> →
>                                 sizeHead redexes <nn (1+d , |pp'ps|)
>        aux'' _ _ = anything
> ------------------------------------------------------
> 
> It reports
> -----------------------------
> Termination checking failed for the following functions:
> Problematic calls:
>   aux' (e reduces? p) (any? (_reduces?_ e) (p' ∷ ps))
>      (at  1669,29-33)
> 
>   aux (1+d d p p' ps 1+d≢0 e-reduces-p) (p' ∷ ps) 1+d≢0
> e-reduces-any-p'ps
>      (at  1691,34-37)
> -----------------------------
> 
> The only recursive call is for  aux.
> The head call is
>    aux (suc d) (p ∷ p' ∷ ps) 1+d≢0 (here e-reduces-p).
> 
> It calls for
>    aux' (e reduces? p) (any? (e reduces?_) (p' ∷ ps)).
> 
> And this latter calls for
>    aux'' (d₂ <? 1+d) (aux 1+d (p' ∷ ps) 1+d≢0
> e-reduces-any-p'ps)
> 
> The latter call for  aux  has  (p' ∷ ps)
> among arguments,
> while the head call of  aux  had  (p ∷ p' ∷ ps)
> for this argument.
> 
> {-# OPTIONS --termination-depth=3 #-}  does not help.
> 
> Can you, please, give a hint:
> why structural recursion does not work here?
> 
> Also the report prints  "aux (1+d d p p' ps 1+d≢0 e-reduces-p) ..."
> instead of
>          "aux (1+d (p' ∷ ps) 1+d≢0 e-reduces-p) ...".
> 
> It is misleading, because  aux  has four arguments,
> while the report prints six arguments.
> 
> ?
> 
> ------
> 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