[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