Software Foundations

MoreInd.v

帰納法のための明示的な証明オブジェクト を読む。

目的の集合を数え上げ尽すことが出来れば、コンストラクタは何でもよい。という意味だと理解。

そういうわけで、以前の l=rev l -> pal l も、

list Xのコンストラクタを変えて、新たな帰納法の原理を作れば出来るんじゃね？と考えた。

Definition list_ind2 :
forall (X:Type) (P : list X -> Prop),
P nil ->
(forall (x:X), P [x]) ->
(forall (x:X) (l:list X), P l -> P (x::(l++[x]))) ->
(forall (x y:X) (l:list X), x <> y -> P l -> P (x::l++[y])) ->
forall l:list X, P l :=
fun P => fun Pnil => fun Px => fun Pxlx => fun Pxly =>
fix f (X:Type) (l:list X) :=
            match l with
             | nil => Pnil
             | [x] => Px
             | x :: l' ++ [x] => Pxlx l' (f l')
             | x :: l' ++ [y] => Pxly l' (f l')
            end.

とかテキトーにでっちあげようとしたが、
コンスラクタ的に、 l' ++ [y]がパターンマッチで上手く展開されないっぽい。

うまく行かないのう。

そのものずばりの問題をStackOverflowで質問してる人がいた。
http://stackoverflow.com/questions/24363319/proving-that-a-reversible-list-is-a-palindrome-in-coq

最初のとこ見ただけだけど、方針は似てる気がする。