diff --git a/util/bigcat.v b/util/bigcat.v
index 4de762e4b0c7a3a669ffbe67bf536176b0fef3d8..89551410426e9f5708667b7208589612f40ea776 100644
--- a/util/bigcat.v
+++ b/util/bigcat.v
@@ -1,66 +1,94 @@
Require Export prosa.util.tactics prosa.util.notation.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
-(* Lemmas about the big concatenation operator. *)
+(** In this section, we introduce useful lemmas about the concatenation operation performed
+ over an arbitrary range of sequences. *)
Section BigCatLemmas.
- Lemma mem_bigcat_nat:
- forall (T: eqType) x m n j (f: _ -> list T),
- m <= j < n ->
- x \in (f j) ->
- x \in \cat_(m <= i < n) (f i).
- Proof.
- intros T x m n j f LE IN; move: LE => /andP [LE LE0].
- rewrite -> big_cat_nat with (n := j); simpl; [| by ins | by apply ltnW].
- rewrite mem_cat; apply/orP; right.
- destruct n; first by rewrite ltn0 in LE0.
- rewrite big_nat_recl; last by ins.
- by rewrite mem_cat; apply/orP; left.
- Qed.
+ (** Consider any type supporting equality comparisons... *)
+ Variable T: eqType.
- Lemma mem_bigcat_nat_exists :
- forall (T: eqType) x m n (f: nat -> list T),
- x \in \cat_(m <= i < n) (f i) ->
- exists i, x \in (f i) /\
- m <= i < n.
- Proof.
- intros T x m n f IN.
- induction n; first by rewrite big_geq // in IN.
- destruct (leqP m n); last by rewrite big_geq ?in_nil // ltnW in IN.
- rewrite big_nat_recr // /= mem_cat in IN.
- move: IN => /orP [HEAD | TAIL].
- {
- apply IHn in HEAD; destruct HEAD; exists x0. move: H => [H /andP [H0 H1]].
- split; first by done.
- by apply/andP; split; [by done | by apply ltnW].
- }
- {
- exists n; split; first by done.
- apply/andP; split; [by done | by apply ltnSn].
- }
- Qed.
+ (** ...and a function that, given an index, yields a sequence. *)
+ Variable f: nat -> list T.
- Lemma bigcat_nat_uniq :
- forall (T: eqType) n1 n2 (F: nat -> list T),
- (forall i, uniq (F i)) ->
- (forall x i1 i2,
- x \in (F i1) -> x \in (F i2) -> i1 = i2) ->
- uniq (\cat_(n1 <= i < n2) (F i)).
- Proof.
- intros T n1 n2 f SINGLE UNIQ.
- case (leqP n1 n2) => [LE | GT]; last by rewrite big_geq // ltnW.
- rewrite -[n2](addKn n1).
- rewrite -addnBA //; set delta := n2 - n1.
- induction delta; first by rewrite addn0 big_geq.
- rewrite addnS big_nat_recr /=; last by apply leq_addr.
- rewrite cat_uniq; apply/andP; split; first by apply IHdelta.
- apply /andP; split; last by apply SINGLE.
- rewrite -all_predC; apply/allP; intros x INx.
- simpl; apply/negP; unfold not; intro BUG.
- apply mem_bigcat_nat_exists in BUG.
- move: BUG => [i [IN /andP [_ LTi]]].
- apply UNIQ with (i1 := i) in INx; last by done.
- by rewrite INx ltnn in LTi.
- Qed.
+ (** 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:
+ forall x m n j,
+ m <= j < n ->
+ x \in f j ->
+ x \in \cat_(m <= i < n) (f i).
+ Proof.
+ intros x m n j LE IN; move: LE => /andP [LE LE0].
+ rewrite -> big_cat_nat with (n := j); simpl; [| by ins | by apply ltnW].
+ rewrite mem_cat; apply/orP; right.
+ destruct n; first by rewrite ltn0 in LE0.
+ rewrite big_nat_recl; last by ins.
+ by rewrite mem_cat; apply/orP; left.
+ Qed.
+
+ (** Conversely, we prove that any element belonging to a concatenation of sequences
+ must come from one of the sequences. *)
+ Lemma mem_bigcat_nat_exists :
+ forall x m n,
+ x \in \cat_(m <= i < n) (f i) ->
+ exists i,
+ x \in f i /\ m <= i < n.
+ Proof.
+ intros x m n IN.
+ induction n; first by rewrite big_geq // in IN.
+ destruct (leqP m n); last by rewrite big_geq ?in_nil // ltnW in IN.
+ rewrite big_nat_recr // /= mem_cat in IN.
+ move: IN => /orP [HEAD | TAIL].
+ {
+ apply IHn in HEAD; destruct HEAD; exists x0. move: H => [H /andP [H0 H1]].
+ split; first by done.
+ by apply/andP; split; [by done | by apply ltnW]. }
+ {
+ exists n; split; first by done.
+ apply/andP; split; [by done | by apply ltnSn]. }
+ Qed.
+
+ 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: forall i, uniq (f i).
+
+ (** ...and that there are no elements in common between the sequences. *)
+ Hypothesis H_no_elements_in_common:
+ forall 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 :
+ forall n1 n2,
+ uniq (\cat_(n1 <= i < n2) (f i)).
+ Proof.
+ intros n1 n2.
+ case (leqP n1 n2) => [LE | GT]; last by rewrite big_geq // ltnW.
+ rewrite -[n2](addKn n1).
+ rewrite -addnBA //; set delta := n2 - n1.
+ induction delta; first by rewrite addn0 big_geq.
+ rewrite addnS big_nat_recr /=; last by apply leq_addr.
+ rewrite cat_uniq; apply/andP; split; first by apply IHdelta.
+ apply /andP; split; last by apply H_uniq_seq.
+ rewrite -all_predC; apply/allP; intros x INx.
+ simpl; apply/negP; unfold not; intro BUG.
+ apply mem_bigcat_nat_exists in BUG.
+ move: BUG => [i [IN /andP [_ LTi]]].
+ apply H_no_elements_in_common with (i1 := i) in INx; last by done.
+ by rewrite INx ltnn in LTi.
+ Qed.
+
+ End BigCatDistinctElements.
End BigCatLemmas.