Daniel's Blog

Going through the Software Foundations textbook, I found an exercise which I really enjoyed solving. This exercise was to define an inductive property that holds iff a list is a palindrome. A subsequent exercise asks to prove that if a list fits the inductive definition we wrote, then it is its own reverse. A more difficult exercise asks to show that a list being its own inverse means that it matches our definition of a palindrome.

I wasn’t sure at first why the problem said that the inductive definition should have three constructors. I came up with two ways to construct a palindrome:

• An empty list is a palindrome.
• Adding the same value to the back and the front of another palindrome makes a longer palindrome.

Of course, my definition led to only having palindromes of even length. In order to allow for palindromes of odd length, one more rule is needed (another base case):

• A list with a single value is a palindrome.

This translates readily into Coq:

Inductive palindrome { X : Type } : list X -> Prop :=
  | palindrome_nil : palindrome []
  | palindrome_x : forall (x : X), palindrome [x]
  | palindrome_xs : forall (x : X) (l : list X),
	   palindrome l -> palindrome (x::l ++ [x]).

It’s nearly trivial to show that a palindrome is its own inverse:

Theorem pal_rev { X : Type } : forall (l : list X), palindrome l -> l = rev l.
Proof.
  intros l H.
  induction H.
  - reflexivity.
  - reflexivity.
  - simpl. Search rev. rewrite rev_app_distr. simpl. rewrite <- IHpalindrome. reflexivity.
Qed.

This follows from the quasi-distributive property of reverse over append.

The proof in the other direction took me a significant amount of time. It was clear that a proof by induction was necessary, but that’s where I got stuck. Structural induction using the definition of list doesn’t work. It’s trivial to prove the base case; However, the inductive step states that if some list is a palindrome, prepending any x to the front of that list will create another palindrome. This is blatantly wrong; we can come up with numerous cases ([1; 1] prepended with 2, for instance) in which prepending a value to a palindrome does not create a new palindrome. The inductive definition of list did not work well with this proof.

Coq’s basic induction wouldn’t do. But structural induction doesn’t limit us to a particular definition of a list; it just states that if:

• We can prove that a proposition holds for the primitive values of a type
• We can prove that if the proposition holds for the building blocks of a value of the type then the proposition holds for the value built of those blocks

Then, the proposition holds for all values of that type. This can be easily seen in the regular induction on lists: we show that a proposition holds on [], and then that if it holds for l, it also holds for x::l. But this is just one way of constructing a list, and structural induction doesn’t dictate how we construct a value.

As I was working with my definition of a palindrome, it dawned on me that generalizing a single variable in that definition would create another inductive definition of a list. If we change the inductive rule in the palindrome definition from saying “surrounding another palindrome with x on both sides” to “surrounding another list with some x on one side and some y on the other”, we can effectively construct any list. We can then state a different structural induction principle:

Theorem alt_induction { X : Type } : forall (P : list X -> Prop),
    P [] ->
    (forall (x : X), P [x]) ->
    (forall (l : list X), P l -> forall (x y : X), P (x::l++[y])) ->
    forall (ln : list X), P ln.

But how would we go about proving this? If we try to just use induction on ln, we get stuck the same way we get stuck in the palindrome proof. What’s missing?

What’s missing is that there’s nothing as yet stating that appending values to the back and the front of another list is an equivalent way to appending a value only to the front of a list. We need to state this explicitly; but how? I decided that the easiest way would be by defining a new inductive property, list_alt which holds for all lists that can be constructed by adding things to the back and the front. Then, we can show that it holds for all lists, and, therefore, that any list can be constructed this way. I defined the property as such:

Inductive list_alt { X : Type } : list X -> Prop :=
| list_alt_base : list_alt []
| list_alt_x : forall (x : X), list_alt [x]
| list_alt_xy : forall (x y : X) (l : list X), list_alt l -> list_alt (x::l++[y]).

Then, to prove it true for all lists, I first showed what is effectively the inductive hypothesis of a proof by induction on the structure of a list:

Theorem list_alt_cons { X : Type } : forall (x : X) (l : list X),
    list_alt l -> list_alt (x::l).
Proof.
  intros x l H.
  induction H.
  - apply list_alt_x.
  - assert (I : [x;x0] = [x] ++ [] ++ [x0]).
    { reflexivity. }
    rewrite I. apply list_alt_xy. apply list_alt_base.
  - inversion IHlist_alt.
    + simpl. assert (I : [x; x0; y] = [x] ++ [x0] ++ [y]).
      { reflexivity. }
      rewrite I. apply list_alt_xy. apply list_alt_x.
    + assert (I : x0::(l0 ++ [y0]) ++ [y] = (x0::(l0++[y0]))++[y]).
      { reflexivity. }
      rewrite I. apply list_alt_xy. apply list_alt_xy. apply H1.
Qed.

Next, the actual proof of equivalence simply used the previous theorem:

Theorem list_alt_correct { X : Type } : forall (l : list X), list_alt l.
Proof.
  induction l.
  - apply list_alt_base.
  - apply list_alt_cons. apply IHl.
Qed.

Finally, we can prove our custom principle of induction (by induction (!) on the property list_alt, which we now know holds for all lists):

Theorem alt_induction { X : Type } : forall (P : list X -> Prop),
    P [] ->
    (forall (x : X), P [x]) ->
    (forall (l : list X), P l -> forall (x y : X), P (x::l++[y])) ->
    forall (ln : list X), P ln.
Proof.
  intros P Hb1 Hb2 Hss ln.
  induction (list_alt_correct ln).
  - apply Hb1.
  - apply Hb2.
  - apply Hss. apply IHl. Qed.

Finally, the palindrome proof can simply use this principle. Coq turns out to have a mechanism to use a custom induction principle via induction … using …:

Theorem rev_pal' { X : Type } : forall (l : list X), l = rev l -> palindrome l.
Proof.
  intros l H. induction l using alt_induction.
  - (* Base case 1; empty list is palindrome by definition. *)
    apply palindrome_nil.
  - (* Base case 2; singleton list is palindrome by definition. *)
    apply palindrome_x.
  - (* Inductive step (and interesting case.) *)

    (* Milk the reverse property to show that we end and begin with the same thing. *)
    assert (Hi1 : x::l ++ [y] = (x::l) ++ [y]). reflexivity. rewrite Hi1 in H.
    rewrite rev_app_distr in H. simpl in H. injection H as Heq1.

    (* Do the same again; This time, we also find that rev l = l. *)
    apply rev_injective in H. repeat (rewrite rev_app_distr in H). simpl in H. injection H as Heq2.

    (* Use the induction hypothesis to deduce that l is a palindrome. *)
    rewrite rev_involutive in H. symmetry in H. apply IHl in H.

    (* We know we start and end with the same thing; Use the third way to construct a palindrome.
       Since l is a palindrome, we are done. *)
    rewrite Heq1. apply palindrome_xs. apply H.
Qed.

Although I’m proud to have figured this out, I’m not sure if my solution can be considered “good” by the experts. I took advantage of the fact that Coq allows proofs by induction on propositions, which may be less direct than otherwise possible. However, the solution works, and the resulting proofs are quite elegant. I should also note that it’s possible to use list_alt to prove rev_pal wihout using induction. It’s not much longer, but perhaps less clean.