[Agda] More rewrite woes

[Jason Hu]

Hi Phil,

Your rewrite is an no-op, because the goal does not have the corresponding left hand side:

Goal: reflᴳ ⊢ M ↑ p ≤ᴹ M ↑ p ⦂ id
Have: (id ⨟ p) ≡ p

You can apply reflexivity to rewrite all p to (id ⨟ p) but this is not want you want. In Agda you cannot specify which p to rewrite so I suppose this is a limitation. There is nothing wrong with the current solution you have.

Thanks,
Jason Hu

From: Philip Wadler<mailto:wadler at inf.ed.ac.uk>
Sent: Sunday, January 9, 2022 10:56 AM
To: Agda mailing list<mailto:agda at lists.chalmers.se>
Subject: [Agda] More rewrite woes

I've attached code where a rewrite should work but does not. There are many places in the full development where I encounter similar issues. Rewrite works fine in the original definition of left-id, but not in the subsequent attempt to prove reflᴹ. Any advice on how to fix it?

The file is cut down from the original---I apologise that it is still rather lengthy. The issue with rewrite appears at the end. I am using Agda version 2.6.1.1-fce01db.

Thank you for your help! Go well, -- P




.   \ Philip Wadler, Professor of Theoretical Computer Science,
.   /\ School of Informatics, University of Edinburgh
.  /  \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20220109/cd16cddf/attachment-0001.html>