Library prosa.util.bigcat

Require Export mathcomp.zify.zify.
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.list.

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

Section BigCatNatLemmas.

Consider any type T supporting equality comparisons...

Variable T : eqType.

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

Variable f : nat → seq T.

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.

We also restate lemma mem_bigcat_nat in terms of ordinals.

  Lemma mem_bigcat_ord :
    ∀ (x : T) (n : nat) (j : 'I_n) (f : 'I_n → seq T),
      j < n →
      x \in (f j ) →
      x \in \cat_(i < n ) (f i ).

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 BigCatNatDistinctElements.

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 )).

  End BigCatNatDistinctElements.

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 bigcat_nat_filter_eq_filter_bigcat_nat :
    ∀ {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 BigCatNatLemmas.

In this section, we introduce a few lemmas about the concatenation operation performed over arbitrary sequences.

Section BigCatLemmas.

Consider any two types X and Y supporting equality comparisons...

Variable X Y : eqType.

...and a function f that, given an index X, yields a sequence of Y.

Variable f : X → seq Y.

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 :
    ∀ x y s,
      x \in s →
      y \in f x →
      y \in \cat_(x <- s ) f x.

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

  Lemma mem_bigcat_exists :
    ∀ {P} s y,
      y \in \cat_(x <- s | P x ) f x →
      ∃ x , x \in s ∧ y \in f x.

Next, we show that a map and filter operation can be done either before or after a concatenation, leading to the same result.

  Lemma bigcat_filter_eq_filter_bigcat :
    ∀ xss P,
      [seq x <- \cat_(xs <- xss ) f xs | P x ]
      = \cat_(xs <- xss ) [seq x <- f xs | P x ].

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.

Consider a list xs, ...

Context {xs : seq X}.

... a filter predicate P, ...

Context {P : pred X}.

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

Hypothesis H_uniq_f : ∀ x, P x → uniq (f x).

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

    Hypothesis H_no_elements_in_common :
      ∀ x y z,
        x \in f y → x \in f z → y = z.

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

    Lemma bigcat_uniq :
        uniq xs →
        uniq (\cat_(x <- xs | P x ) (f x )).

  End BigCatDistinctElements.

In this section, we show some properties of the concatenation of sequences in combination with a function g that cancels f.

Section BigCatWithCancelFunctions.

Consider a function g...

Variable g : Y → X.

... and assume that g can cancel f starting from an element of the sequence f x.

Hypothesis H_g_cancels_f : ∀ x y, y \in f x → g y = x.

First, we show that no element of a sequence f x1 can be fed into g and obtain an element x2 which differs from x1. Hence, filtering by this condition always leads to the empty sequence.

    Lemma seq_different_elements_nil :
      ∀ x1 x2,
        x1 != x2 →
        [seq x <- f x1 | g x == x2 ] = [::].

Finally, assume we are given an element y which is contained in a duplicate-free sequence xs. Then, f is applied to each element of xs, but only the elements for which g yields y are kept. In this scenario, concatenating the resulting sequences will always lead to f y.

    Lemma bigcat_seq_uniqK :
      ∀ y xs,
        y \in xs →
        uniq xs →
        \cat_(x <- xs ) [seq x' <- f x | g x' == y ] = f y.
  End BigCatWithCancelFunctions.

End BigCatLemmas.

In the following section we introduce a lemma that relates to partitioning.

Section BigCatPartitionLemma.

Consider an item type X and partition type Y both supporting equality comparisons.

Variable X Y : eqType.

Consider a sequence of items of type X ...

Variable xs : seq X.

... and a sequence of partitions.

Variable ys : seq Y.

Consider a predicate P on X.

Variable P : pred X.

Define a mapping from items to partitions.

Variable x_to_y : X → Y.

We assume that any item in xs has its corresponding partition in the sequence of partitions ys.

Hypothesis H_no_partition_missing : ∀ x, x \in xs → P x → x_to_y x \in ys.

Consider a partition of xs.

Let partitioned_seq (y : Y) := [seq x <- xs | P x && (x_to_y x == y )].

We prove that any element in xs is also contained in the union of the partitions.

  Lemma bigcat_partitions :
    ∀ j,
      (j \in [seq x <- xs | P x ])
      = (j \in \cat_(y <- ys ) partitioned_seq y ).
End BigCatPartitionLemma.