Library prosa.util.bigcat
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.
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).
Proof.
intros x m n j LE IN; move: LE ⇒ /andP [LE LE0].
rewrite → big_cat_nat with (n := j); simpl; [| by ins | by apply ltnW].
rewrite mem_cat; apply/orP; right.
destruct n; first by rewrite ltn0 in LE0.
rewrite big_nat_recl; last by ins.
by rewrite mem_cat; apply/orP; left.
Qed.
∀ x m n j,
m ≤ j < n →
x \in f j →
x \in \cat_(m ≤ i < n) (f i).
Proof.
intros x m n j LE IN; move: LE ⇒ /andP [LE LE0].
rewrite → big_cat_nat with (n := j); simpl; [| by ins | by apply ltnW].
rewrite mem_cat; apply/orP; right.
destruct n; first by rewrite ltn0 in LE0.
rewrite big_nat_recl; last by ins.
by rewrite mem_cat; apply/orP; left.
Qed.
Conversely, we prove that any element belonging to a concatenation of sequences
must come from one of the sequences.
Lemma mem_bigcat_nat_exists:
∀ x m n,
x \in \cat_(m ≤ i < n) (f i) →
∃ i,
x \in f i ∧ m ≤ i < n.
Proof.
intros x m n IN.
induction n; first by rewrite big_geq // in IN.
destruct (leqP m n); last by rewrite big_geq ?in_nil // ltnW in IN.
rewrite big_nat_recr // /= mem_cat in IN.
move: IN ⇒ /orP [HEAD | TAIL].
{
apply IHn in HEAD; destruct HEAD; ∃ x0. move: H ⇒ [H /andP [H0 H1]].
split; first by done.
by apply/andP; split; [by done | by apply ltnW]. }
{
∃ n; split; first by done.
apply/andP; split; [by done | by apply ltnSn]. }
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).
Proof.
move⇒ x; elim⇒ [//|n IHn] j f' Hj Hx.
rewrite big_ord_recr /= mem_cat; apply /orP.
move: Hj; rewrite ltnS leq_eqVlt ⇒ /orP [/eqP Hj|Hj].
{ by right; rewrite (_ : ord_max = j); [|apply ord_inj]. }
left.
apply (IHn (Ordinal Hj)); [by []|].
by set j' := widen_ord _ _; have → : j' = j; [apply ord_inj|].
Qed.
End BigCatElements.
∀ x m n,
x \in \cat_(m ≤ i < n) (f i) →
∃ i,
x \in f i ∧ m ≤ i < n.
Proof.
intros x m n IN.
induction n; first by rewrite big_geq // in IN.
destruct (leqP m n); last by rewrite big_geq ?in_nil // ltnW in IN.
rewrite big_nat_recr // /= mem_cat in IN.
move: IN ⇒ /orP [HEAD | TAIL].
{
apply IHn in HEAD; destruct HEAD; ∃ x0. move: H ⇒ [H /andP [H0 H1]].
split; first by done.
by apply/andP; split; [by done | by apply ltnW]. }
{
∃ n; split; first by done.
apply/andP; split; [by done | by apply ltnSn]. }
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).
Proof.
move⇒ x; elim⇒ [//|n IHn] j f' Hj Hx.
rewrite big_ord_recr /= mem_cat; apply /orP.
move: Hj; rewrite ltnS leq_eqVlt ⇒ /orP [/eqP Hj|Hj].
{ by right; rewrite (_ : ord_max = j); [|apply ord_inj]. }
left.
apply (IHn (Ordinal Hj)); [by []|].
by set j' := widen_ord _ _; have → : j' = j; [apply ord_inj|].
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)).
Proof.
intros n1 n2.
case (leqP n1 n2) ⇒ [LE | GT]; last by rewrite big_geq // ltnW.
rewrite -[n2](addKn n1).
rewrite -addnBA //; set delta := n2 - n1.
induction delta; first by rewrite addn0 big_geq.
rewrite addnS big_nat_recr /=; last by apply leq_addr.
rewrite cat_uniq; apply/andP; split; first by apply IHdelta.
apply /andP; split; last by apply H_uniq_seq.
rewrite -all_predC; apply/allP; intros x INx.
simpl; apply/negP; unfold not; intro BUG.
apply mem_bigcat_nat_exists in BUG.
move: BUG ⇒ [i [IN /andP [_ LTi]]].
apply H_no_elements_in_common with (i1 := i) in INx; last by done.
by rewrite INx ltnn in LTi.
Qed.
∀ n1 n2,
uniq (\cat_(n1 ≤ i < n2) (f i)).
Proof.
intros n1 n2.
case (leqP n1 n2) ⇒ [LE | GT]; last by rewrite big_geq // ltnW.
rewrite -[n2](addKn n1).
rewrite -addnBA //; set delta := n2 - n1.
induction delta; first by rewrite addn0 big_geq.
rewrite addnS big_nat_recr /=; last by apply leq_addr.
rewrite cat_uniq; apply/andP; split; first by apply IHdelta.
apply /andP; split; last by apply H_uniq_seq.
rewrite -all_predC; apply/allP; intros x INx.
simpl; apply/negP; unfold not; intro BUG.
apply mem_bigcat_nat_exists in BUG.
move: BUG ⇒ [i [IN /andP [_ LTi]]].
apply H_no_elements_in_common with (i1 := i) in INx; last by done.
by rewrite INx ltnn in LTi.
Qed.
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).
Proof.
case⇒ [|n]; [by move⇒ f' Huniq x; case|].
elim: n ⇒ [|n IHn] f' Huniq x i1 i2 Hi1 Hi2.
{ move: i1 i2 {Hi1 Hi2}; case; case⇒ [i1|//]; case; case⇒ [i2|//].
apply f_equal, eq_irrelevance. }
move: (leq_ord i1); rewrite leq_eqVlt ⇒ /orP [H'i1|H'i1];
move: (leq_ord i2); rewrite leq_eqVlt ⇒ /orP [H'i2|H'i2].
{ by apply ord_inj; move: H'i1 H'i2 ⇒ /eqP → /eqP →. }
{ exfalso.
move: Huniq; rewrite big_ord_recr cat_uniq ⇒ /andP [_ /andP [H _]].
move: H; apply /negP; rewrite Bool.negb_involutive.
apply /hasP; ∃ x ⇒ /=.
{ set o := ord_max; suff → : o = i1; [by []|].
by apply ord_inj; move: H'i1 ⇒ /eqP →. }
apply (mem_bigcat_ord _ _ (Ordinal H'i2)) ⇒ //.
by set o := widen_ord _ _; suff → : o = i2; [|apply ord_inj]. }
{ exfalso.
move: Huniq; rewrite big_ord_recr cat_uniq ⇒ /andP [_ /andP [H _]].
move: H; apply /negP; rewrite Bool.negb_involutive.
apply /hasP; ∃ x ⇒ /=.
{ set o := ord_max; suff → : o = i2; [by []|].
by apply ord_inj; move: H'i2 ⇒ /eqP →. }
apply (mem_bigcat_ord _ _ (Ordinal H'i1)) ⇒ //.
by set o := widen_ord _ _; suff → : o = i1; [|apply ord_inj]. }
move: Huniq; rewrite big_ord_recr cat_uniq ⇒ /andP [Huniq _].
apply ord_inj; rewrite -(inordK H'i1) -(inordK H'i2); apply f_equal.
apply (IHn _ Huniq x).
{ set i1' := widen_ord _ _; suff → : i1' = i1; [by []|].
by apply ord_inj; rewrite /= inordK. }
set i2' := widen_ord _ _; suff → : i2' = i2; [by []|].
by apply ord_inj; rewrite /= inordK.
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).
Proof.
case⇒ [|n]; [by move⇒ f' Huniq x; case|].
elim: n ⇒ [|n IHn] f' Huniq x i1 i2 Hi1 Hi2.
{ move: i1 i2 {Hi1 Hi2}; case; case⇒ [i1|//]; case; case⇒ [i2|//].
apply f_equal, eq_irrelevance. }
move: (leq_ord i1); rewrite leq_eqVlt ⇒ /orP [H'i1|H'i1];
move: (leq_ord i2); rewrite leq_eqVlt ⇒ /orP [H'i2|H'i2].
{ by apply ord_inj; move: H'i1 H'i2 ⇒ /eqP → /eqP →. }
{ exfalso.
move: Huniq; rewrite big_ord_recr cat_uniq ⇒ /andP [_ /andP [H _]].
move: H; apply /negP; rewrite Bool.negb_involutive.
apply /hasP; ∃ x ⇒ /=.
{ set o := ord_max; suff → : o = i1; [by []|].
by apply ord_inj; move: H'i1 ⇒ /eqP →. }
apply (mem_bigcat_ord _ _ (Ordinal H'i2)) ⇒ //.
by set o := widen_ord _ _; suff → : o = i2; [|apply ord_inj]. }
{ exfalso.
move: Huniq; rewrite big_ord_recr cat_uniq ⇒ /andP [_ /andP [H _]].
move: H; apply /negP; rewrite Bool.negb_involutive.
apply /hasP; ∃ x ⇒ /=.
{ set o := ord_max; suff → : o = i2; [by []|].
by apply ord_inj; move: H'i2 ⇒ /eqP →. }
apply (mem_bigcat_ord _ _ (Ordinal H'i1)) ⇒ //.
by set o := widen_ord _ _; suff → : o = i1; [|apply ord_inj]. }
move: Huniq; rewrite big_ord_recr cat_uniq ⇒ /andP [Huniq _].
apply ord_inj; rewrite -(inordK H'i1) -(inordK H'i2); apply f_equal.
apply (IHn _ Huniq x).
{ set i1' := widen_ord _ _; suff → : i1' = i1; [by []|].
by apply ord_inj; rewrite /= inordK. }
set i2' := widen_ord _ _; suff → : i2' = i2; [by []|].
by apply ord_inj; rewrite /= inordK.
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].
Proof.
intros.
specialize (leq_total t1 t2) ⇒ /orP [T1_LT | T2_LT].
+ have EX: ∃ Δ, t2 = t1 + Δ by ∃ (t2 - t1); ssrlia.
move: EX ⇒ [Δ EQ]; subst t2.
induction Δ.
{ now rewrite addn0 !big_geq ⇒ //. }
{ rewrite addnS !big_nat_recr ⇒ //=; try by rewrite leq_addr.
rewrite filter_cat IHΔ ⇒ //.
now ssrlia.
}
+ now rewrite !big_geq ⇒ //.
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].
Proof.
intros.
specialize (leq_total t1 t2) ⇒ /orP [T1_LT | T2_LT].
+ have EX: ∃ Δ, t2 = t1 + Δ by ∃ (t2 - t1); ssrlia.
move: EX ⇒ [Δ EQ]; subst t2.
induction Δ.
{ now rewrite addn0 !big_geq ⇒ //. }
{ rewrite addnS !big_nat_recr ⇒ //=; try by rewrite leq_addr.
rewrite filter_cat IHΔ ⇒ //.
now ssrlia.
}
+ now rewrite !big_geq ⇒ //.
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).
Proof.
intros.
specialize (leq_total t1 t2) ⇒ /orP [T1_LT | T2_LT].
+ have EX: ∃ Δ, t2 = t1 + Δ by ∃ (t2 - t1); ssrlia.
move: EX ⇒ [Δ EQ]; subst t2.
induction Δ.
{ now rewrite addn0 !big_geq ⇒ //. }
{ rewrite addnS !big_nat_recr ⇒ //=; try by rewrite leq_addr.
rewrite size_cat IHΔ ⇒ //.
now ssrlia.
}
+ now rewrite !big_geq ⇒ //.
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).
Proof.
intros.
specialize (leq_total t1 t2) ⇒ /orP [T1_LT | T2_LT].
+ have EX: ∃ Δ, t2 = t1 + Δ by ∃ (t2 - t1); ssrlia.
move: EX ⇒ [Δ EQ]; subst t2.
induction Δ.
{ now rewrite addn0 !big_geq ⇒ //. }
{ rewrite addnS !big_nat_recr ⇒ //=; try by rewrite leq_addr.
rewrite size_cat IHΔ ⇒ //.
now ssrlia.
}
+ now rewrite !big_geq ⇒ //.
Qed.
End BigCatLemmas.