Subset_seq.v

(**
This file is part of the Elfic library

Copyright (C) Boldo, Clément, Faissole, Martin, Mayero

This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 3 of the License, or (at your option) any later version.

This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
*)

(** Countable iterations of operators on subsets (definitions and properties).

  Subsets of type U are represented by functions of type U -> Prop.

  Most identities can be found on Wikipedia:
  https://en.wikipedia.org/wiki/List_of_set_identities_and_relations

  All or parts of this file could use results on BigOps from MathComp. *)

From Coq Require Import Classical FunctionalExtensionality FinFun.
From Coq Require Import Arith Lia Even.

Require Import countable_sets nat_compl.
Require Import Subset Subset_finite.


Section Def0.

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

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

Definition mix : nat -> U -> Prop :=
  fun n => if even_odd_dec n then A (Nat.div2 n) else B (Nat.div2 n).

End Def0.


Section Seq_Def.

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

Variable C : U -> Prop.
Variable A B : nat -> U -> Prop. (* Subset sequences. *)
Variable phi : nat -> nat * nat.

(** Binary and unary predicates on sequences of subsets. *)

Definition incl_seq : Prop :=
  forall n, incl (A n) (B n).

Definition same_seq : Prop :=
  forall n, same (A n) (B n).

(* Warning: incr actually means nondecreasing. *)
Definition incr_seq : Prop :=
  forall n, incl (A n) (A (S n)).

(* Warning: decr actually means nonincreasing. *)
Definition decr_seq : Prop :=
  forall n, incl (A (S n)) (A n).

Definition disj_seq : Prop :=
  forall n1 n2, n1 < n2 -> disj (A n1) (A n2).

Definition disj_seq_alt : Prop :=
  forall n1 n2 x, A n1 x -> A n2 x -> n1 = n2.

(** Unary and binary operations on sequences of subsets. *)

Definition compl_seq : nat -> U -> Prop :=
  fun n => compl (A n).

Definition x_inter_seq : nat -> U -> Prop :=
  fun n => inter (A (fst (phi n))) (B (snd (phi n))).

(** Reduce operations on sequences of subsets. *)

Definition union_seq : U -> Prop :=
  fun x => exists n, A n x.

Definition inter_seq : U -> Prop :=
  fun x => forall n, A n x.

(** Properties of sequences of subsets. *)

Definition partition_seq : Prop :=
  C = union_seq /\ disj_seq.

End Seq_Def.


Ltac subset_seq_unfold :=
  unfold incl_seq, same_seq, incr_seq, decr_seq, disj_seq, disj_seq_alt,
    compl_seq, x_inter_seq, union_seq, inter_seq.

Ltac subset_seq_full_unfold :=
  subset_seq_unfold; subset_finite_full_unfold.

Ltac subset_seq_auto :=
  subset_seq_unfold; try tauto; try easy.

Ltac subset_seq_full_auto :=
  subset_seq_unfold; subset_finite_full_auto.


Section Seq_Facts.

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

(** Extensionality of sequences of subsets. *)

Lemma subset_seq_ext :
  forall (A B : nat -> U -> Prop),
    same_seq A B -> A = B.
Proof.
intros A B H.
apply functional_extensionality; intros n.
apply subset_ext, H.
Qed.

Lemma subset_seq_ext_equiv :
  forall (A B : nat -> U -> Prop),
    A = B <-> incl_seq A B /\ incl_seq B A.
Proof.
intros; split.
intros H; split; now rewrite H.
intros [H1 H2]; apply subset_seq_ext; split; [apply H1 | apply H2].
Qed.

(** Facts about predicates on sequences of subsets. *)

(** Equivalent definitions from _finite version. *)

Lemma incl_seq_equiv_def :
  forall (A B : nat -> U -> Prop),
    incl_seq A B <-> forall N, incl_finite A B N.
Proof.
intros A B; split; intros H; try easy.
intros n; apply (H (S n)); lia.
Qed.

Lemma same_seq_equiv_def :
  forall (A B : nat -> U -> Prop),
    same_seq A B <-> forall N, same_finite A B N.
Proof.
intros A B; split; intros H; try easy.
intros n; apply (H (S n)); lia.
Qed.

Lemma incr_seq_equiv_def :
  forall (A : nat -> U -> Prop),
    incr_seq A <-> forall N, incr_finite A N.
Proof.
intros A; split; intros H; try easy.
intros n; apply (H (S (S n))); lia.
Qed.

Lemma decr_seq_equiv_def :
  forall (A : nat -> U -> Prop),
    decr_seq A <-> forall N, decr_finite A N.
