<div dir="ltr"><div><div>One solution is to use &#39;let&#39; instead of &#39;where&#39;:<br><br><div style="margin-left:40px">lemma :  ∀ n → n ≤ n + 1<br>lemma 0             =  z≤n<br>lemma 1             =  s≤s z≤n<br>lemma (suc (suc n)) =<br>  let n&#39;≤n&#39;+1 = lemma (suc n)<br>  in  s≤s n&#39;≤n&#39;+1<br><br></div>I&#39;m not sure why Agda accepts the let-version, but not the where-version, though.<br><br></div>cheers,<br></div>Jesper<br><div><div><div><div><br></div></div></div></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Mon, May 2, 2016 at 11:47 AM, Sergei Meshveliani <span dir="ltr">&lt;<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi,<br>
<br>
Can people advise, please, on the following subject?<br>
The below program can be rewritten with removing a double `suc&#39; pattern.<br>
But let it be a contrived example:<br>
<br>
------------------------------------------------------------------<br>
open import Relation.Binary.PropositionalEquality as PE using (_≡_)<br>
open import Data.Nat using (ℕ; suc; _+_; _≤_; pred)<br>
<br>
open _≤_<br>
<br>
lemma :  ∀ n → n ≤ n + 1<br>
lemma 0             =  z≤n<br>
lemma 1             =  s≤s z≤n<br>
lemma (suc (suc n)) =  s≤s n&#39;≤n&#39;+1  where<br>
                                    n&#39;≤n&#39;+1 = lemma (suc n)<br>
------------------------------------------------------------------<br>
<br>
Agda does not see termination here.<br>
What is the nicest way to prove termination with preserving this suc-suc<br>
pattern?<br>
I write it this way:<br>
<br>
--------------------------------<br>
lemma n =  aux n (pred n) PE.refl<br>
  where<br>
  aux : (n m : ℕ) → m ≡ pred n → n ≤ n + 1<br>
  aux 0             _  _    =  z≤n<br>
  aux 1             _  _    =  s≤s z≤n<br>
  aux (suc (suc n)) 0  ()<br>
  aux (suc (suc n)) (suc m) m&#39;≡pred-n&#39;&#39; =  s≤s n&#39;≤n&#39;+1<br>
                               where<br>
                               m≡pred-n&#39; = PE.cong pred m&#39;≡pred-n&#39;&#39;<br>
                               n&#39;≤n&#39;+1   = aux (suc n) m m≡pred-n&#39;<br>
---------------------------------<br>
<br>
And it looks awkward.<br>
<br>
Thanks,<br>
<br>
------<br>
Sergei<br>
<br>
<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div><br></div>