Permuting things

Ej3_generalised.v

Inductive perm (A:Set): (list A) -> (list A) -> Prop:=
 p_refl: forall l:(list A), perm A l l
|p_trans: forall l m n: (list A), (perm A l m) -> (perm A m n) -> perm A l n
|p_ccons: forall (a b: A) (l:(list A)), 
	perm A (cons a (cons b l)) (cons b (cons a l))
|p_cons: forall (a:A) (l m: (list A)), (perm A l m) -> perm A (cons a l) (cons a m).

Fixpoint swap (A:Set) (l:(list A)) {struct l}: (list A) :=
    match l with 
      nil  => nil
      | (cons a l2) => match l2 with 
			 nil => l
      		       | (cons b l3) => cons b (cons a (swap A l3))
		       end
    end.


Fixpoint list_ind_by_2 
  (A : Set) (P : list A -> Prop)
  (Pnil       : P nil)
  (Psingleton : forall a, P (cons a nil))
  (Pcons2     : forall a b xs, P xs -> P (cons a (cons b xs)))
  (xs : list A) : P xs :=

  match xs return P xs with
  | nil                  => Pnil
  | (cons a nil)         => Psingleton a
  | (cons a (cons b xs)) => Pcons2 a b xs (list_ind_by_2 A P Pnil Psingleton Pcons2 xs)
  end.

Lemma Ej3_generalised: forall (A:Set) (l : list A), perm A l (swap A l).
Proof.
intros A l; eapply list_ind_by_2 with (xs := l).
 - constructor.
 - constructor.
 - intros a b xs Ih.
   eapply p_trans, p_ccons.
   do 2 apply p_cons; assumption.
Qed.