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

[Sergei Meshveliani]

I am sorry for disturbance.

I did another attempt, and it occurs that it has fixed itself!
So that  lemma1  can be written similar as  lemma0.
This effect of auto-fix happens for the second time for the example of
this kind.

Also sometimes expressions like, say,   {xs : List ℕ} → x ∈ (append0 xs)
are not parsed, 
then I re-type the whole line, and they get parsed! 
As if the system plays jokes. 
(Maybe, this is due to details of  emacs  usage?). 

I do not recall all the details. May be this effect with lemma1 is due
to that I often omit the remaining patterns -- for debugging. If it
reports "missing patterns",  then it often occurs that the current
patterns are correct, and then I proceed with the remaining ones. 
May be it is more reliable to provide all patterns for the same purpose,
with setting `postulate' in the remaining ones. 

Thanks,

------
Sergei



On Wed, 2013-12-18 at 18:52 +0100, Andreas Abel wrote:
> 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
> >
> 
>