[Agda] join 2 `with'|

[Arseniy Alekseyev]

>> 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...

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 = {!!}


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/