[Agda] join 2 `with'|
Andreas Abel
andreas.abel at ifi.lmu.de
Mon Nov 3 11:59:56 CET 2014
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/
More information about the Agda
mailing list