[Agda] double constructor termination

[Jesper Cockx]

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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160502/684aeeb3/attachment.html