[Agda] x ∈ (append y xs) → ..
Andreas Abel
andreas.abel at ifi.lmu.de
Wed Dec 18 18:52:25 CET 2013
As always, self-contained code is appreciated to answer your question.
--Andreas
On 18.12.2013 12:23, Sergei Meshveliani wrote:
> Can anybody explain, please, why the below lemma1 is more difficult to
> prove to Agda than lemma0
> ?
>
> append0 : List ℕ → List ℕ
> append0 [] = 0 ∷ []
> append0 (x ∷ xs) = x ∷ (append0 xs)
>
> append : ℕ → List ℕ → List ℕ
> append x [] = x ∷ []
> append x (y ∷ xs) = y ∷ (append x xs)
>
> open module Mem-ℕ = Membership natSetoid using (_∈_)
>
> ---------------------------------------------------------------------
> lemma0 : (x : ℕ) → (xs : List ℕ) → x ∈ (append0 xs) → x ≡ 0 ⊎ (x ∈ xs)
>
> lemma0 _ [] (here x=y) = inj₁ x=y
> ...
> -- skip other patterns
>
> --------------------------------------------------------------------
> lemma1 : (x y : ℕ) → (xs : List ℕ) → x ∈ (append y xs) →
> x ≡ y ⊎ (x ∈ xs)
> lemma1 _ _ [] (here x=y) = inj₁ x=y
> --------------------------------------------------------------------
>
> lemma0 is proved in a natural way, and is type-checked.
>
> For lemma1,
> I expected of the checker to report of "missing patterns" -- which will
> mean that the first pattern is all right.
>
> And the development Agda of November ~20 2013
> reports
> "
> I'm not sure if there should be a case for the constructor here,
> because I get stuck when trying to solve the following unification
> problems (inferred index ≟ expected index):
> x₁ ∷ xs₁ ≟ append y xs
> when checking the definition of lemma1
> ".
>
> I fix the proof by writing a strange complicated code instead of the
> first pattern:
>
> lemma1 x y [] x∈app-y-xs = inj₁ x=y
> where
> x=y : x ≡ y
> x=y with x∈app-y-xs
> ... | here eq = eq
> ... | there ()
>
> This looks strange: the checker is sure and "is not sure" in a pattern
> which is actually the same.
> I guess that for the first pattern, it is not sure that append y []
> is non-empty. But it follows only from normalization.
>
> Does this present a bug?
>
> Thanks,
>
> ------
> Sergei
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
--
Andreas Abel <>< Du bist der geliebte Mensch.
Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY
andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/
More information about the Agda
mailing list