[Agda] x ∈ (append y xs) → ..
Sergei Meshveliani
mechvel at botik.ru
Wed Dec 18 12:23:10 CET 2013
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
More information about the Agda
mailing list