Library prosa.util.bigcat
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.11.2 (June 2020)
----------------------------------------------------------------------------- *)
Require Export prosa.util.tactics prosa.util.notation.
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.
Lemma mem_bigcat_nat:
∀ x m n j,
m ≤ j < n →
x \in f j →
x \in \cat_(m ≤ i < n) (f i).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 37)
T : eqType
f : nat -> seq T
============================
forall (x : T) (m n j : nat),
m <= j < n -> x \in f j -> x \in \big[cat/[::]]_(m <= i < n) f i
----------------------------------------------------------------------------- *)
Proof.
intros x m n j LE IN; move: LE ⇒ /andP [LE LE0].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 85)
T : eqType
f : nat -> seq T
x : T
m, n, j : nat
IN : x \in f j
LE : m <= j
LE0 : j < n
============================
x \in \big[cat/[::]]_(m <= i < n) f i
----------------------------------------------------------------------------- *)
rewrite → big_cat_nat with (n := j); simpl; [| by ins | by apply ltnW].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 90)
T : eqType
f : nat -> seq T
x : T
m, n, j : nat
IN : x \in f j
LE : m <= j
LE0 : j < n
============================
x \in \big[cat/[::]]_(m <= i < j) f i ++ \big[cat/[::]]_(j <= i < n) f i
----------------------------------------------------------------------------- *)
rewrite mem_cat; apply/orP; right.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 129)
T : eqType
f : nat -> seq T
x : T
m, n, j : nat
IN : x \in f j
LE : m <= j
LE0 : j < n
============================
x \in \big[cat/[::]]_(j <= i < n) f i
----------------------------------------------------------------------------- *)
destruct n; first by rewrite ltn0 in LE0.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 141)
T : eqType
f : nat -> seq T
x : T
m, n, j : nat
IN : x \in f j
LE : m <= j
LE0 : j < n.+1
============================
x \in \big[cat/[::]]_(j <= i < n.+1) f i
----------------------------------------------------------------------------- *)
rewrite big_nat_recl; last by ins.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 190)
T : eqType
f : nat -> seq T
x : T
m, n, j : nat
IN : x \in f j
LE : m <= j
LE0 : j < n.+1
============================
x \in f j ++ \big[cat/[::]]_(j <= i < n) f i.+1
----------------------------------------------------------------------------- *)
by rewrite mem_cat; apply/orP; left.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
∀ x m n j,
m ≤ j < n →
x \in f j →
x \in \cat_(m ≤ i < n) (f i).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 37)
T : eqType
f : nat -> seq T
============================
forall (x : T) (m n j : nat),
m <= j < n -> x \in f j -> x \in \big[cat/[::]]_(m <= i < n) f i
----------------------------------------------------------------------------- *)
Proof.
intros x m n j LE IN; move: LE ⇒ /andP [LE LE0].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 85)
T : eqType
f : nat -> seq T
x : T
m, n, j : nat
IN : x \in f j
LE : m <= j
LE0 : j < n
============================
x \in \big[cat/[::]]_(m <= i < n) f i
----------------------------------------------------------------------------- *)
rewrite → big_cat_nat with (n := j); simpl; [| by ins | by apply ltnW].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 90)
T : eqType
f : nat -> seq T
x : T
m, n, j : nat
IN : x \in f j
LE : m <= j
LE0 : j < n
============================
x \in \big[cat/[::]]_(m <= i < j) f i ++ \big[cat/[::]]_(j <= i < n) f i
----------------------------------------------------------------------------- *)
rewrite mem_cat; apply/orP; right.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 129)
T : eqType
f : nat -> seq T
x : T
m, n, j : nat
IN : x \in f j
LE : m <= j
LE0 : j < n
============================
x \in \big[cat/[::]]_(j <= i < n) f i
----------------------------------------------------------------------------- *)
destruct n; first by rewrite ltn0 in LE0.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 141)
T : eqType
f : nat -> seq T
x : T
m, n, j : nat
IN : x \in f j
LE : m <= j
LE0 : j < n.+1
============================
x \in \big[cat/[::]]_(j <= i < n.+1) f i
----------------------------------------------------------------------------- *)
rewrite big_nat_recl; last by ins.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 190)
T : eqType
f : nat -> seq T
x : T
m, n, j : nat
IN : x \in f j
LE : m <= j
LE0 : j < n.+1
============================
x \in f j ++ \big[cat/[::]]_(j <= i < n) f i.+1
----------------------------------------------------------------------------- *)
by rewrite mem_cat; apply/orP; left.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
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 :
∀ x m n,
x \in \cat_(m ≤ i < n) (f i) →
∃ i,
x \in f i ∧ m ≤ i < n.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 58)
T : eqType
f : nat -> seq T
============================
forall (x : T) (m n : nat),
x \in \big[cat/[::]]_(m <= i < n) f i ->
exists i : nat, x \in f i /\ m <= i < n
----------------------------------------------------------------------------- *)
Proof.
intros x m n IN.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 62)
T : eqType
f : nat -> seq T
x : T
m, n : nat
IN : x \in \big[cat/[::]]_(m <= i < n) f i
============================
exists i : nat, x \in f i /\ m <= i < n
----------------------------------------------------------------------------- *)
induction n; first by rewrite big_geq // in IN.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 75)
T : eqType
f : nat -> seq T
x : T
m, n : nat
IN : x \in \big[cat/[::]]_(m <= i < n.+1) f i
IHn : x \in \big[cat/[::]]_(m <= i < n) f i ->
exists i : nat, x \in f i /\ m <= i < n
============================
exists i : nat, x \in f i /\ m <= i < n.+1
----------------------------------------------------------------------------- *)
destruct (leqP m n); last by rewrite big_geq ?in_nil // ltnW in IN.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 142)
T : eqType
f : nat -> seq T
x : T
m, n : nat
IN : x \in \big[cat/[::]]_(m <= i < n.+1) f i
IHn : x \in \big[cat/[::]]_(m <= i < n) f i ->
exists i : nat, x \in f i /\ m <= i < n
i : m <= n
============================
exists i0 : nat, x \in f i0 /\ m <= i0 < n.+1
----------------------------------------------------------------------------- *)
rewrite big_nat_recr // /= mem_cat in IN.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 257)
T : eqType
f : nat -> seq T
x : T
m, n : nat
IHn : x \in \big[cat/[::]]_(m <= i < n) f i ->
exists i : nat, x \in f i /\ m <= i < n
i : m <= n
IN : (x \in \big[cat/[::]]_(m <= i < n) f i) || (x \in f n)
============================
exists i0 : nat, x \in f i0 /\ m <= i0 < n.+1
----------------------------------------------------------------------------- *)
move: IN ⇒ /orP [HEAD | TAIL].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 302)
T : eqType
f : nat -> seq T
x : T
m, n : nat
IHn : x \in \big[cat/[::]]_(m <= i < n) f i ->
exists i : nat, x \in f i /\ m <= i < n
i : m <= n
HEAD : x \in \big[cat/[::]]_(m <= i < n) f i
============================
exists i0 : nat, x \in f i0 /\ m <= i0 < n.+1
subgoal 2 (ID 303) is:
exists i0 : nat, x \in f i0 /\ m <= i0 < n.+1
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 302)
T : eqType
f : nat -> seq T
x : T
m, n : nat
IHn : x \in \big[cat/[::]]_(m <= i < n) f i ->
exists i : nat, x \in f i /\ m <= i < n
i : m <= n
HEAD : x \in \big[cat/[::]]_(m <= i < n) f i
============================
exists i0 : nat, x \in f i0 /\ m <= i0 < n.+1
----------------------------------------------------------------------------- *)
apply IHn in HEAD; destruct HEAD; ∃ x0.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 312)
T : eqType
f : nat -> seq T
x : T
m, n : nat
IHn : x \in \big[cat/[::]]_(m <= i < n) f i ->
exists i : nat, x \in f i /\ m <= i < n
i : m <= n
x0 : nat
H : x \in f x0 /\ m <= x0 < n
============================
x \in f x0 /\ m <= x0 < n.+1
----------------------------------------------------------------------------- *)
move: H ⇒ [H /andP [H0 H1]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 364)
T : eqType
f : nat -> seq T
x : T
m, n : nat
IHn : x \in \big[cat/[::]]_(m <= i < n) f i ->
exists i : nat, x \in f i /\ m <= i < n
i : m <= n
x0 : nat
H : x \in f x0
H0 : m <= x0
H1 : x0 < n
============================
x \in f x0 /\ m <= x0 < n.+1
----------------------------------------------------------------------------- *)
split; first by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 367)
T : eqType
f : nat -> seq T
x : T
m, n : nat
IHn : x \in \big[cat/[::]]_(m <= i < n) f i ->
exists i : nat, x \in f i /\ m <= i < n
i : m <= n
x0 : nat
H : x \in f x0
H0 : m <= x0
H1 : x0 < n
============================
m <= x0 < n.+1
----------------------------------------------------------------------------- *)
by apply/andP; split; [by done | by apply ltnW].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 303)
subgoal 1 (ID 303) is:
exists i0 : nat, x \in f i0 /\ m <= i0 < n.+1
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 303)
T : eqType
f : nat -> seq T
x : T
m, n : nat
IHn : x \in \big[cat/[::]]_(m <= i < n) f i ->
exists i : nat, x \in f i /\ m <= i < n
i : m <= n
TAIL : x \in f n
============================
exists i0 : nat, x \in f i0 /\ m <= i0 < n.+1
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 303)
T : eqType
f : nat -> seq T
x : T
m, n : nat
IHn : x \in \big[cat/[::]]_(m <= i < n) f i ->
exists i : nat, x \in f i /\ m <= i < n
i : m <= n
TAIL : x \in f n
============================
exists i0 : nat, x \in f i0 /\ m <= i0 < n.+1
----------------------------------------------------------------------------- *)
∃ n; split; first by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 400)
T : eqType
f : nat -> seq T
x : T
m, n : nat
IHn : x \in \big[cat/[::]]_(m <= i < n) f i ->
exists i : nat, x \in f i /\ m <= i < n
i : m <= n
TAIL : x \in f n
============================
m <= n < n.+1
----------------------------------------------------------------------------- *)
apply/andP; split; [by done | by apply ltnSn].
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End BigCatElements.
∀ x m n,
x \in \cat_(m ≤ i < n) (f i) →
∃ i,
x \in f i ∧ m ≤ i < n.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 58)
T : eqType
f : nat -> seq T
============================
forall (x : T) (m n : nat),
x \in \big[cat/[::]]_(m <= i < n) f i ->
exists i : nat, x \in f i /\ m <= i < n
----------------------------------------------------------------------------- *)
Proof.
intros x m n IN.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 62)
T : eqType
f : nat -> seq T
x : T
m, n : nat
IN : x \in \big[cat/[::]]_(m <= i < n) f i
============================
exists i : nat, x \in f i /\ m <= i < n
----------------------------------------------------------------------------- *)
induction n; first by rewrite big_geq // in IN.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 75)
T : eqType
f : nat -> seq T
x : T
m, n : nat
IN : x \in \big[cat/[::]]_(m <= i < n.+1) f i
IHn : x \in \big[cat/[::]]_(m <= i < n) f i ->
exists i : nat, x \in f i /\ m <= i < n
============================
exists i : nat, x \in f i /\ m <= i < n.+1
----------------------------------------------------------------------------- *)
destruct (leqP m n); last by rewrite big_geq ?in_nil // ltnW in IN.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 142)
T : eqType
f : nat -> seq T
x : T
m, n : nat
IN : x \in \big[cat/[::]]_(m <= i < n.+1) f i
IHn : x \in \big[cat/[::]]_(m <= i < n) f i ->
exists i : nat, x \in f i /\ m <= i < n
i : m <= n
============================
exists i0 : nat, x \in f i0 /\ m <= i0 < n.+1
----------------------------------------------------------------------------- *)
rewrite big_nat_recr // /= mem_cat in IN.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 257)
T : eqType
f : nat -> seq T
x : T
m, n : nat
IHn : x \in \big[cat/[::]]_(m <= i < n) f i ->
exists i : nat, x \in f i /\ m <= i < n
i : m <= n
IN : (x \in \big[cat/[::]]_(m <= i < n) f i) || (x \in f n)
============================
exists i0 : nat, x \in f i0 /\ m <= i0 < n.+1
----------------------------------------------------------------------------- *)
move: IN ⇒ /orP [HEAD | TAIL].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 302)
T : eqType
f : nat -> seq T
x : T
m, n : nat
IHn : x \in \big[cat/[::]]_(m <= i < n) f i ->
exists i : nat, x \in f i /\ m <= i < n
i : m <= n
HEAD : x \in \big[cat/[::]]_(m <= i < n) f i
============================
exists i0 : nat, x \in f i0 /\ m <= i0 < n.+1
subgoal 2 (ID 303) is:
exists i0 : nat, x \in f i0 /\ m <= i0 < n.+1
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 302)
T : eqType
f : nat -> seq T
x : T
m, n : nat
IHn : x \in \big[cat/[::]]_(m <= i < n) f i ->
exists i : nat, x \in f i /\ m <= i < n
i : m <= n
HEAD : x \in \big[cat/[::]]_(m <= i < n) f i
============================
exists i0 : nat, x \in f i0 /\ m <= i0 < n.+1
----------------------------------------------------------------------------- *)
apply IHn in HEAD; destruct HEAD; ∃ x0.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 312)
T : eqType
f : nat -> seq T
x : T
m, n : nat
IHn : x \in \big[cat/[::]]_(m <= i < n) f i ->
exists i : nat, x \in f i /\ m <= i < n
i : m <= n
x0 : nat
H : x \in f x0 /\ m <= x0 < n
============================
x \in f x0 /\ m <= x0 < n.+1
----------------------------------------------------------------------------- *)
move: H ⇒ [H /andP [H0 H1]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 364)
T : eqType
f : nat -> seq T
x : T
m, n : nat
IHn : x \in \big[cat/[::]]_(m <= i < n) f i ->
exists i : nat, x \in f i /\ m <= i < n
i : m <= n
x0 : nat
H : x \in f x0
H0 : m <= x0
H1 : x0 < n
============================
x \in f x0 /\ m <= x0 < n.+1
----------------------------------------------------------------------------- *)
split; first by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 367)
T : eqType
f : nat -> seq T
x : T
m, n : nat
IHn : x \in \big[cat/[::]]_(m <= i < n) f i ->
exists i : nat, x \in f i /\ m <= i < n
i : m <= n
x0 : nat
H : x \in f x0
H0 : m <= x0
H1 : x0 < n
============================
m <= x0 < n.+1
----------------------------------------------------------------------------- *)
by apply/andP; split; [by done | by apply ltnW].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 303)
subgoal 1 (ID 303) is:
exists i0 : nat, x \in f i0 /\ m <= i0 < n.+1
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 303)
T : eqType
f : nat -> seq T
x : T
m, n : nat
IHn : x \in \big[cat/[::]]_(m <= i < n) f i ->
exists i : nat, x \in f i /\ m <= i < n
i : m <= n
TAIL : x \in f n
============================
exists i0 : nat, x \in f i0 /\ m <= i0 < n.+1
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 303)
T : eqType
f : nat -> seq T
x : T
m, n : nat
IHn : x \in \big[cat/[::]]_(m <= i < n) f i ->
exists i : nat, x \in f i /\ m <= i < n
i : m <= n
TAIL : x \in f n
============================
exists i0 : nat, x \in f i0 /\ m <= i0 < n.+1
----------------------------------------------------------------------------- *)
∃ n; split; first by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 400)
T : eqType
f : nat -> seq T
x : T
m, n : nat
IHn : x \in \big[cat/[::]]_(m <= i < n) f i ->
exists i : nat, x \in f i /\ m <= i < n
i : m <= n
TAIL : x \in f n
============================
m <= n < n.+1
----------------------------------------------------------------------------- *)
apply/andP; split; [by done | by apply ltnSn].
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
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.
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.
Lemma bigcat_nat_uniq :
∀ n1 n2,
uniq (\cat_(n1 ≤ i < n2) (f i)).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 43)
T : eqType
f : nat -> seq T
H_uniq_seq : forall i : nat, uniq (f i)
H_no_elements_in_common : forall (x : T) (i1 i2 : nat),
x \in f i1 -> x \in f i2 -> i1 = i2
============================
forall n1 n2 : nat, uniq (\big[cat/[::]]_(n1 <= i < n2) f i)
----------------------------------------------------------------------------- *)
Proof.
intros n1 n2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 45)
T : eqType
f : nat -> seq T
H_uniq_seq : forall i : nat, uniq (f i)
H_no_elements_in_common : forall (x : T) (i1 i2 : nat),
x \in f i1 -> x \in f i2 -> i1 = i2
n1, n2 : nat
============================
uniq (\big[cat/[::]]_(n1 <= i < n2) f i)
----------------------------------------------------------------------------- *)
case (leqP n1 n2) ⇒ [LE | GT]; last by rewrite big_geq // ltnW.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 48)
T : eqType
f : nat -> seq T
H_uniq_seq : forall i : nat, uniq (f i)
H_no_elements_in_common : forall (x : T) (i1 i2 : nat),
x \in f i1 -> x \in f i2 -> i1 = i2
n1, n2 : nat
LE : n1 <= n2
============================
uniq (\big[cat/[::]]_(n1 <= i < n2) f i)
----------------------------------------------------------------------------- *)
rewrite -[n2](addKn n1).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 94)
T : eqType
f : nat -> seq T
H_uniq_seq : forall i : nat, uniq (f i)
H_no_elements_in_common : forall (x : T) (i1 i2 : nat),
x \in f i1 -> x \in f i2 -> i1 = i2
n1, n2 : nat
LE : n1 <= n2
============================
uniq (\big[cat/[::]]_(n1 <= i < n1 + n2 - n1) f i)
----------------------------------------------------------------------------- *)
rewrite -addnBA //; set delta := n2 - n1.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 125)
T : eqType
f : nat -> seq T
H_uniq_seq : forall i : nat, uniq (f i)
H_no_elements_in_common : forall (x : T) (i1 i2 : nat),
x \in f i1 -> x \in f i2 -> i1 = i2
n1, n2 : nat
LE : n1 <= n2
delta := n2 - n1 : nat
============================
uniq (\big[cat/[::]]_(n1 <= i < n1 + delta) f i)
----------------------------------------------------------------------------- *)
induction delta; first by rewrite addn0 big_geq.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 134)
T : eqType
f : nat -> seq T
H_uniq_seq : forall i : nat, uniq (f i)
H_no_elements_in_common : forall (x : T) (i1 i2 : nat),
x \in f i1 -> x \in f i2 -> i1 = i2
n1, n2 : nat
LE : n1 <= n2
delta : nat
IHdelta : uniq (\big[cat/[::]]_(n1 <= i < n1 + delta) f i)
============================
uniq (\big[cat/[::]]_(n1 <= i < n1 + delta.+1) f i)
----------------------------------------------------------------------------- *)
rewrite addnS big_nat_recr /=; last by apply leq_addr.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 166)
T : eqType
f : nat -> seq T
H_uniq_seq : forall i : nat, uniq (f i)
H_no_elements_in_common : forall (x : T) (i1 i2 : nat),
x \in f i1 -> x \in f i2 -> i1 = i2
n1, n2 : nat
LE : n1 <= n2
delta : nat
IHdelta : uniq (\big[cat/[::]]_(n1 <= i < n1 + delta) f i)
============================
uniq (\big[cat/[::]]_(n1 <= i < n1 + delta) f i ++ f (n1 + delta))
----------------------------------------------------------------------------- *)
rewrite cat_uniq; apply/andP; split; first by apply IHdelta.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 199)
T : eqType
f : nat -> seq T
H_uniq_seq : forall i : nat, uniq (f i)
H_no_elements_in_common : forall (x : T) (i1 i2 : nat),
x \in f i1 -> x \in f i2 -> i1 = i2
n1, n2 : nat
LE : n1 <= n2
delta : nat
IHdelta : uniq (\big[cat/[::]]_(n1 <= i < n1 + delta) f i)
============================
~~ has (mem (\big[cat/[::]]_(n1 <= i < n1 + delta) f i)) (f (n1 + delta)) &&
uniq (f (n1 + delta))
----------------------------------------------------------------------------- *)
apply /andP; split; last by apply H_uniq_seq.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 225)
T : eqType
f : nat -> seq T
H_uniq_seq : forall i : nat, uniq (f i)
H_no_elements_in_common : forall (x : T) (i1 i2 : nat),
x \in f i1 -> x \in f i2 -> i1 = i2
n1, n2 : nat
LE : n1 <= n2
delta : nat
IHdelta : uniq (\big[cat/[::]]_(n1 <= i < n1 + delta) f i)
============================
~~ has (mem (\big[cat/[::]]_(n1 <= i < n1 + delta) f i)) (f (n1 + delta))
----------------------------------------------------------------------------- *)
rewrite -all_predC; apply/allP; intros x INx.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 262)
T : eqType
f : nat -> seq T
H_uniq_seq : forall i : nat, uniq (f i)
H_no_elements_in_common : forall (x : T) (i1 i2 : nat),
x \in f i1 -> x \in f i2 -> i1 = i2
n1, n2 : nat
LE : n1 <= n2
delta : nat
IHdelta : uniq (\big[cat/[::]]_(n1 <= i < n1 + delta) f i)
x : T
INx : x \in f (n1 + delta)
============================
predC (mem (\big[cat/[::]]_(n1 <= i < n1 + delta) f i)) x
----------------------------------------------------------------------------- *)
simpl; apply/negP; unfold not; intro BUG.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 287)
T : eqType
f : nat -> seq T
H_uniq_seq : forall i : nat, uniq (f i)
H_no_elements_in_common : forall (x : T) (i1 i2 : nat),
x \in f i1 -> x \in f i2 -> i1 = i2
n1, n2 : nat
LE : n1 <= n2
delta : nat
IHdelta : uniq (\big[cat/[::]]_(n1 <= i < n1 + delta) f i)
x : T
INx : x \in f (n1 + delta)
BUG : x \in \big[cat/[::]]_(n1 <= i < n1 + delta) f i
============================
False
----------------------------------------------------------------------------- *)
apply mem_bigcat_nat_exists in BUG.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 288)
T : eqType
f : nat -> seq T
H_uniq_seq : forall i : nat, uniq (f i)
H_no_elements_in_common : forall (x : T) (i1 i2 : nat),
x \in f i1 -> x \in f i2 -> i1 = i2
n1, n2 : nat
LE : n1 <= n2
delta : nat
IHdelta : uniq (\big[cat/[::]]_(n1 <= i < n1 + delta) f i)
x : T
INx : x \in f (n1 + delta)
BUG : exists i : nat, x \in f i /\ n1 <= i < n1 + delta
============================
False
----------------------------------------------------------------------------- *)
move: BUG ⇒ [i [IN /andP [_ LTi]]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 351)
T : eqType
f : nat -> seq T
H_uniq_seq : forall i : nat, uniq (f i)
H_no_elements_in_common : forall (x : T) (i1 i2 : nat),
x \in f i1 -> x \in f i2 -> i1 = i2
n1, n2 : nat
LE : n1 <= n2
delta : nat
IHdelta : uniq (\big[cat/[::]]_(n1 <= i < n1 + delta) f i)
x : T
INx : x \in f (n1 + delta)
i : nat
IN : x \in f i
LTi : i < n1 + delta
============================
False
----------------------------------------------------------------------------- *)
apply H_no_elements_in_common with (i1 := i) in INx; last by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 352)
T : eqType
f : nat -> seq T
H_uniq_seq : forall i : nat, uniq (f i)
H_no_elements_in_common : forall (x : T) (i1 i2 : nat),
x \in f i1 -> x \in f i2 -> i1 = i2
n1, n2 : nat
LE : n1 <= n2
delta : nat
IHdelta : uniq (\big[cat/[::]]_(n1 <= i < n1 + delta) f i)
x : T
i : nat
INx : i = n1 + delta
IN : x \in f i
LTi : i < n1 + delta
============================
False
----------------------------------------------------------------------------- *)
by rewrite INx ltnn in LTi.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End BigCatDistinctElements.
End BigCatLemmas.
∀ n1 n2,
uniq (\cat_(n1 ≤ i < n2) (f i)).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 43)
T : eqType
f : nat -> seq T
H_uniq_seq : forall i : nat, uniq (f i)
H_no_elements_in_common : forall (x : T) (i1 i2 : nat),
x \in f i1 -> x \in f i2 -> i1 = i2
============================
forall n1 n2 : nat, uniq (\big[cat/[::]]_(n1 <= i < n2) f i)
----------------------------------------------------------------------------- *)
Proof.
intros n1 n2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 45)
T : eqType
f : nat -> seq T
H_uniq_seq : forall i : nat, uniq (f i)
H_no_elements_in_common : forall (x : T) (i1 i2 : nat),
x \in f i1 -> x \in f i2 -> i1 = i2
n1, n2 : nat
============================
uniq (\big[cat/[::]]_(n1 <= i < n2) f i)
----------------------------------------------------------------------------- *)
case (leqP n1 n2) ⇒ [LE | GT]; last by rewrite big_geq // ltnW.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 48)
T : eqType
f : nat -> seq T
H_uniq_seq : forall i : nat, uniq (f i)
H_no_elements_in_common : forall (x : T) (i1 i2 : nat),
x \in f i1 -> x \in f i2 -> i1 = i2
n1, n2 : nat
LE : n1 <= n2
============================
uniq (\big[cat/[::]]_(n1 <= i < n2) f i)
----------------------------------------------------------------------------- *)
rewrite -[n2](addKn n1).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 94)
T : eqType
f : nat -> seq T
H_uniq_seq : forall i : nat, uniq (f i)
H_no_elements_in_common : forall (x : T) (i1 i2 : nat),
x \in f i1 -> x \in f i2 -> i1 = i2
n1, n2 : nat
LE : n1 <= n2
============================
uniq (\big[cat/[::]]_(n1 <= i < n1 + n2 - n1) f i)
----------------------------------------------------------------------------- *)
rewrite -addnBA //; set delta := n2 - n1.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 125)
T : eqType
f : nat -> seq T
H_uniq_seq : forall i : nat, uniq (f i)
H_no_elements_in_common : forall (x : T) (i1 i2 : nat),
x \in f i1 -> x \in f i2 -> i1 = i2
n1, n2 : nat
LE : n1 <= n2
delta := n2 - n1 : nat
============================
uniq (\big[cat/[::]]_(n1 <= i < n1 + delta) f i)
----------------------------------------------------------------------------- *)
induction delta; first by rewrite addn0 big_geq.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 134)
T : eqType
f : nat -> seq T
H_uniq_seq : forall i : nat, uniq (f i)
H_no_elements_in_common : forall (x : T) (i1 i2 : nat),
x \in f i1 -> x \in f i2 -> i1 = i2
n1, n2 : nat
LE : n1 <= n2
delta : nat
IHdelta : uniq (\big[cat/[::]]_(n1 <= i < n1 + delta) f i)
============================
uniq (\big[cat/[::]]_(n1 <= i < n1 + delta.+1) f i)
----------------------------------------------------------------------------- *)
rewrite addnS big_nat_recr /=; last by apply leq_addr.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 166)
T : eqType
f : nat -> seq T
H_uniq_seq : forall i : nat, uniq (f i)
H_no_elements_in_common : forall (x : T) (i1 i2 : nat),
x \in f i1 -> x \in f i2 -> i1 = i2
n1, n2 : nat
LE : n1 <= n2
delta : nat
IHdelta : uniq (\big[cat/[::]]_(n1 <= i < n1 + delta) f i)
============================
uniq (\big[cat/[::]]_(n1 <= i < n1 + delta) f i ++ f (n1 + delta))
----------------------------------------------------------------------------- *)
rewrite cat_uniq; apply/andP; split; first by apply IHdelta.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 199)
T : eqType
f : nat -> seq T
H_uniq_seq : forall i : nat, uniq (f i)
H_no_elements_in_common : forall (x : T) (i1 i2 : nat),
x \in f i1 -> x \in f i2 -> i1 = i2
n1, n2 : nat
LE : n1 <= n2
delta : nat
IHdelta : uniq (\big[cat/[::]]_(n1 <= i < n1 + delta) f i)
============================
~~ has (mem (\big[cat/[::]]_(n1 <= i < n1 + delta) f i)) (f (n1 + delta)) &&
uniq (f (n1 + delta))
----------------------------------------------------------------------------- *)
apply /andP; split; last by apply H_uniq_seq.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 225)
T : eqType
f : nat -> seq T
H_uniq_seq : forall i : nat, uniq (f i)
H_no_elements_in_common : forall (x : T) (i1 i2 : nat),
x \in f i1 -> x \in f i2 -> i1 = i2
n1, n2 : nat
LE : n1 <= n2
delta : nat
IHdelta : uniq (\big[cat/[::]]_(n1 <= i < n1 + delta) f i)
============================
~~ has (mem (\big[cat/[::]]_(n1 <= i < n1 + delta) f i)) (f (n1 + delta))
----------------------------------------------------------------------------- *)
rewrite -all_predC; apply/allP; intros x INx.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 262)
T : eqType
f : nat -> seq T
H_uniq_seq : forall i : nat, uniq (f i)
H_no_elements_in_common : forall (x : T) (i1 i2 : nat),
x \in f i1 -> x \in f i2 -> i1 = i2
n1, n2 : nat
LE : n1 <= n2
delta : nat
IHdelta : uniq (\big[cat/[::]]_(n1 <= i < n1 + delta) f i)
x : T
INx : x \in f (n1 + delta)
============================
predC (mem (\big[cat/[::]]_(n1 <= i < n1 + delta) f i)) x
----------------------------------------------------------------------------- *)
simpl; apply/negP; unfold not; intro BUG.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 287)
T : eqType
f : nat -> seq T
H_uniq_seq : forall i : nat, uniq (f i)
H_no_elements_in_common : forall (x : T) (i1 i2 : nat),
x \in f i1 -> x \in f i2 -> i1 = i2
n1, n2 : nat
LE : n1 <= n2
delta : nat
IHdelta : uniq (\big[cat/[::]]_(n1 <= i < n1 + delta) f i)
x : T
INx : x \in f (n1 + delta)
BUG : x \in \big[cat/[::]]_(n1 <= i < n1 + delta) f i
============================
False
----------------------------------------------------------------------------- *)
apply mem_bigcat_nat_exists in BUG.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 288)
T : eqType
f : nat -> seq T
H_uniq_seq : forall i : nat, uniq (f i)
H_no_elements_in_common : forall (x : T) (i1 i2 : nat),
x \in f i1 -> x \in f i2 -> i1 = i2
n1, n2 : nat
LE : n1 <= n2
delta : nat
IHdelta : uniq (\big[cat/[::]]_(n1 <= i < n1 + delta) f i)
x : T
INx : x \in f (n1 + delta)
BUG : exists i : nat, x \in f i /\ n1 <= i < n1 + delta
============================
False
----------------------------------------------------------------------------- *)
move: BUG ⇒ [i [IN /andP [_ LTi]]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 351)
T : eqType
f : nat -> seq T
H_uniq_seq : forall i : nat, uniq (f i)
H_no_elements_in_common : forall (x : T) (i1 i2 : nat),
x \in f i1 -> x \in f i2 -> i1 = i2
n1, n2 : nat
LE : n1 <= n2
delta : nat
IHdelta : uniq (\big[cat/[::]]_(n1 <= i < n1 + delta) f i)
x : T
INx : x \in f (n1 + delta)
i : nat
IN : x \in f i
LTi : i < n1 + delta
============================
False
----------------------------------------------------------------------------- *)
apply H_no_elements_in_common with (i1 := i) in INx; last by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 352)
T : eqType
f : nat -> seq T
H_uniq_seq : forall i : nat, uniq (f i)
H_no_elements_in_common : forall (x : T) (i1 i2 : nat),
x \in f i1 -> x \in f i2 -> i1 = i2
n1, n2 : nat
LE : n1 <= n2
delta : nat
IHdelta : uniq (\big[cat/[::]]_(n1 <= i < n1 + delta) f i)
x : T
i : nat
INx : i = n1 + delta
IN : x \in f i
LTi : i < n1 + delta
============================
False
----------------------------------------------------------------------------- *)
by rewrite INx ltnn in LTi.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End BigCatDistinctElements.
End BigCatLemmas.