<div dir="ltr"><div>Hi,</div><div><br></div>To prove lemma1 you'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've an assumption like mem-x in scope, the only thing that'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 "with" then the body of the clause will be typechecked in an environment where all occurrences of (filterMem (x ∷ [])) are replaced by what we'll match it against, ignoring what (filterMem (x ∷ [])) itself would evaluate to. In this case that's only going to produce the problems you'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's thesis [1] and its citations, maybe it should be ported to the wiki. It doesn'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'd want to use "here {x = x} refl" 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"><<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>></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>
ℕ !=< 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' 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''<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>