[Agda] Re: double constructor termination

[Sergei Meshveliani]

Jesper, thank you. 
Such an unexpected power of `let' !

Dear Agda developers, can `where' be improved so that to support
termination similarly as `let' does in this example?

------
Sergei


On Mon, 2016-05-02 at 12:07 +0200, Jesper Cockx wrote:
> One solution is to use 'let' instead of 'where':
> 
> lemma :  ∀ n → n ≤ n + 1
> lemma 0             =  z≤n
> lemma 1             =  s≤s z≤n
> lemma (suc (suc n)) =
>   let n'≤n'+1 = lemma (suc n)
>   in  s≤s n'≤n'+1
> 
> 
> I'm not sure why Agda accepts the let-version, but not the
> where-version, though.
> 
> 
> cheers,
> 
> Jesper
> 
> 
> 
> On Mon, May 2, 2016 at 11:47 AM, Sergei Meshveliani <mechvel at botik.ru>
> wrote:
>         Hi,
>         
>         Can people advise, please, on the following subject?
>         The below program can be rewritten with removing a double
>         `suc' pattern.
>         But let it be a contrived example:
>         
>
------------------------------------------------------------------
>         open import Relation.Binary.PropositionalEquality as PE using
>         (_≡_)
>         open import Data.Nat using (ℕ; suc; _+_; _≤_; pred)
>         
>         open _≤_
>         
>         lemma :  ∀ n → n ≤ n + 1
>         lemma 0             =  z≤n
>         lemma 1             =  s≤s z≤n
>         lemma (suc (suc n)) =  s≤s n'≤n'+1  where
>                                             n'≤n'+1 = lemma (suc n)
>
------------------------------------------------------------------
>         
>         Agda does not see termination here.
>         What is the nicest way to prove termination with preserving
>         this suc-suc
>         pattern?
>         I write it this way:
>         
>         --------------------------------
>         lemma n =  aux n (pred n) PE.refl
>           where
>           aux : (n m : ℕ) → m ≡ pred n → n ≤ n + 1
>           aux 0             _  _    =  z≤n
>           aux 1             _  _    =  s≤s z≤n
>           aux (suc (suc n)) 0  ()
>           aux (suc (suc n)) (suc m) m'≡pred-n'' =  s≤s n'≤n'+1
>                                        where
>                                        m≡pred-n' = PE.cong pred
>         m'≡pred-n''
>                                        n'≤n'+1   = aux (suc n) m
>         m≡pred-n'
>         ---------------------------------
>         
>         And it looks awkward.
>         
>         Thanks,
>         
>         ------
>         Sergei
>         
>         
>         _______________________________________________
>         Agda mailing list
>         Agda at lists.chalmers.se
>         https://lists.chalmers.se/mailman/listinfo/agda
> 
>