[Agda] join 2 `with'|
Gabriel Scherer
gabriel.scherer at gmail.com
Thu Nov 20 12:33:12 CET 2014
I see that you end your post suggesting that Youtube may be a better
distribution channel for your content. I beg to differ. I hate video
onlines (and don't watch them) because they remove the freedom of the
user to pace through the material at their own rythm (slowly if
necessary, quickly if they just want a quick glance to get a feel of
what this is about, which is what I do for most content before reading
it in full). Your blog posts are *much* better than videos for this.
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/
(The interactive version is better semantically than pictures, but may
not be optimal for accessibility purposes.)
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
>
More information about the Agda
mailing list