[Agda] join 2 `with'|
Arseniy Alekseyev
arseniy.alekseyev at gmail.com
Mon Nov 3 09:47:23 CET 2014
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
More information about the Agda
mailing list