[Agda] Termination checking with Lexicographic recursive calls

[Sergey Goncharov]

Dear Nils,

OK, thanks! Indeed, it works with --termination-depth=2.

I sort of expected that the problem could be the recursive calls before 
the equality sign, but eliminating such calls does not seem to be 
enough, because the with-abstraction can occur also after the equality 
sign. That I did not expect. I believe, I had a version of this example, 
when precisely only the latter happened, but the termination checker 
still did not accept it.

Why do you say that the example is not self-contained? It uses the 
standard library -- otherwise it is complete.

Best,
Sergey



On 18/02/2020 13:04, Nils Anders Danielsson wrote:
> On 2020-02-17 19:03, Sergey Goncharov wrote:
>> Any ideas why the following is not accepted?
> 
>> h₁ (suc n) (suc k) p rewrite +-suc (π′ n + suc n) k with (π₁⁻¹ (π′ n + suc n + k)) | inspect π₁⁻¹ (π′ n + suc n + k)
>> h₁ (suc n) (suc k) p | zero  | [ eq ] = ⊥-elim (1+n≰n (≤-trans (m∸n≡0⇒m≤n {suc n} {k} (trans (sym (h₁ (suc n) k (≤-trans (n≤1+n k) p))) eq)) (≤-pred p)))
> 
> Auxiliary functions are generated when you use rewrite or with. In this
> case the auxiliary functions get n and k as arguments, and then you call
> h₁ with suc n as one of the arguments.
> 
> Your code is not self-contained, but I suspect that you can make it work
> by using --termination-depth=2.
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5384 bytes
Desc: S/MIME Cryptographic Signature
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200218/26b777cf/attachment.p7s>