coq lemmas (regexp)

Definition substring {T} (s s' : list T) := exists a b, s = a ++ s' ++ b.

Fixpoint StringTake {T} (l : list T) n :=
  match n with
  | 0 => []
  | S n' => match l with
            | [] => []
            | x :: l' => x :: StringTake l' n'
            end
  end.

Fixpoint StringDrop {T} (l : list T) n :=
  match n with
  | 0 => l
  | S n' => match l with
            | [] => []
            | x :: l' => StringDrop l' n'
            end
  end.

Definition StringRTake {T} (l : list T) n := StringDrop l (length l - n).
Definition StringRDrop {T} (l : list T) n := StringTake l (length l - n).
Definition ConstString {T} (x : T) n := napp n [x].
Definition BinStr a b := ConstString 0 a ++ ConstString 1 b.

Lemma ConstStr_length : forall T (x : T) n, length (ConstStr x n) = n.
Lemma BinStr_length : forall n m, length (BinStr n m) = n + m.
Lemma StringTake_Const : forall T (a : T) n m, m <= n ->
  StringTake (ConstStr a n) m = ConstStr a m.
Lemma StringDrop_Const : forall T (x : T) m n,
  StringDrop (ConstStr x m) n = ConstStr x (m - n).
Lemma StringTake_0 : forall T (l : list T), StringTake l 0 = [].
Lemma StringDrop_0 : forall T (l : list T), StringDrop l 0 = l.
Lemma StringTake_length : forall T (l : list T), StringTake l (length l) = l.
Lemma StringDrop_length : forall T (l : list T), StringDrop l (length l) = [].
Lemma StringTake_length_le : forall T (l : list T) n,
  length l <= n -> StringTake l n = l.
Lemma StringDrop_length_le : forall T (l : list T) n,
  length l <= n -> StringDrop l n = [].
Lemma StringTakeLength : forall T (l : list T) n,
  n <= length l -> length (StringTake l n) = n.
Lemma StringDropLength : forall T (l : list T) n,
  length (StringDrop l n) = length l - n.
Lemma StringTake_nil : forall T n, StringTake (@nil T) n = [].
Lemma StringDrop_nil : forall T n, StringDrop (@nil T) n = [].
Lemma StringTake_app_length : forall T (a b : list T),
  StringTake (a ++ b) (length a) = a.
Lemma StringDrop_app_length : forall T (a b : list T),
  StringDrop (a ++ b) (length a) = b.
Lemma StringRTake_0 : forall T (l : list T), StringRTake l 0 = [].
Lemma StringDecomposition : forall T (l : list T) n,
  l = StringTake l n ++ StringDrop l n.
Lemma StringDrop_sum : forall T (l : list T) a b,
  StringDrop (StringDrop l a) b = StringDrop l (a + b).
Lemma Substring' : forall T (a b : list T),
  substring a b -> exists m n, b = StringTake (StringDrop a m) n.
Lemma Substring'' : forall T (a b : list T),
  (exists m n, b = StringTake (StringDrop a m) n) -> substring a b.
Lemma StringDrop_app_length_le : forall T (a b : list T) n,
  length a <= n -> StringDrop (a ++ b) n = StringDrop b (n - length a).
Lemma StringDrop_app_length_ge : forall T (a b : list T) n,
  n <= length a -> StringDrop (a ++ b) n = StringDrop a n ++ b.
Lemma length0 : forall T (a : list T), length a = 0 -> a = [].
Lemma app_injective_r : forall T (a b c : list T), a ++ b = a ++ c -> b = c.
Lemma app_injective_l : forall T (a b c : list T), a ++ c = b ++ c -> a = b.
Lemma StringTake_app_length_le : forall T (a b : list T) n,
  length a <= n -> StringTake (a ++ b) n = a ++ StringTake b (n - length a).
Lemma StringTake_app_length_ge : forall T (a b : list T) n,
  n <= length a -> StringTake (a ++ b) n = StringTake a n.
Lemma Substring_app : forall T (a b s : list T),
  substring (a ++ b) s -> substring a s \/ substring b s \/ exists m n,
    m <= length a /\ n <= length b /\ s = StringRTake a m ++ StringTake b n.
Lemma Substring_Const : forall T (x : T) n s, substring (ConstStr x n) s ->
  exists n', n' <= n /\ s = ConstStr x n'.
Lemma Substring_BinStr : forall m n s, substring (BinStr m n) s ->
  exists m' n', s = BinStr m' n'.
Lemma StringTake_BinStr : forall m n m',
  m' <= m -> StringTake (BinStr m n) m' = ConstStr 0 m'.
Lemma StringDrop_BinStr : forall m n m',
  m <= m' -> StringDrop (BinStr m n) m' = ConstStr 1 (m + n - m').
Lemma BinStr_n_0 : forall n, BinStr n 0 = ConstStr 0 n.
Lemma BinStr_0_n : forall n, BinStr 0 n = ConstStr 1 n.
Lemma ConstStr_app : forall T a b (x : T),
  ConstStr x a ++ ConstStr x b = ConstStr x (a + b).
Lemma ConstStr_decomposition : forall T (x : T) n a b, ConstStr x n = a ++ b ->
  exists m' n', a = ConstStr x m' /\ b = ConstStr x n'.
Lemma ConstStr_count : forall x n, count (ConstStr x n) x = n.
Lemma ConstStr_count' : forall x y n, x <> y -> count (ConstStr x n) y = 0.
Lemma count_app : forall l1 l2 n, count (l1 ++ l2) n = count l1 n + count l2 n.
Lemma BinStr_count_l : forall m n, count (BinStr m n) 0 = m.
Lemma BinStr_count_r : forall m n, count (BinStr m n) 1 = n.
Theorem RegExp_BinStr : ~ exists re,
  (forall s, s =~ re <-> exists n, s = BinStr n n).