PiLambda.v

(*** PiLambda.v
 * A Coq file for proving the pi-lambda theorem, and using it to prove the uniqueness of independent combination. 
 * see https://neuppl.khoury.northeastern.edu/blog/2023/pi-lambda/ 
 * Author: John M. Li https://johnm.li/ 
 ***)
Require Import Reals.
Require Import Psatz.

Axiom LEM : forall P, P \/ ~ P.
Axiom funext : forall A B, forall f g : A -> B, (forall x, f x = g x) -> f = g.
Axiom propext : forall P Q : Prop, P <-> Q -> P = Q.

Ltac rw := autorewrite with DB.
Ltac aut := auto with DB.
Ltac eaut := eauto 20 with DB.

(** ** ---------- Sets ---------- *)

Definition set X := X -> Prop.

Definition binary_union {X} (S T : set X) : set X := fun x => S x \/ T x.
Definition binary_intersection {X} (S T : set X) : set X := fun x => S x /\ T x.
Definition complement {X} (S : set X) : set X := fun x => ~ S x.
Definition member {X} (x : X) (S : set X) : Prop := S x.
Definition top {X} : set X := fun _ => True.
Definition bot {X} : set X := fun _ => False.
Infix "∪" := binary_union (at level 60).
Infix "∩" := binary_intersection (at level 60).
Notation "¬ S" := (complement S) (at level 60).
Infix "∈" := member (at level 70).

Definition subset {X} (S T : set X) : Prop := forall x, x ∈ S -> x ∈ T.
Infix "⊆" := subset (at level 70).
Definition equiv {X} (S T : set X) : Prop := S ⊆ T /\ T ⊆ S.
Infix "≡" := equiv (at level 70).

Lemma set_ext : forall {X} (S T : set X), S ≡ T -> S = T. Proof. intros. apply funext; intros; apply propext; firstorder. Qed.

Definition countable_union {X} (F : nat -> set X) : set X := fun x => exists n, x ∈ F n.
Definition empty {X} (S : set X) := forall x, x ∈ S -> False.
Definition disjoint {X} (F : nat -> set X) : Prop := forall m n, m <> n -> empty (F m ∩ F n).
Definition nonempty {X} (S : set X) := exists x, x ∈ S.

Lemma top_unit_l {X} (S : set X) : top ∩ S = S. Proof. apply set_ext; firstorder. Qed.
Lemma top_unit_r {X} (S : set X) : S ∩ top = S. Proof. apply set_ext; firstorder. Qed.
Lemma bot_unit_l {X} (S : set X) : bot ∪ S = S. Proof. apply set_ext; firstorder. Qed.
Lemma bot_unit_r {X} (S : set X) : S ∪ bot = S. Proof. apply set_ext; firstorder. Qed.
Lemma bot_zero_l {X} (S : set X) : bot ∩ S = bot. Proof. apply set_ext; firstorder. Qed.
Lemma bot_zero_r {X} (S : set X) : S ∩ bot = bot. Proof. apply set_ext; firstorder. Qed.
Lemma top_zero_l {X} (S : set X) : top ∪ S = top. Proof. apply set_ext; firstorder. Qed.
Lemma top_zero_r {X} (S : set X) : S ∪ top = top. Proof. apply set_ext; firstorder. Qed.
Lemma set_lem {X} (S : set X) : S ∪ (¬ S) = top. Proof. apply set_ext; split; intros x; destruct (LEM (S x)); firstorder. Qed.
Lemma neg_bot {X} : ¬ (bot (X:=X)) = top. Proof. apply set_ext; firstorder. Qed.
Lemma neg_top {X} : ¬ (top (X:=X)) = bot. Proof. apply set_ext; firstorder. Qed.
Lemma binary_intersection_assoc {X} (R S T : set X) : (R ∩ S) ∩ T = R ∩ (S ∩ T). Proof. apply set_ext; firstorder. Qed.
Lemma demorgan_or {X} (S T : set X) : ¬ (S ∪ T) = ¬ S ∩ ¬ T. Proof. apply set_ext; firstorder. Qed.
Lemma demorgan_and {X} (S T : set X) : ¬ (S ∩ T) = ¬ S ∪ ¬ T. Proof. apply set_ext; split; [intros x|firstorder]. destruct (LEM (S x)); firstorder. Qed.
Lemma dne {X} (S : set X) : ¬ (¬ S) = S. Proof. apply set_ext; split; [intros x; destruct (LEM (S x))|]; firstorder. Qed.
Lemma and_distrib_r {X} (A B C : set X) : (A ∪ B) ∩ C = (A ∩ C) ∪ (B ∩ C). Proof. apply set_ext; firstorder. Qed.
Lemma and_distrib_l {X} (A B C : set X) : C ∩ (A ∪ B) = (C ∩ A) ∪ (C ∩ B). Proof. apply set_ext; firstorder. Qed.
Lemma and_neg_or {X} (A B : set X) : (A ∩ ¬ B) ∪ B = A ∪ B. Proof. apply set_ext; split; [|intros x; pose proof (LEM (B x))]; firstorder. Qed.
Lemma and_neg {X} (A : set X) : (A ∩ ¬ A) = bot. Proof. apply set_ext; firstorder. Qed.
Lemma neg_and {X} (A : set X) : (¬ A ∩ A) = bot. Proof. apply set_ext; firstorder. Qed.
Lemma and_countable_union_l {X} (A : set X) F : A ∩ countable_union F = countable_union (fun n => A ∩ F n). Proof. apply set_ext; firstorder. Qed.
Lemma and_countable_union_r {X} (A : set X) F : countable_union F ∩ A = countable_union (fun n => A ∩ F n). Proof. apply set_ext; firstorder. Qed.
Lemma and_comm {X} (A B : set X) : A ∩ B = B ∩ A. Proof. apply set_ext; firstorder. Qed.
#[local] Hint Rewrite
  @bot_unit_l @bot_unit_r @bot_zero_l @bot_zero_r
  @top_unit_l @top_unit_r @top_zero_l @top_zero_r @set_lem
  @neg_bot @neg_top @binary_intersection_assoc @demorgan_or @demorgan_and @dne
  @and_distrib_l @and_distrib_r @and_neg @neg_and @and_countable_union_l
  @and_countable_union_r
