[Agda] rewrite on the right?
Martin Stone Davis
martin.stone.davis at gmail.com
Sat Feb 13 08:43:23 CET 2016
Thanks to all for those suggestions. I wound-up writing it from scratch,
which was helpful in my learning reflection in agda.
"Reright" is now available on my fork
<https://github.com/m0davis/agda-prelude> of agda-prelude. Some (very
messy) sample code is here
<https://github.com/m0davis/agda-prelude/blob/master/test/Reright.agda>.
Due to issue #1833 <https://github.com/agda/agda/issues/1833>, a parameter
needs to be supplied to the macro, counting (roughly speaking) the number
of arguments on the lhs.
--
Martin Stone Davis
Postal/Residential:
1223 Ferry St
Apt 5
Eugene, OR 97401
Talk / Text / Voicemail: (310) 699-3578 <3106993578>
Electronic Mail: martin.stone.davis at gmail.com
Website: martinstonedavis.com
On Fri, Jan 22, 2016 at 4:51 AM, Victor Miraldo <victor.cacciari at gmail.com>
wrote:
> Hello,
>
> 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,
> and, in fact, this new API provides a lot of interesting oportunities to
> improve it. If you're using a "not so recent" version of Agda
> it might be worth to check it out.
>
> https://github.com/VictorCMiraldo/agda-rw
>
> Cheers,
> Victor
>
> On Wed, Jan 20, 2016 at 6:59 PM, Jesper Cockx <Jesper at sikanda.be> wrote:
>
>> 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
>>>
>>
>>
>> _______________________________________________
>> 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/20160212/e98723e1/attachment.html
More information about the Agda
mailing list