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

[Ulf Norell]

I'm not sure why you are leaving out cases. If you give all the appropriate
cases lemma1 goes through with no problems. Here's my version (with
slightly different definitions from yours):

lemma1 : ∀ x y xs → x ∈ append y xs → x ≡ y ∨ x ∈ xs
lemma1 x .x [] here = inl refl
lemma1 x y [] (there p) = inr p
lemma1 x y (.x ∷ xs) here = inr here
lemma1 x y (x₁ ∷ xs) (there p) with lemma1 x y xs p
lemma1 x y (x₂ ∷ xs) (there p) | inl x=y = inl x=y
lemma1 x y (x₂ ∷ xs) (there p) | inr x∈xs = inr (there x∈xs)

The reason you get the "I'm not sure..." error is that Agda gets confused
when trying to figure out which patterns are missing. I get the same error
for lemma0 though.

/ Ulf



On Wed, Dec 18, 2013 at 6:52 PM, Andreas Abel <andreas.abel at ifi.lmu.de>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
>>
>>
>
> --
> 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/
>
> _______________________________________________
> 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/20131218/36d4d55c/attachment.html