: DB.

Lemma union_l X (A B : set X) x : x ∈ A -> x ∈ A ∪ B. Proof. firstorder. Qed.
Lemma union_r X (A B : set X) x : x ∈ B -> x ∈ A ∪ B. Proof. firstorder. Qed.
Lemma subset_union_l X (C A B : set X) : C ⊆ A -> C ⊆ A ∪ B. Proof. firstorder. Qed.
Lemma subset_union_r X (C A B : set X) : C ⊆ B -> C ⊆ A ∪ B. Proof. firstorder. Qed.
Lemma subset_refl X (A : set X) : A ⊆ A. Proof. firstorder. Qed.
Lemma union_subset_ump X (A B C : set X) : A ⊆ C -> B ⊆ C -> A ∪ B ⊆ C. Proof. firstorder. Qed.
#[local] Hint Resolve union_l union_r union_subset_ump subset_union_l subset_union_r subset_refl : DB.

Lemma countable_union_top X (F : nat -> set X) n : F n = top -> countable_union F = top.
Proof. intros H; apply set_ext; split; [firstorder|]; intros x []; exists n; now rewrite H. Qed.
Lemma countable_union_bot X (F : nat -> set X) : (forall n, F n = bot) -> countable_union F = bot.
Proof. intros H; apply set_ext; split; [|firstorder]. intros x [n Hn]. now rewrite H in Hn. Qed.

Fixpoint union_prefix {X} (F : nat -> set X) n : set X :=
  match n with
  | 0 => bot
  | S n => F n ∪ union_prefix F n
  end.

Lemma union_prefix_in_countable_union {X} (F : nat -> set X) n :
  union_prefix F n ⊆ countable_union F.
Proof. induction n; firstorder. Qed.

Lemma countable_unions_agree_if_prefixes_agree' {X} (F G : nat -> set X) :
  (forall n, union_prefix F n = union_prefix G n) ->
  countable_union F ⊆ countable_union G.
Proof.
  intros prefixes_agree x [n x_in_Fn].
  assert (x_in_prefix : x ∈ union_prefix F (S n)) by firstorder.
  rewrite prefixes_agree in x_in_prefix.
  eapply union_prefix_in_countable_union; eauto.
Qed.

Lemma countable_unions_agree_if_prefixes_agree {X} (F G : nat -> set X) :
  (forall n, union_prefix F n = union_prefix G n) ->
  countable_union F = countable_union G.
