<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">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="gmail_extra"><br><div class="gmail_quote">On Wed, Jan 20, 2016 at 6:33 PM, Andrea Vezzosi <span dir="ltr"><<a href="mailto:sanzhiyan@gmail.com" target="_blank">sanzhiyan@gmail.com</a>></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'd have to generate an helper like you did manually, that'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 class="h5"><br>
<br>
<br>
<br>
<br>
<br>
On Wed, Jan 20, 2016 at 1:39 AM, Martin Stone Davis<br>
<<a href="mailto:martin.stone.davis@gmail.com">martin.stone.davis@gmail.com</a>> wrote:<br>
> I've found myself wishing that 'rewrite' or with-abstractions were invokable<br>
> from lambda expressions. A (contrived) case in point is as follows, where a<br>
> helper function is used to complete 'foo'. NB, I realize that, in this case,<br>
> I could have simply used a with-abstraction (as in 'bar'), but there are<br>
> other cases (not shown here) where one of the variables being ≟-compared<br>
> only exists on the rhs, thus requiring a call to 'case_of_'.<br>
><br>
> Is there a way to 'subst' my way out of the need for foo-helper?<br>
><br>
> module RewriteOnRight where<br>
> open import Data.Product using (∃ ; _,_)<br>
> open import Relation.Nullary using (Dec ; yes ; no)<br>
> open import Function using (case_of_)<br>
> open import Relation.Nullary.Negation using (contradiction)<br>
> open import Relation.Binary using (IsDecEquivalence)<br>
> open import Relation.Binary.PropositionalEquality using (_≡_ ; subst ;<br>
> trans ; refl)<br>
><br>
> postulate<br>
> K : Set<br>
> V : K → Set<br>
> M : Set<br>
> _∈_ : K → M → Set<br>
> get : ∀ {k : K} {m : M} → k ∈ m → V k<br>
> isDecEquivalence/K : IsDecEquivalence {A = K} _≡_<br>
><br>
> open IsDecEquivalence isDecEquivalence/K using (_≟_ ; sym)<br>
><br>
> foo-helper :<br>
> ∀ {x : M}<br>
> {y : M}<br>
> {a : K}<br>
> {b : K}<br>
> {a∈x : a ∈ x}<br>
> {b∈x : b ∈ x}<br>
> {a∈y : a ∈ y}<br>
> (gax≡gay : get a∈x ≡ get a∈y)<br>
> (a≡b : a ≡ b)<br>
> (gbx≡gax : get b∈x ≡ subst V a≡b (get a∈x))<br>
> → get b∈x ≡ get (subst (λ k → k ∈ y) a≡b a∈y)<br>
> foo-helper gax≡gay a≡b gbx≡gax rewrite a≡b = trans gbx≡gax gax≡gay<br>
><br>
> foo : ∀ {x : M}<br>
> {y : M}<br>
> (a : K)<br>
> (b : K)<br>
> {a∈x : a ∈ x}<br>
> {b∈x : b ∈ x}<br>
> {a∈y : a ∈ y}<br>
> (gax≡gay : get a∈x ≡ get a∈y)<br>
> → Dec (∃ λ (a≡b : a ≡ b) → (gbx≡gax : get b∈x ≡ subst V a≡b (get<br>
> a∈x)) → get b∈x ≡ get (subst (λ k → k ∈ y) a≡b a∈y))<br>
> foo a b gax≡gay = case a ≟ b of λ<br>
> { (yes a≡b) → yes (a≡b , (λ {gbx≡gax → foo-helper gax≡gay a≡b gbx≡gax}))<br>
> ; (no a≢b) → no (λ { (a≡b , _) → contradiction a≡b a≢b })<br>
> }<br>
><br>
> bar : ∀ {x : M}<br>
> {y : M}<br>
> (a : K)<br>
> (b : K)<br>
> {a∈x : a ∈ x}<br>
> (b∈x : b ∈ x)<br>
> {a∈y : a ∈ y}<br>
> (gax≡gay : get a∈x ≡ get a∈y)<br>
> → Dec (∃ λ (a≡b : a ≡ b) → (gbx≡gax : get b∈x ≡ subst V a≡b (get<br>
> a∈x)) → get b∈x ≡ get (subst (λ k → k ∈ y) a≡b a∈y))<br>
> bar a b _ _ with a ≟ b<br>
> bar _ ._ b∈x gax≡gay | yes refl = yes (refl , (λ {gbx≡gax → trans gbx≡gax<br>
> gax≡gay}))<br>
> bar _ _ _ _ | no a≢b = no (λ { (a≡b , _) → contradiction a≡b a≢b<br>
> })<br>
><br>
> --<br>
> Martin Stone Davis<br>
><br>
> Postal/Residential:<br>
> 1223 Ferry St<br>
> Apt 5<br>
> Eugene, OR 97401<br>
> Talk / Text / Voicemail: <a href="tel:%28310%29%20699-3578" value="+13106993578">(310) 699-3578</a><br>
> Electronic Mail: <a href="mailto:martin.stone.davis@gmail.com">martin.stone.davis@gmail.com</a><br>
> Website: <a href="http://martinstonedavis.com" rel="noreferrer" target="_blank">martinstonedavis.com</a><br>
><br>
</div></div>> _______________________________________________<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>
_______________________________________________<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>
</blockquote></div><br></div>