Proof.
intros A; split; intros H; try easy.
intros n; apply (H (S (S n))); lia.
Qed.

Lemma disj_seq_equiv_def :
  forall (A : nat -> U -> Prop),
    disj_seq A <-> forall N, disj_finite A N.
Proof.
intros A; split; intros H.
intros N n1 n2 _ _ Hn; now apply H.
intros n1 n2 Hn; apply (H (S n2)); lia.
Qed.

Lemma disj_seq_alt_equiv_def :
  forall (A : nat -> U -> Prop),
    disj_seq_alt A <-> forall N, disj_finite_alt A N.
Proof.
intros A; split; intros H.
intros N n1 n2 x _ _ Hx1 Hx2; now apply (H n1 n2 x).
intros n1 n2 x Hx1 Hx2;
    case (lt_eq_lt_dec n1 n2); [intros [Hn | Hn] | intros Hn]; try easy.
apply (H (S n2) n1 n2 x); now try lia.
apply (H (S n1) n1 n2 x); now try lia.
Qed.

(** incl_seq is an order binary relation. *)

Lemma incl_seq_refl :
  forall (A B : nat -> U -> Prop),
    same_seq A B -> incl_seq A B.
Proof.
intros A B; rewrite same_seq_equiv_def, incl_seq_equiv_def.
intros H N; now apply incl_finite_refl.
Qed.

Lemma incl_seq_antisym :
  forall (A B : nat -> U -> Prop),
    incl_seq A B -> incl_seq B A -> same_seq A B.
Proof.
intros A B H1 H2.
assert (HH : A = B -> same_seq A B).
  intros H'; now rewrite H'.
now apply HH, subset_seq_ext_equiv.
Qed.

Lemma incl_seq_trans :
  forall (A B C : nat -> U -> Prop),
    incl_seq A B -> incl_seq B C -> incl_seq A C.
Proof.
intros A B C H1 H2 n x Hx; now apply H2, H1.
Qed.

(** same_seq is an equivalence binary relation. *)

(* Useless?
Lemma same_seq_refl :
  forall (A : nat -> U -> Prop),
    same_seq A A.
Proof.
easy.
Qed.*)

Lemma same_seq_sym :
  forall (A B : nat -> U -> Prop),
    same_seq A B -> same_seq B A.
Proof.
intros A B H n; apply same_sym, (H n).
Qed.

Lemma same_seq_trans :
  forall (A B C : nat -> U -> Prop),
    same_seq A B -> same_seq B C -> same_seq A C.
Proof.
intros A B C H1 H2 n; apply same_trans with (B n).
apply (H1 n).
apply (H2 n).
Qed.

(** Facts about incr_seq and decr_seq. *)

Lemma incr_seq_le :
  forall (A : nat -> U -> Prop) n1 n2,
    incr_seq A -> n1 <= n2 -> incl (A n1) (A n2).
Proof.
intros; apply incr_finite_le with (N := S n2); try lia.
now rewrite incr_seq_equiv_def in H.
Qed.

Lemma decr_seq_le :
  forall (A : nat -> U -> Prop) n1 n2,
    decr_seq A -> n1 <= n2 -> incl (A n2) (A n1).
Proof.
intros; apply decr_finite_le with (N := S n2); try lia.
now rewrite decr_seq_equiv_def in H.
Qed.

Lemma incr_finite_seq :
  forall (A : nat -> U -> Prop) N,
    incr_finite A N <-> incr_seq (extend A N).
Proof.
intros A N; unfold extend; split.
(* *)
intros H n x Hx.
destruct (lt_dec n (S N)) as [Hn1 | Hn1];
    destruct (lt_dec (S n) (S N)) as [Hn2 | Hn2]; [ | | lia | easy].
apply H in Hx; [easy | lia].
assert (Hn3 : N = n) by lia; now rewrite Hn3.
(* *)
intros H n Hn x Hx; specialize (H n x); simpl in H.
destruct (lt_dec n (S N)) as [Hn1 | Hn1]; [ | lia];
    destruct (lt_dec (S n) (S N)) as [Hn2 | Hn2]; [ | lia].
now apply H.
Qed.

Lemma decr_finite_seq :
  forall (A : nat -> U -> Prop) N,
    decr_finite A N <-> decr_seq (extend A N).
Proof.
intros A N; unfold extend; split.
(* *)
intros H n x Hx.
destruct (lt_dec n (S N)) as [Hn1 | Hn1];
    destruct (lt_dec (S n) (S N)) as [Hn2 | Hn2]; [ | | lia | easy].
