Subset_seq.v

intros; now rewrite diff_equiv_def_inter, distrib_inter_union_seq_r.
Qed.

Lemma diff_union_seq_r :
  forall (A : U -> Prop) (B : nat -> U -> Prop),
    diff A (union_seq B) = inter_seq (fun n => diff A (B n)).
Proof.
intros; now rewrite diff_equiv_def_inter, compl_union_seq, distrib_inter_inter_seq_l.
Qed.

Lemma diff_inter_seq_l :
  forall (A : nat -> U -> Prop) (B : U -> Prop),
    diff (inter_seq A) B = inter_seq (fun n => diff (A n) B).
Proof.
intros; now rewrite diff_equiv_def_inter, distrib_inter_inter_seq_r.
Qed.

Lemma diff_inter_seq_r :
  forall (A : U -> Prop) (B : nat -> U -> Prop),
    diff A (inter_seq B) = union_seq (fun n => diff A (B n)).
Proof.
intros; now rewrite diff_equiv_def_inter, compl_inter_seq, distrib_inter_union_seq_l.
Qed.

(** Facts about partition_seq. *)

Lemma partition_seq_inter_l :
  forall (A C : U -> Prop) (B : nat -> U -> Prop),
    partition_seq A B ->
    partition_seq (inter C A) (fun n => inter C (B n)).
Proof.
intros A C B [H1 H2]; split.
rewrite H1; apply distrib_inter_union_seq_l.
now apply disj_seq_inter_l.
Qed.

Lemma partition_seq_inter_r :
  forall (A C : U -> Prop) (B : nat -> U -> Prop),
    partition_seq A B ->
    partition_seq (inter A C) (fun n => inter (B n) C).
Proof.
intros A C B [H1 H2]; split.
rewrite H1; apply distrib_inter_union_seq_r.
now apply disj_seq_inter_r.
Qed.

Lemma partition_seq_inter :
  forall (A B : U -> Prop) (A' B' : nat -> U -> Prop) (phi : nat -> nat * nat),
    partition_seq A A' -> partition_seq B B' -> Bijective phi ->
    partition_seq (inter A B) (x_inter_seq A' B' phi).
Proof.
intros A B A' B' phi [HA1 HA2] [HB1 HB2] Hphi; split.
rewrite HA1, HB1; now apply distrib_inter_union_seq.
apply disj_seq_equiv, disj_seq_alt_x_inter_seq; now try apply disj_seq_equiv.
Qed.

End Seq_Facts.


Section Limit_Def.

Context {U : Type}. (* Universe. *)

Variable A : nat -> U -> Prop. (* Subset sequence. *)

Definition liminf : U -> Prop :=
  union_seq (fun n => inter_seq (shift A n)).

Definition limsup : U -> Prop :=
  inter_seq (fun n => union_seq (shift A n)).

(* Useful?
Definition ex_lim : Prop :=
  same liminf limsup.*)

Definition is_lim (B : U -> Prop) : Prop :=
  same B liminf /\ same B limsup.

End Limit_Def.


Ltac subset_lim_unfold :=
  unfold liminf, limsup.

Ltac subset_lim_full_unfold :=
  subset_lim_unfold; subset_seq_full_unfold.

Ltac subset_lim_auto :=
  subset_lim_unfold; try tauto; try easy.

Ltac subset_lim_full_auto :=
  subset_lim_unfold; subset_seq_full_auto.


Section Limit_Facts.

Context {U : Type}. (* Universe. *)

Lemma liminf_ext :
  forall (A B : nat -> U -> Prop),
    same_seq A B -> liminf A = liminf B.
Proof.
intros A B H; apply subset_seq_ext in H; now rewrite H.
Qed.

Lemma limsup_ext :
  forall (A B : nat -> U -> Prop),
    same_seq A B -> limsup A = limsup B.
Proof.
intros A B H; apply subset_seq_ext in H; now rewrite H.
Qed.

Lemma liminf_shift :
  forall (A : nat -> U -> Prop) N,
    liminf (shift A N) = liminf A.
Proof.
intros A N1; apply subset_ext; split; intros [N2 Hx].
rewrite shift_add in Hx; now exists (N1 + N2).
exists N2; intros n; rewrite shift_add, plus_comm.
specialize (Hx (N1 + n)); now rewrite shift_assoc in Hx.
Qed.

Lemma limsup_shift :
  forall (A : nat -> U -> Prop) N,
    limsup (shift A N) = limsup A.
Proof.
intros A N1; apply subset_ext; subset_lim_unfold; split; intros Hx N2.
specialize (Hx N2); destruct Hx as [n Hx];
    exists (N1 + n); now rewrite shift_assoc, plus_comm, <- shift_add.
specialize (Hx (N1 + N2)); now rewrite shift_add.
Qed.

Lemma incl_liminf_limsup :
  forall (A : nat -> U -> Prop),
    incl (liminf A) (limsup A).
Proof.
intros A x [n H] p; exists n.
unfold shift; rewrite plus_comm; apply H.
Qed.