Proof.
  pose proof (countable_unions_agree_if_prefixes_agree' F G).
  pose proof (countable_unions_agree_if_prefixes_agree' G F).
  intros; apply set_ext; firstorder.
Qed.

Lemma union_prefix_mono {X} (F : nat -> set X) m n :
  union_prefix F n ⊆ union_prefix F (m + n).
Proof. induction m; firstorder. Qed.

Definition truncate {X} (F : nat -> set X) n :=
  fun n' => if Nat.ltb n' n then F n' else bot.

Lemma union_prefix_as_countable_union {X} (F : nat -> set X) n :
  union_prefix F n = countable_union (truncate F n).
Proof.
  unfold truncate; induction n; [cbn; apply set_ext; firstorder|].
  cbn in *; apply set_ext; split.
  - intros x [x_in_Fn|x_in_union]. 
    + exists n. now rewrite PeanoNat.Nat.leb_refl.
    + rewrite IHn in x_in_union.
      destruct x_in_union as [n' x_in_F'n'].
      unfold "∈" in x_in_F'n'.
      destruct n as [|n]; [easy|].
      exists n'.
      destruct (PeanoNat.Nat.leb_spec n' n); [|easy].
      destruct (PeanoNat.Nat.leb_spec n' (S n)); [easy|lia].
  - intros x [n' x_in_F'n']. rewrite IHn.
    destruct (PeanoNat.Nat.leb_spec n' n); [|easy].
    assert (cases : n' = n \/ n' < n) by lia.
    destruct cases; [left; subst; easy|right].
    exists n'. destruct n as [|n]; [easy|].
    destruct (PeanoNat.Nat.leb_spec n' n); [easy|lia].
Qed.

Definition disjointify {X} (F : nat -> set X) : nat -> set X :=
  fun n => F n ∩ ¬ union_prefix F n.

Lemma disjointify_disjoint {X} (F : nat -> set X) : disjoint (disjointify F).
Proof.
  enough (goal' : forall m n, empty (disjointify F n ∩ disjointify F (m + S n))).
  { intros m n m_ne_n.
    assert (cases : m < n \/ n < m) by lia.
    assert (rw : forall m n, m < n <-> n = (n - m - 1) + S m) by lia.
    repeat rewrite rw in *.
    destruct cases as [-> | ->]; [|rewrite and_comm]; auto. }
  unfold disjointify. intros m n.
  pose proof (union_prefix_mono F m (S n)).
  firstorder.
Qed.

Lemma disjointify_same_prefixes {X} (F : nat -> set X) n :
  union_prefix F n = union_prefix (disjointify F) n.
Proof.
  induction n as [|n IHn]; [reflexivity|].
  cbn; rewrite <- IHn. unfold disjointify.
  now rewrite and_neg_or.
Qed.

Lemma disjointify_same_union {X} (F : nat -> set X) :
  countable_union F = countable_union (disjointify F).
Proof. apply countable_unions_agree_if_prefixes_agree, disjointify_same_prefixes. Qed.

Definition binary_union_as_F {X} (A B : set X) : nat -> set X :=
  fun n => match n with 0 => A | 1 => B | _ => bot end.
Lemma binary_union_as_F_ok {X} (A B : set X) :
  A ∪ B = countable_union (binary_union_as_F A B).
Proof.
  apply set_ext; split; [intros x [Ax|Bx]; [exists 0|exists 1]; easy|]. 
  intros x [[|[|]] ]; [now left|now right|contradiction].
Qed.

(** ** ---------- σ-algebras, π-systems, and λ-systems ---------- *)

Definition closed_under_complements {X} (Σ : set (set X)) :=
  forall A, A ∈ Σ -> ¬ A ∈ Σ.
Definition closed_under_countable_unions {X} (Σ : set (set X)) :=
  forall F, (forall n, F n ∈ Σ) -> countable_union F ∈ Σ.
Definition closed_under_finite_intersections {X} (Σ : set (set X)) :=
  forall A B, A ∈ Σ -> B ∈ Σ -> A ∩ B ∈ Σ.
Definition closed_under_countable_disjoint_unions {X} (Σ : set (set X)) :=
  forall F, disjoint F -> (forall n, F n ∈ Σ) -> countable_union F ∈ Σ.

Definition σ_algebra {X} (Σ : set (set X)) :=
  bot ∈ Σ /\ 
  closed_under_complements Σ /\ 
  closed_under_countable_unions Σ.

Definition π_system {X} (Σ : set (set X)) :=
  nonempty Σ /\ closed_under_finite_intersections Σ.

Definition λ_system {X} (Σ : set (set X)) :=
  bot ∈ Σ /\ 
  closed_under_complements Σ /\ 
  closed_under_countable_disjoint_unions Σ.

(** The σ-algebra, π-system, and λ-system generated by a collection G. *)

Definition σ {X} (G : set (set X)) : set (set X) :=
  fun A => forall Σ, σ_algebra Σ -> G ⊆ Σ -> A ∈ Σ.
Definition π {X} (G : set (set X)) : set (set X) :=
  fun A => forall Σ, π_system Σ -> G ⊆ Σ -> A ∈ Σ.
Definition λ {X} (G : set (set X)) : set (set X) :=
  fun A => forall Σ, λ_system Σ -> G ⊆ Σ -> A ∈ Σ.

(** The corresponding induction principles *)

Lemma σ_ind {X} (G : set (set X)) (P : set X -> Prop) :
  (** Base cases: generators and bot *)
  (forall A, A ∈ G -> P A) -> P bot ->
  (** Inductive case: complements *)
  (forall A, P A -> P (¬ A)) ->
  (** Inductive case: countable unions *)
  (forall F, (forall n, P (F n)) -> P (countable_union F)) ->
  σ G ⊆ P.
Proof. firstorder. Qed.

Lemma λ_ind {X} (G : set (set X)) (P : set X -> Prop) :
  (** Base cases: generators and bot *)
  (forall A, A ∈ G -> P A) -> P bot ->
  (** Inductive case: complements *)
  (forall A, P A -> P (¬ A)) ->
  (** Inductive case: countable disjoint unions *)
  (forall F, disjoint F -> (forall n, P (F n)) -> P (countable_union F)) ->
  λ G ⊆ P.
Proof. firstorder. Qed.

Ltac induction_on x :=
  let go lemma gen x H G :=
    pattern x;
    lazymatch goal with
    | |- ?P x =>
      revert x H;
      change (gen _ G ⊆ P);
      apply (lemma _ G P)
    end
  in
  match goal with
  | H : x ∈ λ ?G |- _ => go @λ_ind @λ x H G
  | H : x ∈ σ ?G |- _ => go @σ_ind @σ x H G
  end.

(** "Obvious" facts about σ-algebras, π-systems, and λ-systems *)

Ltac randomapply :=
  multimatch goal with
  H : _ |- _ => apply H
  end.

Lemma σ_ok X (G : set (set X)) : σ_algebra (σ G). Proof. cbv; firstorder; randomapply; firstorder. Qed.
Lemma π_ok X (G : set (set X)) : nonempty G -> π_system (π G). Proof. cbv; firstorder; randomapply; firstorder. Qed.
Lemma λ_ok X (G : set (set X)) : λ_system (λ G). Proof. cbv; firstorder; randomapply; firstorder. Qed.
Lemma σ_has_generators X (G : set (set X)) A : A ∈ G -> A ∈ σ G. Proof. firstorder. Qed.
Lemma λ_has_generators X (G : set (set X)) A : A ∈ G -> A ∈ λ G. Proof. firstorder. Qed.
Lemma π_has_generators X (G : set (set X)) A : A ∈ G -> A ∈ π G. Proof. firstorder. Qed.
Lemma λ_has_bot X (G : set (set X)) : bot ∈ λ G. Proof. firstorder. Qed.
Lemma λ_has_complements X (G : set (set X)) A : A ∈ λ G -> ¬ A ∈ λ G. Proof. firstorder. Qed.
Lemma λ_has_complements' X (G : set (set X)) A : ¬ A ∈ λ G -> A ∈ λ G. Proof. intros; rewrite <- (dne A). now apply λ_has_complements. Qed.
Lemma π_has_intersections X (G : set (set X)) A B : A ∈ π G -> B ∈ π G -> A ∩ B ∈ π G. Proof. cbv; firstorder; randomapply; firstorder. Qed.
Lemma λ_has_countable_disjoint_unions X (G : set (set X)) F : disjoint F -> (forall n, F n ∈ λ G) -> countable_union F ∈ λ G. Proof. cbv; firstorder; randomapply; firstorder. Qed.
Lemma σ_union_subset X (G : set (set X)) A : A ⊆ G -> A ⊆ σ G. Proof. firstorder. Qed.
Lemma top_bot_complements X (L : set (set X)) : top ∈ L -> closed_under_complements L -> bot ∈ L. Proof. intros ? H; rewrite <- (dne bot). apply H; now rw. Qed.
#[local] Hint Resolve
  λ_ok π_ok σ_ok σ_has_generators λ_has_generators π_has_generators
  λ_has_bot λ_has_complements π_has_intersections σ_union_subset top_bot_complements
: DB.

Lemma λ_system_has_disjoint_unions {X} A B L : 
  λ_system (X:=X) L -> A ∈ L -> B ∈ L -> empty (A ∩ B) -> A ∪ B ∈ L.
Proof.
  intros Lλ AinλG BinλG ABdisjoint.
  rewrite binary_union_as_F_ok.
  destruct Lλ as [?[complements unions]]. apply unions.
  - intros [|[|m]] [|[|n]]; firstorder.
  - intros [|[|n]]; cbn; eaut.
Qed.

Lemma λ_has_disjoint_unions {X} (G : set (set X)) A B : 
  A ∈ λ G -> B ∈ λ G -> empty (A ∩ B) -> A ∪ B ∈ λ G.
Proof. pose proof (λ_ok _ G). now apply λ_system_has_disjoint_unions. Qed.

Lemma λ_and_π_imply_σ {X} (Σ : set (set X)) :
  λ_system Σ -> π_system Σ -> σ_algebra Σ.
Proof.
  intros [? [complements unions]] [? intersections]; split; [|split]; [firstorder..|].
  intros F IHF. rewrite disjointify_same_union.
  apply unions; [apply disjointify_disjoint|].
  induction n using Wf_nat.lt_wf_ind; unfold disjointify.
  apply intersections; [easy|apply complements].
  rewrite disjointify_same_prefixes.
  rewrite union_prefix_as_countable_union.
  apply unions; unfold truncate.
  - intros j k j_ne_k.
    destruct (PeanoNat.Nat.ltb_spec j n); [|now rw].
    destruct (PeanoNat.Nat.ltb_spec k n); [|now rw].
    now apply disjointify_disjoint.
  - intros m. destruct (PeanoNat.Nat.ltb_spec m n); eaut.
Qed.

#[local] Hint Resolve λ_system_has_disjoint_unions λ_has_disjoint_unions λ_and_π_imply_σ : DB.

Lemma π_of_π_system {X} (G : set (set X)) : π_system G -> G = π G.
Proof. intros Gπ; apply set_ext; split; [unfold "⊆"; eaut|firstorder]. Qed.
Lemma σ_of_σ_algebra {X} (G : set (set X)) : σ_algebra G -> G = σ G.
Proof. intros Gσ; apply set_ext; split; [unfold "⊆"; eaut|firstorder]. Qed.

Lemma σ_mono X (G H : set (set X)) : G ⊆ H -> σ G ⊆ σ H. Proof. firstorder. Qed.
Lemma σ_idem X (G H : set (set X)) : σ (σ G) = σ G. Proof. apply set_ext; split; firstorder. Qed.
Lemma σ_bind X (G H : set (set X)) : G ⊆ σ H -> σ G ⊆ σ H. Proof. intros GσH; apply σ_mono in GσH. now rewrite σ_idem in GσH. Qed.
Lemma σ_algebra_has_bot X (Σ : set (set X)) : σ_algebra Σ -> bot ∈ Σ. Proof. firstorder. Qed.
Lemma σ_algebra_has_complements X (Σ : set (set X)) A : σ_algebra Σ -> A ∈ Σ -> ¬ A ∈ Σ. Proof. firstorder. Qed.
Lemma σ_algebra_has_top X (Σ : set (set X)) : σ_algebra Σ -> top ∈ Σ. Proof. rewrite <- (dne top). intros; apply σ_algebra_has_complements; auto. rw; firstorder. Qed.
Lemma σ_algebra_has_unions X (Σ : set (set X)) A B : σ_algebra Σ -> A ∈ Σ -> B ∈ Σ -> A ∪ B ∈ Σ. Proof. rewrite binary_union_as_F_ok; intros [?[? unions]]??; apply unions; intros [|[|]]; [easy..|cbn; now apply σ_algebra_has_bot]. Qed.
Lemma σ_algebra_has_countable_unions X (Σ : set (set X)) (F : nat -> set X) : σ_algebra Σ -> (forall n, F n ∈ Σ) -> countable_union F ∈ Σ. Proof. firstorder. Qed.
#[local] Hint Resolve
  σ_mono σ_bind
  σ_algebra_has_top
  σ_algebra_has_complements
  σ_algebra_has_bot
  σ_algebra_has_unions
  σ_algebra_has_countable_unions
: DB.
Lemma σ_algebra_has_intersections X (Σ : set (set X)) A B : σ_algebra Σ -> A ∈ Σ -> B ∈ Σ -> A ∩ B ∈ Σ. Proof. replace (A ∩ B) with (¬ (¬ A ∪ ¬ B)) by now rw. intros; eaut. Qed.
#[local] Hint Resolve σ_algebra_has_intersections : DB.

(** ** ---------- The π-λ theorem ---------- *)

Lemma λπ_is_π_system X (P : set (set X)) :
  π_system P -> π_system (λ P).
Proof.
  (** λP is nonempty because P is nonempty.
      All that remains is to show closure under finite intersections. *)
  intros Pπ; split; [firstorder|intros A B AinλP BinλP].
  (** Since A is a member of the λ-system λP, we can proceed by
      λ-system-induction on it: *)
  induction_on A.
  (** There are two base cases. In the first base case, we must show
      the statement for all A in P. *)
  - intros A AinP.
    (** In this case we use a nested λ-system-induction on B: *)
    induction_on B.
    (** The first base case, B in P, follows directly from the fact that P, as
        a π-system, is closed under finite intersections. This is the only place
        in the induction where we make use of the fact that P is a π-system. *)
    + firstorder.
    (** The second base case, B = bot, follows from properties of sets. *)
    + rw. eaut.
    (** In the first inductive case we need to show A ∩ ¬ B ∈ λP given
        the induction hypothesis that A ∩ B ∈ λP. *)
    + intros B IHB.
      (** For this we use a trick: A ∩ ¬ B is equal to
            ¬ (¬ A ∪ (A ∩ B)),
          a complement of a disjoint union of sets in λP. *)
      replace (A ∩ (¬ B)) with (¬ (¬ A ∪ (A ∩ B))) by now rw.
      (** The rest of the proof follows from closure properties of λ-systems. *)
      apply λ_has_complements.
      apply λ_has_disjoint_unions; eaut; firstorder.
    (** In the second inductive case we have a disjoint family of sets F
        and need to show that A ∩ union F is in λP. The induction
        hypothesis says that each A ∩ F(n) is in λP; the result follows
        by properties of sets. *)
    + intros F Fdisjoint IHF. rw.
      apply λ_has_countable_disjoint_unions; firstorder.
  (** Now resuming the outer induction, the second base case A = top follows from
      properties of sets. *)
  - rw. eaut.
  (** In the first inductive case we need to show ¬ A ∩ B ∈ λP given
      the induction hypothesis that A ∩ B ∈ λP. *)
  - intros A IHA.
    (** The proof is analogous to the first inductive case of the inner induction
        above: we use the fact that
          ¬ A ∩ B = ¬ (¬ B ∪ (A ∩ B))
        where RHS is in λP by closure properties of λ-systems. *)
    replace ((¬ A) ∩ B) with (¬ (¬ B ∪ (A ∩ B))) by (rw; apply and_comm).
    apply λ_has_complements, λ_has_disjoint_unions; eaut; firstorder.
  (** In the second inductive case we have a disjoint family of sets F
      and need to show union F ∩ B ∈ λP given an induction hypothesis
      that F(n) ∩ B ∈ λP for all n; this follows from properties of sets. *)
  - intros F Fdisjoint IHF. rw.
    apply λ_has_countable_disjoint_unions; [firstorder|].
    intros; rewrite and_comm; eauto.
Qed.

Theorem σπ_is_λπ {X} (P : set (set X)) :
  π_system P -> σ P = λ P.
Proof.
  (** The right-to-left inclusion holds because every σ-algebra is a λ-system. *)
  intros Gnonempty; apply set_ext; split; [|firstorder].
  (** The left-to-right inclusion follows from the above lemma: σP is the
      smallest σ-algebra containing P, and λP is a σ-algebra, so σP must 
      also contain λP. *)
  assert (λπG_is_σ : σ_algebra (λ P)) by (eauto using λπ_is_π_system with DB).
  assert (λπG_has_πG : P ⊆ λ P) by (intros ?; eaut).
  intro; auto.
Qed.

(** The usual statement of the π-λ theorem *)
Corollary π_λ {X} (G L : set (set X)) :
  π_system G ->
  λ_system L ->
  G ⊆ L ->
  σ G ⊆ L.
Proof. intros ?; rewrite σπ_is_λπ; firstorder. Qed.

(** ** ---------- Probability spaces form a KRM (Theorem 2.4 of the paper) ---------- *)

Section KRM.

Variable Ω : Type.

(** Probability spaces on Ω *)

Definition produces_probabilities (Σ : set (set Ω)) (μ : set Ω -> R) :=
  (forall E, E ∈ Σ -> 0 <= μ E /\ μ E <= 1)%R.

Definition countably_additive (Σ : set (set Ω)) (μ : set Ω -> R) :=
  forall F, disjoint F -> (forall n, F n ∈ Σ) ->
  exists p, infinite_sum (fun n => μ (F n)) p /\ μ (countable_union F) = p.

Definition finitely_additive (Σ : set (set Ω)) (μ : set Ω -> R) :=
  forall A B, A ∈ Σ -> B ∈ Σ -> empty (A ∩ B) -> (μ (A ∪ B) = μ A + μ B)%R.

Definition probability_measure Σ μ :=
  produces_probabilities Σ μ /\
  μ top = 1%R /\
  countably_additive Σ μ /\
  finitely_additive Σ μ. (* technically not necessary, but makes proofs easier *)

Definition probability_space Σ μ := σ_algebra Σ /\ probability_measure Σ μ.

Definition equal_measures (Σ : set (set Ω)) (μ : set Ω -> R) ν :=
  forall E, E ∈ Σ -> μ E = ν E.
Notation "μ =[ Σ ] ν" := (equal_measures Σ μ ν) (at level 70).

Lemma bot_in_probability_space Σ μ : probability_space Σ μ -> bot ∈ Σ. Proof. intros []; eaut. Qed.
Lemma top_in_probability_space Σ μ : probability_space Σ μ -> top ∈ Σ. Proof. intros []; eaut. Qed.
Lemma μ_top_is_1 Σ μ : probability_space Σ μ -> μ top = 1%R. Proof. firstorder. Qed.
Lemma probability_space_has_σ_algebra Σ μ : probability_space Σ μ -> σ_algebra Σ. Proof. firstorder. Qed.
Lemma probability_space_has_probability_measure Σ μ : probability_space Σ μ -> probability_measure Σ μ. Proof. firstorder. Qed.
#[local] Hint Resolve top_in_probability_space μ_top_is_1 probability_space_has_σ_algebra probability_space_has_probability_measure : DB.

Lemma probability_measure_neg (Σ : set (set Ω)) μ A :
  σ_algebra Σ -> A ∈ Σ ->
  probability_measure Σ μ -> μ (¬ A) = (1 - μ A)%R.
Proof.
  intros HΣ HA [? [top [? additive]]].
  enough (μ A + μ (¬ A) = 1)%R by lra.
  rewrite <- top, <- additive; aut; firstorder.
  now rw.
Qed.
Lemma μ_bot_is_0 Σ μ : probability_space Σ μ -> μ bot = 0%R.
Proof.
  replace bot with (¬ (top (X:=Ω))) by now rw.
  intros. pose proof H; destruct H; erewrite probability_measure_neg; try eassumption; eaut.
  erewrite μ_top_is_1; eaut. nra.
Qed.
#[local] Hint Resolve μ_bot_is_0 : DB.

Ltac μ_rw :=
  repeat progress multimatch goal with
  | H : probability_space ?Σ ?μ |- context [?μ top] => rewrite !(μ_top_is_1 Σ μ H)
  | H : probability_space ?Σ ?μ |- context [?μ bot] => rewrite !(μ_bot_is_0 Σ μ H)
  | H : probability_space ?Σ ?μ |- context [?μ (¬ ?A)] =>
    rewrite !(probability_measure_neg Σ μ A); eaut
  end.

(** Independent combinations *)

Definition independent_combination (Σ : set (set Ω)) μ T ν ρ :=
  probability_space (σ (Σ ∪ T)) ρ /\
  forall E F, E ∈ Σ -> F ∈ T -> (ρ (E ∩ F) = μ E * ν F)%R.

Definition leq : set (set Ω) * (set Ω -> R) -> _ -> Prop :=
  fun '(Σ, μ) '(T, ν) => Σ ⊆ T /\ μ =[Σ] ν.

(** [leq] is a partial ordering *)
Lemma leq_refl Σ μ : leq (Σ, μ) (Σ, μ). Proof. firstorder. Qed.
Lemma leq_trans Σ μ T ν U ρ :
  leq (Σ, μ) (T, ν) ->
  leq (T, ν) (U, ρ) -> 
  leq (Σ, μ) (U, ρ).
Proof.
  intros [ΣT μν] [TU νρ]; split; [firstorder|].
  intros E HE. specialize (μν _ HE).
  apply ΣT in HE. specialize (νρ _ HE).
  congruence.
Qed.
Lemma leq_antisym Σ μ T ν :
  leq (Σ, μ) (T, ν) ->
  leq (T, ν) (Σ, μ) ->
  Σ = T /\ μ =[Σ] ν.
Proof. intros [ΣT μν] [TΣ νμ]. assert (Σ = T) by now apply set_ext. easy. Qed.

Definition intersections {X} (Σ T : set (set X)) : set (set X) :=
  fun G => exists E F, E ∈ Σ /\ F ∈ T /\ G = E ∩ F.

Lemma intersections_π_system (Σ T : set (set Ω)) :
  σ_algebra Σ -> σ_algebra T ->
  π_system (intersections Σ T).
Proof.
  intros Σσ Tσ; split; [exists top; exists top, top; rw; intuition eaut|].
  intros ? ? [A [B [HA [HB ->]]]] [A' [B' [HA' [HB' ->]]]].
  replace ((A ∩ B) ∩ (A' ∩ B')) with ((A ∩ A') ∩ (B ∩ B')) by (apply set_ext; firstorder).
  do 2 eexists; repeat split; eaut.
Qed.
Hint Resolve intersections_π_system : DB.

Lemma σΣT_is_λintersections (Σ T : set (set Ω)) :
  σ_algebra Σ -> σ_algebra T ->
  σ (Σ ∪ T) = λ (intersections Σ T).
Proof.
  intros Σσ Tσ. rewrite <- σπ_is_λπ by aut. apply set_ext; split.
  - apply σ_mono; intros E [HE|HE]; [exists E, top|exists top, E]; intuition eaut; now rw.
  - intros A HA; induction_on A; [|aut..]. intros ? [A [B [HA [HB ->]]]]; eaut.
Qed.

Ltac commute_countable_union x Hx :=
  match goal with
  | H : probability_space ?Σ ?μ, HF : disjoint ?F
    |- context [?μ (countable_union ?F)] => 
    destruct (proj1 (proj2 (proj2 (proj2 H))) F HF)
      as [x [Hx ->]]
  end.

(** Lemma 2.3 of the paper *)
Theorem independent_combinations_unique Σ μ T ν ρ :
  probability_space Σ μ ->
  probability_space T ν ->
  independent_combination Σ μ T ν ρ ->
  forall ρ', independent_combination Σ μ T ν ρ' ->
  ρ' =[σ(Σ ∪ T)] ρ.
Proof.
  intros Σμ Tν [ΣTρ indep] ρ' [ΣTρ' indep'] E EinΣT.
  rewrite σΣT_is_λintersections in EinΣT by firstorder.
  enough (E ∈ σ (Σ ∪ T) /\ ρ' E = ρ E) by tauto.
  induction_on E.
  - intros ? [A [B [AΣ [BT ->]]]].
    unfold independent_combination in *.
    rewrite indep, indep'; aut.
  - split; [now eaut|μ_rw; lra].
  - intros A []. split; [intuition eaut|]. μ_rw. lra.
  - intros F disjointF IHF.
    split; [apply σ_algebra_has_countable_unions; eaut; firstorder|].
    commute_countable_union l' Hl'; [firstorder|].
    commute_countable_union l Hl; [firstorder|].
    replace (fun n => ρ' (F n)) with (fun n => ρ (F n)) in *
      by (apply funext; intros n; specialize (IHF n); intuition congruence).
    eapply uniqueness_sum; eauto.
Qed.

Lemma probability_space_antimono (Σ' Σ : set (set Ω)) μ :
  Σ' ⊆ Σ -> σ_algebra Σ' ->
  probability_space Σ μ ->
  probability_space Σ' μ.
Proof.
  intros inclusion Σ'ok [?[?[?[additive fin_additive]]]].
  split; [|split; [|split; [|split]]]; auto.
  - unfold produces_probabilities in *; intros E HE; eauto.
  - intros ???; apply additive; auto.
  - intros A B HA HB HAB. apply inclusion in HA. apply inclusion in HB.
    eapply fin_additive; eauto.
Qed.

Lemma arith_fact x y : x <> 0%R -> (x * (y * / x) = y)%R. Proof. intros; rewrite Rmult_comm, Rmult_assoc, (Rmult_comm _ x), Rinv_r by auto; nra. Qed.

Lemma infinite_sum_mul x f l :
  infinite_sum (fun n => f n) l ->
  infinite_sum (fun n => x * f n)%R (x * l)%R.
Proof.
  intros lim ε Hε.
  replace (fun n => x * f n)%R with (fun n => f n * x)%R
    by (apply funext; intros; nra).
  destruct (LEM (x = 0)%R) as [->|x_nonzero].
  - exists 0; intros. rewrite <- scal_sum, R_dist_mult_l, Rabs_R0; nra.
  - pose proof Rabs_pos_lt x x_nonzero as abs_x_pos.
    pose proof Rinv_0_lt_compat (Rabs x) abs_x_pos as abs_x_inv_pos.
    pose proof Rmult_lt_0_compat _ _ Hε abs_x_inv_pos as Hε'.
    specialize (lim _ Hε'); destruct lim as [N HN].
    exists N; intros n Hn; specialize (HN n Hn).
    rewrite <- scal_sum, R_dist_mult_l.
    apply (Rmult_lt_compat_l (Rabs x) _ _ abs_x_pos) in HN.
    now rewrite arith_fact in HN by now apply Rabs_no_R0.
Qed.

Definition trivial_σ_algebra : set (set Ω) := fun A => A = top \/ A = bot.

Lemma trivial_σ_algebra_closed_under_countable_unions :
  closed_under_countable_unions trivial_σ_algebra.
Proof.
  intros F HF. destruct (LEM (exists n, F n = top)) as [[n Fn_top]|no_n].
  - left; apply set_ext; split; [firstorder|].
    intros ω []; exists n; rewrite Fn_top; easy.
  - right; apply set_ext; split; [|firstorder]. intros ω [n ω_in_Fn].
    assert (Fn_bot : F n = bot) by (destruct (HF n); auto; contradiction no_n; eauto).
    rewrite Fn_bot in ω_in_Fn; contradiction.
Qed.

Lemma trivial_σ_algebra_ok : σ_algebra trivial_σ_algebra.
Proof.
  split; [firstorder|split; [intros ? [->| ->]; rw; firstorder|]].
  apply trivial_σ_algebra_closed_under_countable_unions.
Qed.
#[local] Hint Resolve trivial_σ_algebra_closed_under_countable_unions trivial_σ_algebra_ok : DB.

Lemma disjoint_Fn_top_others_bot (F : nat -> set Ω) Σ μ n :
  disjoint F -> F n = top -> probability_space Σ μ ->
  forall m, m <> n -> F m = bot.
Proof.
  intros disjointF Fn_top space m m_ne_n.
  specialize (disjointF m n m_ne_n).
  apply set_ext; split; [|firstorder].
  rewrite Fn_top in *. autorewrite with DB in *.
  firstorder.
Qed.

Lemma disjoint_Fn_top_sum_prefix_0 F Σ μ n :
  disjoint F -> F n = top -> probability_space Σ μ ->
  forall m, m < n -> sum_f_R0 (fun n => μ (F n)) m = 0%R.
Proof.
  intros disjointF Fn_top space m m_lt_n.
  assert (H : exists k, n = m + S k) by (exists (n - m - 1); lia).
  destruct H as [k ->]. revert dependent k. induction m; cbn; intros.
  - cbn in *. assert (H : F 0 = bot) by now apply (disjoint_Fn_top_others_bot F Σ μ (S k)); auto.
    rewrite H. eaut.
  - cbn. assert (H : F (S m) = bot) by (apply (disjoint_Fn_top_others_bot F Σ μ (S m + S k)); auto; lia).
    rewrite H. replace (μ bot) with 0%R by (symmetry; eaut). rewrite (IHm (S k)); [lra|lia|].
    rewrite <- Fn_top; f_equal; lia.
Qed.

Lemma disjoint_Fn_top_eventually_1 F Σ μ n :
  disjoint F -> F n = top -> probability_space Σ μ ->
  forall m, m >= n -> sum_f_R0 (fun n => μ (F n)) m = 1%R.
Proof.
  intros disjointF Fn_top space m m_ge_n.
  assert (H : exists k, m = k + n) by (exists (m - n); lia).
  destruct H as [k ->]. induction k.
  - destruct n.
    + cbn; rewrite Fn_top. eaut.
    + cbn. erewrite disjoint_Fn_top_sum_prefix_0; eauto. rewrite Fn_top.
      erewrite μ_top_is_1; eaut; lra.
  - cbn. rewrite IHk by lia.
    replace (F (S (k + n))) with (bot (X:=Ω)).
    + erewrite μ_bot_is_0; eaut; lra.
    + symmetry; eapply disjoint_Fn_top_others_bot; eauto; lia.
Qed.

Lemma trivial_measure_exists_if_any_measure_does Σ μ :
  probability_space Σ μ ->
  probability_space trivial_σ_algebra μ.
Proof.
  intros Σspace. split; [eaut|split; [|split; [|split]]].
  - intros ? [-> | ->]; [unfold probability_space, probability_measure in *; lra|].
    replace (bot (X:=Ω)) with (¬ (top(X:=Ω))) by (now rw).
    rewrite (probability_measure_neg Σ); eaut. μ_rw. lra.
  - μ_rw; lra.
  - intros F disjointF Ftrivial.
    destruct (LEM (exists n, F n = top)) as [[n Fn_top]|no_n].
    + exists 1%R. erewrite countable_union_top by eauto. split; [|eaut].
      intros ε Hε; exists n; intros m m_ge_n.
      erewrite disjoint_Fn_top_eventually_1; eaut.
      unfold R_dist. replace (1 - 1)%R with 0%R by lra. now rewrite Rabs_R0.
    + exists 0%R. erewrite countable_union_bot
        by (intros n; destruct (Ftrivial n); auto; contradiction no_n; eauto).
      split; eaut.
      assert (all_bot : forall n, F n = bot).
      { intros n; destruct (Ftrivial n); [contradiction no_n; eaut|easy]. }
      assert (sums_0 : forall n, sum_f_R0 (fun n => μ (F n)) n = 0%R).
      { assert (μ bot = 0%R) by eaut.
        induction n as [|n IHn]; cbn; rewrite all_bot; [lra|].
        rewrite IHn. lra. }
      intros ε Hε; exists 0; intros n n_ge_0; rewrite sums_0.
      unfold R_dist; replace (0 - 0)%R with 0%R by lra; now rewrite Rabs_R0.
  - assert (μ top = 1 /\ μ bot = 0)%R by intuition eaut.
    intros ? ? [-> | ->] [-> | ->]; rw; [|lra..].
    intros Htop. assert (top (X:=Ω) = bot) by (apply set_ext; split; firstorder).
    assert (1 = 0)%R by intuition congruence. lra.
Qed.

Lemma trivial_σ_algebra_union Σ :
  σ_algebra Σ -> σ (Σ ∪ trivial_σ_algebra) = Σ.
Proof.
  intros HΣ; apply set_ext; split; [|firstorder].
  rewrite σ_of_σ_algebra by auto.
  apply σ_mono; apply union_subset_ump; eaut.
  intros A [->| ->]; eaut.
Qed.

(** Together the following theorems constitute Theorem 2.4 of the paper. *)

Theorem independent_combination_unit Σ μ ν :
  probability_space Σ μ ->
  probability_space trivial_σ_algebra ν ->
  independent_combination Σ μ trivial_σ_algebra ν μ.
Proof.
  intros Σspace trivial_space; split; [rewrite trivial_σ_algebra_union; eaut|].
  intros E F HE [->| ->]; rw; μ_rw; lra.
Qed.

Theorem independent_combination_commutative Σ μ T ν ρ :
  probability_space Σ μ ->
  probability_space T ν ->
  independent_combination Σ μ T ν ρ ->
  independent_combination T ν Σ μ ρ.
Proof.
  intros Σspace Tspace [space indep].
  split; [eapply probability_space_antimono; try eassumption; eaut|].
  intros E F HE HF. rewrite and_comm, indep by auto. lra.
Qed.

Theorem independent_combination_associative Σ₁ μ₁ Σ₂ μ₂ Σ₃ μ₃ μ₁₂ μ₁₂_₃ :
  probability_space Σ₁ μ₁ ->
  probability_space Σ₂ μ₂ ->
  probability_space Σ₃ μ₃ ->
  independent_combination Σ₁ μ₁ Σ₂ μ₂ μ₁₂ ->
  independent_combination (σ (Σ₁ ∪ Σ₂)) μ₁₂ Σ₃ μ₃ μ₁₂_₃ ->
  exists μ₂₃ μ₁_₂₃,
  independent_combination Σ₂ μ₂ Σ₃ μ₃ μ₂₃ /\
  independent_combination Σ₁ μ₁ (σ (Σ₂ ∪ Σ₃)) μ₂₃ μ₁_₂₃ /\
  μ₁_₂₃ = μ₁₂_₃.
Proof.
  intros space₁ space₂ space₃ [space₁₂ indep₁₂] [space₁₂_₃ indep₁₂_₃].
  exists μ₁₂_₃, μ₁₂_₃; split; [|split; [|reflexivity]];
    (split; [eapply probability_space_antimono; try eassumption; eaut|]).
  - intros E₂ E₃ HE₂ HE₃. replace (E₂ ∩ E₃) with ((top ∩ E₂) ∩ E₃) by now rw.
    rewrite indep₁₂_₃, indep₁₂ by eaut. μ_rw. nra.
  - intros E₁ E₂₃ HE₁ HE₂₃.
    (** This `revert` generalizes our induction hypothesis so that it is strong
        enough for the proof to go through. It corresponds to the construction
        of the set $\mathcal G$ described in the post. *)
    revert E₁ HE₁.
    match goal with |- ?P => enough (E₂₃ ∈ σ (Σ₂ ∪ Σ₃) /\ P) by tauto end.
    rewrite σΣT_is_λintersections in HE₂₃ by eaut.
    induction_on E₂₃.
    + intros ? [E₂ [E₃ [HE₂ [HE₃ ->]]]]; split; [now aut|]; intros E₁ HE₁.
      rewrite <- binary_intersection_assoc, !indep₁₂_₃, indep₁₂ by aut.
      replace (μ₁₂ E₂) with (μ₁₂ (top ∩ E₂)) by now rw.
      rewrite indep₁₂ by eaut. μ_rw; nra.
    + split; [now aut|]; intros E₁ HE₁.
      rewrite indep₁₂_₃ by eaut.
      replace (μ₁₂ E₁) with (μ₁₂ (E₁ ∩ top)) by now rw.
      rewrite indep₁₂ by eaut. μ_rw; nra.
    + intros E₂₃ [HE₂₃ IH]; split; [intuition eaut|]; intros E₁ HE₁.
      pose proof (proj2 space₁₂_₃).
      destruct space₁₂_₃ as [?[?[?[? additive]]]].
      replace (E₁ ∩ (¬ E₂₃)) with (¬ (¬ E₁ ∪ (E₁ ∩ E₂₃))) by now rw.
      erewrite !probability_measure_neg; try eassumption; eaut.
      rewrite additive by (eaut; firstorder).
      erewrite !probability_measure_neg; try eassumption; eaut.
      rewrite IH by auto.
      enough (μ₁ E₁ = μ₁₂_₃ E₁) by nra.
      replace (μ₁₂_₃ E₁) with (μ₁₂_₃ ((E₁ ∩ top) ∩ top)) by now rw.
      rewrite indep₁₂_₃, indep₁₂ by eaut. μ_rw; lra.
    + intros F Fdisjoint IHF; split; [apply σ_algebra_has_countable_unions; [eaut|firstorder]|].
      intros E₁ HE₁; rw.
      assert (Fn_in_Σ₁₂₃ : forall n, F n ∈ σ (σ (Σ₁ ∪ Σ₂) ∪ Σ₃)).
      { assert (inclusion : σ (Σ₂ ∪ Σ₃) ⊆ σ (σ (Σ₁ ∪ Σ₂) ∪ Σ₃)) by eaut.
        intros n; apply inclusion. firstorder. }
      commute_countable_union l Hl; [firstorder|].
      assert (disjoint (fun n => E₁ ∩ F n)).
      { intros m n m_ne_n. specialize (Fdisjoint m n m_ne_n). firstorder. }
      commute_countable_union r Hr; [now eaut|].
      replace (fun n => μ₁₂_₃ (E₁ ∩ F n)) with (fun n => μ₁ E₁ * μ₁₂_₃ (F n))%R in *
        by (apply funext; intros n; rewrite (proj2 (IHF n)); auto).
      apply (infinite_sum_mul (μ₁ E₁)) in Hl.
      eapply uniqueness_sum; eauto.
Qed.

Theorem independent_combination_respects_leq Σ μ Σ' μ' T ν T' ν' ρ' :
  probability_space Σ μ ->
  probability_space Σ' μ' ->
  probability_space T ν ->
  probability_space T' ν' ->
  leq (Σ, μ) (Σ', μ') ->
  leq (T, ν) (T', ν') ->
  independent_combination Σ' μ' T' ν' ρ' ->
  exists ρ, independent_combination Σ μ T ν ρ /\
  leq (σ (Σ ∪ T), ρ) (σ (Σ' ∪ T'), ρ').
Proof.
  intros Σspace Σspace' Tspace Tspace' [ΣΣ' μμ'] [TT' νν'] [prob indep].
  exists ρ'; split.
  - split; [eapply probability_space_antimono; try eassumption; eaut|].
    intros E F HE HF. specialize (ΣΣ' _ HE); specialize (TT' _ HF).
    rewrite indep; eaut. rewrite μμ', νν'; eaut.
  - split; [eaut|intro; easy].
Qed.

End KRM.