[Agda] elem x (filter xs)

[Andrea Vezzosi]

Hi,

To prove lemma1 you've to proceed like this:

lemma1 : (x : ℕ) → member x → Any (_≡_ x) (filterMem (x ∷ []))
lemma1 x mem-x with member? x
...               | (yes _) = here refl
...               | no notx = ⊥-elim (notx mem-x)


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.

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.

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.

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

    here : ∀ {x xs} (px  : P x) → Any P (x ∷ xs)

as a function its type is actually

    here : ∀ {a p} {A : Set a} {P : A → Set p} {x xs} (px  : P x) → Any P
(x ∷ xs)

so you'd want to use "here {x = x} refl" in your case.

In patterns it works as if the type is still the declared one instead.

Hoping this helps,
   Andrea

[1] http://www.cse.chalmers.se/~ulfn/papers/thesis.html




On Wed, Aug 14, 2013 at 1:51 PM, Sergei Meshveliani <mechvel at botik.ru>wrote:

> Can you, please, help with the following example with a filtered list?
>
> -----------------------------------------------------------------------
> open import Level            using (Level) renaming (zero to 0L)
> open import Function         using (case_of_)
> open import Relation.Nullary using (Dec; yes; no)
> open import Relation.Binary.Core using (_≡_; refl)
> open import Data.Empty       using (⊥-elim)
> open import Data.Nat         using (ℕ; _≟_)
> open import Data.List        using (List; []; _∷_)
> open import Data.List.Any    using (Any; module Any)
>
> postulate member  : ℕ → Set
> postulate member? : (x : ℕ) → Dec (member x)
>
> filterMem : List ℕ → List ℕ
> filterMem []       = []
> filterMem (x ∷ xs)  with member? x
> ...                    | yes _ = x ∷ (filterMem xs)
> ...                    | _     = filterMem xs
>
> open Any
>
> lemma1 : (x : ℕ) → member x → Any (_≡_ x) (filterMem (x ∷ []))
>
> lemma1 x mem-x  with  member? x | filterMem (x ∷ [])
>
> ...                 | (yes _) | .(x ∷ []) =  here {x} {[]} refl
>
> -----------------------------------------------------------------------
>
> This is an attempt to prove this trivial statement:
>
>   if  x  is in a subset  S  then  x  is in  filterMem (x :: []),
>   where  filterMem  filters my membership to S.
>
> To be more explicit, I replace  x \in ys  with  Any (_≡_ x) ys.
>
> The  Agda-2.3.2.1  (lib-0.7)  report is
> ------
> Failed to infer the value of dotted pattern
> when checking that the pattern .(x ∷ []) has type List ℕ
> ------
>
> 1. Having  mem-x : member x,  why does not it accept  .(x ∷ [])
>    for  filterMem (x ∷ [])  ?
>
> 2. Then, I change the last line to
>
> ...           | (yes _) | (_ ∷ _) =  here {x} {[]} refl
>
> And it reports
> -------
> ℕ !=< Level of type Set
> when checking that the expression x has type Level
> -------
>
> This is on the {x} occurrence in the last line.
> Why  x  needs to be of  Level ?
> `here' has not Level among its argument types.
>
> 3. Having  mem-x  and normalization by  filterMem,
>    I expected that a simple                  `` = here refl''
> would do the implementation. But it does not.
>
> 4. Changing to
> ...     | (yes _) | y :: ys =  here {x} {_} x=y
>                                where
>                                x=y = x ≡ y
>                                x=y = ?
>
> we need to prove x ≡ y,  which is not simpler than the initial goal.
>
>
> 5. How to prove the goal?
>
>
> Thank you in advance for explanation,
>
> ------
> Sergei
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130814/00d9c02c/attachment.html