Lemma compl_liminf :
  forall (A : nat -> U -> Prop),
    compl (liminf A) = limsup (compl_seq A).
Proof.
intros; subset_lim_unfold; rewrite compl_union_seq; f_equal.
apply compl_seq_inter_seq, compl_seq_shift.
Qed.

Lemma compl_limsup :
  forall (A : nat -> U -> Prop),
    compl (limsup A) = liminf (compl_seq A).
Proof.
intros; subset_lim_unfold; rewrite compl_inter_seq; f_equal.
apply compl_seq_union_seq, compl_seq_shift.
Qed.

Lemma is_lim_unique :
  forall (A : nat -> U -> Prop) (B1 B2 : U -> Prop),
    is_lim A B1 -> is_lim A B2 -> B1 = B2.
Proof.
intros A B1 B2 [H1 _] [H2 _]; apply same_sym in H2; apply subset_ext.
now apply same_trans with (liminf A).
Qed.

Lemma is_lim_ext :
  forall (A1 A2 : nat -> U -> Prop) (B1 B2 : U -> Prop),
    same_seq A1 A2 -> is_lim A1 B1 -> is_lim A2 B2 -> B1 = B2.
Proof.
intros A1 A2 B1 B2 HA H1 H2.
apply subset_seq_ext in HA; rewrite HA in H1; now apply (is_lim_unique A2).
Qed.

Lemma is_lim_shift :
  forall (A : nat -> U -> Prop) (B : U -> Prop),
    is_lim A B -> forall N, is_lim (shift A N) B.
Proof.
intros A B [H1 H2] N; split.
now rewrite liminf_shift.
now rewrite limsup_shift.
Qed.

Lemma is_lim_compl :
  forall (A : nat -> U -> Prop) (B : U -> Prop),
    is_lim (compl_seq A) (compl B) <-> is_lim A B.
Proof.
intros A B; unfold is_lim.
rewrite <- compl_liminf, <- compl_limsup.
now do 2 rewrite same_compl_equiv.
Qed.

Lemma lim_incr_seq :
  forall (A : nat -> U -> Prop),
    incr_seq A -> is_lim A (union_seq A).