apply H; [lia | easy].
assert (Hn3 : n = N) by lia; now rewrite Hn3.
(* *)
intros H n Hn x Hx; specialize (H n x); simpl in H.
destruct (lt_dec n (S N)) as [Hn1 | Hn1]; [ | lia];
    destruct (lt_dec (S n) (S N)) as [Hn2 | Hn2]; [ | lia].
now apply H.
Qed.

Lemma union_finite_id :
  forall (A : nat -> U -> Prop),
    incr_seq A -> union_finite A = A.
Proof.
intros A H; apply subset_seq_ext; intros N; now rewrite incr_union_finite.
Qed.

Lemma union_finite_id_rev :
  forall (A : nat -> U -> Prop),
    union_finite A = A -> incr_seq A.
Proof.
intros A H n x Hx; rewrite <- H; exists n; split; [lia | easy].
Qed.

Lemma union_finite_id_equiv :
  forall (A : nat -> U -> Prop),
    incr_seq A <-> union_finite A = A.
Proof.
intros; split; [apply union_finite_id | apply union_finite_id_rev].
Qed.

Lemma inter_finite_id :
  forall (A : nat -> U -> Prop),
    decr_seq A -> inter_finite A = A.
Proof.
intros A H; apply subset_seq_ext; intros N; now rewrite decr_inter_finite.
Qed.

Lemma inter_finite_id_rev :
  forall (A : nat -> U -> Prop),
    inter_finite A = A -> decr_seq A.
Proof.
intros A H n x Hx; rewrite <- H in Hx; apply Hx; lia.
Qed.

Lemma inter_finite_id_equiv :
  forall (A : nat -> U -> Prop),
    decr_seq A <-> inter_finite A = A.
Proof.
intros; split; [apply inter_finite_id | apply inter_finite_id_rev].
Qed.

Lemma incr_seq_union_finite :
  forall (A : nat -> U -> Prop),
    incr_seq (union_finite A).
Proof.
intros A N x [n [Hn Hx]]; exists n; split; [lia | easy].
Qed.

Lemma decr_seq_inter_finite :
  forall (A : nat -> U -> Prop),
    decr_seq (inter_finite A).
Proof.
intros A N x Hx n Hn; apply Hx; lia.
Qed.

Lemma incr_seq_union_compat_l :
  forall (A : nat -> U -> Prop) (B : U -> Prop),
    incr_seq A -> incr_seq (fun n => union B (A n)).
Proof.
intros A B H n x [Hx | Hx]; [now left | right; now apply H].
Qed.

Lemma incr_seq_union_compat_r :
  forall (A : nat -> U -> Prop) (B : U -> Prop),
    incr_seq A -> incr_seq (fun n => union (A n) B).
Proof.
intros A B H n x [Hx | Hx]; [left; now apply H | now right].
Qed.

Lemma incr_seq_inter_compat_l :
  forall (A : nat -> U -> Prop) (B : U -> Prop),
    incr_seq A -> incr_seq (fun n => inter B (A n)).
Proof.
intros A B H n x [Hx1 Hx2]; split; [easy | now apply H].
Qed.

Lemma incr_seq_inter_compat_r :
  forall (A : nat -> U -> Prop) (B : U -> Prop),
    incr_seq A -> incr_seq (fun n => inter (A n) B).
Proof.
intros A B H n x [Hx1 Hx2]; split; [now apply H | easy].
Qed.

Lemma incr_seq_diff_compat_l :
  forall (A : nat -> U -> Prop) (B : U -> Prop),
    incr_seq A -> decr_seq (fun n => diff B (A n)).
Proof.
intros A B H n x [Hx1 Hx2]; split; [easy | intros Hx3; now apply Hx2, H].
Qed.

Lemma incr_seq_diff_compat_r :
  forall (A : nat -> U -> Prop) (B : U -> Prop),
    incr_seq A -> incr_seq (fun n => diff (A n) B).
Proof.
intros A B H n x [Hx1 Hx2]; split; [now apply H | easy].
Qed.

Lemma decr_seq_union_compat_l :
  forall (A : nat -> U -> Prop) (B : U -> Prop),
    decr_seq A -> decr_seq (fun n => union B (A n)).
Proof.
intros A B H n x [Hx | Hx]; [now left | right; now apply H].
Qed.

Lemma decr_seq_union_compat_r :
  forall (A : nat -> U -> Prop) (B : U -> Prop),
    decr_seq A -> decr_seq (fun n => union (A n) B).
Proof.
intros A B H n x [Hx | Hx]; [left; now apply H | now right].
Qed.

Lemma decr_seq_inter_compat_l :
  forall (A : nat -> U -> Prop) (B : U -> Prop),
    decr_seq A -> decr_seq (fun n => inter B (A n)).
