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

(* vocabulaire *)
Require Import MoreZArith.
Require Import Words.
Require Import WordsContinuity.
Require Import BalancedWords.
Require Import GenericTactics.

Open Local Scope Z_scope.

Definition balance u := Z_of_nat (|u|a) - Z_of_nat (|u|b).

Definition balanced u := balance u = 0.

Ltac progress2 g :=
     everywhere ltac:(fun g => (progress (unfold balance;unfold balanced))) g
  || progress1 g.
Ltac splitsolve2 n := splitsolve progress2 split0 noni0 n 0.

Lemma continuous_balance : continuous balance.
intros u x.
destruct x; splitsolve2 2%nat. (* 0%nat non longer enough since omega does not handle the constructive version of the disjunction... *)
Qed.

Lemma continuous_opp_balance : continuous (fun v => - balance v).
intros u x.
unfold balance.
destruct x; splitsolve2 2%nat. (* same pb *)
Qed.

(* JF -> Judicael : rendre exists informatif *)
Lemma unbalanced_insert_a :
  forall u, balance u = 1 ->
    { v : word & { w : word | balanced v /\ balanced w /\ u = v@[a]@w }}.
intros.
assert (Hstep : step_up balance 0 u).
  generalize continuous_balance (int_val balance 0).
  splitsolve2 1%nat...
  inversion Hstep as [ u0 x v0 H2 H3 H4 ].
  destruct x.
  exists u0. exists v0. splitsolve2 0%nat...
splitsolve2 0%nat.
Qed.

Lemma unbalanced_insert_b :
  forall u, - balance u = 1 ->
    { v : word & { w : word | balanced v /\ balanced w /\ u = v@[b]@w }}.
intros.
assert (Hstep : step_up (fun v => - balance v) 0 u).
  generalize continuous_opp_balance (int_val (fun v => - balance v)).
  splitsolve2 1%nat...
  inversion Hstep as [ u0 x v0 H2 H3 H4 ].
  induction x.
  splitsolve2 0%nat...
exists u0. exists v0. splitsolve2 0%nat...
Qed.


Theorem B1_compl : forall u, |u|a = |u|b -> B1 u.
(** The proof proceeds by induction over the length of $u$: *)
intro u; pattern u; apply length_rect; clear u.
intros u HypInd Hbal_u.
(** We do a case analysis over $u$: *) 
destruct u as  [ | v x ].
  (** -
  The case [u = Eps] is trivial: *)
  splitsolve2 1%nat...
  (** -
  Otherwise, [u = v :: x]. Then we have: *)
  assert ({ - balance v = 1 }+{ balance v = 1 }).
    (** --
    which can be proved by a simple case analysis over [x]:*)
    destruct x; splitsolve2 1%nat... (* 1%nat instead of 0%nat because of limitation of omega *)
    (** --
    Using the previous results on unbalanced words, we can conclude with
    a simple case analysis over [x]: *)
    generalize (unbalanced_insert_b v) (unbalanced_insert_a v).
    destruct x; splitsolve2 2%nat...
Qed.

Theorem B2_compl : forall u, |u|a = |u|b -> B2 u.
intro u; pattern u; apply length_rect; clear u.
intro u; destruct u as  [ | v x ].
  splitsolve2 1%nat...
  intros HypInd Hbal_u. assert ({- balance v = 1 }+{ balance v = 1 }).
    destruct x;  splitsolve2 1%nat... (*1%nat instead of 0%nat again *)
    generalize (unbalanced_insert_b v) (unbalanced_insert_a v).
    destruct x; splitsolve2 2%nat...
Qed.