[Agda] double constructor termination

[Andreas Abel]

Let is just a notation for a substitution.
Where introduces new declarations.

The 'let'-fix is equivalent to

   lemma (suc (suc n)) =s≤s (lemma (suc n))

The 'where'-version should be equivalent to

   lemma (suc (suc n)) = s≤s (aux n)

   aux n = lemma (suc n)

This should work with OPTIONS --termination-depth=2
(untested).

On 02.05.2016 12:07, 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
> <mailto: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 <mailto: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
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/