Proof.
intros A B H n x [Hx1 Hx2]; split; [easy | now apply H].
Qed.

Lemma decr_seq_inter_compat_r :
  forall (A : nat -> U -> Prop) (B : U -> Prop),
    decr_seq A -> decr_seq (fun n => inter (A n) B).
Proof.
intros A B H n x [Hx1 Hx2]; split; [now apply H | easy].
Qed.

Lemma decr_seq_diff_compat_l :
  forall (A : nat -> U -> Prop) (B : U -> Prop),
    decr_seq A -> incr_seq (fun n => diff B (A n)).
Proof.
intros A B H n x [Hx1 Hx2]; split; [easy | intros Hx3; now apply Hx2, H].
Qed.

Lemma decr_seq_diff_compat_r :
  forall (A : nat -> U -> Prop) (B : U -> Prop),
    decr_seq A -> decr_seq (fun n => diff (A n) B).
Proof.
intros A B H n x [Hx1 Hx2]; split; [now apply H | easy].
Qed.

(** Facts about disj_seq and disj_seq_alt. *)

Lemma disj_seq_equiv :
  forall (A : nat -> U -> Prop),
    disj_seq_alt A <-> disj_seq A.
Proof.
intros A; rewrite disj_seq_alt_equiv_def, disj_seq_equiv_def; split; intros H N.
now rewrite <- disj_finite_equiv.
now rewrite disj_finite_equiv.
Qed.

Lemma disj_finite_seq :
  forall (A : nat -> U -> Prop) N,
    disj_finite A N <-> disj_seq (trunc emptyset A N).
Proof.
intros A N; unfold trunc; split.
(* *)
intros H n1 n2 Hn x Hx1 Hx2.
destruct (lt_dec n1 (S N)) as [Hn1 | Hn1];
    destruct (lt_dec n2 (S N)) as [Hn2 | Hn2]; try easy.
now apply (H n1 n2 Hn1 Hn2 Hn x).
(* *)
intros H n1 n2 Hn1 Hn2 Hn x Hx1 Hx2; specialize (H n1 n2 Hn x); simpl in H.
destruct (lt_dec n1 (S N)) as [Hn1' | Hn1'];
    destruct (lt_dec n2 (S N)) as [Hn2' | Hn2']; try easy.
now apply H.
Qed.

Lemma disj_seq_inter_l :
  forall (A : nat -> U -> Prop) (B : U -> Prop),
    disj_seq A -> disj_seq (fun n => inter B (A n)).
Proof.
intros A B H; rewrite disj_seq_equiv_def in H; rewrite disj_seq_equiv_def.
intros; now apply disj_finite_inter_l.
Qed.

Lemma disj_seq_inter_r :
  forall (A : nat -> U -> Prop) (B : U -> Prop),
    disj_seq A -> disj_seq (fun n => inter (A n) B).
Proof.
intros A B H; rewrite disj_seq_equiv_def in H; rewrite disj_seq_equiv_def.
intros; now apply disj_finite_inter_r.
Qed.

Lemma disj_seq_alt_x_inter_seq :
  forall (A B : nat -> U -> Prop) (phi : nat -> nat * nat),
    disj_seq_alt A -> disj_seq_alt B -> Bijective phi ->
    disj_seq_alt (x_inter_seq A B phi).
Proof.
intros A B phi HA HB [psi [Hphi _]] p1 p2 x [HAx1 HBx1] [HAx2 HBx2].
rewrite <- (Hphi p1), <- (Hphi p2); f_equal; apply injective_projections.
now apply (HA _ _ x).
now apply (HB _ _ x).
Qed.

(** Facts about operations on sequences of subsets. *)

(** Facts about compl_seq. *)

Lemma compl_seq_invol :
  forall (A : nat -> U -> Prop),
    compl_seq (compl_seq A) = A.
Proof.
intros; apply subset_seq_ext.
intros n x; subset_seq_full_auto.
Qed.

Lemma compl_seq_shift :
  forall (A : nat -> U -> Prop) N,
    compl_seq (shift A N) = shift (compl_seq A) N.
Proof.
intros; apply subset_seq_ext; subset_seq_auto.
Qed.

Lemma incl_compl_seq :
  forall (A B : nat -> U -> Prop),
    incl_seq A B -> incl_seq (compl_seq B) (compl_seq A).
Proof.
subset_seq_unfold; intros; now apply incl_compl, H.
Qed.

Lemma incl_compl_seq_equiv :
  forall (A B : nat -> U -> Prop),
    incl_seq A B <-> incl_seq (compl_seq B) (compl_seq A).
