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

Require Import Words.
Require Import BalancedWords.
Require Import Other. 
Require Import GenericTactics. 
Require Import MoreArith.

(* ------------------------------------------------------------------------------ *)

Fixpoint puiss (x:V) (n:nat) {struct n} : word :=
  match n with
    | O => Eps
    | S n => (puiss x n) :: x
  end.

Notation "x ^ n" := (puiss x n). 

Lemma append_puiss : forall u x n, u :: x @ x^n = u @ (x^(S n)).
intros u x n; elim n; clear n; simpl; congruence. (*  ou splitsolve0 0*)
Qed.

Hint Rewrite append_puiss : rew_db.

(* ------------------------------------------------------------------------------ *)

Lemma B1_completeness_aux : forall u n y, |u|other y = n + |u|y -> B1 (u @ y^n).
(** The proof is by induction on $u$. *)
induction u as [ |u IndHyp x]; intros n y. 
(** - The case where $u=\emp$ reduces to
  [0 = n -> B1 (Eps @ y^n) ] because [|Eps|y = 0 *) 
(** - The following tactic amounts to applying clause [B1_e].*)
  splitsolve0 1... (* by B1_e *)
  (** -
  In the inductive step, we consider the word [u :: x], which yields the goal:%\\%
  [|u :: x|other y = n + |u :: x|y -> B1 (u :: x @ y^n)].
  Let us compare [y] with [other x]. *)
  case (eq_or_other y x); intro e; rewrite e; clear e y; splitsolve0 0.
    (** --
    When [y=x], we get: 
    [|u|other x = n + S (|u|x)] $\:$ [|-] $\:$ [B1 (]$u\,x^{n+1}$[)], 
    hence we can use the induction hypothesis on $n+1$ and [x]:*)
    apply (IndHyp (S n) x); splitsolve0 0...      
    (** --
    When [y=other x], we get:
    [|u|x + 1 = n + |u|other x] $\:$ [|-] $\:$ [B1 (u :: x @ other x^n)]. 
    Then we decide to compare [n] with [0].  *)
    destruct n; simpl in * |- * . 
      (** ---
      When [n=0], the goal reduces to [B1 (u :: x)].
      Then we apply the induction hypothesis on 1 and the %\emph{opposite}% letter. *)
      apply (IndHyp 1 x); splitsolve0 0...
      (** ---
      When the previous [n] is a successor (the successor of the new [n] 
      provided by the tactic %\emph{destruct}%), 
      the new goal is [B1 (u :: x @ other x^n :: other x)].
      We can apply [B1_other] with the induction hypothesis on [n] and [other x]. *)
      apply B1_other. apply (IndHyp n (other x)); splitsolve0 0...
Qed.

(* Completeness of B1 *)
Theorem B1_completeness : forall u, |u|a = |u|b -> B1 u.
intros u e; apply (B1_completeness_aux u 0 b); simpl; auto.
Qed.

(* ------------------------------------------------------------------------------ *)

(* B2 *)


Lemma B2_app : forall u, B2 u -> forall v, B2 v -> B2 (u @ v).
intros u lu. induction 1 as [ | v w lv Hv lw Hw | ]; splitsolve0 1.
Qed.

Ltac noniB2a t g := (apply B2_app; t g) || noni0 t g.
Ltac splitsolveB2a n := splitsolve progress0 split0 noniB2a n 0.

Inductive split (P:word->Set) (x: V) : word -> Set :=
  | split_ex : forall u v, P u -> B2 v -> split P x (u :: x @ v).

Definition C (x:V) : nat -> word -> Set :=
  fix C (n:nat) : word -> Set :=
    match n with
      | O => B2
      | S n => split (C n) x
    end.

Lemma C_app : forall x u n, C x n u -> forall v, B2 v -> C x n (u @ v).
destruct n as [| n]; simpl.
  splitsolveB2a 1...
  intros (u1,u2,cu1,lu2,v,lv). rewrite <- append_assoc. exists; splitsolveB2a 1...
Qed.

Lemma C_other : forall x u v n, C (other x) n u -> B2 v -> C (other x) n (u :: other x @ v :: x).
intros; assert (C (other x) n (u @ ([other x] @ v :: x))). 
   apply C_app; [ assumption | splitsolveB2o 2]. 
   splitsolve0 0.
Qed.

Lemma B2_completeness_aux : forall u n y, |u|y = n + |u|other y -> C y n u.
induction u as [ |u IndHyp x]; intros n y. 
  (** -
  The case where $u=\emp$ reduces to [0 = n -> C y n Eps ] because [|Eps|y = 0 *)
  splitsolve0 1...
  (** -
  In the inductive step, we consider the word [u :: x], which yields the goal:%\\%
  [|u :: x|y = n + |u :: x|other y -> C y n (u :: x)].
  Let us compare [y] with [other x]. *)
  case (eq_or_other y x); intro e; rewrite e; clear e y; splitsolve0 0.
    (** --
    When [y=x], we get: 
    [S(|u|x) = n + |u|other x] $\:$ [|-] $\:$ [C x n (u :: x)].
    Then we decide to compare [n] with [0].  *)
    destruct n; simpl in * |- * . (* A FAIRE simplif par eq_add_S serait bien *)
      (** ---
      When [n=0], the goal reduces to [B2 (u :: x)].
      Then we apply the induction hypothesis with 1 and the %\emph{opposite}% letter. *)
      elim (IndHyp 1 (other x)); splitsolveB2o 1...
      (** --- 
      When the previous [n] is a successor (the successor of the new [n] provided 
      by the tactic %\emph{destruct}%), the new goal is [split (C x n) x (u :: x)].
      The witnesses are [u] and [Eps], using the induction hypothesis on [n] and [x]. *)
      generalize (IndHyp n x) B2_e; intros. refine (split_ex _ _ u Eps _ _); auto...
    (** --
    When [y=other x], we get:
    [|u|other x = n + (|u|x + 1) ]  $\:$ [|-] $\:$ [C (other x) n (u :: x)]. 
    By induction hypothesis on [n+1] and [other x],
    we get [w] and [v] such that [u= w :: x @ v)], [C (other x) n w] and [B2 v],
    so that we apply lemma [C_other]. *)
    elim (IndHyp (S n) (other x)); [intros w v cnw bv | splitsolve0 0].
    apply C_other; assumption...
Qed.

(* Completeness of B2 *)
Theorem B2_completeness : forall u, |u|a = |u|b -> B2 u.
intros u e; apply (B2_completeness_aux u O b); simpl; auto.
Qed.