Library prosa.util.bigcat

Require Export prosa.util.tactics prosa.util.notation.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Require Export prosa.util.tactics prosa.util.ssrlia.

In this section, we introduce useful lemmas about the concatenation operation performed over an arbitrary range of sequences.

Section BigCatLemmas.

Consider any type supporting equality comparisons...

Variable T: eqType.

...and a function that, given an index, yields a sequence.

Variable f: nat → list T.

In this section, we prove that the concatenation over sequences works as expected: no element is lost during the concatenation, and no new element is introduced.

Section BigCatElements.

First, we show that the concatenation comprises all the elements of each sequence; i.e. any element contained in one of the sequences will also be an element of the result of the concatenation.

    Lemma mem_bigcat_nat:
      ∀ x m n j,
        m ≤ j < n →
        x \in f j →
        x \in \cat_(m ≤ i < n ) (f i ).

Conversely, we prove that any element belonging to a concatenation of sequences must come from one of the sequences.

    Lemma mem_bigcat_nat_exists:
      ∀ x m n,
        x \in \cat_(m ≤ i < n ) (f i ) →
        ∃ i,
          x \in f i ∧ m ≤ i < n.
    Lemma mem_bigcat_ord:
      ∀ x n (j: 'I_n) (f: 'I_n → list T),
        j < n →
        x \in (f j ) →
        x \in \cat_(i < n ) (f i ).

  End BigCatElements.

In this section, we show how we can preserve uniqueness of the elements (i.e. the absence of a duplicate) over a concatenation of sequences.

Section BigCatDistinctElements.

Assume that there are no duplicates in each of the possible sequences to concatenate...

Hypothesis H_uniq_seq: ∀ i, uniq (f i).

...and that there are no elements in common between the sequences.

Hypothesis H_no_elements_in_common:
∀ x i1 i2, x \in f i1 → x \in f i2 → i1 = i2.

We prove that the concatenation will yield a sequence with unique elements.

    Lemma bigcat_nat_uniq:
      ∀ n1 n2,
        uniq (\cat_(n1 ≤ i < n2 ) (f i )).

Conversely, if the concatenation of the sequences has no duplicates, any element can only belong to a single sequence.

    Lemma bigcat_ord_uniq_reverse :
      ∀ n (f: 'I_n → list T),
        uniq (\cat_(i < n ) (f i )) →
        (∀ x i1 i2,
           x \in (f i1 ) → x \in (f i2 ) → i1 = i2 ).

  End BigCatDistinctElements.

We show that filtering a concatenated sequence by any predicate P is the same as concatenating the elements of the sequence that satisfy P.

  Lemma cat_filter_eq_filter_cat:
    ∀ {X : Type} (F : nat → seq X) (P : X → bool) (t1 t2 : nat),
      [seq x <- \cat_(t1 ≤t<t2 ) F t | P x ] = \cat_(t1 ≤t<t2 )[seq x <- F t | P x ].

We show that the size of a concatenated sequence is the same as summation of sizes of each element of the sequence.

  Lemma size_big_nat:
    ∀ {X : Type} (F : nat → seq X) (t1 t2 : nat),
      \sum_(t1 ≤ t < t2 ) size (F t) =
      size (\cat_(t1 ≤ t < t2 ) F t).

End BigCatLemmas.