(* AUTEURS / AUTHORS :                          *)
(* Judicaël Courant,   Jean-François Monin      *)
(* VERIMAG, Université Joseph Fourier, Grenoble *)
(*                                         2006 *)

Require Import GenericTactics.

(* alphabet *)
Inductive V : Set := a : V | b : V.

Definition eqV (x y : V) : {x=y}+{x<>y}.
destruct x; destruct y;splitsolve0 1.
Defined.

Lemma eqV_refl : forall x, eqV x x = left (x<>x) (refl_equal x).
destruct x; trivial.
Qed.
Hint Rewrite eqV_refl : rew_db.

Inductive word : Set :=  Eps : word  | Snoc : word -> V -> word.

Notation "u :: x" := (Snoc u x) (at level 60, left associativity).

Notation "[ x ]" := (Snoc Eps x) (at level 1).

Fixpoint append (u v: word) {struct v} : word :=
  match v with
    | Eps => u
    | v :: x => (append u v) :: x
  end.
Notation "u @ v" := (append u v) (at level 60, left associativity).

Lemma append_assoc : forall u v w, u @ (v @ w) = u @ v @ w.
intros u v w; elim w; clear w; simpl. 
  reflexivity.
  intros w Hrec x. case Hrec. reflexivity. 
Qed. 

Lemma append_eps_u : forall u, Eps @ u = u.
induction u; simpl; congruence.
Qed.
Lemma append_snoc : forall u v x, u @ (v :: x) = (u@v) :: x.
trivial.
Qed.
Hint Rewrite append_assoc append_eps_u append_snoc : rew_db.

(* length of a word *)
Fixpoint length (u: word) {struct u} : nat :=
  match u with
    | Eps => 0
    | u :: y => (length u + 1)
  end.

Notation "|| u ||" := (length u) (at level 40).

Lemma length_append : forall u v, ||u@v|| = ||u|| + ||v||.
induction v; splitsolve0 0.
Qed.
Hint Rewrite length_append : rew_db.

Require Import Compare_dec.

Lemma length_rect :
  forall (P : word -> Type) u,
  (forall u0, (forall v, ||v|| < ||u0|| -> P v) -> P u0) -> P u.
(** We first introduce variables and the inductive step: *)
intros P u H_Step.
(** We claim the following properties over natural numbers: *)
assert (Gen : (forall n u1, length u1 < n -> P u1)).
  (** - To prove it, we can use the induction principle for natural numbers: *)
  induction n.
    (** -- The case [0] is trivial thanks to [H_Step]: *)
    splitsolve0 1...
    (** -- The case [(S n)] holds thanks to [H_Step] and the induction
        hypothesis: *)
(* JF -> Judicael : revoir, case inerdit sur informatif -> echec splitsolve *)
(*    splitsolve0 2...  ancien ok dans Prop -> bug de Ltac (pb inversion) *)
    intros u1 l_u1_Sn; case (le_lt_eq_dec (||u1||) n).  
      auto with arith...
      exact (IHn u1)...
      intro e; apply H_Step. rewrite e. exact IHn...
       
  (** - The main claim now clearly holds (just apply [Gen] to
      [(S ||u||)] and [u]): *)
(* JF -> Judicael : revoir, echec splitsolve *)
(*splitsolve0 1.*)
  apply (Gen (S (||u||)) u). splitsolve0 1.
Qed.

(* Occurrences of a letter in a word *)
Fixpoint nb_occ (x: V) (u: word) {struct u} : nat :=
  match u with
    | Eps => 0
    | u :: y => if eqV x y then S (nb_occ x u) else nb_occ x u
  end.

Notation "| u | x" := (nb_occ x u) (at level 40).

Lemma nb_occ_snoc :
  forall u x y, |u::x|y = (|u|y) + (if eqV x y then 1 else 0).
destruct x; destruct y; splitsolve0 0.
Qed.

Lemma nb_occ_snoc_ab : forall u, |u :: a|b = |u|b.
splitsolve0 0.
Qed.

Lemma nb_occ_snoc_ba : forall u, |u :: b|a = |u|a.
splitsolve0 0.
Qed.

Hint Rewrite nb_occ_snoc nb_occ_snoc_ba nb_occ_snoc_ab : rew_db.

Lemma nb_occ_app : forall u v x, |u @ v|x = (|u|x) + (|v|x).
intros; elim v; clear v.
  splitsolve0 0.
  splitsolve0 0.
Qed.

Hint Rewrite nb_occ_app : rew_db.

(* ad-hoc lemma for exo-induc *)
Lemma lg_S : forall u x v, |u::x@v|x = S(|u@v|x).
splitsolve0 0.
Qed.

Lemma lg_eq : forall u x y,  y<>x -> forall v, |u :: x @ v|y = (|u @ v|y).
destruct x ; destruct y; splitsolve0 0.
Qed.