[Agda] rewrite on the right?

[Jesper Cockx]

I implemented a simple rewrite tactic using the reflection in Agda back in
2014, see https://lists.chalmers.se/pipermail/agda/2014/007032.html. 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.

cheers,
Jesper

On Wed, Jan 20, 2016 at 6:33 PM, Andrea Vezzosi <sanzhiyan at gmail.com> wrote:

> Yes, having rewrite on the right would be very nice.
>
> It'd have to generate an helper like you did manually, that's how
> rewrite on the left is implemented too, so it might not make sense as
> an expression because it mangles the context, maybe it can have the
> same status as the macros of reflection.
>
> In your case you cannot really get away with just a subst, however you
> can get somewhere if you have proven that get commutes with subst, so
> you can fill the open goal here:
>
> (λ { gbx≡gax → trans gbx≡gax (trans (cong (subst V a≡b) gax≡gay) ?) })
>
> Best,
> Andrea
>
>
>
>
>
>
> On Wed, Jan 20, 2016 at 1:39 AM, Martin Stone Davis
> <martin.stone.davis at gmail.com> wrote:
> > I've found myself wishing that 'rewrite' or with-abstractions were
> invokable
> > from lambda expressions. A (contrived) case in point is as follows,
> where a
> > helper function is used to complete 'foo'. NB, I realize that, in this
> case,
> > I could have simply used a with-abstraction (as in 'bar'), but there are
> > other cases (not shown here) where one of the variables being ≟-compared
> > only exists on the rhs, thus requiring a call to 'case_of_'.
> >
> > Is there a way to 'subst' my way out of the need for foo-helper?
> >
> > module RewriteOnRight where
> >   open import Data.Product using (∃ ; _,_)
> >   open import Relation.Nullary using (Dec ; yes ; no)
> >   open import Function using (case_of_)
> >   open import Relation.Nullary.Negation using (contradiction)
> >   open import Relation.Binary using (IsDecEquivalence)
> >   open import Relation.Binary.PropositionalEquality using (_≡_ ; subst ;
> > trans ; refl)
> >
> >   postulate
> >     K : Set
> >     V : K → Set
> >     M : Set
> >     _∈_ : K → M → Set
> >     get : ∀ {k : K} {m : M} → k ∈ m → V k
> >     isDecEquivalence/K : IsDecEquivalence {A = K} _≡_
> >
> >   open IsDecEquivalence isDecEquivalence/K using (_≟_ ; sym)
> >
> >   foo-helper :
> >     ∀ {x : M}
> >       {y : M}
> >       {a : K}
> >       {b : K}
> >       {a∈x : a ∈ x}
> >       {b∈x : b ∈ x}
> >       {a∈y : a ∈ y}
> >       (gax≡gay : get a∈x ≡ get a∈y)
> >       (a≡b : a ≡ b)
> >       (gbx≡gax : get b∈x ≡ subst V a≡b (get a∈x))
> >       → get b∈x ≡ get (subst (λ k → k ∈ y) a≡b a∈y)
> >   foo-helper gax≡gay a≡b gbx≡gax rewrite a≡b = trans gbx≡gax gax≡gay
> >
> >   foo : ∀ {x : M}
> >           {y : M}
> >           (a : K)
> >           (b : K)
> >           {a∈x : a ∈ x}
> >           {b∈x : b ∈ x}
> >           {a∈y : a ∈ y}
> >           (gax≡gay : get a∈x ≡ get a∈y)
> >         → Dec (∃ λ (a≡b : a ≡ b) → (gbx≡gax : get b∈x ≡ subst V a≡b (get
> > a∈x)) → get b∈x ≡ get (subst (λ k → k ∈ y) a≡b a∈y))
> >   foo a b gax≡gay = case a ≟ b of λ
> >     { (yes a≡b) → yes (a≡b , (λ {gbx≡gax → foo-helper gax≡gay a≡b
> gbx≡gax}))
> >     ; (no a≢b) → no (λ { (a≡b , _) → contradiction a≡b a≢b })
> >     }
> >
> >   bar : ∀ {x : M}
> >           {y : M}
> >           (a : K)
> >           (b : K)
> >           {a∈x : a ∈ x}
> >           (b∈x : b ∈ x)
> >           {a∈y : a ∈ y}
> >           (gax≡gay : get a∈x ≡ get a∈y)
> >         → Dec (∃ λ (a≡b : a ≡ b) → (gbx≡gax : get b∈x ≡ subst V a≡b (get
> > a∈x)) → get b∈x ≡ get (subst (λ k → k ∈ y) a≡b a∈y))
> >   bar a  b _   _       with a ≟ b
> >   bar _ ._ b∈x gax≡gay | yes refl = yes (refl , (λ {gbx≡gax → trans
> gbx≡gax
> > gax≡gay}))
> >   bar _  _ _   _       | no a≢b = no (λ { (a≡b , _) → contradiction a≡b
> a≢b
> > })
> >
> > --
> > Martin Stone Davis
> >
> > Postal/Residential:
> > 1223 Ferry St
> > Apt 5
> > Eugene, OR 97401
> > Talk / Text / Voicemail: (310) 699-3578
> > Electronic Mail: martin.stone.davis at gmail.com
> > Website: martinstonedavis.com
> >
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda
> >
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160120/7f7c9413/attachment.html