Library Subsets.Subset_any
This file is part of the Coq Numerical Analysis library
Copyright (C) Boldo, Clément, Martin, Mayero, Mouhcine
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.
Support for uncountable iterations of operators on subsets.
Uncountable collections of subsets of type U are either represented
by functions of type Idx → U → Prop for some type of indices Idx, or
by subset systems of type (U → Prop) → Prop (ie subsets of the power set
of U).
Most of the properties are tautologies, and can be found on Wikipedia:
https://en.wikipedia.org/wiki/List_of_set_identities_and_relations
This module may be used through the import of Subsets.Subsets,
Subsets.Subsets_wDep, Algebra.Algebra_wDep, Lebesgue.Lebesgue_p_wDep, or
Lebesgue.Bochner.Bochner_wDep, where it is exported.
Brief description
Description
Used logic axioms
- fun_ext, an alias for functional_extensionality.
Usage
From Logic Require Import logic_compl.
From Subsets Require Import Subset Subset_dec.
Section Any_Def.
Implementation using an arbitrary index.
Context {U U1 U2 : Type}. Context {Idx : Type}.
Variable A B : Idx → U → Prop.
Definition incl_any : Prop := ∀ i, incl (A i) (B i).
Definition same_any : Prop := ∀ i, same (A i) (B i).
Definition compl_any : Idx → U → Prop := fun i ⇒ compl (A i).
Definition union_any : U → Prop := fun x ⇒ ∃ i, A i x.
Definition inter_any : U → Prop := fun x ⇒ ∀ i, A i x.
Variable A1 : Idx → U1 → Prop. Variable B2 : U2 → Prop. Variable B1 : U1 → Prop. Variable A2 : Idx → U2 → Prop.
Definition prod_any_l : Idx → U1 × U2 → Prop := fun i ⇒ prod (A1 i) B2.
Definition prod_any_r : Idx → U1 × U2 → Prop := fun i ⇒ prod B1 (A2 i).
End Any_Def.
Section Prop_Def.
Implementation using a predicate.
Context {U U1 U2 : Type}.
Variable PA PB : (U → Prop) → Prop.
Definition incl_Prop : Prop := incl PA PB.
Definition same_Prop : Prop := same PA PB.
Definition compl_Prop : (U → Prop) → Prop := fun A ⇒ PA (compl A).
Definition union_Prop : U → Prop := fun x ⇒ ∃ A, PA A ∧ A x.
Definition inter_Prop : U → Prop := fun x ⇒ ∀ A, PA A → A x.
Variable P1 : (U1 → Prop) → Prop. Variable B2 : U2 → Prop. Variable B1 : U1 → Prop. Variable P2 : (U2 → Prop) → Prop.
Inductive prod_Prop_l : (U1 × U2 → Prop) → Prop :=
| PPL : ∀ A1, P1 A1 → prod_Prop_l (prod A1 B2).
Inductive prod_Prop_r : (U1 × U2 → Prop) → Prop :=
| PPR : ∀ A2, P2 A2 → prod_Prop_r (prod B1 A2).
End Prop_Def.
Section Any_Facts0.
Context {U Idx : Type}.
Extensionality of collections of subsets.
Lemma subset_any_ext :
∀ (A B : Idx → U → Prop),
same_any A B → A = B.
Proof.
intros A B H; apply fun_ext; intros i.
apply subset_ext, H.
Qed.
Lemma subset_any_ext_equiv :
∀ (A B : Idx → U → Prop),
A = B ↔ incl_any A B ∧ incl_any B A.
Proof.
intros; split.
intros H; split; now rewrite H.
intros [H1 H2]; apply subset_any_ext; split; [apply H1 | apply H2].
Qed.
End Any_Facts0.
Section Prop_Facts0.
Context {U : Type}.
Extensionality of collections of subsets.
Lemma subset_Prop_ext :
∀ (PA PB : (U → Prop) → Prop),
same_Prop PA PB → PA = PB.
Proof.
exact subset_ext.
Qed.
Lemma subset_Prop_ext_equiv :
∀ (PA PB : (U → Prop) → Prop),
PA = PB ↔ incl_Prop PA PB ∧ incl_Prop PB PA.
Proof.
exact subset_ext_equiv.
Qed.
End Prop_Facts0.
Ltac subset_any_unfold :=
repeat unfold
same_any, incl_any, same_Prop, incl_Prop,
prod_any_r, prod_any_l, inter_any, union_any, compl_any,
inter_Prop, union_Prop, compl_Prop.
Ltac subset_any_full_unfold :=
subset_any_unfold; subset_unfold.
Ltac subset_any_auto :=
subset_any_unfold; try easy; try tauto; auto.
Ltac subset_any_full_auto :=
subset_any_unfold; subset_auto.
Section Any_Facts.
Context {U Idx : Type}.
Facts about predicates on collections of subsets.
incl_any is an order binary relation.
Lemma incl_any_refl :
∀ (A B : Idx → U → Prop),
same_any A B → incl_any A B.
Proof.
intros A B H i; apply incl_refl; auto.
Qed.
Lemma incl_any_antisym :
∀ (A B : Idx → U → Prop),
incl_any A B → incl_any B A → same_any A B.
Proof.
intros A B H1 H2.
assert (HH : A = B → same_any A B).
intros H'; now rewrite H'.
now apply HH, subset_any_ext_equiv.
Qed.
Lemma incl_any_trans :
∀ (A B C : Idx → U → Prop),
incl_any A B → incl_any B C → incl_any A C.
Proof.
intros A B C H1 H2 n x Hx; now apply H2, H1.
Qed.
same_any is an equivalence binary relation.
Lemma same_any_sym :
∀ (A B : Idx → U → Prop),
same_any A B → same_any B A.
Proof.
intros A B H n; apply same_sym, (H n).
Qed.
Lemma same_any_trans :
∀ (A B C : Idx → U → Prop),
same_any A B → same_any B C → same_any 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 operations on collections of subsets.
Facts about compl_any.
Lemma compl_any_invol :
∀ (A : Idx → U → Prop),
compl_any (compl_any A) = A.
Proof.
intros; apply subset_any_ext.
intros i x; subset_any_full_auto.
Qed.
Lemma compl_any_monot :
∀ (A B : Idx → U → Prop),
incl_any A B → incl_any (compl_any B) (compl_any A).
Proof.
subset_any_unfold; intros; now apply compl_monot, H.
Qed.
Lemma incl_compl_any_equiv :
∀ (A B : Idx → U → Prop),
incl_any A B ↔ incl_any (compl_any B) (compl_any A).
Proof.
intros; split.
apply compl_any_monot.
rewrite <- (compl_any_invol A) at 2; rewrite <- (compl_any_invol B) at 2.
apply compl_any_monot.
Qed.
Lemma same_compl_any :
∀ (A B : Idx → U → Prop),
same_any A B → same_any (compl_any A) (compl_any B).
Proof.
intros A B H i; apply same_compl, H.
Qed.
Lemma same_compl_any_equiv :
∀ (A B : Idx → U → Prop),
same_any A B ↔ same_any (compl_any A) (compl_any B).
Proof.
intros; split.
apply same_compl_any.
rewrite <- (compl_any_invol A) at 2; rewrite <- (compl_any_invol B) at 2.
apply same_compl_any.
Qed.
Lemma compl_any_reg :
∀ (A B : Idx → U → Prop),
same_any (compl_any A) (compl_any B) → A = B.
Proof.
intros; now apply subset_any_ext, same_compl_any_equiv.
Qed.
Facts about union_any and inter_any.
Lemma union_any_nullary :
¬ inhabited Idx →
∀ (A : Idx → U → Prop), union_any A = emptyset.
Proof.
intros H A; apply empty_emptyset; intros x [i Hx].
apply H; easy.
Qed.
Lemma union_any_empty :
∀ (A : Idx → U → Prop),
union_any A = emptyset ↔ ∀ i, A i = emptyset.
Proof.
intros A; rewrite <- empty_emptyset; split; intros H.
intros i; rewrite <- empty_emptyset; intros x Hx; apply (H x); now ∃ i.
intros x [i Hx]; specialize (H i); rewrite <- empty_emptyset in H; now apply (H x).
Qed.
Lemma union_any_monot :
∀ (A B : Idx → U → Prop),
incl_any A B →
incl (union_any A) (union_any B).
Proof.
intros A B H x [i Hx]; ∃ i; now apply H.
Qed.
Lemma union_any_ub :
∀ (A : Idx → U → Prop) i,
incl (A i) (union_any A).
Proof.
intros A i x Hx; now ∃ i.
Qed.
Lemma union_any_full :
∀ (A : Idx → U → Prop),
(∃ i, A i = fullset) →
union_any A = fullset.
Proof.
intros A [i HAi].
apply subset_ext_equiv; split; try easy.
rewrite <- HAi; now apply union_any_ub.
Qed.
Lemma union_any_lub :
∀ (A : Idx → U → Prop) (B : U → Prop),
(∀ i, incl (A i) B) →
incl (union_any A) B.
Proof.
intros A B H x [i Hx]; now apply (H i).
Qed.
Lemma incl_union_any :
∀ (A : Idx → U → Prop) (B : U → Prop),
incl (union_any A) B →
∀ i, incl (A i) B.
Proof.
intros A B H i x Hx; apply H; now ∃ i.
Qed.
Lemma union_union_any_distr_l :
inhabited Idx →
∀ (A : U → Prop) (B : Idx → U → Prop),
union A (union_any B) = union_any (fun i ⇒ union A (B i)).
Proof.
intros [i0] A B; apply subset_ext; intros x; split.
intros [Hx | [i Hx]]; [∃ i0; now left | ∃ i; now right].
intros [i [Hx | Hx]]; [now left | right; now ∃ i].
Qed.
Lemma union_union_any_distr_r :
inhabited Idx →
∀ (A : Idx → U → Prop) (B : U → Prop),
union (union_any A) B = union_any (fun i ⇒ union (A i) B).
Proof.
intros; rewrite union_comm, union_union_any_distr_l; try easy.
f_equal; apply fun_ext; intros; apply union_comm.
Qed.
Lemma inter_union_any_distr_l :
∀ (A : U → Prop) (B : Idx → U → Prop),
inter A (union_any B) = union_any (fun i ⇒ inter A (B i)).
Proof.
intros A B; apply subset_ext; intros x; split.
intros [Hx1 [i Hx2]]; now ∃ i.
intros [i [Hx1 Hx2]]; split; [easy | now ∃ i].
Qed.
Lemma inter_union_any_distr_r :
∀ (A : Idx → U → Prop) (B : U → Prop),
inter (union_any A) B = union_any (fun i ⇒ inter (A i) B).
Proof.
intros; rewrite inter_comm, inter_union_any_distr_l.
f_equal; apply fun_ext; intros; apply inter_comm.
Qed.
Lemma inter_any_nullary :
¬ inhabited Idx →
∀ (A : Idx → U → Prop), inter_any A = fullset.
Proof.
intros H A; apply (full_fullset (_ A)); intros x i.
contradict H; easy.
Qed.
Lemma inter_any_full :
∀ (A : Idx → U → Prop),
inter_any A = fullset ↔ ∀ i, A i = fullset.
Proof.
intros A; rewrite <- full_fullset; split; intros H.
intros i; rewrite <- full_fullset; intros x; now apply (H x).
intros x i; specialize (H i); rewrite <- full_fullset in H; now apply (H x).
Qed.
Lemma inter_any_monot :
∀ (A B : Idx → U → Prop),
incl_any A B →
incl (inter_any A) (inter_any B).
Proof.
intros A B H x Hx i; apply H, Hx.
Qed.
Lemma inter_any_empty :
∀ (A : Idx → U → Prop),
(∃ i, A i = emptyset) →
inter_any A = emptyset.
Proof.
intros A [i HAi].
apply subset_ext_equiv; split; try easy.
now rewrite <- HAi.
Qed.
Lemma inter_any_glb :
∀ (A : Idx → U → Prop) (B : U → Prop),
(∀ i, incl B (A i)) →
incl B (inter_any A).
Proof.
intros A B H x Hx i; now apply H.
Qed.
Lemma incl_inter_any :
∀ (A : Idx → U → Prop) (B : U → Prop),
incl B (inter_any A) →
∀ i, incl B (A i).
Proof.
intros A B H i x Hx; now apply H.
Qed.
Lemma union_inter_any_distr_l :
∀ (A : U → Prop) (B : Idx → U → Prop),
union A (inter_any B) = inter_any (fun i ⇒ union A (B i)).
Proof.
intros A B; apply subset_ext; intros x; split.
intros [Hx | Hx] i; [now left | right; apply Hx].
intros Hx1; case (in_dec A x); intros Hx2.
now left.
right; intros i; now destruct (Hx1 i).
Qed.
Lemma union_inter_any_distr_r :
∀ (A : Idx → U → Prop) (B : U → Prop),
union (inter_any A) B = inter_any (fun i ⇒ union (A i) B).
Proof.
intros; rewrite union_comm, union_inter_any_distr_l.
f_equal; apply fun_ext; intros; apply union_comm.
Qed.
Lemma inter_inter_any_distr_l :
inhabited Idx →
∀ (A : U → Prop) (B : Idx → U → Prop),
inter A (inter_any B) = inter_any (fun i ⇒ inter A (B i)).
Proof.
intros [i0] A B; apply subset_ext; intros x; split.
intros [Hx1 Hx2] i; split; [easy | apply Hx2].
intros Hx; split; [apply (Hx i0) | intros i; apply (Hx i)].
Qed.
Lemma inter_inter_any_distr_r :
inhabited Idx →
∀ (A : Idx → U → Prop) (B : U → Prop),
inter (inter_any A) B = inter_any (fun i ⇒ inter (A i) B).
Proof.
intros; rewrite inter_comm, inter_inter_any_distr_l; try easy.
f_equal; apply fun_ext; intros; apply inter_comm.
Qed.
Lemma incl_inter_union_any :
inhabited Idx →
∀ (A : Idx → U → Prop),
incl (inter_any A) (union_any A).
Proof.
intros [i0] A x Hx; ∃ i0; apply (Hx i0).
Qed.
De Morgan's laws.
Lemma compl_union_any :
∀ (A : Idx → U → Prop),
compl (union_any A) = inter_any (compl_any A).
Proof.
intros; apply subset_ext; split.
intros H i Hx; apply H; now ∃ i.
intros H [i Hx]; now apply (H i).
Qed.
Lemma compl_inter_any :
∀ (A : Idx → U → Prop),
compl (inter_any A) = union_any (compl_any A).
Proof.
intros; apply compl_reg; rewrite compl_union_any.
now rewrite compl_invol, compl_any_invol.
Qed.
Lemma compl_any_union_any :
∀ (A : Idx → U → Prop)
(f : (Idx → U → Prop) → Idx → Idx → U → Prop),
(∀ (A : Idx → U → Prop) i0,
compl_any (f A i0) = f (compl_any A) i0) →
compl_any (fun i ⇒ union_any (f A i)) =
(fun i ⇒ inter_any (f (compl_any A) i)).
Proof.
intros A f Hf; apply subset_any_ext; intros i x; unfold compl_any.
now rewrite compl_union_any, Hf.
Qed.
Lemma compl_any_inter_any :
∀ (A : Idx → U → Prop)
(f : (Idx → U → Prop) → Idx → Idx → U → Prop),
(∀ (A : Idx → U → Prop) i0,
compl_any (f A i0) = f (compl_any A) i0) →
compl_any (fun i ⇒ inter_any (f A i)) =
(fun i ⇒ union_any (f (compl_any A) i)).
Proof.
intros A f Hf; apply subset_any_ext; intros i x; unfold compl_any.
now rewrite compl_inter_any, Hf.
Qed.
``Distributivity'' of diff.
Lemma diff_union_any_distr_l :
∀ (A : Idx → U → Prop) (B : U → Prop),
diff (union_any A) B = union_any (fun i ⇒ diff (A i) B).
Proof.
intros; now rewrite diff_equiv_def_inter, inter_union_any_distr_r.
Qed.
Lemma diff_union_any_r :
inhabited Idx →
∀ (A : U → Prop) (B : Idx → U → Prop),
diff A (union_any B) = inter_any (fun i ⇒ diff A (B i)).
Proof.
intros; now rewrite diff_equiv_def_inter, compl_union_any, inter_inter_any_distr_l.
Qed.
Lemma diff_union_any :
inhabited Idx →
∀ (A B : Idx → U → Prop),
diff (union_any A) (union_any B) =
union_any (fun i ⇒ inter_any (fun j ⇒ diff (A i) (B j))).
Proof.
intros; rewrite diff_union_any_distr_l; f_equal.
apply fun_ext; intros; now apply diff_union_any_r.
Qed.
Lemma diff_union_any_alt :
inhabited Idx →
∀ (A B : Idx → U → Prop),
diff (union_any A) (union_any B) =
inter_any (fun j ⇒ union_any (fun i ⇒ diff (A i) (B j))).
Proof.
intros; rewrite diff_union_any_r; try easy; f_equal.
apply fun_ext; intros; apply diff_union_any_distr_l.
Qed.
Lemma diff_inter_any_distr_l :
inhabited Idx →
∀ (A : Idx → U → Prop) (B : U → Prop),
diff (inter_any A) B = inter_any (fun i ⇒ diff (A i) B).
Proof.
intros; now rewrite diff_equiv_def_inter, inter_inter_any_distr_r.
Qed.
Lemma diff_inter_any_r :
∀ (A : U → Prop) (B : Idx → U → Prop),
diff A (inter_any B) = union_any (fun i ⇒ diff A (B i)).
Proof.
intros; now rewrite diff_equiv_def_inter, compl_inter_any, inter_union_any_distr_l.
Qed.
Lemma diff_inter_any :
inhabited Idx →
∀ (A B : Idx → U → Prop),
diff (inter_any A) (inter_any B) =
inter_any (fun i ⇒ union_any (fun j ⇒ diff (A i) (B j))).
Proof.
intros; rewrite diff_inter_any_distr_l; try easy; f_equal.
apply fun_ext; intros; apply diff_inter_any_r.
Qed.
Lemma diff_inter_any_alt :
inhabited Idx →
∀ (A B : Idx → U → Prop),
diff (inter_any A) (inter_any B) =
union_any (fun j ⇒ inter_any (fun i ⇒ diff (A i) (B j))).
Proof.
intros; rewrite diff_inter_any_r; f_equal.
apply fun_ext; intros; now apply diff_inter_any_distr_l.
Qed.
Lemma diff_union_inter_any :
∀ (A B : Idx → U → Prop),
diff (union_any A) (inter_any B) =
union_any (fun i ⇒ union_any (fun j ⇒ diff (A i) (B j))).
Proof.
intros; rewrite diff_union_any_distr_l; f_equal.
apply fun_ext; intros; apply diff_inter_any_r.
Qed.
Lemma diff_union_inter_any_alt :
∀ (A B : Idx → U → Prop),
diff (union_any A) (inter_any B) =
union_any (fun j ⇒ union_any (fun i ⇒ diff (A i) (B j))).
Proof.
intros; rewrite diff_inter_any_r; f_equal.
apply fun_ext; intros; apply diff_union_any_distr_l.
Qed.
Lemma diff_inter_union_any :
inhabited Idx →
∀ (A B : Idx → U → Prop),
diff (inter_any A) (union_any B) =
inter_any (fun i ⇒ inter_any (fun j ⇒ diff (A i) (B j))).
Proof.
intros; rewrite diff_inter_any_distr_l; try easy; f_equal.
apply fun_ext; intros; now apply diff_union_any_r.
Qed.
Lemma diff_inter_union_any_alt :
inhabited Idx →
∀ (A B : Idx → U → Prop),
diff (inter_any A) (union_any B) =
inter_any (fun j ⇒ inter_any (fun i ⇒ diff (A i) (B j))).
Proof.
intros; rewrite diff_union_any_r; try easy; f_equal.
apply fun_ext; intros; now apply diff_inter_any_distr_l.
Qed.
End Any_Facts.
Section Prod_Facts.
Facts about Cartesian product.
Context {U1 U2 Idx : Type}.
Lemma prod_union_any_full :
∀ (A1 : Idx → U1 → Prop),
prod (union_any A1) (@fullset U2) =
union_any (prod_any_l A1 fullset).
Proof.
intros; apply subset_ext; subset_any_full_unfold.
intros A; split.
intros [[i HA] _]; now ∃ i.
intros [i [HA _]]; split; now try ∃ i.
Qed.
Lemma prod_full_union_any :
∀ (A2 : Idx → U2 → Prop),
prod (@fullset U1) (union_any A2) =
union_any (prod_any_r fullset A2).
Proof.
intros; apply subset_ext; subset_any_full_unfold.
intros A; split.
intros [_ [i HA]]; now ∃ i.
intros [i [_ HA]]; split; now try ∃ i.
Qed.
Lemma prod_inter_any_full :
∀ (A1 : Idx → U1 → Prop),
prod (inter_any A1) (@fullset U2) =
inter_any (prod_any_l A1 fullset).
Proof.
intros; apply subset_ext; subset_any_full_unfold.
intros A; split.
intros [HA _] i; split; now try apply (HA i).
intros HA; split; try easy; apply HA.
Qed.
Lemma prod_full_inter_any :
∀ (A2 : Idx → U2 → Prop),
prod (@fullset U1) (inter_any A2) =
inter_any (prod_any_r fullset A2).
Proof.
intros; apply subset_ext; subset_any_full_unfold.
intros A; split.
intros [_ HA] i; split; now try apply (HA i).
intros HA; split; try easy; apply HA.
Qed.
End Prod_Facts.