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">&lt;<a href="mailto:arseniy.alekseyev@gmail.com" target="_blank">arseniy.alekseyev@gmail.com</a>&gt;</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&#39; : {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&#39; (exact [] _ ph) refl = inj₁ ph<br>
AnyP[h∷t]⇒Ph⊎AnyPt&#39; (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&#39; any refl<br>
<br>
My primitive understanding of the reason it didn&#39;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&#39;t infer anything about any of the variables involved (it doesn&#39;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&#39;, it won&#39;t work anymore!<br>
<br>
Once you&#39;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 &lt;<a href="mailto:d.starosud@gmail.com">d.starosud@gmail.com</a>&gt; wrote:<br>
&gt; Hello everyone!<br>
&gt;<br>
&gt; In stdlib-0.6 we have:<br>
&gt; data Any {a p} {A : Set a} (P : A → Set p) : List A → Set (a ⊔ p) where<br>
&gt;   here  : ∀ {x xs} (px  : P x)      → Any P (x ∷ xs)<br>
&gt;   there : ∀ {x xs} (pxs : Any P xs) → Any P (x ∷ xs)<br>
&gt;<br>
&gt; When I didn&#39;t know about it, I tried to do it in the following way:<br>
&gt; data Any {A : Set} (P : A → Set) : List A → Set where<br>
&gt;   exact : ∀ {x} l r → P x → Any P (l ++ x ∷ r)<br>
&gt;<br>
&gt; For the reasoning I needed a function:<br>
&gt; AnyP[h∷t]⇒Ph⊎AnyPt : {A : Set} {P : A → Set} {h : A} {t : List A} → Any P (h<br>
&gt; ∷ t) → P h ⊎ Any P t<br>
&gt; AnyP[h∷t]⇒Ph⊎AnyPt .{h = x} .{t = r} (exact {x = x} [] r p) = _<br>
&gt; AnyP[h∷t]⇒Ph⊎AnyPt .{h = l} .{t = ls ++ x ∷ r} (exact {x = x} (l ∷ ls) r p)<br>
&gt; = _<br>
&gt;<br>
&gt; But I got stuck in implementation.<br>
&gt; Could you please help me with it?<br>
&gt; *I don&#39;t need such &quot;Any&quot; type, but I am interested whether it is possible to<br>
&gt; do it. And if it is not possible, then why?<br>
&gt; **I think here some information might be missed like in square function:<br>
&gt; having x^2 we don&#39;t know whether x is positive or negative.<br>
&gt;<br>
&gt; Thank you,<br>
&gt; Dmytro<br>
&gt;<br>
</div></div>&gt; _______________________________________________<br>
&gt; Agda mailing list<br>
&gt; <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
&gt; <a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
&gt;<br>
</blockquote></div><br>