<div dir="ltr"><div><div><div><div><div>Hello,<br><br></div>I did implement a library for doing exactly that as my Msc thesis. My code is not up-to-date with the new API for reflection aswell, <br></div>and, in fact, this new API provides a lot of interesting oportunities to improve it. If you&#39;re using a &quot;not so recent&quot; version of Agda<br></div>it might be worth to check it out.<br><br><a href="https://github.com/VictorCMiraldo/agda-rw">https://github.com/VictorCMiraldo/agda-rw</a><br><br></div>Cheers,<br></div>Victor<br></div><div class="gmail_extra"><br><div class="gmail_quote">On Wed, Jan 20, 2016 at 6:59 PM, Jesper Cockx <span dir="ltr">&lt;<a href="mailto:Jesper@sikanda.be" target="_blank">Jesper@sikanda.be</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div><div>I implemented a simple rewrite tactic using the reflection in Agda back in 2014, see <a href="https://lists.chalmers.se/pipermail/agda/2014/007032.html" target="_blank">https://lists.chalmers.se/pipermail/agda/2014/007032.html</a>. The code is not up-to-date with the new reflection API (and you could now probably make something that has a much nicer syntax anyway, using the new macro system) but it shows that there is nothing preventing you to do this using reflection. So I would say there is no need to implement something as a language extension if it is already possible as a library.<br><br></div>cheers,<br></div>Jesper<br></div><div class="HOEnZb"><div class="h5"><div class="gmail_extra"><br><div class="gmail_quote">On Wed, Jan 20, 2016 at 6:33 PM, Andrea Vezzosi <span dir="ltr">&lt;<a href="mailto:sanzhiyan@gmail.com" target="_blank">sanzhiyan@gmail.com</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Yes, having rewrite on the right would be very nice.<br>
<br>
It&#39;d have to generate an helper like you did manually, that&#39;s how<br>
rewrite on the left is implemented too, so it might not make sense as<br>
an expression because it mangles the context, maybe it can have the<br>
same status as the macros of reflection.<br>
<br>
In your case you cannot really get away with just a subst, however you<br>
can get somewhere if you have proven that get commutes with subst, so<br>
you can fill the open goal here:<br>
<br>
(λ { gbx≡gax → trans gbx≡gax (trans (cong (subst V a≡b) gax≡gay) ?) })<br>
<br>
Best,<br>
Andrea<br>
<div><div><br>
<br>
<br>
<br>
<br>
<br>
On Wed, Jan 20, 2016 at 1:39 AM, Martin Stone Davis<br>
&lt;<a href="mailto:martin.stone.davis@gmail.com" target="_blank">martin.stone.davis@gmail.com</a>&gt; wrote:<br>
&gt; I&#39;ve found myself wishing that &#39;rewrite&#39; or with-abstractions were invokable<br>
&gt; from lambda expressions. A (contrived) case in point is as follows, where a<br>
&gt; helper function is used to complete &#39;foo&#39;. NB, I realize that, in this case,<br>
&gt; I could have simply used a with-abstraction (as in &#39;bar&#39;), but there are<br>
&gt; other cases (not shown here) where one of the variables being ≟-compared<br>
&gt; only exists on the rhs, thus requiring a call to &#39;case_of_&#39;.<br>
&gt;<br>
&gt; Is there a way to &#39;subst&#39; my way out of the need for foo-helper?<br>
&gt;<br>
&gt; module RewriteOnRight where<br>
&gt;   open import Data.Product using (∃ ; _,_)<br>
&gt;   open import Relation.Nullary using (Dec ; yes ; no)<br>
&gt;   open import Function using (case_of_)<br>
&gt;   open import Relation.Nullary.Negation using (contradiction)<br>
&gt;   open import Relation.Binary using (IsDecEquivalence)<br>
&gt;   open import Relation.Binary.PropositionalEquality using (_≡_ ; subst ;<br>
&gt; trans ; refl)<br>
&gt;<br>
&gt;   postulate<br>
&gt;     K : Set<br>
&gt;     V : K → Set<br>
&gt;     M : Set<br>
&gt;     _∈_ : K → M → Set<br>
&gt;     get : ∀ {k : K} {m : M} → k ∈ m → V k<br>
&gt;     isDecEquivalence/K : IsDecEquivalence {A = K} _≡_<br>
&gt;<br>
&gt;   open IsDecEquivalence isDecEquivalence/K using (_≟_ ; sym)<br>
&gt;<br>
&gt;   foo-helper :<br>
&gt;     ∀ {x : M}<br>
&gt;       {y : M}<br>
&gt;       {a : K}<br>
&gt;       {b : K}<br>
&gt;       {a∈x : a ∈ x}<br>
&gt;       {b∈x : b ∈ x}<br>
&gt;       {a∈y : a ∈ y}<br>
&gt;       (gax≡gay : get a∈x ≡ get a∈y)<br>
&gt;       (a≡b : a ≡ b)<br>
&gt;       (gbx≡gax : get b∈x ≡ subst V a≡b (get a∈x))<br>
&gt;       → get b∈x ≡ get (subst (λ k → k ∈ y) a≡b a∈y)<br>
&gt;   foo-helper gax≡gay a≡b gbx≡gax rewrite a≡b = trans gbx≡gax gax≡gay<br>
&gt;<br>
&gt;   foo : ∀ {x : M}<br>
&gt;           {y : M}<br>
&gt;           (a : K)<br>
&gt;           (b : K)<br>
&gt;           {a∈x : a ∈ x}<br>
&gt;           {b∈x : b ∈ x}<br>
&gt;           {a∈y : a ∈ y}<br>
&gt;           (gax≡gay : get a∈x ≡ get a∈y)<br>
&gt;         → Dec (∃ λ (a≡b : a ≡ b) → (gbx≡gax : get b∈x ≡ subst V a≡b (get<br>
&gt; a∈x)) → get b∈x ≡ get (subst (λ k → k ∈ y) a≡b a∈y))<br>
&gt;   foo a b gax≡gay = case a ≟ b of λ<br>
&gt;     { (yes a≡b) → yes (a≡b , (λ {gbx≡gax → foo-helper gax≡gay a≡b gbx≡gax}))<br>
&gt;     ; (no a≢b) → no (λ { (a≡b , _) → contradiction a≡b a≢b })<br>
&gt;     }<br>
&gt;<br>
&gt;   bar : ∀ {x : M}<br>
&gt;           {y : M}<br>
&gt;           (a : K)<br>
&gt;           (b : K)<br>
&gt;           {a∈x : a ∈ x}<br>
&gt;           (b∈x : b ∈ x)<br>
&gt;           {a∈y : a ∈ y}<br>
&gt;           (gax≡gay : get a∈x ≡ get a∈y)<br>
&gt;         → Dec (∃ λ (a≡b : a ≡ b) → (gbx≡gax : get b∈x ≡ subst V a≡b (get<br>
&gt; a∈x)) → get b∈x ≡ get (subst (λ k → k ∈ y) a≡b a∈y))<br>
&gt;   bar a  b _   _       with a ≟ b<br>
&gt;   bar _ ._ b∈x gax≡gay | yes refl = yes (refl , (λ {gbx≡gax → trans gbx≡gax<br>
&gt; gax≡gay}))<br>
&gt;   bar _  _ _   _       | no a≢b = no (λ { (a≡b , _) → contradiction a≡b a≢b<br>
&gt; })<br>
&gt;<br>
&gt; --<br>
&gt; Martin Stone Davis<br>
&gt;<br>
&gt; Postal/Residential:<br>
&gt; 1223 Ferry St<br>
&gt; Apt 5<br>
&gt; Eugene, OR 97401<br>
&gt; Talk / Text / Voicemail: <a href="tel:%28310%29%20699-3578" value="+13106993578" target="_blank">(310) 699-3578</a><br>
&gt; Electronic Mail: <a href="mailto:martin.stone.davis@gmail.com" target="_blank">martin.stone.davis@gmail.com</a><br>
&gt; Website: <a href="http://martinstonedavis.com" rel="noreferrer" target="_blank">martinstonedavis.com</a><br>
&gt;<br>
</div></div>&gt; _______________________________________________<br>
&gt; Agda mailing list<br>
&gt; <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
&gt; <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
&gt;<br>
_______________________________________________<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><br></div>
</div></div><br>_______________________________________________<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/mailman/listinfo/agda</a><br>
<br></blockquote></div><br></div>