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.
Require Export prosa.util.tactics prosa.util.ssrlia.
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.
Lemma mem_bigcat_ord:
∀ x n (j: 'I_n) (f: 'I_n → list T),
j < n →
x \in (f j) →
x \in \cat_(i < n) (f i).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 79)
T : eqType
f : nat -> seq T
============================
forall (x : T) (n : nat) (j : 'I_n) (f0 : 'I_n -> seq T),
j < n -> x \in f0 j -> x \in \big[cat/[::]]_(i < n) f0 i
----------------------------------------------------------------------------- *)
Proof.
move⇒ x; elim⇒ [//|n IHn] j f' Hj Hx.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 126)
T : eqType
f : nat -> seq T
x : T
n : nat
IHn : forall (j : 'I_n) (f : 'I_n -> seq T),
j < n -> x \in f j -> x \in \big[cat/[::]]_(i < n) f i
j : 'I_n.+1
f' : 'I_n.+1 -> seq T
Hj : j < n.+1
Hx : x \in f' j
============================
x \in \big[cat/[::]]_(i < n.+1) f' i
----------------------------------------------------------------------------- *)
rewrite big_ord_recr /= mem_cat; apply /orP.
(* ----------------------------------[ coqtop ]---------------------------------
1 focused subgoal
(shelved: 1) (ID 165)
T : eqType
f : nat -> seq T
x : T
n : nat
IHn : forall (j : 'I_n) (f : 'I_n -> seq T),
j < n -> x \in f j -> x \in \big[cat/[::]]_(i < n) f i
j : 'I_n.+1
f' : 'I_n.+1 -> seq T
Hj : j < n.+1
Hx : x \in f' j
============================
x \in \big[cat/[::]]_(i < n) f' (widen_ord (m:=n.+1) (leqnSn n) i) \/
x \in f' ord_max
----------------------------------------------------------------------------- *)
move: Hj; rewrite ltnS leq_eqVlt ⇒ /orP [/eqP Hj|Hj].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 250)
T : eqType
f : nat -> seq T
x : T
n : nat
IHn : forall (j : 'I_n) (f : 'I_n -> seq T),
j < n -> x \in f j -> x \in \big[cat/[::]]_(i < n) f i
j : 'I_n.+1
f' : 'I_n.+1 -> seq T
Hx : x \in f' j
Hj : j = n
============================
x \in \big[cat/[::]]_(i < n) f' (widen_ord (m:=n.+1) (leqnSn n) i) \/
x \in f' ord_max
subgoal 2 (ID 251) is:
x \in \big[cat/[::]]_(i < n) f' (widen_ord (m:=n.+1) (leqnSn n) i) \/
x \in f' ord_max
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 250)
T : eqType
f : nat -> seq T
x : T
n : nat
IHn : forall (j : 'I_n) (f : 'I_n -> seq T),
j < n -> x \in f j -> x \in \big[cat/[::]]_(i < n) f i
j : 'I_n.+1
f' : 'I_n.+1 -> seq T
Hx : x \in f' j
Hj : j = n
============================
x \in \big[cat/[::]]_(i < n) f' (widen_ord (m:=n.+1) (leqnSn n) i) \/
x \in f' ord_max
----------------------------------------------------------------------------- *)
by right; rewrite (_ : ord_max = j); [|apply ord_inj].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 251)
subgoal 1 (ID 251) is:
x \in \big[cat/[::]]_(i < n) f' (widen_ord (m:=n.+1) (leqnSn n) i) \/
x \in f' ord_max
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 251)
T : eqType
f : nat -> seq T
x : T
n : nat
IHn : forall (j : 'I_n) (f : 'I_n -> seq T),
j < n -> x \in f j -> x \in \big[cat/[::]]_(i < n) f i
j : 'I_n.+1
f' : 'I_n.+1 -> seq T
Hx : x \in f' j
Hj : j < n
============================
x \in \big[cat/[::]]_(i < n) f' (widen_ord (m:=n.+1) (leqnSn n) i) \/
x \in f' ord_max
----------------------------------------------------------------------------- *)
left.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 286)
T : eqType
f : nat -> seq T
x : T
n : nat
IHn : forall (j : 'I_n) (f : 'I_n -> seq T),
j < n -> x \in f j -> x \in \big[cat/[::]]_(i < n) f i
j : 'I_n.+1
f' : 'I_n.+1 -> seq T
Hx : x \in f' j
Hj : j < n
============================
x \in \big[cat/[::]]_(i < n) f' (widen_ord (m:=n.+1) (leqnSn n) i)
----------------------------------------------------------------------------- *)
apply (IHn (Ordinal Hj)); [by []|].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 290)
T : eqType
f : nat -> seq T
x : T
n : nat
IHn : forall (j : 'I_n) (f : 'I_n -> seq T),
j < n -> x \in f j -> x \in \big[cat/[::]]_(i < n) f i
j : 'I_n.+1
f' : 'I_n.+1 -> seq T
Hx : x \in f' j
Hj : j < n
============================
x \in f' (widen_ord (m:=n.+1) (leqnSn n) (Ordinal (n:=n) (m:=j) Hj))
----------------------------------------------------------------------------- *)
by set j' := widen_ord _ _; have → : j' = j; [apply ord_inj|].
(* ----------------------------------[ 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.
Lemma mem_bigcat_ord:
∀ x n (j: 'I_n) (f: 'I_n → list T),
j < n →
x \in (f j) →
x \in \cat_(i < n) (f i).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 79)
T : eqType
f : nat -> seq T
============================
forall (x : T) (n : nat) (j : 'I_n) (f0 : 'I_n -> seq T),
j < n -> x \in f0 j -> x \in \big[cat/[::]]_(i < n) f0 i
----------------------------------------------------------------------------- *)
Proof.
move⇒ x; elim⇒ [//|n IHn] j f' Hj Hx.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 126)
T : eqType
f : nat -> seq T
x : T
n : nat
IHn : forall (j : 'I_n) (f : 'I_n -> seq T),
j < n -> x \in f j -> x \in \big[cat/[::]]_(i < n) f i
j : 'I_n.+1
f' : 'I_n.+1 -> seq T
Hj : j < n.+1
Hx : x \in f' j
============================
x \in \big[cat/[::]]_(i < n.+1) f' i
----------------------------------------------------------------------------- *)
rewrite big_ord_recr /= mem_cat; apply /orP.
(* ----------------------------------[ coqtop ]---------------------------------
1 focused subgoal
(shelved: 1) (ID 165)
T : eqType
f : nat -> seq T
x : T
n : nat
IHn : forall (j : 'I_n) (f : 'I_n -> seq T),
j < n -> x \in f j -> x \in \big[cat/[::]]_(i < n) f i
j : 'I_n.+1
f' : 'I_n.+1 -> seq T
Hj : j < n.+1
Hx : x \in f' j
============================
x \in \big[cat/[::]]_(i < n) f' (widen_ord (m:=n.+1) (leqnSn n) i) \/
x \in f' ord_max
----------------------------------------------------------------------------- *)
move: Hj; rewrite ltnS leq_eqVlt ⇒ /orP [/eqP Hj|Hj].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 250)
T : eqType
f : nat -> seq T
x : T
n : nat
IHn : forall (j : 'I_n) (f : 'I_n -> seq T),
j < n -> x \in f j -> x \in \big[cat/[::]]_(i < n) f i
j : 'I_n.+1
f' : 'I_n.+1 -> seq T
Hx : x \in f' j
Hj : j = n
============================
x \in \big[cat/[::]]_(i < n) f' (widen_ord (m:=n.+1) (leqnSn n) i) \/
x \in f' ord_max
subgoal 2 (ID 251) is:
x \in \big[cat/[::]]_(i < n) f' (widen_ord (m:=n.+1) (leqnSn n) i) \/
x \in f' ord_max
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 250)
T : eqType
f : nat -> seq T
x : T
n : nat
IHn : forall (j : 'I_n) (f : 'I_n -> seq T),
j < n -> x \in f j -> x \in \big[cat/[::]]_(i < n) f i
j : 'I_n.+1
f' : 'I_n.+1 -> seq T
Hx : x \in f' j
Hj : j = n
============================
x \in \big[cat/[::]]_(i < n) f' (widen_ord (m:=n.+1) (leqnSn n) i) \/
x \in f' ord_max
----------------------------------------------------------------------------- *)
by right; rewrite (_ : ord_max = j); [|apply ord_inj].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 251)
subgoal 1 (ID 251) is:
x \in \big[cat/[::]]_(i < n) f' (widen_ord (m:=n.+1) (leqnSn n) i) \/
x \in f' ord_max
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 251)
T : eqType
f : nat -> seq T
x : T
n : nat
IHn : forall (j : 'I_n) (f : 'I_n -> seq T),
j < n -> x \in f j -> x \in \big[cat/[::]]_(i < n) f i
j : 'I_n.+1
f' : 'I_n.+1 -> seq T
Hx : x \in f' j
Hj : j < n
============================
x \in \big[cat/[::]]_(i < n) f' (widen_ord (m:=n.+1) (leqnSn n) i) \/
x \in f' ord_max
----------------------------------------------------------------------------- *)
left.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 286)
T : eqType
f : nat -> seq T
x : T
n : nat
IHn : forall (j : 'I_n) (f : 'I_n -> seq T),
j < n -> x \in f j -> x \in \big[cat/[::]]_(i < n) f i
j : 'I_n.+1
f' : 'I_n.+1 -> seq T
Hx : x \in f' j
Hj : j < n
============================
x \in \big[cat/[::]]_(i < n) f' (widen_ord (m:=n.+1) (leqnSn n) i)
----------------------------------------------------------------------------- *)
apply (IHn (Ordinal Hj)); [by []|].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 290)
T : eqType
f : nat -> seq T
x : T
n : nat
IHn : forall (j : 'I_n) (f : 'I_n -> seq T),
j < n -> x \in f j -> x \in \big[cat/[::]]_(i < n) f i
j : 'I_n.+1
f' : 'I_n.+1 -> seq T
Hx : x \in f' j
Hj : j < n
============================
x \in f' (widen_ord (m:=n.+1) (leqnSn n) (Ordinal (n:=n) (m:=j) Hj))
----------------------------------------------------------------------------- *)
by set j' := widen_ord _ _; have → : j' = j; [apply ord_inj|].
(* ----------------------------------[ 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.
∀ 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.
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 (f: 'I_n → list T),
uniq (\cat_(i < n) (f i)) →
(∀ x i1 i2,
x \in (f i1) → x \in (f i2) → i1 = i2).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 69)
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 (n : nat) (f0 : 'I_n -> seq T),
uniq (\big[cat/[::]]_(i < n) f0 i) ->
forall (x : T) (i1 i2 : 'I_n), x \in f0 i1 -> x \in f0 i2 -> i1 = i2
----------------------------------------------------------------------------- *)
Proof.
case⇒ [|n]; [by move⇒ f' Huniq x; case|].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 80)
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
n : nat
============================
forall f0 : 'I_n.+1 -> seq T,
uniq (\big[cat/[::]]_(i < n.+1) f0 i) ->
forall (x : T) (i1 i2 : 'I_n.+1), x \in f0 i1 -> x \in f0 i2 -> i1 = i2
----------------------------------------------------------------------------- *)
elim: n ⇒ [|n IHn] f' Huniq x i1 i2 Hi1 Hi2.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 147)
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
f' : 'I_1 -> seq T
Huniq : uniq (\big[cat/[::]]_(i < 1) f' i)
x : T
i1, i2 : 'I_1
Hi1 : x \in f' i1
Hi2 : x \in f' i2
============================
i1 = i2
subgoal 2 (ID 148) is:
i1 = i2
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 147)
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
f' : 'I_1 -> seq T
Huniq : uniq (\big[cat/[::]]_(i < 1) f' i)
x : T
i1, i2 : 'I_1
Hi1 : x \in f' i1
Hi2 : x \in f' i2
============================
i1 = i2
----------------------------------------------------------------------------- *)
move: i1 i2 {Hi1 Hi2}; case; case⇒ [i1|//]; case; case⇒ [i2|//].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 219)
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
f' : 'I_1 -> seq T
Huniq : uniq (\big[cat/[::]]_(i < 1) f' i)
x : T
i1, i2 : 0 < 1
============================
Ordinal (n:=1) (m:=0) i1 = Ordinal (n:=1) (m:=0) i2
----------------------------------------------------------------------------- *)
apply f_equal, eq_irrelevance.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 148)
subgoal 1 (ID 148) is:
i1 = i2
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 148)
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
n : nat
IHn : forall f : 'I_n.+1 -> seq T,
uniq (\big[cat/[::]]_(i < n.+1) f i) ->
forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f' : 'I_n.+2 -> seq T
Huniq : uniq (\big[cat/[::]]_(i < n.+2) f' i)
x : T
i1, i2 : 'I_n.+2
Hi1 : x \in f' i1
Hi2 : x \in f' i2
============================
i1 = i2
----------------------------------------------------------------------------- *)
move: (leq_ord i1); rewrite leq_eqVlt ⇒ /orP [H'i1|H'i1];
move: (leq_ord i2); rewrite leq_eqVlt ⇒ /orP [H'i2|H'i2].
(* ----------------------------------[ coqtop ]---------------------------------
4 subgoals (ID 347)
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
n : nat
IHn : forall f : 'I_n.+1 -> seq T,
uniq (\big[cat/[::]]_(i < n.+1) f i) ->
forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f' : 'I_n.+2 -> seq T
Huniq : uniq (\big[cat/[::]]_(i < n.+2) f' i)
x : T
i1, i2 : 'I_n.+2
Hi1 : x \in f' i1
Hi2 : x \in f' i2
H'i1 : i1 == n.+1
H'i2 : i2 == n.+1
============================
i1 = i2
subgoal 2 (ID 348) is:
i1 = i2
subgoal 3 (ID 395) is:
i1 = i2
subgoal 4 (ID 396) is:
i1 = i2
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 347)
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
n : nat
IHn : forall f : 'I_n.+1 -> seq T,
uniq (\big[cat/[::]]_(i < n.+1) f i) ->
forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f' : 'I_n.+2 -> seq T
Huniq : uniq (\big[cat/[::]]_(i < n.+2) f' i)
x : T
i1, i2 : 'I_n.+2
Hi1 : x \in f' i1
Hi2 : x \in f' i2
H'i1 : i1 == n.+1
H'i2 : i2 == n.+1
============================
i1 = i2
----------------------------------------------------------------------------- *)
by apply ord_inj; move: H'i1 H'i2 ⇒ /eqP → /eqP →.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 348)
subgoal 1 (ID 348) is:
i1 = i2
subgoal 2 (ID 395) is:
i1 = i2
subgoal 3 (ID 396) is:
i1 = i2
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 348)
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
n : nat
IHn : forall f : 'I_n.+1 -> seq T,
uniq (\big[cat/[::]]_(i < n.+1) f i) ->
forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f' : 'I_n.+2 -> seq T
Huniq : uniq (\big[cat/[::]]_(i < n.+2) f' i)
x : T
i1, i2 : 'I_n.+2
Hi1 : x \in f' i1
Hi2 : x \in f' i2
H'i1 : i1 == n.+1
H'i2 : i2 < n.+1
============================
i1 = i2
subgoal 2 (ID 395) is:
i1 = i2
subgoal 3 (ID 396) is:
i1 = i2
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 348)
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
n : nat
IHn : forall f : 'I_n.+1 -> seq T,
uniq (\big[cat/[::]]_(i < n.+1) f i) ->
forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f' : 'I_n.+2 -> seq T
Huniq : uniq (\big[cat/[::]]_(i < n.+2) f' i)
x : T
i1, i2 : 'I_n.+2
Hi1 : x \in f' i1
Hi2 : x \in f' i2
H'i1 : i1 == n.+1
H'i2 : i2 < n.+1
============================
i1 = i2
----------------------------------------------------------------------------- *)
exfalso.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 475)
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
n : nat
IHn : forall f : 'I_n.+1 -> seq T,
uniq (\big[cat/[::]]_(i < n.+1) f i) ->
forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f' : 'I_n.+2 -> seq T
Huniq : uniq (\big[cat/[::]]_(i < n.+2) f' i)
x : T
i1, i2 : 'I_n.+2
Hi1 : x \in f' i1
Hi2 : x \in f' i2
H'i1 : i1 == n.+1
H'i2 : i2 < n.+1
============================
False
----------------------------------------------------------------------------- *)
move: Huniq; rewrite big_ord_recr cat_uniq ⇒ /andP [_ /andP [H _]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 569)
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
n : nat
IHn : forall f : 'I_n.+1 -> seq T,
uniq (\big[cat/[::]]_(i < n.+1) f i) ->
forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f' : 'I_n.+2 -> seq T
x : T
i1, i2 : 'I_n.+2
Hi1 : x \in f' i1
Hi2 : x \in f' i2
H'i1 : i1 == n.+1
H'i2 : i2 < n.+1
H : ~~
has
(mem
(\big[cat_monoid T/[::]]_(i < n.+1) f'
(widen_ord (m:=n.+2)
(leqnSn n.+1) i)))
(f' ord_max)
============================
False
----------------------------------------------------------------------------- *)
move: H; apply /negP; rewrite Bool.negb_involutive.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 616)
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
n : nat
IHn : forall f : 'I_n.+1 -> seq T,
uniq (\big[cat/[::]]_(i < n.+1) f i) ->
forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f' : 'I_n.+2 -> seq T
x : T
i1, i2 : 'I_n.+2
Hi1 : x \in f' i1
Hi2 : x \in f' i2
H'i1 : i1 == n.+1
H'i2 : i2 < n.+1
============================
has
(mem
(\big[cat_monoid T/[::]]_(i < n.+1) f'
(widen_ord (m:=n.+2)
(leqnSn n.+1) i)))
(f' ord_max)
----------------------------------------------------------------------------- *)
apply /hasP; ∃ x ⇒ /=.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 648)
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
n : nat
IHn : forall f : 'I_n.+1 -> seq T,
uniq (\big[cat/[::]]_(i < n.+1) f i) ->
forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f' : 'I_n.+2 -> seq T
x : T
i1, i2 : 'I_n.+2
Hi1 : x \in f' i1
Hi2 : x \in f' i2
H'i1 : i1 == n.+1
H'i2 : i2 < n.+1
============================
x \in f' ord_max
subgoal 2 (ID 649) is:
x \in \big[cat/[::]]_(i < n.+1) f' (widen_ord (m:=n.+2) (leqnSn n.+1) i)
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 648)
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
n : nat
IHn : forall f : 'I_n.+1 -> seq T,
uniq (\big[cat/[::]]_(i < n.+1) f i) ->
forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f' : 'I_n.+2 -> seq T
x : T
i1, i2 : 'I_n.+2
Hi1 : x \in f' i1
Hi2 : x \in f' i2
H'i1 : i1 == n.+1
H'i2 : i2 < n.+1
============================
x \in f' ord_max
----------------------------------------------------------------------------- *)
set o := ord_max; suff → : o = i1; [by []|].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 656)
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
n : nat
IHn : forall f : 'I_n.+1 -> seq T,
uniq (\big[cat/[::]]_(i < n.+1) f i) ->
forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f' : 'I_n.+2 -> seq T
x : T
i1, i2 : 'I_n.+2
Hi1 : x \in f' i1
Hi2 : x \in f' i2
H'i1 : i1 == n.+1
H'i2 : i2 < n.+1
o := ord_max : 'I_n.+2
============================
o = i1
----------------------------------------------------------------------------- *)
by apply ord_inj; move: H'i1 ⇒ /eqP →.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 649)
subgoal 1 (ID 649) is:
x \in \big[cat/[::]]_(i < n.+1) f' (widen_ord (m:=n.+2) (leqnSn n.+1) i)
subgoal 2 (ID 395) is:
i1 = i2
subgoal 3 (ID 396) is:
i1 = i2
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 649)
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
n : nat
IHn : forall f : 'I_n.+1 -> seq T,
uniq (\big[cat/[::]]_(i < n.+1) f i) ->
forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f' : 'I_n.+2 -> seq T
x : T
i1, i2 : 'I_n.+2
Hi1 : x \in f' i1
Hi2 : x \in f' i2
H'i1 : i1 == n.+1
H'i2 : i2 < n.+1
============================
x \in \big[cat/[::]]_(i < n.+1) f' (widen_ord (m:=n.+2) (leqnSn n.+1) i)
----------------------------------------------------------------------------- *)
apply (mem_bigcat_ord _ _ (Ordinal H'i2)) ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 708)
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
n : nat
IHn : forall f : 'I_n.+1 -> seq T,
uniq (\big[cat/[::]]_(i < n.+1) f i) ->
forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f' : 'I_n.+2 -> seq T
x : T
i1, i2 : 'I_n.+2
Hi1 : x \in f' i1
Hi2 : x \in f' i2
H'i1 : i1 == n.+1
H'i2 : i2 < n.+1
============================
x
\in f'
(widen_ord (m:=n.+2) (leqnSn n.+1) (Ordinal (n:=n.+1) (m:=i2) H'i2))
----------------------------------------------------------------------------- *)
by set o := widen_ord _ _; suff → : o = i2; [|apply ord_inj].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 395)
subgoal 1 (ID 395) is:
i1 = i2
subgoal 2 (ID 396) is:
i1 = i2
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 395)
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
n : nat
IHn : forall f : 'I_n.+1 -> seq T,
uniq (\big[cat/[::]]_(i < n.+1) f i) ->
forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f' : 'I_n.+2 -> seq T
Huniq : uniq (\big[cat/[::]]_(i < n.+2) f' i)
x : T
i1, i2 : 'I_n.+2
Hi1 : x \in f' i1
Hi2 : x \in f' i2
H'i1 : i1 < n.+1
H'i2 : i2 == n.+1
============================
i1 = i2
subgoal 2 (ID 396) is:
i1 = i2
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 395)
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
n : nat
IHn : forall f : 'I_n.+1 -> seq T,
uniq (\big[cat/[::]]_(i < n.+1) f i) ->
forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f' : 'I_n.+2 -> seq T
Huniq : uniq (\big[cat/[::]]_(i < n.+2) f' i)
x : T
i1, i2 : 'I_n.+2
Hi1 : x \in f' i1
Hi2 : x \in f' i2
H'i1 : i1 < n.+1
H'i2 : i2 == n.+1
============================
i1 = i2
----------------------------------------------------------------------------- *)
exfalso.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 748)
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
n : nat
IHn : forall f : 'I_n.+1 -> seq T,
uniq (\big[cat/[::]]_(i < n.+1) f i) ->
forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f' : 'I_n.+2 -> seq T
Huniq : uniq (\big[cat/[::]]_(i < n.+2) f' i)
x : T
i1, i2 : 'I_n.+2
Hi1 : x \in f' i1
Hi2 : x \in f' i2
H'i1 : i1 < n.+1
H'i2 : i2 == n.+1
============================
False
----------------------------------------------------------------------------- *)
move: Huniq; rewrite big_ord_recr cat_uniq ⇒ /andP [_ /andP [H _]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 842)
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
n : nat
IHn : forall f : 'I_n.+1 -> seq T,
uniq (\big[cat/[::]]_(i < n.+1) f i) ->
forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f' : 'I_n.+2 -> seq T
x : T
i1, i2 : 'I_n.+2
Hi1 : x \in f' i1
Hi2 : x \in f' i2
H'i1 : i1 < n.+1
H'i2 : i2 == n.+1
H : ~~
has
(mem
(\big[cat_monoid T/[::]]_(i < n.+1) f'
(widen_ord (m:=n.+2)
(leqnSn n.+1) i)))
(f' ord_max)
============================
False
----------------------------------------------------------------------------- *)
move: H; apply /negP; rewrite Bool.negb_involutive.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 889)
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
n : nat
IHn : forall f : 'I_n.+1 -> seq T,
uniq (\big[cat/[::]]_(i < n.+1) f i) ->
forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f' : 'I_n.+2 -> seq T
x : T
i1, i2 : 'I_n.+2
Hi1 : x \in f' i1
Hi2 : x \in f' i2
H'i1 : i1 < n.+1
H'i2 : i2 == n.+1
============================
has
(mem
(\big[cat_monoid T/[::]]_(i < n.+1) f'
(widen_ord (m:=n.+2)
(leqnSn n.+1) i)))
(f' ord_max)
----------------------------------------------------------------------------- *)
apply /hasP; ∃ x ⇒ /=.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 921)
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
n : nat
IHn : forall f : 'I_n.+1 -> seq T,
uniq (\big[cat/[::]]_(i < n.+1) f i) ->
forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f' : 'I_n.+2 -> seq T
x : T
i1, i2 : 'I_n.+2
Hi1 : x \in f' i1
Hi2 : x \in f' i2
H'i1 : i1 < n.+1
H'i2 : i2 == n.+1
============================
x \in f' ord_max
subgoal 2 (ID 922) is:
x \in \big[cat/[::]]_(i < n.+1) f' (widen_ord (m:=n.+2) (leqnSn n.+1) i)
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 921)
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
n : nat
IHn : forall f : 'I_n.+1 -> seq T,
uniq (\big[cat/[::]]_(i < n.+1) f i) ->
forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f' : 'I_n.+2 -> seq T
x : T
i1, i2 : 'I_n.+2
Hi1 : x \in f' i1
Hi2 : x \in f' i2
H'i1 : i1 < n.+1
H'i2 : i2 == n.+1
============================
x \in f' ord_max
----------------------------------------------------------------------------- *)
set o := ord_max; suff → : o = i2; [by []|].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 929)
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
n : nat
IHn : forall f : 'I_n.+1 -> seq T,
uniq (\big[cat/[::]]_(i < n.+1) f i) ->
forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f' : 'I_n.+2 -> seq T
x : T
i1, i2 : 'I_n.+2
Hi1 : x \in f' i1
Hi2 : x \in f' i2
H'i1 : i1 < n.+1
H'i2 : i2 == n.+1
o := ord_max : 'I_n.+2
============================
o = i2
----------------------------------------------------------------------------- *)
by apply ord_inj; move: H'i2 ⇒ /eqP →.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 922)
subgoal 1 (ID 922) is:
x \in \big[cat/[::]]_(i < n.+1) f' (widen_ord (m:=n.+2) (leqnSn n.+1) i)
subgoal 2 (ID 396) is:
i1 = i2
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 922)
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
n : nat
IHn : forall f : 'I_n.+1 -> seq T,
uniq (\big[cat/[::]]_(i < n.+1) f i) ->
forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f' : 'I_n.+2 -> seq T
x : T
i1, i2 : 'I_n.+2
Hi1 : x \in f' i1
Hi2 : x \in f' i2
H'i1 : i1 < n.+1
H'i2 : i2 == n.+1
============================
x \in \big[cat/[::]]_(i < n.+1) f' (widen_ord (m:=n.+2) (leqnSn n.+1) i)
----------------------------------------------------------------------------- *)
apply (mem_bigcat_ord _ _ (Ordinal H'i1)) ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 981)
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
n : nat
IHn : forall f : 'I_n.+1 -> seq T,
uniq (\big[cat/[::]]_(i < n.+1) f i) ->
forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f' : 'I_n.+2 -> seq T
x : T
i1, i2 : 'I_n.+2
Hi1 : x \in f' i1
Hi2 : x \in f' i2
H'i1 : i1 < n.+1
H'i2 : i2 == n.+1
============================
x
\in f'
(widen_ord (m:=n.+2) (leqnSn n.+1) (Ordinal (n:=n.+1) (m:=i1) H'i1))
----------------------------------------------------------------------------- *)
by set o := widen_ord _ _; suff → : o = i1; [|apply ord_inj].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 396)
subgoal 1 (ID 396) is:
i1 = i2
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 396)
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
n : nat
IHn : forall f : 'I_n.+1 -> seq T,
uniq (\big[cat/[::]]_(i < n.+1) f i) ->
forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f' : 'I_n.+2 -> seq T
Huniq : uniq (\big[cat/[::]]_(i < n.+2) f' i)
x : T
i1, i2 : 'I_n.+2
Hi1 : x \in f' i1
Hi2 : x \in f' i2
H'i1 : i1 < n.+1
H'i2 : i2 < n.+1
============================
i1 = i2
----------------------------------------------------------------------------- *)
move: Huniq; rewrite big_ord_recr cat_uniq ⇒ /andP [Huniq _].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1076)
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
n : nat
IHn : forall f : 'I_n.+1 -> seq T,
uniq (\big[cat/[::]]_(i < n.+1) f i) ->
forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f' : 'I_n.+2 -> seq T
x : T
i1, i2 : 'I_n.+2
Hi1 : x \in f' i1
Hi2 : x \in f' i2
H'i1 : i1 < n.+1
H'i2 : i2 < n.+1
Huniq : uniq
(\big[cat_monoid T/[::]]_(i < n.+1) f'
(widen_ord (m:=n.+2)
(leqnSn n.+1) i))
============================
i1 = i2
----------------------------------------------------------------------------- *)
apply ord_inj; rewrite -(inordK H'i1) -(inordK H'i2); apply f_equal.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1090)
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
n : nat
IHn : forall f : 'I_n.+1 -> seq T,
uniq (\big[cat/[::]]_(i < n.+1) f i) ->
forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f' : 'I_n.+2 -> seq T
x : T
i1, i2 : 'I_n.+2
Hi1 : x \in f' i1
Hi2 : x \in f' i2
H'i1 : i1 < n.+1
H'i2 : i2 < n.+1
Huniq : uniq
(\big[cat_monoid T/[::]]_(i < n.+1) f'
(widen_ord (m:=n.+2)
(leqnSn n.+1) i))
============================
inord i1 = inord i2
----------------------------------------------------------------------------- *)
apply (IHn _ Huniq x).
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1093)
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
n : nat
IHn : forall f : 'I_n.+1 -> seq T,
uniq (\big[cat/[::]]_(i < n.+1) f i) ->
forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f' : 'I_n.+2 -> seq T
x : T
i1, i2 : 'I_n.+2
Hi1 : x \in f' i1
Hi2 : x \in f' i2
H'i1 : i1 < n.+1
H'i2 : i2 < n.+1
Huniq : uniq
(\big[cat_monoid T/[::]]_(i < n.+1) f'
(widen_ord (m:=n.+2)
(leqnSn n.+1) i))
============================
x \in f' (widen_ord (m:=n.+2) (leqnSn n.+1) (inord i1))
subgoal 2 (ID 1094) is:
x \in f' (widen_ord (m:=n.+2) (leqnSn n.+1) (inord i2))
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1093)
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
n : nat
IHn : forall f : 'I_n.+1 -> seq T,
uniq (\big[cat/[::]]_(i < n.+1) f i) ->
forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f' : 'I_n.+2 -> seq T
x : T
i1, i2 : 'I_n.+2
Hi1 : x \in f' i1
Hi2 : x \in f' i2
H'i1 : i1 < n.+1
H'i2 : i2 < n.+1
Huniq : uniq
(\big[cat_monoid T/[::]]_(i < n.+1) f'
(widen_ord (m:=n.+2)
(leqnSn n.+1) i))
============================
x \in f' (widen_ord (m:=n.+2) (leqnSn n.+1) (inord i1))
----------------------------------------------------------------------------- *)
set i1' := widen_ord _ _; suff → : i1' = i1; [by []|].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1106)
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
n : nat
IHn : forall f : 'I_n.+1 -> seq T,
uniq (\big[cat/[::]]_(i < n.+1) f i) ->
forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f' : 'I_n.+2 -> seq T
x : T
i1, i2 : 'I_n.+2
Hi1 : x \in f' i1
Hi2 : x \in f' i2
H'i1 : i1 < n.+1
H'i2 : i2 < n.+1
Huniq : uniq
(\big[cat_monoid T/[::]]_(i < n.+1) f'
(widen_ord (m:=n.+2)
(leqnSn n.+1) i))
i1' := widen_ord (m:=n.+2) (leqnSn n.+1) (inord i1) : 'I_n.+2
============================
i1' = i1
----------------------------------------------------------------------------- *)
by apply ord_inj; rewrite /= inordK.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1094)
subgoal 1 (ID 1094) is:
x \in f' (widen_ord (m:=n.+2) (leqnSn n.+1) (inord i2))
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1094)
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
n : nat
IHn : forall f : 'I_n.+1 -> seq T,
uniq (\big[cat/[::]]_(i < n.+1) f i) ->
forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f' : 'I_n.+2 -> seq T
x : T
i1, i2 : 'I_n.+2
Hi1 : x \in f' i1
Hi2 : x \in f' i2
H'i1 : i1 < n.+1
H'i2 : i2 < n.+1
Huniq : uniq
(\big[cat_monoid T/[::]]_(i < n.+1) f'
(widen_ord (m:=n.+2)
(leqnSn n.+1) i))
============================
x \in f' (widen_ord (m:=n.+2) (leqnSn n.+1) (inord i2))
----------------------------------------------------------------------------- *)
set i2' := widen_ord _ _; suff → : i2' = i2; [by []|].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1130)
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
n : nat
IHn : forall f : 'I_n.+1 -> seq T,
uniq (\big[cat/[::]]_(i < n.+1) f i) ->
forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f' : 'I_n.+2 -> seq T
x : T
i1, i2 : 'I_n.+2
Hi1 : x \in f' i1
Hi2 : x \in f' i2
H'i1 : i1 < n.+1
H'i2 : i2 < n.+1
Huniq : uniq
(\big[cat_monoid T/[::]]_(i < n.+1) f'
(widen_ord (m:=n.+2)
(leqnSn n.+1) i))
i2' := widen_ord (m:=n.+2) (leqnSn n.+1) (inord i2) : 'I_n.+2
============================
i2' = i2
----------------------------------------------------------------------------- *)
by apply ord_inj; rewrite /= inordK.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End BigCatDistinctElements.
∀ n (f: 'I_n → list T),
uniq (\cat_(i < n) (f i)) →
(∀ x i1 i2,
x \in (f i1) → x \in (f i2) → i1 = i2).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 69)
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 (n : nat) (f0 : 'I_n -> seq T),
uniq (\big[cat/[::]]_(i < n) f0 i) ->
forall (x : T) (i1 i2 : 'I_n), x \in f0 i1 -> x \in f0 i2 -> i1 = i2
----------------------------------------------------------------------------- *)
Proof.
case⇒ [|n]; [by move⇒ f' Huniq x; case|].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 80)
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
n : nat
============================
forall f0 : 'I_n.+1 -> seq T,
uniq (\big[cat/[::]]_(i < n.+1) f0 i) ->
forall (x : T) (i1 i2 : 'I_n.+1), x \in f0 i1 -> x \in f0 i2 -> i1 = i2
----------------------------------------------------------------------------- *)
elim: n ⇒ [|n IHn] f' Huniq x i1 i2 Hi1 Hi2.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 147)
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
f' : 'I_1 -> seq T
Huniq : uniq (\big[cat/[::]]_(i < 1) f' i)
x : T
i1, i2 : 'I_1
Hi1 : x \in f' i1
Hi2 : x \in f' i2
============================
i1 = i2
subgoal 2 (ID 148) is:
i1 = i2
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 147)
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
f' : 'I_1 -> seq T
Huniq : uniq (\big[cat/[::]]_(i < 1) f' i)
x : T
i1, i2 : 'I_1
Hi1 : x \in f' i1
Hi2 : x \in f' i2
============================
i1 = i2
----------------------------------------------------------------------------- *)
move: i1 i2 {Hi1 Hi2}; case; case⇒ [i1|//]; case; case⇒ [i2|//].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 219)
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
f' : 'I_1 -> seq T
Huniq : uniq (\big[cat/[::]]_(i < 1) f' i)
x : T
i1, i2 : 0 < 1
============================
Ordinal (n:=1) (m:=0) i1 = Ordinal (n:=1) (m:=0) i2
----------------------------------------------------------------------------- *)
apply f_equal, eq_irrelevance.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 148)
subgoal 1 (ID 148) is:
i1 = i2
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 148)
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
n : nat
IHn : forall f : 'I_n.+1 -> seq T,
uniq (\big[cat/[::]]_(i < n.+1) f i) ->
forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f' : 'I_n.+2 -> seq T
Huniq : uniq (\big[cat/[::]]_(i < n.+2) f' i)
x : T
i1, i2 : 'I_n.+2
Hi1 : x \in f' i1
Hi2 : x \in f' i2
============================
i1 = i2
----------------------------------------------------------------------------- *)
move: (leq_ord i1); rewrite leq_eqVlt ⇒ /orP [H'i1|H'i1];
move: (leq_ord i2); rewrite leq_eqVlt ⇒ /orP [H'i2|H'i2].
(* ----------------------------------[ coqtop ]---------------------------------
4 subgoals (ID 347)
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
n : nat
IHn : forall f : 'I_n.+1 -> seq T,
uniq (\big[cat/[::]]_(i < n.+1) f i) ->
forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f' : 'I_n.+2 -> seq T
Huniq : uniq (\big[cat/[::]]_(i < n.+2) f' i)
x : T
i1, i2 : 'I_n.+2
Hi1 : x \in f' i1
Hi2 : x \in f' i2
H'i1 : i1 == n.+1
H'i2 : i2 == n.+1
============================
i1 = i2
subgoal 2 (ID 348) is:
i1 = i2
subgoal 3 (ID 395) is:
i1 = i2
subgoal 4 (ID 396) is:
i1 = i2
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 347)
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
n : nat
IHn : forall f : 'I_n.+1 -> seq T,
uniq (\big[cat/[::]]_(i < n.+1) f i) ->
forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f' : 'I_n.+2 -> seq T
Huniq : uniq (\big[cat/[::]]_(i < n.+2) f' i)
x : T
i1, i2 : 'I_n.+2
Hi1 : x \in f' i1
Hi2 : x \in f' i2
H'i1 : i1 == n.+1
H'i2 : i2 == n.+1
============================
i1 = i2
----------------------------------------------------------------------------- *)
by apply ord_inj; move: H'i1 H'i2 ⇒ /eqP → /eqP →.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 348)
subgoal 1 (ID 348) is:
i1 = i2
subgoal 2 (ID 395) is:
i1 = i2
subgoal 3 (ID 396) is:
i1 = i2
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 348)
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
n : nat
IHn : forall f : 'I_n.+1 -> seq T,
uniq (\big[cat/[::]]_(i < n.+1) f i) ->
forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f' : 'I_n.+2 -> seq T
Huniq : uniq (\big[cat/[::]]_(i < n.+2) f' i)
x : T
i1, i2 : 'I_n.+2
Hi1 : x \in f' i1
Hi2 : x \in f' i2
H'i1 : i1 == n.+1
H'i2 : i2 < n.+1
============================
i1 = i2
subgoal 2 (ID 395) is:
i1 = i2
subgoal 3 (ID 396) is:
i1 = i2
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 348)
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
n : nat
IHn : forall f : 'I_n.+1 -> seq T,
uniq (\big[cat/[::]]_(i < n.+1) f i) ->
forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f' : 'I_n.+2 -> seq T
Huniq : uniq (\big[cat/[::]]_(i < n.+2) f' i)
x : T
i1, i2 : 'I_n.+2
Hi1 : x \in f' i1
Hi2 : x \in f' i2
H'i1 : i1 == n.+1
H'i2 : i2 < n.+1
============================
i1 = i2
----------------------------------------------------------------------------- *)
exfalso.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 475)
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
n : nat
IHn : forall f : 'I_n.+1 -> seq T,
uniq (\big[cat/[::]]_(i < n.+1) f i) ->
forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f' : 'I_n.+2 -> seq T
Huniq : uniq (\big[cat/[::]]_(i < n.+2) f' i)
x : T
i1, i2 : 'I_n.+2
Hi1 : x \in f' i1
Hi2 : x \in f' i2
H'i1 : i1 == n.+1
H'i2 : i2 < n.+1
============================
False
----------------------------------------------------------------------------- *)
move: Huniq; rewrite big_ord_recr cat_uniq ⇒ /andP [_ /andP [H _]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 569)
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
n : nat
IHn : forall f : 'I_n.+1 -> seq T,
uniq (\big[cat/[::]]_(i < n.+1) f i) ->
forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f' : 'I_n.+2 -> seq T
x : T
i1, i2 : 'I_n.+2
Hi1 : x \in f' i1
Hi2 : x \in f' i2
H'i1 : i1 == n.+1
H'i2 : i2 < n.+1
H : ~~
has
(mem
(\big[cat_monoid T/[::]]_(i < n.+1) f'
(widen_ord (m:=n.+2)
(leqnSn n.+1) i)))
(f' ord_max)
============================
False
----------------------------------------------------------------------------- *)
move: H; apply /negP; rewrite Bool.negb_involutive.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 616)
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
n : nat
IHn : forall f : 'I_n.+1 -> seq T,
uniq (\big[cat/[::]]_(i < n.+1) f i) ->
forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f' : 'I_n.+2 -> seq T
x : T
i1, i2 : 'I_n.+2
Hi1 : x \in f' i1
Hi2 : x \in f' i2
H'i1 : i1 == n.+1
H'i2 : i2 < n.+1
============================
has
(mem
(\big[cat_monoid T/[::]]_(i < n.+1) f'
(widen_ord (m:=n.+2)
(leqnSn n.+1) i)))
(f' ord_max)
----------------------------------------------------------------------------- *)
apply /hasP; ∃ x ⇒ /=.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 648)
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
n : nat
IHn : forall f : 'I_n.+1 -> seq T,
uniq (\big[cat/[::]]_(i < n.+1) f i) ->
forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f' : 'I_n.+2 -> seq T
x : T
i1, i2 : 'I_n.+2
Hi1 : x \in f' i1
Hi2 : x \in f' i2
H'i1 : i1 == n.+1
H'i2 : i2 < n.+1
============================
x \in f' ord_max
subgoal 2 (ID 649) is:
x \in \big[cat/[::]]_(i < n.+1) f' (widen_ord (m:=n.+2) (leqnSn n.+1) i)
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 648)
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
n : nat
IHn : forall f : 'I_n.+1 -> seq T,
uniq (\big[cat/[::]]_(i < n.+1) f i) ->
forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f' : 'I_n.+2 -> seq T
x : T
i1, i2 : 'I_n.+2
Hi1 : x \in f' i1
Hi2 : x \in f' i2
H'i1 : i1 == n.+1
H'i2 : i2 < n.+1
============================
x \in f' ord_max
----------------------------------------------------------------------------- *)
set o := ord_max; suff → : o = i1; [by []|].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 656)
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
n : nat
IHn : forall f : 'I_n.+1 -> seq T,
uniq (\big[cat/[::]]_(i < n.+1) f i) ->
forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f' : 'I_n.+2 -> seq T
x : T
i1, i2 : 'I_n.+2
Hi1 : x \in f' i1
Hi2 : x \in f' i2
H'i1 : i1 == n.+1
H'i2 : i2 < n.+1
o := ord_max : 'I_n.+2
============================
o = i1
----------------------------------------------------------------------------- *)
by apply ord_inj; move: H'i1 ⇒ /eqP →.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 649)
subgoal 1 (ID 649) is:
x \in \big[cat/[::]]_(i < n.+1) f' (widen_ord (m:=n.+2) (leqnSn n.+1) i)
subgoal 2 (ID 395) is:
i1 = i2
subgoal 3 (ID 396) is:
i1 = i2
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 649)
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
n : nat
IHn : forall f : 'I_n.+1 -> seq T,
uniq (\big[cat/[::]]_(i < n.+1) f i) ->
forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f' : 'I_n.+2 -> seq T
x : T
i1, i2 : 'I_n.+2
Hi1 : x \in f' i1
Hi2 : x \in f' i2
H'i1 : i1 == n.+1
H'i2 : i2 < n.+1
============================
x \in \big[cat/[::]]_(i < n.+1) f' (widen_ord (m:=n.+2) (leqnSn n.+1) i)
----------------------------------------------------------------------------- *)
apply (mem_bigcat_ord _ _ (Ordinal H'i2)) ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 708)
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
n : nat
IHn : forall f : 'I_n.+1 -> seq T,
uniq (\big[cat/[::]]_(i < n.+1) f i) ->
forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f' : 'I_n.+2 -> seq T
x : T
i1, i2 : 'I_n.+2
Hi1 : x \in f' i1
Hi2 : x \in f' i2
H'i1 : i1 == n.+1
H'i2 : i2 < n.+1
============================
x
\in f'
(widen_ord (m:=n.+2) (leqnSn n.+1) (Ordinal (n:=n.+1) (m:=i2) H'i2))
----------------------------------------------------------------------------- *)
by set o := widen_ord _ _; suff → : o = i2; [|apply ord_inj].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 395)
subgoal 1 (ID 395) is:
i1 = i2
subgoal 2 (ID 396) is:
i1 = i2
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 395)
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
n : nat
IHn : forall f : 'I_n.+1 -> seq T,
uniq (\big[cat/[::]]_(i < n.+1) f i) ->
forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f' : 'I_n.+2 -> seq T
Huniq : uniq (\big[cat/[::]]_(i < n.+2) f' i)
x : T
i1, i2 : 'I_n.+2
Hi1 : x \in f' i1
Hi2 : x \in f' i2
H'i1 : i1 < n.+1
H'i2 : i2 == n.+1
============================
i1 = i2
subgoal 2 (ID 396) is:
i1 = i2
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 395)
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
n : nat
IHn : forall f : 'I_n.+1 -> seq T,
uniq (\big[cat/[::]]_(i < n.+1) f i) ->
forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f' : 'I_n.+2 -> seq T
Huniq : uniq (\big[cat/[::]]_(i < n.+2) f' i)
x : T
i1, i2 : 'I_n.+2
Hi1 : x \in f' i1
Hi2 : x \in f' i2
H'i1 : i1 < n.+1
H'i2 : i2 == n.+1
============================
i1 = i2
----------------------------------------------------------------------------- *)
exfalso.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 748)
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
n : nat
IHn : forall f : 'I_n.+1 -> seq T,
uniq (\big[cat/[::]]_(i < n.+1) f i) ->
forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f' : 'I_n.+2 -> seq T
Huniq : uniq (\big[cat/[::]]_(i < n.+2) f' i)
x : T
i1, i2 : 'I_n.+2
Hi1 : x \in f' i1
Hi2 : x \in f' i2
H'i1 : i1 < n.+1
H'i2 : i2 == n.+1
============================
False
----------------------------------------------------------------------------- *)
move: Huniq; rewrite big_ord_recr cat_uniq ⇒ /andP [_ /andP [H _]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 842)
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
n : nat
IHn : forall f : 'I_n.+1 -> seq T,
uniq (\big[cat/[::]]_(i < n.+1) f i) ->
forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f' : 'I_n.+2 -> seq T
x : T
i1, i2 : 'I_n.+2
Hi1 : x \in f' i1
Hi2 : x \in f' i2
H'i1 : i1 < n.+1
H'i2 : i2 == n.+1
H : ~~
has
(mem
(\big[cat_monoid T/[::]]_(i < n.+1) f'
(widen_ord (m:=n.+2)
(leqnSn n.+1) i)))
(f' ord_max)
============================
False
----------------------------------------------------------------------------- *)
move: H; apply /negP; rewrite Bool.negb_involutive.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 889)
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
n : nat
IHn : forall f : 'I_n.+1 -> seq T,
uniq (\big[cat/[::]]_(i < n.+1) f i) ->
forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f' : 'I_n.+2 -> seq T
x : T
i1, i2 : 'I_n.+2
Hi1 : x \in f' i1
Hi2 : x \in f' i2
H'i1 : i1 < n.+1
H'i2 : i2 == n.+1
============================
has
(mem
(\big[cat_monoid T/[::]]_(i < n.+1) f'
(widen_ord (m:=n.+2)
(leqnSn n.+1) i)))
(f' ord_max)
----------------------------------------------------------------------------- *)
apply /hasP; ∃ x ⇒ /=.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 921)
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
n : nat
IHn : forall f : 'I_n.+1 -> seq T,
uniq (\big[cat/[::]]_(i < n.+1) f i) ->
forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f' : 'I_n.+2 -> seq T
x : T
i1, i2 : 'I_n.+2
Hi1 : x \in f' i1
Hi2 : x \in f' i2
H'i1 : i1 < n.+1
H'i2 : i2 == n.+1
============================
x \in f' ord_max
subgoal 2 (ID 922) is:
x \in \big[cat/[::]]_(i < n.+1) f' (widen_ord (m:=n.+2) (leqnSn n.+1) i)
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 921)
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
n : nat
IHn : forall f : 'I_n.+1 -> seq T,
uniq (\big[cat/[::]]_(i < n.+1) f i) ->
forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f' : 'I_n.+2 -> seq T
x : T
i1, i2 : 'I_n.+2
Hi1 : x \in f' i1
Hi2 : x \in f' i2
H'i1 : i1 < n.+1
H'i2 : i2 == n.+1
============================
x \in f' ord_max
----------------------------------------------------------------------------- *)
set o := ord_max; suff → : o = i2; [by []|].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 929)
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
n : nat
IHn : forall f : 'I_n.+1 -> seq T,
uniq (\big[cat/[::]]_(i < n.+1) f i) ->
forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f' : 'I_n.+2 -> seq T
x : T
i1, i2 : 'I_n.+2
Hi1 : x \in f' i1
Hi2 : x \in f' i2
H'i1 : i1 < n.+1
H'i2 : i2 == n.+1
o := ord_max : 'I_n.+2
============================
o = i2
----------------------------------------------------------------------------- *)
by apply ord_inj; move: H'i2 ⇒ /eqP →.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 922)
subgoal 1 (ID 922) is:
x \in \big[cat/[::]]_(i < n.+1) f' (widen_ord (m:=n.+2) (leqnSn n.+1) i)
subgoal 2 (ID 396) is:
i1 = i2
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 922)
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
n : nat
IHn : forall f : 'I_n.+1 -> seq T,
uniq (\big[cat/[::]]_(i < n.+1) f i) ->
forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f' : 'I_n.+2 -> seq T
x : T
i1, i2 : 'I_n.+2
Hi1 : x \in f' i1
Hi2 : x \in f' i2
H'i1 : i1 < n.+1
H'i2 : i2 == n.+1
============================
x \in \big[cat/[::]]_(i < n.+1) f' (widen_ord (m:=n.+2) (leqnSn n.+1) i)
----------------------------------------------------------------------------- *)
apply (mem_bigcat_ord _ _ (Ordinal H'i1)) ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 981)
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
n : nat
IHn : forall f : 'I_n.+1 -> seq T,
uniq (\big[cat/[::]]_(i < n.+1) f i) ->
forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f' : 'I_n.+2 -> seq T
x : T
i1, i2 : 'I_n.+2
Hi1 : x \in f' i1
Hi2 : x \in f' i2
H'i1 : i1 < n.+1
H'i2 : i2 == n.+1
============================
x
\in f'
(widen_ord (m:=n.+2) (leqnSn n.+1) (Ordinal (n:=n.+1) (m:=i1) H'i1))
----------------------------------------------------------------------------- *)
by set o := widen_ord _ _; suff → : o = i1; [|apply ord_inj].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 396)
subgoal 1 (ID 396) is:
i1 = i2
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 396)
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
n : nat
IHn : forall f : 'I_n.+1 -> seq T,
uniq (\big[cat/[::]]_(i < n.+1) f i) ->
forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f' : 'I_n.+2 -> seq T
Huniq : uniq (\big[cat/[::]]_(i < n.+2) f' i)
x : T
i1, i2 : 'I_n.+2
Hi1 : x \in f' i1
Hi2 : x \in f' i2
H'i1 : i1 < n.+1
H'i2 : i2 < n.+1
============================
i1 = i2
----------------------------------------------------------------------------- *)
move: Huniq; rewrite big_ord_recr cat_uniq ⇒ /andP [Huniq _].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1076)
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
n : nat
IHn : forall f : 'I_n.+1 -> seq T,
uniq (\big[cat/[::]]_(i < n.+1) f i) ->
forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f' : 'I_n.+2 -> seq T
x : T
i1, i2 : 'I_n.+2
Hi1 : x \in f' i1
Hi2 : x \in f' i2
H'i1 : i1 < n.+1
H'i2 : i2 < n.+1
Huniq : uniq
(\big[cat_monoid T/[::]]_(i < n.+1) f'
(widen_ord (m:=n.+2)
(leqnSn n.+1) i))
============================
i1 = i2
----------------------------------------------------------------------------- *)
apply ord_inj; rewrite -(inordK H'i1) -(inordK H'i2); apply f_equal.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1090)
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
n : nat
IHn : forall f : 'I_n.+1 -> seq T,
uniq (\big[cat/[::]]_(i < n.+1) f i) ->
forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f' : 'I_n.+2 -> seq T
x : T
i1, i2 : 'I_n.+2
Hi1 : x \in f' i1
Hi2 : x \in f' i2
H'i1 : i1 < n.+1
H'i2 : i2 < n.+1
Huniq : uniq
(\big[cat_monoid T/[::]]_(i < n.+1) f'
(widen_ord (m:=n.+2)
(leqnSn n.+1) i))
============================
inord i1 = inord i2
----------------------------------------------------------------------------- *)
apply (IHn _ Huniq x).
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1093)
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
n : nat
IHn : forall f : 'I_n.+1 -> seq T,
uniq (\big[cat/[::]]_(i < n.+1) f i) ->
forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f' : 'I_n.+2 -> seq T
x : T
i1, i2 : 'I_n.+2
Hi1 : x \in f' i1
Hi2 : x \in f' i2
H'i1 : i1 < n.+1
H'i2 : i2 < n.+1
Huniq : uniq
(\big[cat_monoid T/[::]]_(i < n.+1) f'
(widen_ord (m:=n.+2)
(leqnSn n.+1) i))
============================
x \in f' (widen_ord (m:=n.+2) (leqnSn n.+1) (inord i1))
subgoal 2 (ID 1094) is:
x \in f' (widen_ord (m:=n.+2) (leqnSn n.+1) (inord i2))
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1093)
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
n : nat
IHn : forall f : 'I_n.+1 -> seq T,
uniq (\big[cat/[::]]_(i < n.+1) f i) ->
forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f' : 'I_n.+2 -> seq T
x : T
i1, i2 : 'I_n.+2
Hi1 : x \in f' i1
Hi2 : x \in f' i2
H'i1 : i1 < n.+1
H'i2 : i2 < n.+1
Huniq : uniq
(\big[cat_monoid T/[::]]_(i < n.+1) f'
(widen_ord (m:=n.+2)
(leqnSn n.+1) i))
============================
x \in f' (widen_ord (m:=n.+2) (leqnSn n.+1) (inord i1))
----------------------------------------------------------------------------- *)
set i1' := widen_ord _ _; suff → : i1' = i1; [by []|].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1106)
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
n : nat
IHn : forall f : 'I_n.+1 -> seq T,
uniq (\big[cat/[::]]_(i < n.+1) f i) ->
forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f' : 'I_n.+2 -> seq T
x : T
i1, i2 : 'I_n.+2
Hi1 : x \in f' i1
Hi2 : x \in f' i2
H'i1 : i1 < n.+1
H'i2 : i2 < n.+1
Huniq : uniq
(\big[cat_monoid T/[::]]_(i < n.+1) f'
(widen_ord (m:=n.+2)
(leqnSn n.+1) i))
i1' := widen_ord (m:=n.+2) (leqnSn n.+1) (inord i1) : 'I_n.+2
============================
i1' = i1
----------------------------------------------------------------------------- *)
by apply ord_inj; rewrite /= inordK.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1094)
subgoal 1 (ID 1094) is:
x \in f' (widen_ord (m:=n.+2) (leqnSn n.+1) (inord i2))
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1094)
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
n : nat
IHn : forall f : 'I_n.+1 -> seq T,
uniq (\big[cat/[::]]_(i < n.+1) f i) ->
forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f' : 'I_n.+2 -> seq T
x : T
i1, i2 : 'I_n.+2
Hi1 : x \in f' i1
Hi2 : x \in f' i2
H'i1 : i1 < n.+1
H'i2 : i2 < n.+1
Huniq : uniq
(\big[cat_monoid T/[::]]_(i < n.+1) f'
(widen_ord (m:=n.+2)
(leqnSn n.+1) i))
============================
x \in f' (widen_ord (m:=n.+2) (leqnSn n.+1) (inord i2))
----------------------------------------------------------------------------- *)
set i2' := widen_ord _ _; suff → : i2' = i2; [by []|].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1130)
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
n : nat
IHn : forall f : 'I_n.+1 -> seq T,
uniq (\big[cat/[::]]_(i < n.+1) f i) ->
forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f' : 'I_n.+2 -> seq T
x : T
i1, i2 : 'I_n.+2
Hi1 : x \in f' i1
Hi2 : x \in f' i2
H'i1 : i1 < n.+1
H'i2 : i2 < n.+1
Huniq : uniq
(\big[cat_monoid T/[::]]_(i < n.+1) f'
(widen_ord (m:=n.+2)
(leqnSn n.+1) i))
i2' := widen_ord (m:=n.+2) (leqnSn n.+1) (inord i2) : 'I_n.+2
============================
i2' = i2
----------------------------------------------------------------------------- *)
by apply ord_inj; rewrite /= inordK.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End BigCatDistinctElements.
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 cat_filter_eq_filter_cat:
∀ {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].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 36)
T : eqType
f : nat -> seq T
============================
forall (X : Type) (F : nat -> seq X) (P : X -> bool) (t1 t2 : nat),
[seq x <- \big[cat/[::]]_(t1 <= t < t2) F t | P x] =
\big[cat/[::]]_(t1 <= t < t2) [seq x <- F t | P x]
----------------------------------------------------------------------------- *)
Proof.
intros.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 41)
T : eqType
f : nat -> seq T
X : Type
F : nat -> seq X
P : X -> bool
t1, t2 : nat
============================
[seq x <- \big[cat/[::]]_(t1 <= t < t2) F t | P x] =
\big[cat/[::]]_(t1 <= t < t2) [seq x <- F t | P x]
----------------------------------------------------------------------------- *)
specialize (leq_total t1 t2) ⇒ /orP [T1_LT | T2_LT].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 86)
T : eqType
f : nat -> seq T
X : Type
F : nat -> seq X
P : X -> bool
t1, t2 : nat
T1_LT : t1 <= t2
============================
[seq x <- \big[cat/[::]]_(t1 <= t < t2) F t | P x] =
\big[cat/[::]]_(t1 <= t < t2) [seq x <- F t | P x]
subgoal 2 (ID 87) is:
[seq x <- \big[cat/[::]]_(t1 <= t < t2) F t | P x] =
\big[cat/[::]]_(t1 <= t < t2) [seq x <- F t | P x]
----------------------------------------------------------------------------- *)
+ have EX: ∃ Δ, t2 = t1 + Δ by ∃ (t2 - t1); ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 235)
T : eqType
f : nat -> seq T
X : Type
F : nat -> seq X
P : X -> bool
t1, t2 : nat
T1_LT : t1 <= t2
EX : exists Δ : nat, t2 = t1 + Δ
============================
[seq x <- \big[cat/[::]]_(t1 <= t < t2) F t | P x] =
\big[cat/[::]]_(t1 <= t < t2) [seq x <- F t | P x]
subgoal 2 (ID 87) is:
[seq x <- \big[cat/[::]]_(t1 <= t < t2) F t | P x] =
\big[cat/[::]]_(t1 <= t < t2) [seq x <- F t | P x]
----------------------------------------------------------------------------- *)
move: EX ⇒ [Δ EQ]; subst t2.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 254)
T : eqType
f : nat -> seq T
X : Type
F : nat -> seq X
P : X -> bool
t1, Δ : nat
T1_LT : t1 <= t1 + Δ
============================
[seq x <- \big[cat/[::]]_(t1 <= t < t1 + Δ) F t | P x] =
\big[cat/[::]]_(t1 <= t < t1 + Δ) [seq x <- F t | P x]
subgoal 2 (ID 87) is:
[seq x <- \big[cat/[::]]_(t1 <= t < t2) F t | P x] =
\big[cat/[::]]_(t1 <= t < t2) [seq x <- F t | P x]
----------------------------------------------------------------------------- *)
induction Δ.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 263)
T : eqType
f : nat -> seq T
X : Type
F : nat -> seq X
P : X -> bool
t1 : nat
T1_LT : t1 <= t1 + 0
============================
[seq x <- \big[cat/[::]]_(t1 <= t < t1 + 0) F t | P x] =
\big[cat/[::]]_(t1 <= t < t1 + 0) [seq x <- F t | P x]
subgoal 2 (ID 267) is:
[seq x <- \big[cat/[::]]_(t1 <= t < t1 + Δ.+1) F t | P x] =
\big[cat/[::]]_(t1 <= t < t1 + Δ.+1) [seq x <- F t | P x]
subgoal 3 (ID 87) is:
[seq x <- \big[cat/[::]]_(t1 <= t < t2) F t | P x] =
\big[cat/[::]]_(t1 <= t < t2) [seq x <- F t | P x]
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 263)
T : eqType
f : nat -> seq T
X : Type
F : nat -> seq X
P : X -> bool
t1 : nat
T1_LT : t1 <= t1 + 0
============================
[seq x <- \big[cat/[::]]_(t1 <= t < t1 + 0) F t | P x] =
\big[cat/[::]]_(t1 <= t < t1 + 0) [seq x <- F t | P x]
----------------------------------------------------------------------------- *)
now rewrite addn0 !big_geq ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 267)
subgoal 1 (ID 267) is:
[seq x <- \big[cat/[::]]_(t1 <= t < t1 + Δ.+1) F t | P x] =
\big[cat/[::]]_(t1 <= t < t1 + Δ.+1) [seq x <- F t | P x]
subgoal 2 (ID 87) is:
[seq x <- \big[cat/[::]]_(t1 <= t < t2) F t | P x] =
\big[cat/[::]]_(t1 <= t < t2) [seq x <- F t | P x]
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 267)
T : eqType
f : nat -> seq T
X : Type
F : nat -> seq X
P : X -> bool
t1, Δ : nat
T1_LT : t1 <= t1 + Δ.+1
IHΔ : t1 <= t1 + Δ ->
[seq x <- \big[cat/[::]]_(t1 <= t < t1 + Δ) F t | P x] =
\big[cat/[::]]_(t1 <= t < t1 + Δ) [seq x <- F t | P x]
============================
[seq x <- \big[cat/[::]]_(t1 <= t < t1 + Δ.+1) F t | P x] =
\big[cat/[::]]_(t1 <= t < t1 + Δ.+1) [seq x <- F t | P x]
subgoal 2 (ID 87) is:
[seq x <- \big[cat/[::]]_(t1 <= t < t2) F t | P x] =
\big[cat/[::]]_(t1 <= t < t2) [seq x <- F t | P x]
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 267)
T : eqType
f : nat -> seq T
X : Type
F : nat -> seq X
P : X -> bool
t1, Δ : nat
T1_LT : t1 <= t1 + Δ.+1
IHΔ : t1 <= t1 + Δ ->
[seq x <- \big[cat/[::]]_(t1 <= t < t1 + Δ) F t | P x] =
\big[cat/[::]]_(t1 <= t < t1 + Δ) [seq x <- F t | P x]
============================
[seq x <- \big[cat/[::]]_(t1 <= t < t1 + Δ.+1) F t | P x] =
\big[cat/[::]]_(t1 <= t < t1 + Δ.+1) [seq x <- F t | P x]
----------------------------------------------------------------------------- *)
rewrite addnS !big_nat_recr ⇒ //=; try by rewrite leq_addr.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 366)
T : eqType
f : nat -> seq T
X : Type
F : nat -> seq X
P : X -> bool
t1, Δ : nat
T1_LT : t1 <= t1 + Δ.+1
IHΔ : t1 <= t1 + Δ ->
[seq x <- \big[cat/[::]]_(t1 <= t < t1 + Δ) F t | P x] =
\big[cat/[::]]_(t1 <= t < t1 + Δ) [seq x <- F t | P x]
============================
[seq x <- \big[cat/[::]]_(t1 <= i < t1 + Δ) F i ++ F (t1 + Δ) | P x] =
\big[cat/[::]]_(t1 <= i < t1 + Δ) [seq x <- F i | P x] ++
[seq x <- F (t1 + Δ) | P x]
----------------------------------------------------------------------------- *)
rewrite filter_cat IHΔ ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 454)
T : eqType
f : nat -> seq T
X : Type
F : nat -> seq X
P : X -> bool
t1, Δ : nat
T1_LT : t1 <= t1 + Δ.+1
IHΔ : t1 <= t1 + Δ ->
[seq x <- \big[cat/[::]]_(t1 <= t < t1 + Δ) F t | P x] =
\big[cat/[::]]_(t1 <= t < t1 + Δ) [seq x <- F t | P x]
============================
t1 <= t1 + Δ
----------------------------------------------------------------------------- *)
now ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 87)
subgoal 1 (ID 87) is:
[seq x <- \big[cat/[::]]_(t1 <= t < t2) F t | P x] =
\big[cat/[::]]_(t1 <= t < t2) [seq x <- F t | P x]
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 87)
T : eqType
f : nat -> seq T
X : Type
F : nat -> seq X
P : X -> bool
t1, t2 : nat
T2_LT : t2 <= t1
============================
[seq x <- \big[cat/[::]]_(t1 <= t < t2) F t | P x] =
\big[cat/[::]]_(t1 <= t < t2) [seq x <- F t | P x]
----------------------------------------------------------------------------- *)
+ now rewrite !big_geq ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
∀ {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].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 36)
T : eqType
f : nat -> seq T
============================
forall (X : Type) (F : nat -> seq X) (P : X -> bool) (t1 t2 : nat),
[seq x <- \big[cat/[::]]_(t1 <= t < t2) F t | P x] =
\big[cat/[::]]_(t1 <= t < t2) [seq x <- F t | P x]
----------------------------------------------------------------------------- *)
Proof.
intros.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 41)
T : eqType
f : nat -> seq T
X : Type
F : nat -> seq X
P : X -> bool
t1, t2 : nat
============================
[seq x <- \big[cat/[::]]_(t1 <= t < t2) F t | P x] =
\big[cat/[::]]_(t1 <= t < t2) [seq x <- F t | P x]
----------------------------------------------------------------------------- *)
specialize (leq_total t1 t2) ⇒ /orP [T1_LT | T2_LT].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 86)
T : eqType
f : nat -> seq T
X : Type
F : nat -> seq X
P : X -> bool
t1, t2 : nat
T1_LT : t1 <= t2
============================
[seq x <- \big[cat/[::]]_(t1 <= t < t2) F t | P x] =
\big[cat/[::]]_(t1 <= t < t2) [seq x <- F t | P x]
subgoal 2 (ID 87) is:
[seq x <- \big[cat/[::]]_(t1 <= t < t2) F t | P x] =
\big[cat/[::]]_(t1 <= t < t2) [seq x <- F t | P x]
----------------------------------------------------------------------------- *)
+ have EX: ∃ Δ, t2 = t1 + Δ by ∃ (t2 - t1); ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 235)
T : eqType
f : nat -> seq T
X : Type
F : nat -> seq X
P : X -> bool
t1, t2 : nat
T1_LT : t1 <= t2
EX : exists Δ : nat, t2 = t1 + Δ
============================
[seq x <- \big[cat/[::]]_(t1 <= t < t2) F t | P x] =
\big[cat/[::]]_(t1 <= t < t2) [seq x <- F t | P x]
subgoal 2 (ID 87) is:
[seq x <- \big[cat/[::]]_(t1 <= t < t2) F t | P x] =
\big[cat/[::]]_(t1 <= t < t2) [seq x <- F t | P x]
----------------------------------------------------------------------------- *)
move: EX ⇒ [Δ EQ]; subst t2.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 254)
T : eqType
f : nat -> seq T
X : Type
F : nat -> seq X
P : X -> bool
t1, Δ : nat
T1_LT : t1 <= t1 + Δ
============================
[seq x <- \big[cat/[::]]_(t1 <= t < t1 + Δ) F t | P x] =
\big[cat/[::]]_(t1 <= t < t1 + Δ) [seq x <- F t | P x]
subgoal 2 (ID 87) is:
[seq x <- \big[cat/[::]]_(t1 <= t < t2) F t | P x] =
\big[cat/[::]]_(t1 <= t < t2) [seq x <- F t | P x]
----------------------------------------------------------------------------- *)
induction Δ.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 263)
T : eqType
f : nat -> seq T
X : Type
F : nat -> seq X
P : X -> bool
t1 : nat
T1_LT : t1 <= t1 + 0
============================
[seq x <- \big[cat/[::]]_(t1 <= t < t1 + 0) F t | P x] =
\big[cat/[::]]_(t1 <= t < t1 + 0) [seq x <- F t | P x]
subgoal 2 (ID 267) is:
[seq x <- \big[cat/[::]]_(t1 <= t < t1 + Δ.+1) F t | P x] =
\big[cat/[::]]_(t1 <= t < t1 + Δ.+1) [seq x <- F t | P x]
subgoal 3 (ID 87) is:
[seq x <- \big[cat/[::]]_(t1 <= t < t2) F t | P x] =
\big[cat/[::]]_(t1 <= t < t2) [seq x <- F t | P x]
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 263)
T : eqType
f : nat -> seq T
X : Type
F : nat -> seq X
P : X -> bool
t1 : nat
T1_LT : t1 <= t1 + 0
============================
[seq x <- \big[cat/[::]]_(t1 <= t < t1 + 0) F t | P x] =
\big[cat/[::]]_(t1 <= t < t1 + 0) [seq x <- F t | P x]
----------------------------------------------------------------------------- *)
now rewrite addn0 !big_geq ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 267)
subgoal 1 (ID 267) is:
[seq x <- \big[cat/[::]]_(t1 <= t < t1 + Δ.+1) F t | P x] =
\big[cat/[::]]_(t1 <= t < t1 + Δ.+1) [seq x <- F t | P x]
subgoal 2 (ID 87) is:
[seq x <- \big[cat/[::]]_(t1 <= t < t2) F t | P x] =
\big[cat/[::]]_(t1 <= t < t2) [seq x <- F t | P x]
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 267)
T : eqType
f : nat -> seq T
X : Type
F : nat -> seq X
P : X -> bool
t1, Δ : nat
T1_LT : t1 <= t1 + Δ.+1
IHΔ : t1 <= t1 + Δ ->
[seq x <- \big[cat/[::]]_(t1 <= t < t1 + Δ) F t | P x] =
\big[cat/[::]]_(t1 <= t < t1 + Δ) [seq x <- F t | P x]
============================
[seq x <- \big[cat/[::]]_(t1 <= t < t1 + Δ.+1) F t | P x] =
\big[cat/[::]]_(t1 <= t < t1 + Δ.+1) [seq x <- F t | P x]
subgoal 2 (ID 87) is:
[seq x <- \big[cat/[::]]_(t1 <= t < t2) F t | P x] =
\big[cat/[::]]_(t1 <= t < t2) [seq x <- F t | P x]
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 267)
T : eqType
f : nat -> seq T
X : Type
F : nat -> seq X
P : X -> bool
t1, Δ : nat
T1_LT : t1 <= t1 + Δ.+1
IHΔ : t1 <= t1 + Δ ->
[seq x <- \big[cat/[::]]_(t1 <= t < t1 + Δ) F t | P x] =
\big[cat/[::]]_(t1 <= t < t1 + Δ) [seq x <- F t | P x]
============================
[seq x <- \big[cat/[::]]_(t1 <= t < t1 + Δ.+1) F t | P x] =
\big[cat/[::]]_(t1 <= t < t1 + Δ.+1) [seq x <- F t | P x]
----------------------------------------------------------------------------- *)
rewrite addnS !big_nat_recr ⇒ //=; try by rewrite leq_addr.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 366)
T : eqType
f : nat -> seq T
X : Type
F : nat -> seq X
P : X -> bool
t1, Δ : nat
T1_LT : t1 <= t1 + Δ.+1
IHΔ : t1 <= t1 + Δ ->
[seq x <- \big[cat/[::]]_(t1 <= t < t1 + Δ) F t | P x] =
\big[cat/[::]]_(t1 <= t < t1 + Δ) [seq x <- F t | P x]
============================
[seq x <- \big[cat/[::]]_(t1 <= i < t1 + Δ) F i ++ F (t1 + Δ) | P x] =
\big[cat/[::]]_(t1 <= i < t1 + Δ) [seq x <- F i | P x] ++
[seq x <- F (t1 + Δ) | P x]
----------------------------------------------------------------------------- *)
rewrite filter_cat IHΔ ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 454)
T : eqType
f : nat -> seq T
X : Type
F : nat -> seq X
P : X -> bool
t1, Δ : nat
T1_LT : t1 <= t1 + Δ.+1
IHΔ : t1 <= t1 + Δ ->
[seq x <- \big[cat/[::]]_(t1 <= t < t1 + Δ) F t | P x] =
\big[cat/[::]]_(t1 <= t < t1 + Δ) [seq x <- F t | P x]
============================
t1 <= t1 + Δ
----------------------------------------------------------------------------- *)
now ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 87)
subgoal 1 (ID 87) is:
[seq x <- \big[cat/[::]]_(t1 <= t < t2) F t | P x] =
\big[cat/[::]]_(t1 <= t < t2) [seq x <- F t | P x]
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 87)
T : eqType
f : nat -> seq T
X : Type
F : nat -> seq X
P : X -> bool
t1, t2 : nat
T2_LT : t2 <= t1
============================
[seq x <- \big[cat/[::]]_(t1 <= t < t2) F t | P x] =
\big[cat/[::]]_(t1 <= t < t2) [seq x <- F t | P x]
----------------------------------------------------------------------------- *)
+ now rewrite !big_geq ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
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).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 51)
T : eqType
f : nat -> seq T
============================
forall (X : Type) (F : nat -> seq X) (t1 t2 : nat),
\sum_(t1 <= t < t2) size (F t) = size (\big[cat/[::]]_(t1 <= t < t2) F t)
----------------------------------------------------------------------------- *)
Proof.
intros.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 55)
T : eqType
f : nat -> seq T
X : Type
F : nat -> seq X
t1, t2 : nat
============================
\sum_(t1 <= t < t2) size (F t) = size (\big[cat/[::]]_(t1 <= t < t2) F t)
----------------------------------------------------------------------------- *)
specialize (leq_total t1 t2) ⇒ /orP [T1_LT | T2_LT].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 100)
T : eqType
f : nat -> seq T
X : Type
F : nat -> seq X
t1, t2 : nat
T1_LT : t1 <= t2
============================
\sum_(t1 <= t < t2) size (F t) = size (\big[cat/[::]]_(t1 <= t < t2) F t)
subgoal 2 (ID 101) is:
\sum_(t1 <= t < t2) size (F t) = size (\big[cat/[::]]_(t1 <= t < t2) F t)
----------------------------------------------------------------------------- *)
+ have EX: ∃ Δ, t2 = t1 + Δ by ∃ (t2 - t1); ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 249)
T : eqType
f : nat -> seq T
X : Type
F : nat -> seq X
t1, t2 : nat
T1_LT : t1 <= t2
EX : exists Δ : nat, t2 = t1 + Δ
============================
\sum_(t1 <= t < t2) size (F t) = size (\big[cat/[::]]_(t1 <= t < t2) F t)
subgoal 2 (ID 101) is:
\sum_(t1 <= t < t2) size (F t) = size (\big[cat/[::]]_(t1 <= t < t2) F t)
----------------------------------------------------------------------------- *)
move: EX ⇒ [Δ EQ]; subst t2.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 268)
T : eqType
f : nat -> seq T
X : Type
F : nat -> seq X
t1, Δ : nat
T1_LT : t1 <= t1 + Δ
============================
\sum_(t1 <= t < t1 + Δ) size (F t) =
size (\big[cat/[::]]_(t1 <= t < t1 + Δ) F t)
subgoal 2 (ID 101) is:
\sum_(t1 <= t < t2) size (F t) = size (\big[cat/[::]]_(t1 <= t < t2) F t)
----------------------------------------------------------------------------- *)
induction Δ.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 277)
T : eqType
f : nat -> seq T
X : Type
F : nat -> seq X
t1 : nat
T1_LT : t1 <= t1 + 0
============================
\sum_(t1 <= t < t1 + 0) size (F t) =
size (\big[cat/[::]]_(t1 <= t < t1 + 0) F t)
subgoal 2 (ID 281) is:
\sum_(t1 <= t < t1 + Δ.+1) size (F t) =
size (\big[cat/[::]]_(t1 <= t < t1 + Δ.+1) F t)
subgoal 3 (ID 101) is:
\sum_(t1 <= t < t2) size (F t) = size (\big[cat/[::]]_(t1 <= t < t2) F t)
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 277)
T : eqType
f : nat -> seq T
X : Type
F : nat -> seq X
t1 : nat
T1_LT : t1 <= t1 + 0
============================
\sum_(t1 <= t < t1 + 0) size (F t) =
size (\big[cat/[::]]_(t1 <= t < t1 + 0) F t)
----------------------------------------------------------------------------- *)
now rewrite addn0 !big_geq ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 281)
subgoal 1 (ID 281) is:
\sum_(t1 <= t < t1 + Δ.+1) size (F t) =
size (\big[cat/[::]]_(t1 <= t < t1 + Δ.+1) F t)
subgoal 2 (ID 101) is:
\sum_(t1 <= t < t2) size (F t) = size (\big[cat/[::]]_(t1 <= t < t2) F t)
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 281)
T : eqType
f : nat -> seq T
X : Type
F : nat -> seq X
t1, Δ : nat
T1_LT : t1 <= t1 + Δ.+1
IHΔ : t1 <= t1 + Δ ->
\sum_(t1 <= t < t1 + Δ) size (F t) =
size (\big[cat/[::]]_(t1 <= t < t1 + Δ) F t)
============================
\sum_(t1 <= t < t1 + Δ.+1) size (F t) =
size (\big[cat/[::]]_(t1 <= t < t1 + Δ.+1) F t)
subgoal 2 (ID 101) is:
\sum_(t1 <= t < t2) size (F t) = size (\big[cat/[::]]_(t1 <= t < t2) F t)
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 281)
T : eqType
f : nat -> seq T
X : Type
F : nat -> seq X
t1, Δ : nat
T1_LT : t1 <= t1 + Δ.+1
IHΔ : t1 <= t1 + Δ ->
\sum_(t1 <= t < t1 + Δ) size (F t) =
size (\big[cat/[::]]_(t1 <= t < t1 + Δ) F t)
============================
\sum_(t1 <= t < t1 + Δ.+1) size (F t) =
size (\big[cat/[::]]_(t1 <= t < t1 + Δ.+1) F t)
----------------------------------------------------------------------------- *)
rewrite addnS !big_nat_recr ⇒ //=; try by rewrite leq_addr.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 379)
T : eqType
f : nat -> seq T
X : Type
F : nat -> seq X
t1, Δ : nat
T1_LT : t1 <= t1 + Δ.+1
IHΔ : t1 <= t1 + Δ ->
\sum_(t1 <= t < t1 + Δ) size (F t) =
size (\big[cat/[::]]_(t1 <= t < t1 + Δ) F t)
============================
\sum_(t1 <= i < t1 + Δ) size (F i) + size (F (t1 + Δ)) =
size (\big[cat/[::]]_(t1 <= i < t1 + Δ) F i ++ F (t1 + Δ))
----------------------------------------------------------------------------- *)
rewrite size_cat IHΔ ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 466)
T : eqType
f : nat -> seq T
X : Type
F : nat -> seq X
t1, Δ : nat
T1_LT : t1 <= t1 + Δ.+1
IHΔ : t1 <= t1 + Δ ->
\sum_(t1 <= t < t1 + Δ) size (F t) =
size (\big[cat/[::]]_(t1 <= t < t1 + Δ) F t)
============================
t1 <= t1 + Δ
----------------------------------------------------------------------------- *)
now ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 101)
subgoal 1 (ID 101) is:
\sum_(t1 <= t < t2) size (F t) = size (\big[cat/[::]]_(t1 <= t < t2) F t)
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 101)
T : eqType
f : nat -> seq T
X : Type
F : nat -> seq X
t1, t2 : nat
T2_LT : t2 <= t1
============================
\sum_(t1 <= t < t2) size (F t) = size (\big[cat/[::]]_(t1 <= t < t2) F t)
----------------------------------------------------------------------------- *)
+ now rewrite !big_geq ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End BigCatLemmas.
∀ {X : Type} (F : nat → seq X) (t1 t2 : nat),
\sum_(t1 ≤ t < t2) size (F t) =
size (\cat_(t1 ≤ t < t2) F t).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 51)
T : eqType
f : nat -> seq T
============================
forall (X : Type) (F : nat -> seq X) (t1 t2 : nat),
\sum_(t1 <= t < t2) size (F t) = size (\big[cat/[::]]_(t1 <= t < t2) F t)
----------------------------------------------------------------------------- *)
Proof.
intros.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 55)
T : eqType
f : nat -> seq T
X : Type
F : nat -> seq X
t1, t2 : nat
============================
\sum_(t1 <= t < t2) size (F t) = size (\big[cat/[::]]_(t1 <= t < t2) F t)
----------------------------------------------------------------------------- *)
specialize (leq_total t1 t2) ⇒ /orP [T1_LT | T2_LT].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 100)
T : eqType
f : nat -> seq T
X : Type
F : nat -> seq X
t1, t2 : nat
T1_LT : t1 <= t2
============================
\sum_(t1 <= t < t2) size (F t) = size (\big[cat/[::]]_(t1 <= t < t2) F t)
subgoal 2 (ID 101) is:
\sum_(t1 <= t < t2) size (F t) = size (\big[cat/[::]]_(t1 <= t < t2) F t)
----------------------------------------------------------------------------- *)
+ have EX: ∃ Δ, t2 = t1 + Δ by ∃ (t2 - t1); ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 249)
T : eqType
f : nat -> seq T
X : Type
F : nat -> seq X
t1, t2 : nat
T1_LT : t1 <= t2
EX : exists Δ : nat, t2 = t1 + Δ
============================
\sum_(t1 <= t < t2) size (F t) = size (\big[cat/[::]]_(t1 <= t < t2) F t)
subgoal 2 (ID 101) is:
\sum_(t1 <= t < t2) size (F t) = size (\big[cat/[::]]_(t1 <= t < t2) F t)
----------------------------------------------------------------------------- *)
move: EX ⇒ [Δ EQ]; subst t2.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 268)
T : eqType
f : nat -> seq T
X : Type
F : nat -> seq X
t1, Δ : nat
T1_LT : t1 <= t1 + Δ
============================
\sum_(t1 <= t < t1 + Δ) size (F t) =
size (\big[cat/[::]]_(t1 <= t < t1 + Δ) F t)
subgoal 2 (ID 101) is:
\sum_(t1 <= t < t2) size (F t) = size (\big[cat/[::]]_(t1 <= t < t2) F t)
----------------------------------------------------------------------------- *)
induction Δ.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 277)
T : eqType
f : nat -> seq T
X : Type
F : nat -> seq X
t1 : nat
T1_LT : t1 <= t1 + 0
============================
\sum_(t1 <= t < t1 + 0) size (F t) =
size (\big[cat/[::]]_(t1 <= t < t1 + 0) F t)
subgoal 2 (ID 281) is:
\sum_(t1 <= t < t1 + Δ.+1) size (F t) =
size (\big[cat/[::]]_(t1 <= t < t1 + Δ.+1) F t)
subgoal 3 (ID 101) is:
\sum_(t1 <= t < t2) size (F t) = size (\big[cat/[::]]_(t1 <= t < t2) F t)
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 277)
T : eqType
f : nat -> seq T
X : Type
F : nat -> seq X
t1 : nat
T1_LT : t1 <= t1 + 0
============================
\sum_(t1 <= t < t1 + 0) size (F t) =
size (\big[cat/[::]]_(t1 <= t < t1 + 0) F t)
----------------------------------------------------------------------------- *)
now rewrite addn0 !big_geq ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 281)
subgoal 1 (ID 281) is:
\sum_(t1 <= t < t1 + Δ.+1) size (F t) =
size (\big[cat/[::]]_(t1 <= t < t1 + Δ.+1) F t)
subgoal 2 (ID 101) is:
\sum_(t1 <= t < t2) size (F t) = size (\big[cat/[::]]_(t1 <= t < t2) F t)
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 281)
T : eqType
f : nat -> seq T
X : Type
F : nat -> seq X
t1, Δ : nat
T1_LT : t1 <= t1 + Δ.+1
IHΔ : t1 <= t1 + Δ ->
\sum_(t1 <= t < t1 + Δ) size (F t) =
size (\big[cat/[::]]_(t1 <= t < t1 + Δ) F t)
============================
\sum_(t1 <= t < t1 + Δ.+1) size (F t) =
size (\big[cat/[::]]_(t1 <= t < t1 + Δ.+1) F t)
subgoal 2 (ID 101) is:
\sum_(t1 <= t < t2) size (F t) = size (\big[cat/[::]]_(t1 <= t < t2) F t)
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 281)
T : eqType
f : nat -> seq T
X : Type
F : nat -> seq X
t1, Δ : nat
T1_LT : t1 <= t1 + Δ.+1
IHΔ : t1 <= t1 + Δ ->
\sum_(t1 <= t < t1 + Δ) size (F t) =
size (\big[cat/[::]]_(t1 <= t < t1 + Δ) F t)
============================
\sum_(t1 <= t < t1 + Δ.+1) size (F t) =
size (\big[cat/[::]]_(t1 <= t < t1 + Δ.+1) F t)
----------------------------------------------------------------------------- *)
rewrite addnS !big_nat_recr ⇒ //=; try by rewrite leq_addr.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 379)
T : eqType
f : nat -> seq T
X : Type
F : nat -> seq X
t1, Δ : nat
T1_LT : t1 <= t1 + Δ.+1
IHΔ : t1 <= t1 + Δ ->
\sum_(t1 <= t < t1 + Δ) size (F t) =
size (\big[cat/[::]]_(t1 <= t < t1 + Δ) F t)
============================
\sum_(t1 <= i < t1 + Δ) size (F i) + size (F (t1 + Δ)) =
size (\big[cat/[::]]_(t1 <= i < t1 + Δ) F i ++ F (t1 + Δ))
----------------------------------------------------------------------------- *)
rewrite size_cat IHΔ ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 466)
T : eqType
f : nat -> seq T
X : Type
F : nat -> seq X
t1, Δ : nat
T1_LT : t1 <= t1 + Δ.+1
IHΔ : t1 <= t1 + Δ ->
\sum_(t1 <= t < t1 + Δ) size (F t) =
size (\big[cat/[::]]_(t1 <= t < t1 + Δ) F t)
============================
t1 <= t1 + Δ
----------------------------------------------------------------------------- *)
now ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 101)
subgoal 1 (ID 101) is:
\sum_(t1 <= t < t2) size (F t) = size (\big[cat/[::]]_(t1 <= t < t2) F t)
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 101)
T : eqType
f : nat -> seq T
X : Type
F : nat -> seq X
t1, t2 : nat
T2_LT : t2 <= t1
============================
\sum_(t1 <= t < t2) size (F t) = size (\big[cat/[::]]_(t1 <= t < t2) F t)
----------------------------------------------------------------------------- *)
+ now rewrite !big_geq ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End BigCatLemmas.