[Agda] join 2 `with'|

Arseniy Alekseyev arseniy.alekseyev at gmail.com
Wed Nov 5 09:21:43 CET 2014 

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> wrote:
>
>
> On Tue, Nov 4, 2014 at 5:18 PM, Arseniy Alekseyev
> <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>
>> wrote:
>> >
>> >
>> > On Mon, Nov 3, 2014 at 2:38 PM, Arseniy Alekseyev
>> > <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> 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> 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
>> >> >>> https://lists.chalmers.se/mailman/listinfo/agda
>> >> >>
>> >> >> _______________________________________________
>> >> >> Agda mailing list
>> >> >> 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
>> >> > http://www2.tcs.ifi.lmu.de/~abel/
>> >> _______________________________________________
>> >> Agda mailing list
>> >> 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

More information about the Agda mailing list