[Agda] Weird termination problem

[William Harrison]

Hi Thorsten,

If you came up with a pithy example and then integrated in with the Agda docs (specifically https://agda.readthedocs.io/en/v2.6.1/language/without-k.html), that’s be welcome. By me, at least.

Bill

Sent from my iPad

> On Aug 15, 2020, at 10:21 AM, Thorsten Altenkirch <Thorsten.Altenkirch at nottingham.ac.uk> wrote:
> 
> 
> I found
> https://github.com/agda/agda/issues/2890
> but this mentions “with” which I wasn’t using. Also increasing termination depth didn’t help in my case.
>  
> I can try to cook up a short example but maybe this is a known issue?
>  
> Thorsten
>  
> From: Agda <agda-bounces at lists.chalmers.se> on behalf of Thorsten Altenkirch <Thorsten.Altenkirch at nottingham.ac.uk>
> Date: Saturday, 15 August 2020 at 15:16
> To: Jason -Zhong Sheng- Hu <fdhzs2010 at hotmail.com>, "agda at lists.chalmers.se" <agda at lists.chalmers.se>
> Subject: Re: [Agda] Weird termination problem
>  
> Yes, indeed this worked. And the difference was that in the previous version I hadn’t used no-K.
>  
> Thanks a lot – I was truly stumped. And I do remember that there were some issues with termination checking when switching on no-K.
>  
> Cheers,
> Thorsten
>  
> From: Jason -Zhong Sheng- Hu <fdhzs2010 at hotmail.com>
> Date: Saturday, 15 August 2020 at 15:10
> To: Thorsten Altenkirch <psztxa at exmail.nottingham.ac.uk>, "agda at lists.chalmers.se" <agda at lists.chalmers.se>
> Subject: Re: Weird termination problem
>  
> I once saw someone else's code where termination checker also failed with no good reason. the author worked around it by turning on K. could you see if K works around it for you?
>  
> Thanks,
> Jason Hu
> https://hustmphrrr.github.io/
> From: Agda <agda-bounces at lists.chalmers.se> on behalf of Thorsten Altenkirch <Thorsten.Altenkirch at nottingham.ac.uk>
> Sent: August 15, 2020 9:25 AM
> To: agda at lists.chalmers.se <agda at lists.chalmers.se>
> Subject: [Agda] Weird termination problem
>  
> Hi,
>  
> I just transferred some code form my lecture notes to my book draft and now the termination checker complains where there was no problem before:
>  
> thm : {P : Form} → ([] ⊢ P) ⇔ ⊢sk P
> proj₁ thm d = skC→sk (⊢→⊢skC d)
> proj₂ thm SS = S-d
> proj₂ thm KK = K-d
> proj₂ thm (app d e) = app (proj₂ thm d) (proj₂ thm e)
>  
> so here ⊢sk P is inductively defined and there should be no problem – and indeed there wasn’t before. But now
>  
> Termination checking failed for the following functions:
>   thm
> Problematic calls:
>   proj₂ thm e
>  
> I can’t make any sense out of it. Has anybody an inkling what could have happened or any advice what I could do to fix it.
>  
> I can prove the <= direction on its own with no problems. The definition of ⇔ is exactly the same as before and it doesn’t help if I expand it. Also the definition of products is the same as before.
>  
> If you want to have a look at the code please let me know – I will give you access to the repo.
>  
> Cheers,
> Thorsten
>  
> This message and any attachment are intended solely for the addressee
> and may contain confidential information. If you have received this
> message in error, please contact the sender and delete the email and
> attachment. 
>  
> Any views or opinions expressed by the author of this email do not
> necessarily reflect the views of the University of Nottingham. Email
> communications with the University of Nottingham may be monitored 
> where permitted by law.
>  
>  
>  
>  
> This message and any attachment are intended solely for the addressee
> and may contain confidential information. If you have received this
> message in error, please contact the sender and delete the email and
> attachment. 
>  
> Any views or opinions expressed by the author of this email do not
> necessarily reflect the views of the University of Nottingham. Email
> communications with the University of Nottingham may be monitored 
> where permitted by law.
>  
>  
>  
> 
> This message and any attachment are intended solely for the addressee
> and may contain confidential information. If you have received this
> message in error, please contact the sender and delete the email and
> attachment. 
> 
> Any views or opinions expressed by the author of this email do not
> necessarily reflect the views of the University of Nottingham. Email
> communications with the University of Nottingham may be monitored 
> where permitted by law.
> 
> 
> 
> _______________________________________________
> 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/20200815/00e3e97b/attachment.html>