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

Require Import Words.
Require Import BalancedWords.
Require Import GenericTactics. 

Definition other x := match x with  a => b | b => a end.

Lemma other_other : forall x, other (other x) = x. 
destruct x; simpl; reflexivity.
Qed.

Lemma eq_or_other : forall x y, {x=y}+{x= other y}. 
destruct x; destruct y; simpl; (left; reflexivity) || (right; reflexivity).
    (* auto is ok, but the extracted algo is poor! *)
Qed.

Lemma nb_occ_eq : forall u x, |u :: x|x = S (|u|x).
intros u x; simpl. destruct x; reflexivity.
Qed.

Lemma nb_occ_other : forall u x, |u :: x|other x = |u|other x.
destruct x; simpl; reflexivity.
Qed.

Lemma B0_other : forall u v w x, B0 (u @ v @ w) -> B0 (u :: x @ v :: other x @ w).
intros u v w x; destruct x; simpl; intro; constructor; assumption. 
Qed.

Lemma B1_other : forall u v x, B1 (u @ v) -> B1 (u :: x @ v :: other x).
intros u v x; destruct x; simpl; intro; constructor; assumption. 
Qed.

Lemma B2_other : forall u v x, B2 u -> B2 v -> B2 (u :: other x @ v :: x).
intros u v x; destruct x; simpl; intro; constructor; assumption. 
Qed.

(* *)

Hint Rewrite other_other nb_occ_eq nb_occ_other : rew_db.

Ltac noniB2o t g := (apply B2_other; t g) || noni0 t g.
Ltac splitsolveB2o n := splitsolve progress0 split0 noniB2o n 0.