(* prelude : add some result to the module Rstar *)

Require Import Relations.
Require Import Rstar.

Lemma Rstar_ind :
 forall (A:Set) (R X:A -> A -> Prop),
   (forall a:A, X a a) ->
   (forall a b c:A, R a b -> X b c -> X a c) ->
   forall a b:A, Rstar _ R a b -> X a b.
Proof.
 intros.
 apply H1; eauto.
Qed.

Lemma Rstar_intro1 :
 forall (A:Set) (R:A -> A -> Prop) (a b:A), R a b -> Rstar _ R a b.
Proof.
 unfold Rstar; intros A R a b H P H0 H1.
 eapply H1; eauto.
Qed.

Lemma Rstar_intro2 :
 forall (A:Set) (R:A -> A -> Prop) (a b c:A),
   R a b -> Rstar _ R b c -> Rstar _ R a c.
Proof.
 intros A R a b c H H0.
 unfold Rstar; intros P H1 H2.
 apply H2 with b; auto.
 apply H0; auto.
Qed.

Lemma Rstar_intro3 :
 forall (A:Set) (R:A -> A -> Prop) (a b c:A),
   R b c -> Rstar _ R a b -> Rstar _ R a c.
Proof.
 intros A R a b c H H0.
 generalize H; pattern a, b; apply H0.
 intros u Hu; apply Rstar_intro1; auto.
 intros u v w H1 H2 H3.
 eapply Rstar_intro2; eauto.
Qed.

Theorem Rstar_sym :
 forall (A:Set) (R:A -> A -> Prop), symmetric _ R -> symmetric _ (Rstar _ R).
Proof.
 intros A R H a b H0.
 pattern a, b. 
 eapply (Rstar_ind _ R); auto.
 unfold Rstar; auto.
 intros a0 b0 c H1 H2; eapply Rstar_intro3. 
 eapply H; eauto.
 assumption.
Qed.

Require Import List.

Set Implicit Arguments.
Unset Strict Implicit.

Require Import Relations.
Section perms.
Variable A : Set.

 Inductive transpose : list A -> list A -> Prop :=
   | transpose_hd :
       forall (a b:A) (l:list A), transpose (a :: b :: l) (b :: a :: l)
   | transpose_tl :
       forall (a:A) (l l':list A),
         transpose l l' -> transpose (a :: l) (a :: l')
  .

Definition perm := Rstar _ transpose.

Lemma transpose_sym : forall l l':list A, transpose l l' -> transpose l' l.
Proof.
 intros l l' H; elim H; [ left | right; auto ].
Qed.

Theorem equiv_perm : equiv _ perm.
Proof.
 unfold perm; repeat split.
 unfold reflexive; apply Rstar_reflexive.
 unfold transitive; apply Rstar_transitive.
 apply Rstar_sym.
 unfold symmetric; apply transpose_sym.
Qed.

End perms.