[Agda] x ∈ (append y xs) → ..

[Andreas Abel]

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/