A proof about a mutually inductive proposition

Question

Consider the following code:

Require Import List.

Set Implicit Arguments.

Inductive even_length {A : Type} : list A -> Prop:=
| e_nil : even_length nil
| e_cons : forall e l, odd_length l -> even_length (e::l)
with
  odd_length {A : Type} : list A -> Prop :=
  | o_cons : forall e l, even_length l -> odd_length (e::l). 

Lemma map_even : forall A B (f : A -> B) (l : list A),
    even_length l -> even_length (map f l).
Proof.
  induction l.
  (** nil *)
  - intros. simpl. econstructor.
  (** cons *)
  - intros. simpl.
    inversion_clear H.
    econstructor.
    Abort. (** odd_length l -> odd_length (map f l) would help *)

Notice that I wish to prove it with induction over the list l.

As explained in here, Coq by default only generates non-mutual induction principles and to get the mutual induction principles the Scheme command is necessary. So this is what I did:

Scheme even_length_mut := Induction for even_length Sort Prop
with odd_length_mut := Induction for odd_length Sort Prop.

Check even_length_mut.
(**   
even_length_mut
     : forall (A : Type) (P : forall l : list A, even_length l -> Prop) (P0 : forall l : list A, odd_length l -> Prop),
       P nil e_nil ->
       (forall (e : A) (l : list A) (o : odd_length l), P0 l o -> P (e :: l) (e_cons e o)) ->
       (forall (e : A) (l : list A) (e0 : even_length l), P l e0 -> P0 (e :: l) (o_cons e e0)) -> forall (l : list A) (e : even_length l), P l e 
*)

From this type above and the examples that I saw, I managed to complete this proof like so:

Lemma map_even : forall A B (f : A -> B) (l : list A),
    even_length l -> even_length (map f l).
Proof.
  intros.
  apply (even_length_mut (fun l (h : even_length l) => even_length (map f l) )
                         (fun l (h : odd_length l) => odd_length (map f l) )
        ); 
    try econstructor; auto.
Qed.

However, this induction wasn't over l, it was the so called "induction over evidence".

My question is what should be the predicates in even_length_mut so the induction is over l?

Edit: Also, would be possible to get the odd_length l -> odd_length (map f l) hypothesis?

Answer 1

To prove this by induction we need either to generalize the lemma to get a stronger induction hypothesis or to use a custom induction scheme which adds two elements at once to the list instead of just one (which will also require such a generalization).

Since the default induction scheme (induction l) only adds one element at a time, we need an intermediate predicate to record the "state" of the list inbetween states where it is of even length, namely, we also need to remember the case where l is of odd length.

Lemma map_odd_even {A B} (f : A -> B) : forall l : list A,
  (even_length l -> even_length (map f l)) /\
  (odd_length l -> odd_length (map f l)).
Proof.
  induction l.

You can apply the same idea to prove a more general induction scheme for even-length lists, from which your map_even theorem would follow quite easily via apply even_list_ind. (EDIT: another candidate, induction l using even_list_ind fails, I don't know why.)

Theorem even_list_ind {A} (P : list A -> Prop) :
  P [] ->
  (forall x y l, even_length l -> P l -> P (x :: y :: l)) ->
  forall l, even_length l -> P l.