Library prosa.util.bigcat
Require Export prosa.util.tactics prosa.util.notation.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
In this section, we introduce useful lemmas about the concatenation operation performed
over an arbitrary range of sequences.
Consider any type supporting equality comparisons...
...and a function 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.
Lemma mem_bigcat_nat_exists :
∀ x m n,
x \in \cat_(m ≤ i < n) (f i) →
∃ i,
x \in f i ∧ m ≤ i < n.
End BigCatElements.
∀ x m n,
x \in \cat_(m ≤ i < n) (f i) →
∃ i,
x \in f i ∧ m ≤ i < n.
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.
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.