Library rt.util.bigcat

Require Import rt.util.tactics rt.util.notation rt.util.bigord.

(* Lemmas about the big concatenation operator. *)
Section BigCatLemmas.

  Lemma mem_bigcat_nat:
     (T: eqType) x m n j (f: _ list T),
      m j < n
      x \in (f j)
      x \in \cat_(m i < n) (f i).

  Lemma mem_bigcat_nat_exists :
     (T: eqType) x m n (f: nat list T),
      x \in \cat_(m i < n) (f i)
       i, x \in (f i)
                m i < n.

  Lemma mem_bigcat_ord:
     (T: eqType) x n (j: 'I_n) (f: 'I_n list T),
      j < n
      x \in (f j)
      x \in \cat_(i < n) (f i).

  Lemma mem_bigcat_ord_exists :
     (T: eqType) x n (f: 'I_n list T),
      x \in \cat_(i < n) (f i)
       i, x \in (f i).
  Lemma bigcat_ord_uniq :
     (T: eqType) n (f: 'I_n list T),
      ( i, uniq (f i))
      ( x i1 i2,
         x \in (f i1) x \in (f i2) i1 = i2)
      uniq (\cat_(i < n) (f i)).

  Lemma map_bigcat_ord {T} {T'} n (f: 'I_n seq T) (g: T T') :
    map g (\cat_(i < n) (f i)) = \cat_(i < n) (map g (f i)).

  Lemma size_bigcat_ord {T} n (f: 'I_n seq T) :
    size (\cat_(i < n) (f i)) = \sum_(i < n) (size (f i)).

  Lemma size_bigcat_ord_max {T} n (f: 'I_n seq T) m :
    ( x, size (f x) m)
    size (\cat_(i < n) (f i)) m×n.

End BigCatLemmas.