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

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.

Consider any type T supporting equality comparisons...

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

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.

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.

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

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

End BigCatNatElements.

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

End BigCatNatElements.

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.

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

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

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

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 : nat) (f : 'I_n → seq T),

uniq (\cat_(i < n) (f i)) →

(∀ x i1 i2,

x \in (f i1) → x \in (f i2) → i1 = i2).

End BigCatNatDistinctElements.

∀ (n : nat) (f : 'I_n → seq T),

uniq (\cat_(i < n) (f i)) →

(∀ x i1 i2,

x \in (f i1) → x \in (f i2) → i1 = i2).

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

∀ {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.

∀ {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.

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.

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

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

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

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

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

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

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

Consider a function g...

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.

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.

∀ y xs,

y \in xs →

uniq xs →

\cat_(x <- xs) [seq x' <- f x | g x' == y] = f y.

End BigCatWithCancelFunctions.

End BigCatLemmas.

In this section, we show that the number of elements of the result
of a nested mapping and concatenation operation is independent from
the order in which the concatenations are performed.

Consider any three types supporting equality comparisons...

... a function F that, given two indices, yields a sequence...

and a predicate P.

Assume that, given two sequences xs and ys, their elements are fed to
F in a pair-wise fashion. The resulting lists are then concatenated.
The following lemma shows that, when the operation described above is performed,
the number of elements respecting P in the resulting list is the same, regardless
of the order in which xs and ys are combined.