[Agda] join 2 `with'|
Andreas Abel
andreas.abel at ifi.lmu.de
Thu Nov 6 22:39:18 CET 2014
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/
More information about the Agda
mailing list