<div dir="ltr"><div>Hi Apostolis,<br></div><div><br></div><div>Excellent question! Unfortunately, the answer is not an unqualified 'yes'. It is true that using such rewrite rules always preserves soundness of the theory, since rewrite rules are in a sense a limited form of equality reflection, and equality reflection is known to be consistent.</div><div><br></div><div>However, other more syntactic properties such as confluence, termination, and subject reduction (aka type preservation) can still be broken. In our 2014 paper, I give one such example: the rewrite rules `(suc x) * y == (x * y) + y` and `x * (suc y) == x + (x * y)` are not confluent unless you also have associativity of + as a rewrite rule. It's not very straightforward, but by tricking Agda's constraint solver to solve equations in a particular order, you can exploit a non-confluence like this to break subject reduction. This manifests as a type error complaining two things should be equal even though they are according to the rules.</div><div><br></div><div>I have actually been working on implementing a confluence checker for rewrite rules (which I'm planning to talk about in an upcoming post). If you want, you can try it out by installing the current master branch of Agda and enabling the --confluence-check flag.<br></div><div><br></div><div>Cheers,</div><div>Jesper</div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Mon, Oct 21, 2019 at 4:21 PM Apostolis Xekoukoulotakis <<a href="mailto:apostolis.xekoukoulotakis@gmail.com">apostolis.xekoukoulotakis@gmail.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 dir="ltr"><div>If you have proved the equality as in your 2nd example, is there any reason not to use REWRITE? <br></div><div>My impression is that I should use REWRITE everywhere where I have proven a propositional equality so as to make it definitional.</div><div><br></div><div>Nice blog post, and a good reference to a book on type theory. I was looking into a good introductory book that would help me understand agda a bit better.<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Mon, Oct 21, 2019 at 4:22 PM Jesper Cockx <<a href="mailto:Jesper@sikanda.be" target="_blank">Jesper@sikanda.be</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 dir="ltr"><div>Hi Agda folks,</div><div><br></div><div>I have another blog post for you on extending Agda with rewrite rules, with no less than six examples of how they can be used. You can read it at <a href="https://jesper.sikanda.be/posts/hack-your-type-theory.html" target="_blank">https://jesper.sikanda.be/posts/hack-your-type-theory.html</a>. Any comments are welcome here on the mailing list as usual.</div><div><br></div><div>Cheers,</div><div>Jesper<br></div></div>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>
</blockquote></div>