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

[Arseniy Alekseyev]

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
>