Proof.
intros; split.
apply incl_compl_seq.
rewrite <- (compl_seq_invol A) at 2; rewrite <- (compl_seq_invol B) at 2.
apply incl_compl_seq.
Qed.

Lemma same_compl_seq :
  forall (A B : nat -> U -> Prop),
    same_seq A B -> same_seq (compl_seq A) (compl_seq B).
Proof.
intros A B H n; apply same_compl, H.
Qed.

Lemma same_compl_seq_equiv :
  forall (A B : nat -> U -> Prop),
    same_seq A B <-> same_seq (compl_seq A) (compl_seq B).
Proof.
intros; split.
apply same_compl_seq.
rewrite <- (compl_seq_invol A) at 2; rewrite <- (compl_seq_invol B) at 2.
apply same_compl_seq.
Qed.

Lemma incr_compl_seq :
  forall (A : nat -> U -> Prop),
    incr_seq (compl_seq A) <-> decr_seq A.
Proof.
intros; subset_seq_full_unfold; split; intros H n x Hx; intuition.
specialize (H n x); apply imply_to_or in H; destruct H as [H | H]; try easy.
now apply NNPP.
Qed.

Lemma decr_compl_seq :
  forall (A : nat -> U -> Prop),
    decr_seq (compl_seq A) <-> incr_seq A.
Proof.
intros; now rewrite <- incr_compl_seq, compl_seq_invol.
Qed.

Lemma compl_seq_reg :
  forall (A B : nat -> U -> Prop),
    same_seq (compl_seq A) (compl_seq B) -> A = B.
Proof.
intros; now apply subset_seq_ext, same_compl_seq_equiv.
Qed.

(** Facts about x_inter_seq. *)

Lemma x_inter_seq_phi :
  forall (A B : nat -> U -> Prop) (phi1 phi2 : nat -> nat * nat),
    Bijective phi1 -> Bijective phi2 ->
    forall p1, exists p2,
      incl (x_inter_seq A B phi1 p1) (x_inter_seq A B phi2 p2).
Proof.
intros A B phi1 phi2 H1 [psi2 [_ H2]] p1.
exists (psi2 (phi1 p1)); intros x [Hx1 Hx2]; split; now rewrite H2.
Qed.

(** Facts about union_seq and inter_seq. *)

Lemma union_finite_seq :
  forall (A : nat -> U -> Prop) N,
    union_finite A N = union_seq (extend A N).
Proof.
intros A N; apply subset_ext; unfold extend; split.
(* *)
intros [n [Hn Hx]]; exists n.
now destruct (lt_dec n (S N)).
(* *)
intros [n Hx]; destruct (lt_dec n (S N)) as [Hn | Hn].
exists n; split; [lia | easy].
exists N; split; [lia | easy].
Qed.

Lemma union_finite_seq_alt :
  forall (A : nat -> U -> Prop) N,
    union_finite A N = union_seq (trunc emptyset A N).
Proof.
intros A N; apply subset_ext; unfold trunc; split.
intros [n [Hn1 Hx]]; exists n; now destruct (lt_dec n (S N)) as [Hn2 | Hn2].
intros [n Hx]; destruct (lt_dec n (S N)) as [Hn | Hn]; try easy.
exists n; split; [lia | easy].
Qed.

Lemma union_seq_finite :
  forall (A : nat -> U -> Prop),
    union_seq (union_finite A) = union_seq A.
Proof.
intros; apply subset_ext; split.
intros [N [n [_ Hx]]]; now exists n.
intros [n Hx]; exists (S n), n; split; [lia | easy].
Qed.

Lemma empty_union_seq :
  forall (A : nat -> U -> Prop),
    union_seq A = emptyset <-> forall n, A n = emptyset.
Proof.
intros A; rewrite <- empty_emptyset; split; intros H.
intros n; rewrite <- empty_emptyset; intros x Hx; apply (H x); now exists n.
intros x [n Hx]; specialize (H n); rewrite <- empty_emptyset in H; now apply (H x).
Qed.

Lemma union_seq_monot :
  forall (A B : nat -> U -> Prop),
    incl_seq A B ->
    incl (union_seq A) (union_seq B).
Proof.
intros A B H x [n Hx]; exists n; now apply H.
Qed.

Lemma union_seq_ub :
  forall (A : nat -> U -> Prop) n,
    incl (A n) (union_seq A).
Proof.
intros A n x Hx; now exists n.
Qed.

Lemma union_seq_full :
  forall (A : nat -> U -> Prop),
    (exists n, A n = fullset) ->
    union_seq A = fullset.
Proof.
intros A [n HAn].
apply subset_ext_equiv; split; try easy.
rewrite <- HAn; now apply union_seq_ub.
Qed.

