<div dir="ltr"><br><div class="gmail_extra"><br><div class="gmail_quote">On Mon, Nov 3, 2014 at 2:38 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"><span class="">
</span>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>
<div class=""><div class="h5"><br>
<br></div></div></blockquote><div><br></div><div>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'<br><br><span style="font-family:courier new,monospace">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 </span><span style="font-family:courier new,monospace">≡ x</span><br><span style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"></span> y false = {!!}</span><span style="font-family:courier new,monospace"> -- Goal: x </span><span style="font-family:courier new,monospace">≡ x</span><br><br></div><div>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.<br></div><div><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 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 variable<br>
> `x`. I thought the only reason to use `with` was when you wanted to 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>
>>> (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>
>>> (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 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>
</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>