<div dir="ltr">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):<div><br></div>
<div><div>lemma1 : ∀ x y xs → x ∈ append y xs → x ≡ y ∨ x ∈ xs</div><div>lemma1 x .x [] here = inl refl</div><div>lemma1 x y [] (there p) = inr p</div><div>lemma1 x y (.x ∷ xs) here = inr here</div><div>lemma1 x y (x₁ ∷ xs) (there p) with lemma1 x y xs p</div>
<div>lemma1 x y (x₂ ∷ xs) (there p) | inl x=y = inl x=y</div><div>lemma1 x y (x₂ ∷ xs) (there p) | inr x∈xs = inr (there x∈xs)</div></div><div><br></div><div>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.</div>
<div><br></div><div>/ Ulf</div><div><br></div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Wed, Dec 18, 2013 at 6:52 PM, Andreas Abel <span dir="ltr"><<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">As always, self-contained code is appreciated to answer your question. --Andreas<div class="HOEnZb"><div class="h5"><br>
<br>
On 18.12.2013 12:23, Sergei Meshveliani wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Can anybody explain, please, why the below lemma1 is more difficult to<br>
prove to Agda than lemma0<br>
?<br>
<br>
append0 : List ℕ → List ℕ<br>
append0 [] = 0 ∷ []<br>
append0 (x ∷ xs) = x ∷ (append0 xs)<br>
<br>
append : ℕ → List ℕ → List ℕ<br>
append x [] = x ∷ []<br>
append x (y ∷ xs) = y ∷ (append x xs)<br>
<br>
open module Mem-ℕ = Membership natSetoid using (_∈_)<br>
<br>
------------------------------<u></u>------------------------------<u></u>---------<br>
lemma0 : (x : ℕ) → (xs : List ℕ) → x ∈ (append0 xs) → x ≡ 0 ⊎ (x ∈ xs)<br>
<br>
lemma0 _ [] (here x=y) = inj₁ x=y<br>
...<br>
-- skip other patterns<br>
<br>
------------------------------<u></u>------------------------------<u></u>--------<br>
lemma1 : (x y : ℕ) → (xs : List ℕ) → x ∈ (append y xs) →<br>
x ≡ y ⊎ (x ∈ xs)<br>
lemma1 _ _ [] (here x=y) = inj₁ x=y<br>
------------------------------<u></u>------------------------------<u></u>--------<br>
<br>
lemma0 is proved in a natural way, and is type-checked.<br>
<br>
For lemma1,<br>
I expected of the checker to report of "missing patterns" -- which will<br>
mean that the first pattern is all right.<br>
<br>
And the development Agda of November ~20 2013<br>
reports<br>
"<br>
I'm not sure if there should be a case for the constructor here,<br>
because I get stuck when trying to solve the following unification<br>
problems (inferred index ≟ expected index):<br>
x₁ ∷ xs₁ ≟ append y xs<br>
when checking the definition of lemma1<br>
".<br>
<br>
I fix the proof by writing a strange complicated code instead of the<br>
first pattern:<br>
<br>
lemma1 x y [] x∈app-y-xs = inj₁ x=y<br>
where<br>
x=y : x ≡ y<br>
x=y with x∈app-y-xs<br>
... | here eq = eq<br>
... | there ()<br>
<br>
This looks strange: the checker is sure and "is not sure" in a pattern<br>
which is actually the same.<br>
I guess that for the first pattern, it is not sure that append y []<br>
is non-empty. But it follows only from normalization.<br>
<br>
Does this present a bug?<br>
<br>
Thanks,<br>
<br>
------<br>
Sergei<br>
<br>
<br>
______________________________<u></u>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/<u></u>mailman/listinfo/agda</a><br>
<br>
</blockquote>
<br>
<br></div></div><span class="HOEnZb"><font color="#888888">
-- <br>
Andreas Abel <>< Du bist der geliebte Mensch.<br>
<br>
Theoretical Computer Science, University of Munich<br>
Oettingenstr. 67, D-80538 Munich, GERMANY<br>
<br>
<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a><br>
<a href="http://www2.tcs.ifi.lmu.de/~abel/" target="_blank">http://www2.tcs.ifi.lmu.de/~<u></u>abel/</a></font></span><div class="HOEnZb"><div class="h5"><br>
______________________________<u></u>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/<u></u>mailman/listinfo/agda</a><br>
</div></div></blockquote></div><br></div>