Lemma union_seq_lub :
  forall (A : nat -> U -> Prop) (B : U -> Prop),
    (forall n, incl (A n) B) ->
    incl (union_seq A) B.
Proof.
intros A B H x [n Hx]; now apply (H n).
Qed.

Lemma incl_union_seq :
  forall (A : nat -> U -> Prop) (B : U -> Prop),
    incl (union_seq A) B ->
    forall n, incl (A n) B.
Proof.
intros A B H n x Hx; apply H; now exists n.
Qed.

Lemma union_seq_incl_compat :
  forall (A B : nat -> U -> Prop),
    (forall N, incl (union_finite A N) (union_finite B N)) ->
    incl (union_seq A) (union_seq B).
Proof.
intros A B H x [N Hx1]; specialize (H N x); destruct H as [n [Hn Hx2]].
apply (union_finite_ub _ N N); [lia | easy].
now apply (union_seq_ub _ n).
Qed.

Lemma union_seq_eq_compat :
  forall (A B : nat -> U -> Prop),
    (forall N, union_finite A N = union_finite B N) ->
    union_seq A = union_seq B.
Proof.
intros; apply subset_ext_equiv; split.
all: apply union_seq_incl_compat; intros N; now rewrite H.
Qed.

Lemma distrib_union_union_seq_l :
  forall (A : U -> Prop) (B : nat -> U -> Prop),
    union A (union_seq B) = union_seq (fun n => union A (B n)).
Proof.
intros A B; apply subset_ext; intros x; split.
intros [Hx | [n Hx]]; [exists 0; now left | exists n; now right].
intros [n [Hx | Hx]]; [now left | right; now exists n].
Qed.

Lemma distrib_union_union_seq_r :
  forall (A : nat -> U -> Prop) (B : U -> Prop),
    union (union_seq A) B = union_seq (fun n => union (A n) B).
Proof.
intros; rewrite union_comm, distrib_union_union_seq_l.
apply union_seq_eq_compat; intros.
rewrite <- distrib_union_union_finite_l, union_comm.
apply distrib_union_union_finite_r.
Qed.

Lemma distrib_inter_union_seq_l :
  forall (A : U -> Prop) (B : nat -> U -> Prop),
    inter A (union_seq B) = union_seq (fun n => inter A (B n)).
Proof.
intros A B; apply subset_ext; intros x; split.
intros [Hx1 [n Hx2]]; now exists n.
intros [n [Hx1 Hx2]]; split; [easy | now exists n].
Qed.

Lemma distrib_inter_union_seq_r :
  forall (A : nat -> U -> Prop) (B : U -> Prop),
    inter (union_seq A) B = union_seq (fun n => inter (A n) B).
Proof.
intros; rewrite inter_comm, distrib_inter_union_seq_l.
apply union_seq_eq_compat; intros.
rewrite <- distrib_inter_union_finite_l, inter_comm.
apply distrib_inter_union_finite_r.
Qed.

Lemma distrib_inter_union_seq :
  forall (A B : nat -> U -> Prop) (phi : nat -> nat * nat),
    Bijective phi ->
    inter (union_seq A) (union_seq B) =
    union_seq (x_inter_seq A B phi).
Proof.
intros A B phi [psi [_ Hphi]]; apply subset_ext; intros x; split.
intros [[n1 Hx1] [n2 Hx2]]; exists (psi (n1, n2)); split; now rewrite Hphi.
intros [n [HAx HBx]]; split.
now exists (fst (phi n)).
now exists (snd (phi n)).
Qed.

Lemma incr_union_seq_shift :
  forall (A : nat -> U -> Prop),
    incr_seq A -> forall N, union_seq (shift A N) = union_seq A.
Proof.
intros A H N; apply subset_ext; split; intros [n Hx].
now exists (N + n).
case (le_lt_dec N n); intros Hn.
exists n; apply (incr_seq_le _ n (N + n)); now try lia.
exists 0; apply (incr_seq_le _ n (N + 0)); now try lia.
Qed.

Lemma decr_union_seq_shift :
  forall (A : nat -> U -> Prop),
    decr_seq A -> forall N, union_seq (shift A N) = A N.
Proof.
intros A H N; apply subset_ext; split.
intros [n Hx]; apply (decr_seq_le _ N (N + n)); now try lia.
intros Hx; exists 0; now rewrite shift_0_r.
Qed.

Lemma disj_union_seq_l :
  forall (A : nat -> U -> Prop) (B : U -> Prop),
    disj (union_seq A) B <-> forall n, disj (A n) B.
Proof.
intros A B; split.
intros H n x Hx1 Hx2; apply (H x); [now exists n | easy].
intros H x [n Hx1] Hx2; now apply (H n x).
Qed.

