[Agda] join 2 `with'|
Christopher Jenkins
cjenkin1 at trinity.edu
Wed Nov 5 02:28:48 CET 2014
On Tue, Nov 4, 2014 at 5:18 PM, Arseniy Alekseyev <
arseniy.alekseyev at gmail.com> wrote:
> That was not a genuine attempt to prove `y : ∀ q → x ≡ z q`. Instead
> that was an example of `with` rewriting the goal from (as you
> demonstrated!) provable one into (as I assert) non-provable one. I
> think that's the property of `with` that's causing you grief when you
> re-order or nest them in a bad way.
>
> 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.
Actually, decided to include it anyway, so you could smell the smelly code
smell:
y : ∀ q → x ≡ z q
y with x
y | true = λ { true → refl ; false → refl }
y | false = λ { true → refl ; false → refl }
> On 4 November 2014 22:43, Christopher Jenkins <cjenkin1 at trinity.edu>
> wrote:
> >
> >
> > On Mon, Nov 3, 2014 at 2:38 PM, Arseniy Alekseyev
> > <arseniy.alekseyev at gmail.com> wrote:
> >>
> >> 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 = {!!}
> >>
> >>
> >
> > 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'
> >
> > f : Bool → Bool
> > f x = true where
> > z : Bool → Bool
> > z true = x
> > z false = x
> >
> > y : ∀ q → x ≡ z q
> > y true = {!!} -- Goal: x ≡ x
> > y false = {!!} -- Goal: x ≡ x
> >
> > 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.
> >
> >
> >>
> >> 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/
> >> _______________________________________________
> >> Agda mailing list
> >> Agda at lists.chalmers.se
> >> https://lists.chalmers.se/mailman/listinfo/agda
> >
> >
> >
> >
> > --
> > Christopher Jenkins
> > Computer Science 2013
> > Trinity University
>
--
Christopher Jenkins
Computer Science 2013
Trinity University
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20141104/b787243c/attachment-0001.html
More information about the Agda
mailing list