Proof.
intros A H; do 2 split.
intros [n Hx]; exists n; intros p; apply (incr_seq_le A n); now try lia.
intros [n Hx]; exists n; rewrite <- (Nat.add_0_r n); apply (Hx 0).
intros [n Hx] N; exists n; apply (incr_seq_le A n); now try lia.
intros Hx; destruct (Hx 0) as [n Hx']; exists n; now rewrite <- (Nat.add_0_l n).
Qed.

Lemma lim_decr_seq :
  forall (A : nat -> U -> Prop),
    decr_seq A -> is_lim A (inter_seq A).
Proof.
intros A.
rewrite <- (compl_seq_invol A), decr_compl_seq, <- compl_union_seq, is_lim_compl.
apply lim_incr_seq.
Qed.

Lemma union_seq_lim :
  forall (A : nat -> U -> Prop),
    is_lim (union_finite A) (union_seq A).
Proof.
intros; rewrite <- union_seq_finite.
apply lim_incr_seq, incr_seq_union_finite.
Qed.

Lemma inter_seq_lim :
  forall (A : nat -> U -> Prop),
    is_lim (inter_finite A) (inter_seq A).
Proof.
intros; rewrite <- inter_seq_finite.
apply lim_decr_seq, decr_seq_inter_finite.
Qed.

Lemma liminf_equiv_def :
  forall (A : nat -> U -> Prop),
    is_lim (fun n => inter_seq (shift A n)) (liminf A).
Proof.
intros; apply lim_incr_seq; unfold shift; intros n x Hx p.
rewrite Nat.add_succ_comm; apply (Hx (S p)).
Qed.

Lemma limsup_equiv_def :
  forall (A : nat -> U -> Prop),
    is_lim (fun n => union_seq (shift A n)) (limsup A).
Proof.
intros; apply lim_decr_seq; unfold shift; intros n x [p Hx].
rewrite Nat.add_succ_comm in Hx; now exists (S p).
Qed.

End Limit_Facts.


Section FU_DU_Def.

Context {U : Type}. (* Universe. *)

Variable A : nat -> U -> Prop. (* Subset sequence. *)

(** FU = finite union.
 It makes any subset sequence a nondecreasing sequence,
 while keeping the partial unions. *)

Definition FU : nat -> U -> Prop := union_finite A.

(** DU = disjoint union.
 It makes any subset sequence a pairwise disjoint sequence,
 while keeping the partial unions. *)

Definition DU : nat -> U -> Prop :=
  fun N => match N with
           | 0 => A 0
           | S N => diff (A (S N)) (FU N) end.

End FU_DU_Def.


Section FU_Facts.

(** Properties of finite union. *)

Context {U : Type}. (* Universe. *)

Lemma FU_0 :
  forall (A : nat -> U -> Prop),
    FU A 0 = A 0.
Proof.
exact union_finite_0.
Qed.

Lemma FU_S :
  forall (A : nat -> U -> Prop) N,
    FU A (S N) = union (FU A N) (A (S N)).
Proof.
exact union_finite_S.
Qed.

Lemma FU_id :
  forall (A : nat -> U -> Prop),
    incr_seq A <-> FU A = A.
Proof.
exact union_finite_id_equiv.
Qed.

Lemma FU_lim :
  forall (A : nat -> U -> Prop),
    is_lim (FU A) (union_seq A).
Proof.
exact union_seq_lim.
Qed.

Lemma FU_incr_seq :
  forall (A : nat -> U -> Prop),
    incr_seq (FU A).
Proof.
exact incr_seq_union_finite.
Qed.

Lemma FU_union_finite :
  forall (A : nat -> U -> Prop) N,
    union_finite (FU A) N = union_finite A N.
Proof.
exact union_finite_idem.
Qed.

Lemma FU_union_seq :
  forall (A : nat -> U -> Prop),
    union_seq (FU A) = union_seq A.
Proof.
exact union_seq_finite.
Qed.

Lemma FU_disj_l :
  forall (A : nat -> U -> Prop) (B : U -> Prop) N,
    disj (FU A N) B <-> (forall n, n < S N -> disj (A n) B).
Proof.
exact disj_union_finite_l.
Qed.

Lemma FU_disj_r :
  forall (A : U -> Prop) (B : nat -> U -> Prop) N,
    disj A (union_finite B N) <-> (forall n, n < S N -> disj A (B n)).
Proof.
exact disj_union_finite_r.
Qed.

End FU_Facts.


Section DU_Facts.

(** Properties of disjoint union. *)

Context {U : Type}. (* Universe. *)

Lemma DU_incl_seq_l :
  forall (A : nat -> U -> Prop),
    incl_seq (DU A) A.
Proof.
intros A n x; destruct n; [easy | now intros [H _]].
Qed.

Lemma DU_union_finite_incl :
  forall (A : nat -> U -> Prop),
    incl_seq (union_finite (DU A)) (union_finite A).
Proof.
intros; rewrite incl_seq_equiv_def; intros N1 N2 HN2.
apply union_finite_monot; intros n Hn; apply DU_incl_seq_l.
Qed.

Lemma DU_union_finite_incl_rev :
  forall (A : nat -> U -> Prop),
    incl_seq (union_finite A) (union_finite (DU A)).
Proof.
assert (H : forall (A B : U -> Prop) x, A x \/ B x -> A x \/ B x /\ ~ A x)
    by (intros; tauto).
intros A N x; induction N; intros [n [Hn Hx]].
rewrite lt_1 in Hn; rewrite Hn in Hx; now rewrite union_finite_0.
rewrite union_finite_S.
destruct H
    with (A := union_finite A N)
         (B := A (S N)) (x := x) as [H' | H'].
  case (le_lt_eq_dec n (S N)); try lia; clear Hn; intros Hn.
  left; exists n; split; [lia | easy].
  right; now rewrite Hn in Hx.
left; now apply IHN.
now right.
Qed.

Lemma DU_union_finite :
  forall (A : nat -> U -> Prop),
    union_finite (DU A) = union_finite A.
Proof.
intros; apply subset_seq_ext_equiv; split.
apply DU_union_finite_incl.
apply DU_union_finite_incl_rev.
Qed.

Lemma DU_equiv_def :
  forall (A : nat -> U -> Prop) N,
    DU A (S N) = diff (A (S N)) (union_finite (DU A) N).
Proof.
intros; now rewrite DU_union_finite.
Qed.

Lemma DU_union_seq :
  forall (A : nat -> U -> Prop),
    union_seq (DU A) = union_seq A.
Proof.
intros; apply union_seq_eq_compat.
intros; now rewrite DU_union_finite.
Qed.

Lemma DU_disj_finite :
  forall (A : nat -> U -> Prop) N,
    disj_finite (DU A) N.
Proof.
intros A N n1 n2 Hn1 Hn2 Hn x Hx1 Hx2.
destruct n1, n2; try lia; simpl in Hx2; destruct Hx2 as [Hx2 Hx2']; apply Hx2'.
apply (union_finite_ub _ _ 0); [lia | easy].
apply DU_incl_seq_l in Hx1; now exists (S n1).
Qed.

Lemma DU_disj_finite_alt :
  forall (A : nat -> U -> Prop) N,
    disj_finite_alt (DU A) N.
Proof.
intros; apply disj_finite_equiv, DU_disj_finite.
Qed.

Lemma DU_disj_seq :
  forall (A : nat -> U -> Prop),
    disj_seq (DU A).
Proof.
intros; rewrite disj_seq_equiv_def; apply DU_disj_finite.
Qed.

Lemma DU_disj_seq_alt :
  forall (A : nat -> U -> Prop),
    disj_seq_alt (DU A).
Proof.
intros; apply disj_seq_equiv, DU_disj_seq.
Qed.

End DU_Facts.