<div dir="ltr">Thank you for the reply!<div><br></div><div>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?</div><div><br></div><div>Thank you again for the help. Go well, -- P</div><div><br clear="all"><div><div dir="ltr" class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><div><div dir="ltr"><div dir="ltr"><div><div dir="ltr">.   \ Philip Wadler, Professor of Theoretical Computer Science,<br>.   /\ School of Informatics, University of Edinburgh<br></div><div>.  /  \ and Senior Research Fellow, IOHK<br></div><div dir="ltr">. <span><a href="http://homepages.inf.ed.ac.uk/wadler/" target="_blank">http://homepages.inf.ed.ac.uk/wadler/</a></span></div></div><div dir="ltr"><br></div></div></div></div></div></div></div><br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Sun, 9 Jan 2022 at 16:38, Jason Hu <<a href="mailto:fdhzs2010@hotmail.com">fdhzs2010@hotmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">




<div lang="EN-US" style="overflow-wrap: break-word;">
<div style="background-color:rgb(255,242,230);border:2px dotted rgb(255,136,77)"><span style="font-size:12pt;font-family:sans-serif;color:black;font-weight:bold;padding:0.2em">This email was sent to you by someone outside the University.</span>
<div style="font-size:10pt;font-family:sans-serif;font-style:normal;padding:0.2em">
You should only click on links or attachments if you are certain that the email is genuine and the content is safe.</div>
</div>
<div>
<div class="gmail-m_3659133150112297130WordSection1">
<p class="MsoNormal">Hi Phil,</p>
<p class="MsoNormal"><u></u> <u></u></p>
<p class="MsoNormal">Your rewrite is an no-op, because the goal does not have the corresponding left hand side:</p>
<p class="MsoNormal"><u></u> <u></u></p>
<p class="MsoNormal">Goal: reflᴳ <span style="font-family:"Cambria Math",serif">⊢</span> M
<span lang="ZH-CN" style="font-family:DengXian">↑</span> p <span lang="ZH-CN" style="font-family:DengXian">
≤</span>ᴹ M <span lang="ZH-CN" style="font-family:DengXian">↑</span> p <span style="font-family:"Cambria Math",serif">
⦂</span> id</p>
<p class="MsoNormal">Have: (id <span style="font-family:"Cambria Math",serif">⨟</span> p)
<span lang="ZH-CN" style="font-family:DengXian">≡</span> p</p>
<p class="MsoNormal"><u></u> <u></u></p>
<p class="MsoNormal">You can apply reflexivity to rewrite all p to (id <span style="font-family:"Cambria Math",serif">
⨟</span> 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.
</p>
<p class="MsoNormal"><u></u> <u></u></p>
<p class="MsoNormal">Thanks,<u></u><u></u></p>
<p class="MsoNormal">Jason Hu<u></u><u></u></p>
<p class="MsoNormal"><u></u> <u></u></p>
<div style="border-right:none;border-bottom:none;border-left:none;border-top:1pt solid rgb(225,225,225);padding:3pt 0in 0in">
<p class="MsoNormal" style="border:none;padding:0in"><b>From: </b><a href="mailto:wadler@inf.ed.ac.uk" target="_blank">Philip Wadler</a><br>
<b>Sent: </b>Sunday, January 9, 2022 10:56 AM<br>
<b>To: </b><a href="mailto:agda@lists.chalmers.se" target="_blank">Agda mailing list</a><br>
<b>Subject: </b>[Agda] More rewrite woes</p>
</div>
<p class="MsoNormal"><u></u> <u></u></p>
<div>
<p class="MsoNormal">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?<u></u><u></u></p>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal">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.<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal">Thank you for your help! Go well, -- P<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal"><br clear="all">
<u></u><u></u></p>
<div>
<div>
<div>
<div>
<div>
<div>
<div>
<div>
<p class="MsoNormal">.   \ Philip Wadler, Professor of Theoretical Computer Science,<br>
.   /\ School of Informatics, University of Edinburgh<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal">.  /  \ and Senior Research Fellow, IOHK<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal">. <a href="http://homepages.inf.ed.ac.uk/wadler/" target="_blank">
http://homepages.inf.ed.ac.uk/wadler/</a><u></u><u></u></p>
</div>
</div>
</div>
</div>
</div>
</div>
</div>
</div>
</div>
</div>
</div>
<p class="MsoNormal"><u></u> <u></u></p>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
</div>
</div>

</blockquote></div>