[Agda] join 2 `with'|

Christopher Jenkins cjenkin1 at trinity.edu
Thu Nov 20 20:50:18 CET 2014


On Thu, Nov 20, 2014 at 5:33 AM, Gabriel Scherer <gabriel.scherer at gmail.com>
wrote:

> I see that you end your post suggesting that Youtube may be a better
> distribution channel for your content. I beg to differ.


Interesting. I actually have made a video, but I am not confident enough in
my presentation skills to recommend it :). On the whole though, I tend to
prefer videos. I think I'll try to use the blog posts as draft scripts for
the videos.


> I like the post format, but if I was to point out a weak point, it is
> the use of screenshot. They take time for your to prepare, and they
> have lesser accessibility (for blind people for example) than text
> format (or even HTML). It would be nice to have a
> "this-Agda-state-to-HTML" command (that would also take into account
> the *Error* and other message buffers), or maybe even a way to
> interactively replay a proof (including errors) in a browser. The Coq
> community has developed a tool in that direction, Proviola :
>   http://mws.cs.ru.nl/proviola/
>

They're not actually so bad - Alt+PrtSc is all it takes, followed by an
upload. I would *love* to use a tool like you're describing, but I'm not
really in a position to implement something like that myself right now. As
for accessibility - well, I doubt I will reach a wide enough audience for
that to matter xD

Thanks for the feedback. (I hope that this type of discussion isn't too
off-topic for the mailing list...?)



> On Thu, Nov 20, 2014 at 12:52 AM, Christopher Jenkins
> <cjenkin1 at trinity.edu> wrote:
> > 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
> >
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda
> >
>



-- 
Christopher Jenkins
Computer Science 2013
Trinity University
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20141120/686b0e52/attachment-0001.html


More information about the Agda mailing list