Library probsa.util.misc
From discprob.prob Require Export prob countable.
From prosa.util Require Import tactics.
From prosa.classic.util Require Import list.
From probsa.util Require Export boolp.
Require Export Reals Psatz.
From mathcomp Require Export ssreflect ssrnat ssrbool seq eqtype fintype bigop.
Local Open Scope nat_scope.
From prosa.util Require Import tactics.
From prosa.classic.util Require Import list.
From probsa.util Require Export boolp.
Require Export Reals Psatz.
From mathcomp Require Export ssreflect ssrnat ssrbool seq eqtype fintype bigop.
Local Open Scope nat_scope.
We prove that any monotone function f : nat → bool falls into one of
the following cases:
(1) f n is false for any n,
(2) there exists t0 such that ∀ t, t > t0 ↔ f t,
(3) or f n is always true.
We note that this lemma uses the classical excluded middle axiom
∀ P : Prop, P ∨ ¬ P.
Lemma swithing_point_of_monotone_function :
∀ (f : nat → bool),
(∀ t1 t2, t1 ≤ t2 → f t1 → f t2)%nat →
(∀ t, ¬ f t) ∨ (∃ t0, ∀ t, t > t0 ↔ f t)%nat ∨ (∀ t, f t).
Proof.
intros f MON.
destruct (Classical_Prop.classic (∃ t, f t)) as [EX|NEX].
- right; destruct EX as [t0 Ft].
induction t0 as [ | t].
+ by right ⇒ t; eapply MON; last by apply Ft.
+ destruct (f t) eqn:Ft0; first by apply IHt.
clear IHt; left; ∃ t; intros t0.
split; intros.
× by eapply MON; last by apply Ft.
× rewrite leqNgt; apply/negP; move ⇒ LE; apply ltnSE in LE.
by apply MON in LE ⇒ //=; rewrite LE in Ft0.
- by rewrite -forallNE in NEX; left.
Qed.
∀ (f : nat → bool),
(∀ t1 t2, t1 ≤ t2 → f t1 → f t2)%nat →
(∀ t, ¬ f t) ∨ (∃ t0, ∀ t, t > t0 ↔ f t)%nat ∨ (∀ t, f t).
Proof.
intros f MON.
destruct (Classical_Prop.classic (∃ t, f t)) as [EX|NEX].
- right; destruct EX as [t0 Ft].
induction t0 as [ | t].
+ by right ⇒ t; eapply MON; last by apply Ft.
+ destruct (f t) eqn:Ft0; first by apply IHt.
clear IHt; left; ∃ t; intros t0.
split; intros.
× by eapply MON; last by apply Ft.
× rewrite leqNgt; apply/negP; move ⇒ LE; apply ltnSE in LE.
by apply MON in LE ⇒ //=; rewrite LE in Ft0.
- by rewrite -forallNE in NEX; left.
Qed.
Definition to_fintype {Job : finType} (s j : Job) (NEQ: s != j) :
Finite.sort (seq_sub_finType (T:=Job) (rem (T:=Job) j (enum Job))).
Proof.
econstructor; instantiate (1 := s).
apply in_neq_impl_rem_in ⇒ //.
by rewrite mem_enum unfold_in.
Defined.
Lemma nth_seq_eq :
∀ {X : eqType} (d : X) (xs : seq X) (i1 i2 : nat),
i1 < size xs →
i2 < size xs →
uniq xs →
nth d xs i1 = nth d xs i2 →
i1 = i2.
Proof.
induction xs; intros i1 i2 LT1 LT2 UNIQ EQ; first by done.
destruct i1, i2; simpl in × =>//.
{ exfalso.
move: UNIQ ⇒ /andP [IN _]; move: IN ⇒ /negP IN; apply: IN.
by rewrite EQ; apply mem_nth; rewrite -(ltn_add2r 1) !addn1.
}
{ exfalso.
move: UNIQ ⇒ /andP [IN _]; move: IN ⇒ /negP IN; apply: IN.
by rewrite -EQ; apply mem_nth; rewrite -(ltn_add2r 1) !addn1.
}
{ apply eq_S, IHxs.
- by rewrite -(ltn_add2r 1) !addn1.
- by rewrite -(ltn_add2r 1) !addn1.
- by move: UNIQ ⇒ /andP [_ UNI].
- by done.
}
Qed.
Lemma nth_mem_o :
∀ {X : eqType} (xs : seq X) (P : pred X) (x : X) (i : nat),
nth None [seq Some x | x <- xs & P x] i = Some x →
x \in xs ∧ P x.
Proof.
induction xs; intros × NTH; first by rewrite nth_default in NTH.
have [/eqP EQ | NEQ] := boolP (x == a).
{ subst; destruct (P a) eqn: Pa.
{ by split ⇒ //; rewrite in_cons eq_refl orTb //. }
{ exfalso.
rewrite //= Pa in NTH; specialize (IHxs P a i NTH).
by destruct IHxs ⇒ //; rewrite Pa in H0.
}
}
{ destruct (P a) eqn: Pa.
{ destruct i; rewrite //= Pa //= in NTH.
{ by inversion NTH; subst; rewrite eq_refl in NEQ. }
{ apply IHxs in NTH; split.
{ by rewrite in_cons; apply/orP; right; apply NTH. }
{ by apply NTH. }
}
}
{ rewrite //= Pa //= in NTH.
apply IHxs in NTH; split.
{ by rewrite in_cons; apply/orP; right; apply NTH. }
{ by apply NTH. }
}
}
Qed.
Lemma perm_eq_allpairs_flatten :
∀ {X Y : eqType} (P : X → pred Y) (F : Y → X) (xs : seq X) (ys : seq Y),
uniq xs →
uniq ys →
(∀ y, y \in ys → F y \in xs) →
(∀ y, y \in ys → P (F y) y) →
(∀ x1 x2 y, y \in ys → P x1 y → P x2 y → x1 = x2) →
perm_eq [seq (F y, y) | y <- ys] [seq (x, y) | x <- xs, y <- filter (P x) ys].
Proof.
clear.
intros × UNIQx UNIQy INF PF EQU; apply/allP ⇒ [[x y]]; rewrite mem_cat ⇒ /orP [IN | IN].
{ rewrite //= eqn_leq; apply/andP; split; apply leq_uniq_count.
{ rewrite map_inj_uniq //.
by intros a b EQ; inversion EQ; subst. }
{ intros [x2 y2]; move ⇒ /mapP2 [y3 IN3 EQ3].
inversion EQ3; subst; clear EQ3.
apply allpairs_f_dep.
- by apply seq_ext.mem_seq_legacy in IN3; apply INF.
- rewrite mem_filter; apply/andP; split.
+ by apply seq_ext.mem_seq_legacy in IN3; apply PF.
+ by apply seq_ext.mem_seq_legacy in IN3.
}
{ apply allpairs_uniq_dep ⇒ //.
{ by intros ? IN0; apply filter_uniq. }
{ by intros [] [] A B EQ; inversion EQ; subst. }
}
{ intros [x2 y2]; move ⇒ /allpairsPdep [x3 [y3 [IN3 IN3F EQ]]]; inversion EQ; subst.
apply/mapP2; ∃ y3.
- apply seq_ext.mem_seq_legacy.
by move: IN3F; rewrite mem_filter ⇒ /andP[A B].
- f_equal; move: IN3F; rewrite mem_filter ⇒ /andP[A B].
by specialize (EQU _ _ _ B (PF y3 B) A); subst.
}
}
{ rewrite //= eqn_leq; apply/andP; split; apply leq_uniq_count.
{ rewrite map_inj_uniq //.
by intros a b EQ; inversion EQ; subst. }
{ intros [x2 y2]; move ⇒ /mapP2 [y3 IN3 EQ3].
inversion EQ3; subst; clear EQ3.
apply allpairs_f_dep.
- by apply seq_ext.mem_seq_legacy in IN3; apply INF.
- rewrite mem_filter; apply/andP; split.
+ by apply seq_ext.mem_seq_legacy in IN3; apply PF.
+ by apply seq_ext.mem_seq_legacy in IN3.
}
{ apply allpairs_uniq_dep ⇒ //.
{ by intros ? IN0; apply filter_uniq. }
{ by intros [] [] A B EQ; inversion EQ; subst. }
}
{ intros [x2 y2]; move ⇒ /allpairsPdep [x3 [y3 [IN3 IN3F EQ]]]; inversion EQ; subst.
apply/mapP2; ∃ y3.
- apply seq_ext.mem_seq_legacy.
by move: IN3F; rewrite mem_filter ⇒ /andP[A B].
- f_equal; move: IN3F; rewrite mem_filter ⇒ /andP[A B].
by specialize (EQU _ _ _ B (PF y3 B) A); subst.
}
}
Qed.
Lemma seq_filter_singleton :
∀ {X : eqType} (P : pred X) (xs : seq X) (x : X),
uniq xs →
P x →
(x \in xs) →
(∀ y, y \in xs → P y → x = y) →
[seq x <- xs | P x] = [:: x].
Proof.
induction xs; first by done.
intros ×. intros UNIQ Px INx OPX. simpl.
destruct (P a) eqn:PA.
{ move: INx; rewrite in_cons ⇒ /orP [/eqP EQ | IN].
{ subst; f_equal.
apply filter_in_pred0 ⇒ y IN; apply/negP ⇒ PY.
have IN2: y \in a :: xs by rewrite in_cons IN orbT.
specialize (OPX _ IN2 PY); subst a.
by move: UNIQ; rewrite //= IN.
}
{ specialize (OPX a).
feed_n 2%nat OPX.
{ by rewrite in_cons eq_refl orTb. }
{ by done. }
subst; f_equal.
apply filter_in_pred0 ⇒ y INY; apply/negP ⇒ PY.
have IN2 : y \in a :: xs by rewrite in_cons INY orbT.
by move: UNIQ; rewrite //= IN.
}
}
{ apply IHxs.
{ by move: UNIQ ⇒ /andP []. }
{ by done. }
{ move: INx; rewrite in_cons ⇒ /orP [/eqP EQ | IN].
{ by subst; rewrite PA in Px. }
{ by done. }
}
{ intros × INy Py; apply OPX ⇒ //.
by rewrite in_cons INy orbT.
}
}
Qed.
Finite.sort (seq_sub_finType (T:=Job) (rem (T:=Job) j (enum Job))).
Proof.
econstructor; instantiate (1 := s).
apply in_neq_impl_rem_in ⇒ //.
by rewrite mem_enum unfold_in.
Defined.
Lemma nth_seq_eq :
∀ {X : eqType} (d : X) (xs : seq X) (i1 i2 : nat),
i1 < size xs →
i2 < size xs →
uniq xs →
nth d xs i1 = nth d xs i2 →
i1 = i2.
Proof.
induction xs; intros i1 i2 LT1 LT2 UNIQ EQ; first by done.
destruct i1, i2; simpl in × =>//.
{ exfalso.
move: UNIQ ⇒ /andP [IN _]; move: IN ⇒ /negP IN; apply: IN.
by rewrite EQ; apply mem_nth; rewrite -(ltn_add2r 1) !addn1.
}
{ exfalso.
move: UNIQ ⇒ /andP [IN _]; move: IN ⇒ /negP IN; apply: IN.
by rewrite -EQ; apply mem_nth; rewrite -(ltn_add2r 1) !addn1.
}
{ apply eq_S, IHxs.
- by rewrite -(ltn_add2r 1) !addn1.
- by rewrite -(ltn_add2r 1) !addn1.
- by move: UNIQ ⇒ /andP [_ UNI].
- by done.
}
Qed.
Lemma nth_mem_o :
∀ {X : eqType} (xs : seq X) (P : pred X) (x : X) (i : nat),
nth None [seq Some x | x <- xs & P x] i = Some x →
x \in xs ∧ P x.
Proof.
induction xs; intros × NTH; first by rewrite nth_default in NTH.
have [/eqP EQ | NEQ] := boolP (x == a).
{ subst; destruct (P a) eqn: Pa.
{ by split ⇒ //; rewrite in_cons eq_refl orTb //. }
{ exfalso.
rewrite //= Pa in NTH; specialize (IHxs P a i NTH).
by destruct IHxs ⇒ //; rewrite Pa in H0.
}
}
{ destruct (P a) eqn: Pa.
{ destruct i; rewrite //= Pa //= in NTH.
{ by inversion NTH; subst; rewrite eq_refl in NEQ. }
{ apply IHxs in NTH; split.
{ by rewrite in_cons; apply/orP; right; apply NTH. }
{ by apply NTH. }
}
}
{ rewrite //= Pa //= in NTH.
apply IHxs in NTH; split.
{ by rewrite in_cons; apply/orP; right; apply NTH. }
{ by apply NTH. }
}
}
Qed.
Lemma perm_eq_allpairs_flatten :
∀ {X Y : eqType} (P : X → pred Y) (F : Y → X) (xs : seq X) (ys : seq Y),
uniq xs →
uniq ys →
(∀ y, y \in ys → F y \in xs) →
(∀ y, y \in ys → P (F y) y) →
(∀ x1 x2 y, y \in ys → P x1 y → P x2 y → x1 = x2) →
perm_eq [seq (F y, y) | y <- ys] [seq (x, y) | x <- xs, y <- filter (P x) ys].
Proof.
clear.
intros × UNIQx UNIQy INF PF EQU; apply/allP ⇒ [[x y]]; rewrite mem_cat ⇒ /orP [IN | IN].
{ rewrite //= eqn_leq; apply/andP; split; apply leq_uniq_count.
{ rewrite map_inj_uniq //.
by intros a b EQ; inversion EQ; subst. }
{ intros [x2 y2]; move ⇒ /mapP2 [y3 IN3 EQ3].
inversion EQ3; subst; clear EQ3.
apply allpairs_f_dep.
- by apply seq_ext.mem_seq_legacy in IN3; apply INF.
- rewrite mem_filter; apply/andP; split.
+ by apply seq_ext.mem_seq_legacy in IN3; apply PF.
+ by apply seq_ext.mem_seq_legacy in IN3.
}
{ apply allpairs_uniq_dep ⇒ //.
{ by intros ? IN0; apply filter_uniq. }
{ by intros [] [] A B EQ; inversion EQ; subst. }
}
{ intros [x2 y2]; move ⇒ /allpairsPdep [x3 [y3 [IN3 IN3F EQ]]]; inversion EQ; subst.
apply/mapP2; ∃ y3.
- apply seq_ext.mem_seq_legacy.
by move: IN3F; rewrite mem_filter ⇒ /andP[A B].
- f_equal; move: IN3F; rewrite mem_filter ⇒ /andP[A B].
by specialize (EQU _ _ _ B (PF y3 B) A); subst.
}
}
{ rewrite //= eqn_leq; apply/andP; split; apply leq_uniq_count.
{ rewrite map_inj_uniq //.
by intros a b EQ; inversion EQ; subst. }
{ intros [x2 y2]; move ⇒ /mapP2 [y3 IN3 EQ3].
inversion EQ3; subst; clear EQ3.
apply allpairs_f_dep.
- by apply seq_ext.mem_seq_legacy in IN3; apply INF.
- rewrite mem_filter; apply/andP; split.
+ by apply seq_ext.mem_seq_legacy in IN3; apply PF.
+ by apply seq_ext.mem_seq_legacy in IN3.
}
{ apply allpairs_uniq_dep ⇒ //.
{ by intros ? IN0; apply filter_uniq. }
{ by intros [] [] A B EQ; inversion EQ; subst. }
}
{ intros [x2 y2]; move ⇒ /allpairsPdep [x3 [y3 [IN3 IN3F EQ]]]; inversion EQ; subst.
apply/mapP2; ∃ y3.
- apply seq_ext.mem_seq_legacy.
by move: IN3F; rewrite mem_filter ⇒ /andP[A B].
- f_equal; move: IN3F; rewrite mem_filter ⇒ /andP[A B].
by specialize (EQU _ _ _ B (PF y3 B) A); subst.
}
}
Qed.
Lemma seq_filter_singleton :
∀ {X : eqType} (P : pred X) (xs : seq X) (x : X),
uniq xs →
P x →
(x \in xs) →
(∀ y, y \in xs → P y → x = y) →
[seq x <- xs | P x] = [:: x].
Proof.
induction xs; first by done.
intros ×. intros UNIQ Px INx OPX. simpl.
destruct (P a) eqn:PA.
{ move: INx; rewrite in_cons ⇒ /orP [/eqP EQ | IN].
{ subst; f_equal.
apply filter_in_pred0 ⇒ y IN; apply/negP ⇒ PY.
have IN2: y \in a :: xs by rewrite in_cons IN orbT.
specialize (OPX _ IN2 PY); subst a.
by move: UNIQ; rewrite //= IN.
}
{ specialize (OPX a).
feed_n 2%nat OPX.
{ by rewrite in_cons eq_refl orTb. }
{ by done. }
subst; f_equal.
apply filter_in_pred0 ⇒ y INY; apply/negP ⇒ PY.
have IN2 : y \in a :: xs by rewrite in_cons INY orbT.
by move: UNIQ; rewrite //= IN.
}
}
{ apply IHxs.
{ by move: UNIQ ⇒ /andP []. }
{ by done. }
{ move: INx; rewrite in_cons ⇒ /orP [/eqP EQ | IN].
{ by subst; rewrite PA in Px. }
{ by done. }
}
{ intros × INy Py; apply OPX ⇒ //.
by rewrite in_cons INy orbT.
}
}
Qed.