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 bigcat_nat_uniq :
    ∀ (T: eqType) n1 n2 (F: nat → list T),
      (∀ i, uniq (F i)) →
      (∀ x i1 i2,
         x \in (F i1 ) → x \in (F i2 ) → i1 = i2 ) →
      uniq (\cat_(n1 ≤ i < n2 ) (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.