Using 'unfold' of a Fixpoint inside the recursive step of the induction

Question

I'm trying to prove something in coq and the same problem keeps coming up; I want to unfold the definition of a Fixpoint inside the recursive (not nil) step of induction. Unfold works as expected, here's an example:

Before unfolding the list reverse (rev) definition:

  n : nat
  l' : natlist
  IHl' : rev (rev l') = l'
  ============================
  rev (rev (n :: l')) = n :: l'

After:

  n : nat
  l' : natlist
  IHl' : rev (rev l') = l'
  ============================
  (fix rev (l : natlist) : natlist := match l with
                                      | [ ] => [ ]
                                      | h :: t => rev t ++ [h]
                                      end)
    ((fix rev (l : natlist) : natlist := match l with
                                         | [ ] => [ ]
                                         | h :: t => rev t ++ [h]
                                         end) l' ++ [n]) = n :: l'

So far so good. Now I would expect simpl to figure out I'm on the non-nil case of the induction since n :: l' can never be nil, and simplify away the nil case of the match ([ ] => [ ]), keeping only the non-nil part of the definition.

Unfortunately it does not do that implicitly. How can I make unfold of a recursive Fixpoint definition play well with induction? How do I get:

  n : nat
  l' : natlist
  IHl' : rev (rev l') = l'
  ============================
  rev (rev l' ++ [n]) = n :: l'

According to the rev definition for the inner rev.

Note: The use of Lists is irrelevant here, the same technique can be used for any inductively defined types.

Edit: Definition of rev and proof that leads to the After state.

Fixpoint rev (l:natlist) : natlist :=
  match l with
  | nil    => nil
  | h :: t => rev t ++ [h]
  end.

Theorem rev_involutive : forall l : natlist,
  rev (rev l) = l.
Proof.
  intros l. induction l as [| n l'].
  - reflexivity.
  - unfold rev.

Please try to submit a Minimal Complete and Verifiable Example. It's a lot easier to answer when we can step through the proof an try different things. — gallais
Added the definition of rev and the proof that leads to the After state. — rausted

gallais gallais · Accepted Answer · 2017-11-21T00:02:36

Your After: is basically rev (rev l' ++ [n]) (with rev unfolded) which means that the reduction you want to see happening has already happened. Now you probably want to prove an auxiliary lemma akin to rev (xs ++ ys) = rev ys ++ rev xs.

Using 'unfold' of a Fixpoint inside the recursive step of the induction

1 Answers