[Agda] join 2 `with'|

[Arseniy Alekseyev]

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.

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