Lemma disj_union_seq_r :
  forall (A : U -> Prop) (B : nat -> U -> Prop),
    disj A (union_seq B) <-> forall n, disj A (B n).
Proof.
intros; rewrite disj_sym, disj_union_seq_l; split;
    intros H n; rewrite disj_sym; now apply H.
Qed.

Lemma inter_finite_seq :
  forall (A : nat -> U -> Prop) N,
    inter_finite A N = inter_seq (extend A N).
Proof.
intros A N; apply subset_ext; unfold extend; split.
intros Hx n; destruct (lt_dec n (S N)) as [Hn | Hn]; apply Hx; lia.
intros Hx n Hn; specialize (Hx n); simpl in Hx.
now destruct (lt_dec n (S N)).
Qed.

Lemma inter_finite_seq_alt :
  forall (A : nat -> U -> Prop) N,
    inter_finite A N = inter_seq (trunc fullset A N).
Proof.
intros A N; apply subset_ext; unfold trunc; split.
intros Hx n; now destruct (lt_dec n (S N)) as [Hn | Hn]; [apply Hx | ].
intros Hx n Hn1; specialize (Hx n); simpl in Hx.
now destruct (lt_dec n (S N)).
Qed.

Lemma inter_seq_finite :
  forall (A : nat -> U -> Prop),
    inter_seq (inter_finite A) = inter_seq A.
Proof.
intros; apply subset_ext; split.
intros H n; apply (H (S n) n); lia.
intros H N n _; apply H.
Qed.

Lemma full_inter_seq :
  forall (A : nat -> U -> Prop),
    inter_seq A = fullset <-> forall n, A n = fullset.
Proof.
intros A; rewrite <- full_fullset; split; intros H.
intros n; rewrite <- full_fullset; intros x; now apply (H x).
intros x n; specialize (H n); rewrite <- full_fullset in H; now apply (H x).
Qed.

Lemma inter_seq_monot :
  forall (A B : nat -> U -> Prop),
    incl_seq A B ->
    incl (inter_seq A) (inter_seq B).
Proof.
intros A B H x Hx n; apply H, Hx.
Qed.

Lemma inter_seq_empty :
  forall (A : nat -> U -> Prop),
    (exists n, A n = emptyset) ->
    inter_seq A = emptyset.
Proof.
intros A [n HAn].
apply subset_ext_equiv; split; try easy.
now rewrite <- HAn.
Qed.

Lemma inter_seq_glb :
  forall (A : nat -> U -> Prop) (B : U -> Prop),
    (forall n, incl B (A n)) ->
    incl B (inter_seq A).
Proof.
intros A B H x Hx n; now apply H.
Qed.

Lemma incl_inter_seq :
  forall (A : nat -> U -> Prop) (B : U -> Prop),
    incl B (inter_seq A) ->
    forall n, incl B (A n).
Proof.
intros A B H n x Hx; now apply H.
Qed.

Lemma inter_seq_incl_compat :
  forall (A B : nat -> U -> Prop),
    (forall N, incl (inter_finite A N) (inter_finite B N)) ->
    incl (inter_seq A) (inter_seq B).
Proof.
intros A B H x Hx N; specialize (H N x).
apply (inter_finite_lb _ N); try lia.
apply H; intros n Hn; apply Hx.
Qed.

Lemma inter_seq_eq_compat :
  forall (A B : nat -> U -> Prop),
    (forall N, inter_finite A N = inter_finite B N) ->
    inter_seq A = inter_seq B.
Proof.
intros; apply subset_ext_equiv; split.
all: apply inter_seq_incl_compat; intros N; now rewrite H.
Qed.

Lemma distrib_union_inter_seq_l :
  forall (A : U -> Prop) (B : nat -> U -> Prop),
    union A (inter_seq B) = inter_seq (fun n => union A (B n)).
Proof.
intros A B; apply subset_ext; intros x; split.
intros [Hx | Hx] n; [now left | right; apply Hx].
intros Hx1; case (classic (A x)); intros Hx2.
now left.
right; intros n; now destruct (Hx1 n).
Qed.

Lemma distrib_union_inter_seq_r :
  forall (A : nat -> U -> Prop) (B : U -> Prop),
    union (inter_seq A) B = inter_seq (fun n => union (A n) B).
Proof.
intros; rewrite union_comm, distrib_union_inter_seq_l.
apply inter_seq_eq_compat; intros.
rewrite <- distrib_union_inter_finite_l, union_comm.
apply distrib_union_inter_finite_r.
Qed.

