<div dir="ltr"><br><div class="gmail_extra"><br><div class="gmail_quote">On Tue, Nov 4, 2014 at 5:18 PM, Arseniy Alekseyev <span dir="ltr"><<a href="mailto:arseniy.alekseyev@gmail.com" target="_blank">arseniy.alekseyev@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">That was not a genuine attempt to prove `y : ∀ q → x ≡ z q`. Instead<br>
that was an example of `with` rewriting the goal from (as you<br>
demonstrated!) provable one into (as I assert) non-provable one. I<br>
think that's the property of `with` that's causing you grief when you<br>
re-order or nest them in a bad way.<br>
<div class=""><div class="h5"><br></div></div></blockquote><div>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.<br></div><div><br></div><div>Actually, decided to include it anyway, so you could smell the smelly code smell:<br><br> y : ∀ q → x ≡ z q<br> y with x<br> y | true = λ { true → refl ; false → refl }<br> y | false = λ { true → refl ; false → refl }<br></div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div class=""><div class="h5">
On 4 November 2014 22:43, Christopher Jenkins <<a href="mailto:cjenkin1@trinity.edu">cjenkin1@trinity.edu</a>> wrote:<br>
><br>
><br>
> On Mon, Nov 3, 2014 at 2:38 PM, Arseniy Alekseyev<br>
> <<a href="mailto:arseniy.alekseyev@gmail.com">arseniy.alekseyev@gmail.com</a>> wrote:<br>
>><br>
>> You are right, there is not much point. I was trying to point out that<br>
>> it's the "proper expression" part that makes `with` complicated.<br>
>><br>
>> Unfortunately, that's not even true. In the following example, I don't<br>
>> think you can fill the holes.<br>
>><br>
>> f : Bool → Bool<br>
>> f x = true where<br>
>><br>
>> z : Bool → Bool<br>
>> z true = x<br>
>> z false = x<br>
>><br>
>> y : ∀ q → x ≡ z q<br>
>> y with x<br>
>> y | true = {!!}<br>
>> y | false = {!!}<br>
>><br>
>><br>
><br>
> I'm not entirely sure why you would expect that approach to be fruitful.<br>
> Essentially, what you're trying to do is unwind the computational nature of<br>
> `z', which is defined by case analysis on its argument (in this case q). To<br>
> trigger the rules, you would have to bring q into scope and inspect q, which<br>
> would then lead to `z true' and `z false' in the equations, respectively,<br>
> and Agda will then go on to normalize the goals as `x \== x'<br>
><br>
> f : Bool → Bool<br>
> f x = true where<br>
> z : Bool → Bool<br>
> z true = x<br>
> z false = x<br>
><br>
> y : ∀ q → x ≡ z q<br>
> y true = {!!} -- Goal: x ≡ x<br>
> y false = {!!} -- Goal: x ≡ x<br>
><br>
> I have actually been thinking about writing a blog post targeted at newbies<br>
> (such as myself) on the sometimes unintuitive behaviour of `with' (and in<br>
> particular, `rewrite'). Should anyone be interested I can send a link on<br>
> this email chain once I have written it.<br>
><br>
><br>
>><br>
>> On 3 November 2014 10:59, Andreas Abel <<a href="mailto:andreas.abel@ifi.lmu.de">andreas.abel@ifi.lmu.de</a>> wrote:<br>
>> > On 03.11.2014 09:47, Arseniy Alekseyev wrote:<br>
>> >> I think the problem goes away if you<br>
>> >> only use `with x` where `x` is a variable.<br>
>> ><br>
>> > Mmh, why use `with` at all then? You could directly split on the<br>
>> > variable<br>
>> > `x`. I thought the only reason to use `with` was when you wanted to<br>
>> > case on<br>
>> > a proper expression and refine your type in the with-branches...<br>
>> ><br>
>> ><br>
>> ><br>
>> > On 03.11.2014 09:47, Arseniy Alekseyev wrote:<br>
>> >><br>
>> >> Indeed that's the usual Agda behaviour.<br>
>> >> Here the reason seems to be an additional occurrence of `lookup k ps`<br>
>> >> in the context produced by pattern-match on `no`.<br>
>> >> You see, `with expr` only rewrites the occurrences of `expr` present<br>
>> >> in the enclosing context, so the new occurrences inside the body of<br>
>> >> `with` don't get rewritten (and you do want it rewritten in this<br>
>> >> case).<br>
>> >><br>
>> >> I do agree this is confusing. I think the problem goes away if you<br>
>> >> only use `with x` where `x` is a variable. That makes `with` much less<br>
>> >> useful though. You can also avoid `with` altogether and write the<br>
>> >> helper functions by hand (that's what `with` is doing after all!).<br>
>> >><br>
>> >> On 2 November 2014 17:14, <<a href="mailto:mechvel@scico.botik.ru">mechvel@scico.botik.ru</a>> wrote:<br>
>> >>><br>
>> >>> People,<br>
>> >>><br>
>> >>> Having the proof<br>
>> >>><br>
>> >>> prove : (k∈ks : k ∈ ks) → proj₂ (lookupIf∈ k (p ∷ ps) k∈k':ks) ≡<br>
>> >>> proj₂ (lookupIf∈ k ps k∈ks)<br>
>> >>> prove k∈ks with k ≟ k'<br>
>> >>> --<br>
>> >>> (I)<br>
>> >>><br>
>> >>> ... | yes k≡k' = ⊥-elim $ k≉k' k≡k'<br>
>> >>> ... | no _ with lookup k ps<br>
>> >>> ... | inj₁ _ = PE.refl<br>
>> >>> ... | inj₂ k∉ks = ⊥-elim $ k∉ks k∈ks<br>
>> >>><br>
>> >>><br>
>> >>> (I do not give the complete code),<br>
>> >>><br>
>> >>> I try to rewrite it in a bit simpler way by joining it into one `with'<br>
>> >>> clause:<br>
>> >>><br>
>> >>><br>
>> >>> prove k∈ks with k ≟ k' | lookup k ps<br>
>> >>> --<br>
>> >>> (II)<br>
>> >>><br>
>> >>> ... | yes k≡k' | _ = ⊥-elim $ k≉k' k≡k'<br>
>> >>> ... | no _ | inj₁ _ = PE.refl<br>
>> >>> ... | no _ | inj₂ k∉ks = ⊥-elim $ k∉ks k∈ks<br>
>> >>><br>
>> >>><br>
>> >>> (I) is type-checked, and (II) is not.<br>
>> >>><br>
>> >>> Is this natural for Agda to decide so?<br>
>> >>><br>
>> >>> (I have spent 4 hours trying to prove a similar real and evident<br>
>> >>> example.<br>
>> >>> Then tried to split `with' into two, and this has succeeded).<br>
>> >>><br>
>> >>> Thanks,<br>
>> >>><br>
>> >>> ------<br>
>> >>> Sergei<br>
>> >>> _______________________________________________<br>
>> >>> Agda mailing list<br>
>> >>> <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
>> >>> <a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
>> >><br>
>> >> _______________________________________________<br>
>> >> Agda mailing list<br>
>> >> <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
>> >> <a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
>> >><br>
>> ><br>
>> ><br>
>> > --<br>
>> > Andreas Abel <>< Du bist der geliebte Mensch.<br>
>> ><br>
>> > Department of Computer Science and Engineering<br>
>> > Chalmers and Gothenburg University, Sweden<br>
>> ><br>
>> > <a href="mailto:andreas.abel@gu.se">andreas.abel@gu.se</a><br>
>> > <a href="http://www2.tcs.ifi.lmu.de/~abel/" target="_blank">http://www2.tcs.ifi.lmu.de/~abel/</a><br>
>> _______________________________________________<br>
>> Agda mailing list<br>
>> <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
>> <a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
><br>
><br>
><br>
><br>
> --<br>
> Christopher Jenkins<br>
> Computer Science 2013<br>
> Trinity University<br>
</div></div></blockquote></div><br><br clear="all"><br>-- <br><div class="gmail_signature"><div dir="ltr"><div>Christopher Jenkins<br>Computer Science 2013<br>Trinity University</div></div></div>
</div></div>