■

Inductive

型とか命題の定義を行う。

回文の定義で、

Inductive pal {X:TYpe} : list X -> Prop :=
 | p_zero: pal []
 | p_one : forall x:X, pal [x]
 | p_2   : forall l,  pal (l ++ (rev l))
 | p_3   : forall l1 l2, pal l2 ->  pal (l1 ++ l2 ++ (rev l1)).

とか、今から考えるとやたらややこしいことやって、pal l -> l = rev lの証明もなんとか出来たけど、

Inductive pal {X:TYpe} : list X -> Prop :=
 | pal_0 : pal []
 | pal_1 : forall x:X, pal [x]
 | pal_n : forall (x:X) l, pal l -> pal (x :: l ++ [x]).

で十分だった。
証明も圧倒的に簡単になった。