Lemma distrib_inter_inter_seq_l :
  forall (A : U -> Prop) (B : nat -> U -> Prop),
    inter A (inter_seq B) = inter_seq (fun n => inter A (B n)).
Proof.
intros A B; apply subset_ext; intros x; split.
intros [Hx1 Hx2] n; split; [easy | apply Hx2].
intros Hx; split; [apply (Hx 0) | intros n; apply (Hx n)].
Qed.

Lemma distrib_inter_inter_seq_r :
  forall (A : nat -> U -> Prop) (B : U -> Prop),
    inter (inter_seq A) B = inter_seq (fun n => inter (A n) B).
Proof.
intros; rewrite inter_comm, distrib_inter_inter_seq_l.
apply inter_seq_eq_compat; intros.
rewrite <- distrib_inter_inter_finite_l, inter_comm.
apply distrib_inter_inter_finite_r.
Qed.

(*
Lemma distrib_inter_seq_union_seq :
  forall (A : nat -> nat -> U -> Prop) (phi : R -> nat -> nat),
    Bijective_pow phi ->
    inter_seq (fun n => union_seq (fun m => A n m)) =
    union_any (fun (x : R) => inter_seq (fun n => A n (phi x n))).
Proof.
Aglopted.

Lemma distrib_union_seq_inter_seq :
  forall (A : nat -> nat -> U -> Prop) (phi : R -> nat -> nat),
    Bijective_pow phi ->
    union_seq (fun n => inter_seq (fun m => A n m)) =
    inter_any (fun (x : R) => union_seq (fun n => A n (phi x n))).
Proof.
Aglopted.
*)

Lemma incr_inter_seq_shift :
  forall (A : nat -> U -> Prop),
    incr_seq A -> forall N, inter_seq (shift A N) = A N.
Proof.
intros A H N; apply subset_ext; split; intros Hx.
rewrite <- (Nat.add_0_r N); apply (Hx 0).
intros n; apply (incr_seq_le _ N (N + n)); now try lia.
Qed.

Lemma decr_inter_seq_shift :
  forall (A : nat -> U -> Prop),
    decr_seq A -> forall N, inter_seq (shift A N) = inter_seq A.
Proof.
intros A H N; apply subset_ext; split; intros Hx n.
case (le_lt_dec N n); intros Hn.
replace n with (N + (n - N)); try lia; apply (Hx (n - N)).
apply (decr_seq_le _ n (N + 0)); [easy | lia | ]; apply (Hx 0).
apply (Hx (N + n)).
Qed.

Lemma incl_inter_union_seq :
  forall (A : nat -> U -> Prop),
    incl (inter_seq A) (union_seq A).
Proof.
intros A x Hx; exists 0; apply (Hx 0).
Qed.

(** De Morgan's laws. *)

Lemma compl_union_seq :
  forall (A : nat -> U -> Prop),
    compl (union_seq A) = inter_seq (compl_seq A).
Proof.
intros; apply subset_ext; split.
intros H n Hx; apply H; now exists n.
intros H [n Hx]; now apply (H n).
Qed.

Lemma compl_inter_seq :
  forall (A : nat -> U -> Prop),
    compl (inter_seq A) = union_seq (compl_seq A).
Proof.
intros; apply compl_reg; rewrite compl_union_seq.
now rewrite compl_invol, compl_seq_invol.
Qed.

Lemma compl_seq_union_seq :
  forall (A : nat -> U -> Prop)
      (f : (nat -> U -> Prop) -> nat -> nat -> U -> Prop),
    (forall (A : nat -> U -> Prop) N,
      compl_seq (f A N) = f (compl_seq A) N) ->
    compl_seq (fun n => union_seq (f A n)) =
      (fun n => inter_seq (f (compl_seq A) n)).
Proof.
intros A f Hf; apply subset_seq_ext; intros n x; unfold compl_seq.
now rewrite compl_union_seq, Hf.
Qed.

Lemma compl_seq_inter_seq :
  forall (A : nat -> U -> Prop)
      (f : (nat -> U -> Prop) -> nat -> nat -> U -> Prop),
    (forall (A : nat -> U -> Prop) N,
      compl_seq (f A N) = f (compl_seq A) N) ->
    compl_seq (fun n => inter_seq (f A n)) =
      (fun n => union_seq (f (compl_seq A) n)).
Proof.
intros A f Hf; apply subset_seq_ext; intros n x; unfold compl_seq.
now rewrite compl_inter_seq, Hf.
Qed.

(** ``Distributivity'' of diff. *)

Lemma diff_union_seq_l :
  forall (A : nat -> U -> Prop) (B : U -> Prop),
    diff (union_seq A) B = union_seq (fun n => diff (A n) B).
Proof.