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