[Agda] More rewrite woes

[Philip Wadler]

Thank you for the reply!

In the particular case I gave, the solution without rewrite isn't
substantially larger than the (non) solution with rewrite, but in many
other places this is not the case. I take the point that the given formula
does not appear in the goal, and so is not rewritten, but it does appear in
a subgoal needed to prove the goal. Is there some standard idiom for moving
such a subgoal into a goal so that rewrite can apply?

Thank you again for the 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/



On Sun, 9 Jan 2022 at 16:38, Jason Hu <fdhzs2010 at hotmail.com> wrote:

> This email was sent to you by someone outside the University.
> You should only click on links or attachments if you are certain that the
> email is genuine and the content is safe.
>
> 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 <wadler at inf.ed.ac.uk>
> *Sent: *Sunday, January 9, 2022 10:56 AM
> *To: *Agda mailing list <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/324fb844/attachment.html>
-------------- next part --------------
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.