[Agda] double constructor termination

[Andreas Abel]

This works:

{-# OPTIONS --termination-depth=2 #-}

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)


On 03.05.2016 18:54, Andreas Abel wrote:
> 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/