<div dir="ltr"><div>Hi,</div><div><br></div>To prove lemma1 you&#39;ve to proceed like this:<div><br></div><div><div>lemma1 : (x : ℕ) → member x → Any (_≡_ x) (filterMem (x ∷ []))</div><div>lemma1 x mem-x with member? x</div>
<div>...               | (yes _) = here refl</div><div>...               | no notx = ⊥-elim (notx mem-x)</div></div><div><br></div><div><br></div><div>This is because the typechecker will never care that you&#39;ve an assumption like mem-x in scope, the only thing that&#39;s handled automatically is normalization (and eta-equivalence), other reasoning has to be made explicitly.</div>
<div><br></div><div>Also, if we add (filterMem (x ∷ [])) to our &quot;with&quot; then the body of the clause will be typechecked in an environment where all occurrences of (filterMem (x ∷ [])) are replaced by what we&#39;ll match it against, ignoring what (filterMem (x ∷ [])) itself would evaluate to. In this case that&#39;s only going to produce the problems you&#39;ve faced in the points 1 and 4.</div>
<div><br></div><div>I think the best available explanation of the with construct is at page 45 of Ulf Norell&#39;s thesis [1] and its citations, maybe it should be ported to the wiki. It doesn&#39;t rely too much on the earlier concepts, and those that remain could be explained in the translation.</div>
<div><br></div><div>As for point 2. the problem is that constructors, when used in expressions, inherit the parameters of their data-type as implicit arguments, so while here is declared as</div><div><br></div><div>    here : ∀ {x xs} (px  : P x) → Any P (x ∷ xs)</div>
<div><br></div><div>as a function its type is actually</div><div><br></div><div>    here : ∀ {a p} {A : Set a} {P : A → Set p} {x xs} (px  : P x) → Any P (x ∷ xs)</div><div><br></div><div>so you&#39;d want to use &quot;here {x = x} refl&quot; in your case.</div>
<div><br></div><div>In patterns it works as if the type is still the declared one instead.</div><div><br></div><div>Hoping this helps,<br></div><div>   Andrea</div><div><br></div><div>[1] <a href="http://www.cse.chalmers.se/~ulfn/papers/thesis.html">http://www.cse.chalmers.se/~ulfn/papers/thesis.html</a><br>
</div><div><br></div><div><br></div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Wed, Aug 14, 2013 at 1:51 PM, Sergei Meshveliani <span dir="ltr">&lt;<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>&gt;</span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Can you, please, help with the following example with a filtered list?<br>
<br>
-----------------------------------------------------------------------<br>
open import Level            using (Level) renaming (zero to 0L)<br>
open import Function         using (case_of_)<br>
open import Relation.Nullary using (Dec; yes; no)<br>
open import Relation.Binary.Core using (_≡_; refl)<br>
open import Data.Empty       using (⊥-elim)<br>
open import Data.Nat         using (ℕ; _≟_)<br>
open import Data.List        using (List; []; _∷_)<br>
open import Data.List.Any    using (Any; module Any)<br>
<br>
postulate member  : ℕ → Set<br>
postulate member? : (x : ℕ) → Dec (member x)<br>
<br>
filterMem : List ℕ → List ℕ<br>
filterMem []       = []<br>
filterMem (x ∷ xs)  with member? x<br>
...                    | yes _ = x ∷ (filterMem xs)<br>
...                    | _     = filterMem xs<br>
<br>
open Any<br>
<br>
lemma1 : (x : ℕ) → member x → Any (_≡_ x) (filterMem (x ∷ []))<br>
<br>
lemma1 x mem-x  with  member? x | filterMem (x ∷ [])<br>
<br>
...                 | (yes _) | .(x ∷ []) =  here {x} {[]} refl<br>
<br>
-----------------------------------------------------------------------<br>
<br>
This is an attempt to prove this trivial statement:<br>
<br>
  if  x  is in a subset  S  then  x  is in  filterMem (x :: []),<br>
  where  filterMem  filters my membership to S.<br>
<br>
To be more explicit, I replace  x \in ys  with  Any (_≡_ x) ys.<br>
<br>
The  Agda-2.3.2.1  (lib-0.7)  report is<br>
------<br>
Failed to infer the value of dotted pattern<br>
when checking that the pattern .(x ∷ []) has type List ℕ<br>
------<br>
<br>
1. Having  mem-x : member x,  why does not it accept  .(x ∷ [])<br>
   for  filterMem (x ∷ [])  ?<br>
<br>
2. Then, I change the last line to<br>
<br>
...           | (yes _) | (_ ∷ _) =  here {x} {[]} refl<br>
<br>
And it reports<br>
-------<br>
ℕ !=&lt; Level of type Set<br>
when checking that the expression x has type Level<br>
-------<br>
<br>
This is on the {x} occurrence in the last line.<br>
Why  x  needs to be of  Level ?<br>
`here&#39; has not Level among its argument types.<br>
<br>
3. Having  mem-x  and normalization by  filterMem,<br>
   I expected that a simple                  `` = here refl&#39;&#39;<br>
would do the implementation. But it does not.<br>
<br>
4. Changing to<br>
...     | (yes _) | y :: ys =  here {x} {_} x=y<br>
                               where<br>
                               x=y = x ≡ y<br>
                               x=y = ?<br>
<br>
we need to prove x ≡ y,  which is not simpler than the initial goal.<br>
<br>
<br>
5. How to prove the goal?<br>
<br>
<br>
Thank you in advance for explanation,<br>
<br>
------<br>
Sergei<br>
<br>
<br>
<br>
_______________________________________________<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>
</blockquote></div><br></div>