[Agda] Another Data.List.Any - Is it possible?

[Dmytro Starosud]

Thanks a lot Arseniy for a quick reply and such a detailed explanation!

Best regards,
Dmytro

2013/1/29 Arseniy Alekseyev <arseniy.alekseyev at gmail.com>

> Dear Dmytro,
>
> Here is a solution for your problem:
>
> AnyP[h∷t]⇒Ph⊎AnyPt' : {A : Set} {P : A → Set} {h : A} {t : List A} {w
> : List A} → Any P w → w ≡ h ∷ t → P h ⊎ Any P t
> AnyP[h∷t]⇒Ph⊎AnyPt' (exact [] _ ph) refl = inj₁ ph
> AnyP[h∷t]⇒Ph⊎AnyPt' (exact (h ∷ ls) r px) refl = inj₂ (exact ls r px)
>
> AnyP[h∷t]⇒Ph⊎AnyPt : {A : Set} {P : A → Set} {h : A} {t : List A} →
> Any P (h ∷ t) → P h ⊎ Any P t
> AnyP[h∷t]⇒Ph⊎AnyPt any = AnyP[h∷t]⇒Ph⊎AnyPt' any refl
>
> My primitive understanding of the reason it didn't work for you is
> that Agda was trying to unify a non-constructor pattern (l ++ x ∷ r)
> with a constructor pattern (h ∷ t), which is impossible because it
> can't infer anything about any of the variables involved (it doesn't
> know whether the h is a part of l or not).
>
> My solution was to abstract away the (h ∷ t) part and to replace it
> with a single variable w, while remembering that w ≡ h ∷ t.
> Then Agda was able to unify (l ++ x ∷ r) with w to replace w with the
> former, yielding l ++ x ∷ r ≡ h ∷ t. [Pattern-match on exact]
> After that I pattern-matched on l constructors, giving me two cases:
> x ∷ r ≡ h ∷ t [l = []]
> and
> h ∷ ls ++ x ∷ r ≡ h ∷ t [l = (h ∷ ls)]
> Now RHS and LHS of both of these identities became unifiable because
> non-constructor patterns are only being unified with free variables.
> [pattern-match on refl].
>
> Note that the order of these pattern matches, and thus the order of
> argument occurrence does matter. If you swap arguments to
> AnyP[h∷t]⇒Ph⊎AnyPt', it won't work anymore!
>
> Once you're comfortable with manual creation of helper functions like
> this you may want to check out with-clauses and standard library stuff
> like Relation.Binary.PropositionalEquality.inspect.
>
> Cheers!
> Arseniy.
>
> On 29 January 2013 20:22, Dmytro Starosud <d.starosud at gmail.com> wrote:
> > Hello everyone!
> >
> > In stdlib-0.6 we have:
> > data Any {a p} {A : Set a} (P : A → Set p) : List A → Set (a ⊔ p) where
> >   here  : ∀ {x xs} (px  : P x)      → Any P (x ∷ xs)
> >   there : ∀ {x xs} (pxs : Any P xs) → Any P (x ∷ xs)
> >
> > When I didn't know about it, I tried to do it in the following way:
> > data Any {A : Set} (P : A → Set) : List A → Set where
> >   exact : ∀ {x} l r → P x → Any P (l ++ x ∷ r)
> >
> > For the reasoning I needed a function:
> > AnyP[h∷t]⇒Ph⊎AnyPt : {A : Set} {P : A → Set} {h : A} {t : List A} → Any
> P (h
> > ∷ t) → P h ⊎ Any P t
> > AnyP[h∷t]⇒Ph⊎AnyPt .{h = x} .{t = r} (exact {x = x} [] r p) = _
> > AnyP[h∷t]⇒Ph⊎AnyPt .{h = l} .{t = ls ++ x ∷ r} (exact {x = x} (l ∷ ls) r
> p)
> > = _
> >
> > But I got stuck in implementation.
> > Could you please help me with it?
> > *I don't need such "Any" type, but I am interested whether it is
> possible to
> > do it. And if it is not possible, then why?
> > **I think here some information might be missed like in square function:
> > having x^2 we don't know whether x is positive or negative.
> >
> > Thank you,
> > Dmytro
> >
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda
> >
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130130/ab3179cf/attachment-0001.html