Pal

Pal.v

Inductive pal {X : Type} : (list X) -> Prop :=
  | p_nil : pal nil
  | p_one : forall x : X, pal [x]
  | p_rec : forall (x : X) (xs : list X), pal xs -> pal (x :: xs ++ [x]).

Example pal_1_2_3_4_4_3_2_1 : pal [1;2;3;4;4;3;2;1].
Proof.
  apply (p_rec 1 [2; 3; 4; 4; 3; 2]).
  apply (p_rec 2 [3; 4; 4; 3]).
  apply (p_rec 3 [4; 4]).
  apply (p_rec 4 []).
  apply p_nil.
Qed.

Example pal_1_2_3_4_3_2_1 : pal [1;2;3;4;3;2;1].
Proof.
  apply (p_rec 1 [2; 3; 4; 3; 2]).
  apply (p_rec 2 [3; 4; 3]).
  apply (p_rec 3 [4]).
  apply p_one.
Qed.

Lemma not_app_nil : forall (X : Type) (xs ys : list X) (y : X),
                      not (xs ++ y :: ys = []).
Proof.
  unfold not.
  intros.
  destruct xs as [|z zs].
  inversion H.
  inversion H.
Qed.

Example not_pal_1_2 : not (pal [1;2]).
Proof.
  unfold "~".
  intros.
  inversion H.
  destruct xs as [|y ys].
  inversion H2. inversion H2. apply not_app_nil in H5. apply H5.
Qed.

Example not_pal_1_2_3_4_5 : not (pal [1;2;3;4;5]).
Proof.
  unfold "~".
  intros.
  inversion H.
  destruct xs as [|y ys].
  Case "nil".
    inversion H2.
  Case "cons".
    inversion H2.
    destruct ys as [|z zs].
    SCase "nil".
      inversion H5.
    SCase "cons".
      inversion H5.
      destruct zs as [|m ms].
      SSCase "nil".
        inversion H7.
      SSCase "cons".
        inversion H7.
        destruct ms as [|n ns].
        SSSCase "nil".
          inversion H9.
        SSSCase "cons".
          inversion H9.
          apply not_app_nil in H11. apply H11.
Qed.