[Agda] join 2 `with'|
Christopher Jenkins
cjenkin1 at trinity.edu
Thu Nov 20 00:52:58 CET 2014
All,
The blog post I promised:
http://serendependy.blogspot.com/2014/11/with-great-power-great-intractibility.html
Feel free to add comments or suggestions on the blog itself or here.
On Thu, Nov 6, 2014 at 3:39 PM, Andreas Abel <andreas.abel at ifi.lmu.de>
wrote:
> Note that I am in the process of outlawing `with` on variables bound by
> module telescopes (because of the issue 1342 that came up during this
> discussion).
>
> Cheers,
> Andreas
>
> On 05.11.2014 23:53, Christopher Jenkins wrote:
>
>> Alright, two people is enough to motivate me. I will try to have a first
>> blog post out this weekend, mostly dealing with pattern-matching after a
>> rewrite and the basic concept of `with', with more to follow.
>>
>> On Wed, Nov 5, 2014 at 2:21 AM, Arseniy Alekseyev
>> <arseniy.alekseyev at gmail.com <mailto:arseniy.alekseyev at gmail.com>> wrote:
>>
>> Oh wow, I should have tried that. I don't understand why this works at
>> all. Note that none of these compile for me:
>>
>> y | true = id {A = (q : Bool) → x ≡ z q} (λ { true → refl ; false
>> → refl }) -- x != true of type Bool
>>
>> y | true = id {A = (q : Bool) → true ≡ z q} (λ { true → refl ;
>> false → refl }) -- true != x of type Bool
>>
>> However, even more confusingly, this one does work:
>>
>> y | true = id {A = _} (λ { true → refl ; false → refl })
>>
>> So what's the value of underscore it infers then?
>> Can anybody explain what's going on?
>>
>> As for the code smell part, I think you can only smell it on toy
>> examples, not on the "real" ones.
>>
>> On 5 November 2014 01:28, Christopher Jenkins <cjenkin1 at trinity.edu
>> <mailto:cjenkin1 at trinity.edu>> wrote:
>> >
>> >
>> > On Tue, Nov 4, 2014 at 5:18 PM, Arseniy Alekseyev
>> > <arseniy.alekseyev at gmail.com
>> <mailto:arseniy.alekseyev at gmail.com>> wrote:
>> >>
>> >> That was not a genuine attempt to prove `y : ∀ q → x ≡ z q`.
>> Instead
>> >> that was an example of `with` rewriting the goal from (as you
>> >> demonstrated!) provable one into (as I assert) non-provable one. I
>> >> think that's the property of `with` that's causing you grief
>> when you
>> >> re-order or nest them in a bad way.
>> >>
>> > Ah, makes sense. Though of course you could probably continue on
>> to prove
>> > the goal by pattern-matching on a lambda argument introduced in
>> both cases,
>> > but by that point hopefully someone would see the code smell.
>> >
>> > Actually, decided to include it anyway, so you could smell the
>> smelly code
>> > smell:
>> >
>> > y : ∀ q → x ≡ z q
>> > y with x
>> > y | true = λ { true → refl ; false → refl }
>> > y | false = λ { true → refl ; false → refl }
>> >
>> >>
>> >> On 4 November 2014 22:43, Christopher Jenkins
>> <cjenkin1 at trinity.edu <mailto:cjenkin1 at trinity.edu>>
>> >> wrote:
>> >> >
>> >> >
>> >> > On Mon, Nov 3, 2014 at 2:38 PM, Arseniy Alekseyev
>> >> > <arseniy.alekseyev at gmail.com
>> <mailto:arseniy.alekseyev at gmail.com>> wrote:
>> >> >>
>> >> >> You are right, there is not much point. I was trying to point
>> out that
>> >> >> it's the "proper expression" part that makes `with`
>> complicated.
>> >> >>
>> >> >> Unfortunately, that's not even true. In the following
>> example, I don't
>> >> >> think you can fill the holes.
>> >> >>
>> >> >> f : Bool → Bool
>> >> >> f x = true where
>> >> >>
>> >> >> z : Bool → Bool
>> >> >> z true = x
>> >> >> z false = x
>> >> >>
>> >> >> y : ∀ q → x ≡ z q
>> >> >> y with x
>> >> >> y | true = {!!}
>> >> >> y | false = {!!}
>> >> >>
>> >> >>
>> >> >
>> >> > I'm not entirely sure why you would expect that approach to be
>> fruitful.
>> >> > Essentially, what you're trying to do is unwind the
>> computational nature
>> >> > of
>> >> > `z', which is defined by case analysis on its argument (in
>> this case q).
>> >> > To
>> >> > trigger the rules, you would have to bring q into scope and
>> inspect q,
>> >> > which
>> >> > would then lead to `z true' and `z false' in the equations,
>> >> > respectively,
>> >> > and Agda will then go on to normalize the goals as `x \== x'
>> >> >
>> >> > f : Bool → Bool
>> >> > f x = true where
>> >> > z : Bool → Bool
>> >> > z true = x
>> >> > z false = x
>> >> >
>> >> > y : ∀ q → x ≡ z q
>> >> > y true = {!!} -- Goal: x ≡ x
>> >> > y false = {!!} -- Goal: x ≡ x
>> >> >
>> >> > I have actually been thinking about writing a blog post
>> targeted at
>> >> > newbies
>> >> > (such as myself) on the sometimes unintuitive behaviour of
>> `with' (and
>> >> > in
>> >> > particular, `rewrite'). Should anyone be interested I can send
>> a link on
>> >> > this email chain once I have written it.
>> >> >
>> >> >
>> >> >>
>> >> >> On 3 November 2014 10:59, Andreas Abel
>> <andreas.abel at ifi.lmu.de <mailto:andreas.abel at ifi.lmu.de>> wrote:
>> >> >> > On 03.11.2014 09:47, Arseniy Alekseyev wrote:
>> >> >> >> I think the problem goes away if you
>> >> >> >> only use `with x` where `x` is a variable.
>> >> >> >
>> >> >> > Mmh, why use `with` at all then? You could directly split
>> on the
>> >> >> > variable
>> >> >> > `x`. I thought the only reason to use `with` was when you
>> wanted to
>> >> >> > case on
>> >> >> > a proper expression and refine your type in the
>> with-branches...
>> >> >> >
>> >> >> >
>> >> >> >
>> >> >> > On 03.11.2014 09:47, Arseniy Alekseyev wrote:
>> >> >> >>
>> >> >> >> Indeed that's the usual Agda behaviour.
>> >> >> >> Here the reason seems to be an additional occurrence of
>> `lookup k
>> >> >> >> ps`
>> >> >> >> in the context produced by pattern-match on `no`.
>> >> >> >> You see, `with expr` only rewrites the occurrences of
>> `expr` present
>> >> >> >> in the enclosing context, so the new occurrences inside
>> the body of
>> >> >> >> `with` don't get rewritten (and you do want it rewritten
>> in this
>> >> >> >> case).
>> >> >> >>
>> >> >> >> I do agree this is confusing. I think the problem goes
>> away if you
>> >> >> >> only use `with x` where `x` is a variable. That makes
>> `with` much
>> >> >> >> less
>> >> >> >> useful though. You can also avoid `with` altogether and
>> write the
>> >> >> >> helper functions by hand (that's what `with` is doing
>> after all!).
>> >> >> >>
>> >> >> >> On 2 November 2014 17:14, <mechvel at scico.botik.ru
>> <mailto:mechvel at scico.botik.ru>> wrote:
>> >> >> >>>
>> >> >> >>> People,
>> >> >> >>>
>> >> >> >>> Having the proof
>> >> >> >>>
>> >> >> >>> prove : (k∈ks : k ∈ ks) → proj₂ (lookupIf∈ k (p ∷ ps)
>> k∈k':ks) ≡
>> >> >> >>> proj₂ (lookupIf∈ k ps k∈ks)
>> >> >> >>> prove k∈ks with k ≟ k'
>> >> >> >>> --
>> >> >> >>> (I)
>> >> >> >>>
>> >> >> >>> ... | yes k≡k' = ⊥-elim $ k≉k' k≡k'
>> >> >> >>> ... | no _ with lookup k ps
>> >> >> >>> ... | inj₁ _ = PE.refl
>> >> >> >>> ... | inj₂ k∉ks = ⊥-elim $ k∉ks k∈ks
>> >> >> >>>
>> >> >> >>>
>> >> >> >>> (I do not give the complete code),
>> >> >> >>>
>> >> >> >>> I try to rewrite it in a bit simpler way by joining it
>> into one
>> >> >> >>> `with'
>> >> >> >>> clause:
>> >> >> >>>
>> >> >> >>>
>> >> >> >>> prove k∈ks with k ≟ k' | lookup k ps
>> >> >> >>> --
>> >> >> >>> (II)
>> >> >> >>>
>> >> >> >>> ... | yes k≡k' | _ = ⊥-elim $ k≉k' k≡k'
>> >> >> >>> ... | no _ | inj₁ _ = PE.refl
>> >> >> >>> ... | no _ | inj₂ k∉ks = ⊥-elim $ k∉ks k∈ks
>> >> >> >>>
>> >> >> >>>
>> >> >> >>> (I) is type-checked, and (II) is not.
>> >> >> >>>
>> >> >> >>> Is this natural for Agda to decide so?
>> >> >> >>>
>> >> >> >>> (I have spent 4 hours trying to prove a similar real and
>> evident
>> >> >> >>> example.
>> >> >> >>> Then tried to split `with' into two, and this has
>> succeeded).
>> >> >> >>>
>> >> >> >>> Thanks,
>> >> >> >>>
>> >> >> >>> ------
>> >> >> >>> Sergei
>> >> >> >>> _______________________________________________
>> >> >> >>> Agda mailing list
>> >> >> >>> Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>> >> >> >>> https://lists.chalmers.se/mailman/listinfo/agda
>> >> >> >>
>> >> >> >> _______________________________________________
>> >> >> >> Agda mailing list
>> >> >> >> Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>> >> >> >> https://lists.chalmers.se/mailman/listinfo/agda
>> >> >> >>
>> >> >> >
>> >> >> >
>> >> >> > --
>> >> >> > Andreas Abel <>< Du bist der geliebte Mensch.
>> >> >> >
>> >> >> > Department of Computer Science and Engineering
>> >> >> > Chalmers and Gothenburg University, Sweden
>> >> >> >
>> >> >> > andreas.abel at gu.se <mailto:andreas.abel at gu.se>
>> >> >> > http://www2.tcs.ifi.lmu.de/~abel/
>> >> >> _______________________________________________
>> >> >> Agda mailing list
>> >> >> Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>> >> >> https://lists.chalmers.se/mailman/listinfo/agda
>> >> >
>> >> >
>> >> >
>> >> >
>> >> > --
>> >> > Christopher Jenkins
>> >> > Computer Science 2013
>> >> > Trinity University
>> >
>> >
>> >
>> >
>> > --
>> > Christopher Jenkins
>> > Computer Science 2013
>> > Trinity University
>>
>>
>>
>>
>> --
>> Christopher Jenkins
>> Computer Science 2013
>> Trinity University
>>
>
>
> --
> Andreas Abel <>< Du bist der geliebte Mensch.
>
> Department of Computer Science and Engineering
> Chalmers and Gothenburg University, Sweden
>
> andreas.abel at gu.se
> http://www2.tcs.ifi.lmu.de/~abel/
>
--
Christopher Jenkins
Computer Science 2013
Trinity University
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20141119/16734f50/attachment-0001.html
More information about the Agda
mailing list