[Agda] rewrite on the right?
Martin Stone Davis
martin.stone.davis at gmail.com
Sun Feb 28 22:18:42 CET 2016
Looks like it's working now
<https://github.com/m0davis/agda-prelude/blob/master/test/Reright.agda>.
The new version presents the user with changed context variabes, to mimic
that done by rewrite. E.g.
simple-reright-test : (A B : Set) (F : Set → Set) → F A → A ≡ B → B → A
simple-reright-test A B F FA A≡B b = reright A≡B $ λ (FB : F B) → b
--
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 Thu, Feb 18, 2016 at 4:21 PM, Martin Stone Davis <
martin.stone.davis at gmail.com> wrote:
> My "Reright" is buggy-by-design. I'm working on a much better version.
> More to come.
>
> --
> 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, Feb 12, 2016 at 11:43 PM, Martin Stone Davis <
> martin.stone.davis at gmail.com> wrote:
>
>> 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/20160228/9e20d2b6/attachment-0001.html
More information about the Agda
mailing list