palindrome

[sven--]

I've been trying to solve "palindrome" problem in prop.v.
To complete my argument, different way of induction is needed such as
p [] ->
forall v : X, p v ->
(forall l : list X, v0 v1 : X
p l -> p ([v0] ++ l ++ [v1])).
However, I was unable to show this with tactics I know.
Can I do this with what I've learnt? or there is some other way?

[sven--]

I admitted it and progressed for now.

[jeehoonkang]

응 그 principle을 찾은건 매우 훌륭한 일이고, 그걸 증명하면 되긴 하는데,

그것보다 다음과 같은 induction principle을 증명하는게 더 편할거야:
forall (P: nat -> Prop) (HP: forall n, (forall m, m < n -> P m) -> P n)
-> forall n, P n.
("m<n인 모든 m에 대해 P가 성립하면, n에 대해서도 P가 성립한다" => "모든 n에 대해 P가 성립한다")

이걸 list의 length에 대한 induction에 쓰면 좋은 결과가 있을듯 해. (참고로 위 명제는 plain induction principle로 (어렵지 않게) 증명할 수 있음.)

induction