[Agda] elem x (filter xs)
Andrea Vezzosi
sanzhiyan at gmail.com
Wed Aug 14 15:29:08 CEST 2013
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
More information about the Agda
mailing list