<div dir="ltr"><div>In your case the reason the proof fails without `abstract` is that the `rewrite` doesn't trigger.</div><div>Here's a simpler example exhibiting the same behaviour:</div><div><br></div><div style="margin-left:40px"><span style="font-family:monospace,monospace">module _ where<br><br>open import Agda.Builtin.Nat<br>open import Agda.Builtin.Bool<br>open import Agda.Builtin.Equality<br><br>module WithAbstract where<br><br> abstract<br> f : Nat → Nat<br> f zero = zero<br> f (suc n) = suc (f n)<br><br> lem : ∀ n → f n ≡ n<br> lem zero = refl<br> lem (suc n) rewrite lem n = refl<br><br> thm : ∀ m n → f (suc m) + n ≡ suc (m + n)<br> thm m n rewrite lem (suc m) = refl<br> -- Works.<br><br>module WithoutAbstract where<br><br> f : Nat → Nat<br> f zero = zero<br> f (suc n) = suc (f n)<br><br> lem : ∀ n → f n ≡ n<br> lem zero = refl<br> lem (suc n) rewrite lem n = refl<br><br> thm : ∀ m n → f (suc m) + n ≡ suc (m + n)<br> thm m n rewrite lem (suc m) = refl<br> -- Fails since rewrite doesn't trigger:<br> -- lem (suc m) : suc (f m) ≡ suc m<br> -- goal : suc (f m + n) ≡ suc (m + n)<br></span></div><div><br></div><div>In general I think it's optimistic to expect tactics (of which rewrite is an example) to be stable under substitution.</div><div><br></div><div>/ Ulf<br></div><div><br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Wed, May 16, 2018 at 9:24 PM, Philip Wadler <span dir="ltr"><<a href="mailto:wadler@inf.ed.ac.uk" target="_blank">wadler@inf.ed.ac.uk</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">Thanks, Martin. So which fragment do you recommend? Cheers, -- P</div><div class="gmail_extra"><span class=""><br clear="all"><div><div class="m_2025256065675378733gmail_signature" data-smartmail="gmail_signature"><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/<wbr>wadler/</a></span></div></div></div></div></div>
<br></span><span class=""><div class="gmail_quote">On 16 May 2018 at 16:03, Martin Escardo <span dir="ltr"><<a href="mailto:m.escardo@cs.bham.ac.uk" target="_blank">m.escardo@cs.bham.ac.uk</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span><br>
<br>
On 16/05/18 20:37, Philip Wadler wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Thanks for following up. It is the latter case. But I don't understand why it should be ok for that to fail. Removing abstract should just replace some abstract terms by their concretions, which have already been type checked. Everything that was provably equal before should still be equal, so why is it ok for the proof of equality to now fail? Doesn't this violate stability under substitution? Cheers, -- P<br>
</blockquote>
<br></span>
It is because of things such as this that I prefer to restrict my usage of Agda to a fragment corresponding to a well-understood type theory.<br>
<br>
This may be limiting in terms of expressivity, conciseness, and efficiency, but at least one can tell whether something is a bug or not, rather than a bug or a feature.<br>
<br>
:-)<span class="m_2025256065675378733HOEnZb"><font color="#888888"><br>
Martin<br>
<br>
</font></span></blockquote></div><br></span></div>
<br>The University of Edinburgh is a charitable body, registered in<br>
Scotland, with registration number SC005336.<br>
<br>______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
<br></blockquote></div><br></div>