Library Lebesgue.Subset_system_gen
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 generated subset systems.
Brief description
From Subsets Require Import Subsets.
From Lebesgue Require Import Subset_system_def Subset_system_base.
Section Subset_system_Gen_Def0.
Context {U : Type}.
Variable Idx : Type.
Variable PP QQ : ((U → Prop) → Prop) → Prop.
Definition IIncl : Prop := @Incl (U → Prop) PP QQ.
Definition SSame : Prop := @Same (U → Prop) PP QQ.
Definition AAnd := fun calS ⇒ PP calS ∧ QQ calS.
Definition IInter_any : Prop := @Inter_any (U → Prop) Idx PP.
End Subset_system_Gen_Def0.
Section Subset_system_Gen_Def.
Context {Idx U : Type}.
Variable PP : ((U → Prop) → Prop) → Prop. Variable gen : (U → Prop) → Prop.
Definition Gen : (U → Prop) → Prop :=
fun A ⇒
∀ (calS : (U → Prop) → Prop),
PP calS → Incl gen calS → calS A.
Definition IInter_compat :=
∀ (PP' : ((U → Prop) → Prop) → Prop),
IIncl PP' PP →
PP (fun A ⇒ ∀ (calS : (U → Prop) → Prop), PP' calS → calS A).
End Subset_system_Gen_Def.
Section Subset_system_Gen_Facts1.
Context {U : Type}.
Variable PP : ((U → Prop) → Prop) → Prop.
Lemma IInter_compat_correct : IInter_compat PP ↔ ∀ Idx, IInter_any Idx PP.
Proof.
split; intros H.
intros Idx calS HcalS.
rewrite Ext with (Q := fun A ⇒ ∀ calT, (∃ idx, calT = calS idx) → calT A).
apply (H (fun calS' ⇒ ∃ idx, calS' = calS idx)).
intros calT [idx HcalT]; now rewrite HcalT.
intros A; split; intros HA.
intros calT [idx Hidx]; now rewrite Hidx.
intros idx; apply (HA (calS idx)); now ∃ idx.
intros PP' HP'.
unfold IInter_any, Inter_any in H.
apply H. intros calS; apply HP'.
Abort.
Lemma Gen_ni_gen : ∀ gen, Incl gen (Gen PP gen).
Proof.
intros gen A HA calS _ HcalS; now apply HcalS.
Qed.
Hypothesis HPP : IInter_compat PP.
Lemma Gen_is_PP : ∀ gen, PP (Gen PP gen).
Proof.
intros gen.
specialize (HPP (fun calS ⇒ PP calS ∧ Incl gen calS)); simpl in HPP.
rewrite (Ext (Gen PP gen)
(fun A ⇒ ∀ calS, PP calS ∧ Incl gen calS → calS A)).
now apply HPP.
intros A; split; intros HA calS;
[intros [HcalS1 HcalS2] | intros HcalS1 HcalS2]; now apply HA.
Qed.
Lemma Gen_lub :
∀ gen calS,
PP calS → Incl gen calS → Incl (Gen PP gen) calS.
Proof.
intros gen calS HcalS1 HcalS2 A HA; now apply HA.
Qed.
Lemma Gen_lub_alt :
∀ gen0 gen1,
Incl gen0 (Gen PP gen1) → Incl (Gen PP gen0) (Gen PP gen1).
Proof.
intros; apply Gen_lub; [apply Gen_is_PP | easy].
Qed.
Lemma Gen_monot :
∀ gen0 gen1, Incl gen0 gen1 → Incl (Gen PP gen0) (Gen PP gen1).
Proof.
intros gen0 gen1 H; apply Gen_lub_alt, (Incl_trans _ _ _ H), Gen_ni_gen.
Qed.
Lemma Gen_idem : ∀ calS, PP calS ↔ Gen PP calS = calS.
Proof.
intros calS; split; intros HcalS.
apply Ext_equiv; split; [now apply Gen_lub | apply Gen_ni_gen].
rewrite <- HcalS; apply Gen_is_PP.
Qed.
Lemma Gen_ext :
∀ gen0 gen1,
Incl gen0 (Gen PP gen1) →
Incl gen1 (Gen PP gen0) →
Gen PP gen0 = Gen PP gen1.
Proof.
intros gen0 gen1 H01 H10.
apply Ext_equiv; split; now apply Gen_lub_alt.
Qed.
Lemma Gen_union_eq :
∀ gen0 gen1,
Incl gen1 (Gen PP gen0) →
Gen PP (union gen0 gen1) = Gen PP gen0.
Proof.
intros gen0 gen1 H10.
apply Gen_ext.
rewrite <- (union_left_equiv gen1 (Gen PP gen0)) in H10.
rewrite <- H10.
apply union_monot_l, Gen_ni_gen.
apply Incl_trans with (union gen0 gen1).
apply union_ub_l.
apply Gen_ni_gen.
Qed.
End Subset_system_Gen_Facts1.
Section Subset_system_Gen_Facts2.
Context {U : Type}.
Variable PP QQ : ((U → Prop) → Prop) → Prop.
Hypothesis HP : IInter_compat PP.
Hypothesis HPQ : IIncl PP QQ.
Lemma Gen_monot_PP : ∀ gen, Incl (Gen QQ gen) (Gen PP gen).
Proof.
intros gen A HA calS HcalS1 HcalS2.
apply HA; try easy.
now apply HPQ.
Qed.
Lemma Gen_comp : ∀ gen, Gen PP gen = Gen PP (Gen QQ gen).
Proof.
intros gen; apply Ext_equiv; split.
now apply Gen_monot, Gen_ni_gen.
apply Gen_lub_alt; try easy.
apply Gen_monot_PP.
Qed.
End Subset_system_Gen_Facts2.
Section Subset_system_Gen_Facts3.
Context {U : Type}.
Variable PP QQ RR : ((U → Prop) → Prop) → Prop.
Hypothesis HQ : IInter_compat QQ.
Hypothesis HPQR : IIncl (AAnd QQ RR) PP.
Lemma Gen_upgrade :
∀ gen,
RR (Gen QQ gen) →
Incl (Gen PP gen) (Gen QQ gen).
Proof.
intros gen HQR.
apply Gen_lub.
apply HPQR; split; try easy.
now apply Gen_is_PP.
apply Gen_ni_gen.
Qed.
End Subset_system_Gen_Facts3.
Section Subset_system_Gen_Facts4.
Context {U : Type}.
Variable PP QQ RR : ((U → Prop) → Prop) → Prop.
Hypothesis HPQ : ∀ gen, Gen PP gen = Gen PP (Gen QQ gen).
Hypothesis HQR : ∀ gen, Gen QQ gen = Gen QQ (Gen RR gen).
Lemma Gen_comp_trans :
∀ gen, Gen PP gen = Gen PP (Gen RR gen).
Proof.
intros gen; now rewrite (HPQ (Gen RR gen)), <- HQR.
Qed.
End Subset_system_Gen_Facts4.
Section Subset_system_Gen_Nonempty_Facts0.
Context {U : Type}.
Variable PP : ((U → Prop) → Prop) → Prop.
Let PP' := AAnd PP Nonempty.
Lemma NNonempty :
∀ calS, Nonempty calS → PP' calS ↔ PP calS.
Proof.
intros; now unfold PP', AAnd.
Qed.
Lemma Gen_Nonempty :
∀ gen, Nonempty gen → Gen PP' gen = Gen PP gen.
Proof.
intros gen Hgen; apply Ext_equiv; split;
intros A HA calS HcalS1 HcalS2; apply HA; try easy.
unfold AAnd; split; try easy.
now apply (Nonempty_Incl gen).
now unfold PP', AAnd in HcalS1.
Qed.
End Subset_system_Gen_Nonempty_Facts0.
Section Subset_system_Gen_Nonempty_Facts1.
Context {U : Type}.
Variable PP QQ RR : ((U → Prop) → Prop) → Prop.
Let PP' := AAnd PP Nonempty.
Lemma Gen_ni_gen_Nonempty :
∀ gen, Nonempty gen → Incl gen (Gen PP' gen).
Proof.
intros gen Hgen.
unfold PP'; rewrite Gen_Nonempty; try easy.
apply Gen_ni_gen.
Qed.
Hypothesis HP : IInter_compat PP.
Lemma Gen_is_PP_Nonempty :
∀ gen, Nonempty gen → PP' (Gen PP' gen).
Proof.
intros gen Hgen.
unfold PP'; rewrite Gen_Nonempty; try easy; split.
now apply Gen_is_PP.
apply Nonempty_Incl with gen; try easy.
apply Gen_ni_gen.
Qed.
Lemma Gen_lub_Nonempty :
∀ gen calS,
Nonempty gen → PP' calS → Incl gen calS → Incl (Gen PP' gen) calS.
Proof.
intros gen calS Hgen [H2 _] H3.
unfold PP'; rewrite Gen_Nonempty; try easy.
now apply Gen_lub.
Qed.
Lemma Gen_lub_alt_Nonempty :
∀ gen0 gen1,
Nonempty gen0 → Nonempty gen1 →
Incl gen0 (Gen PP' gen1) → Incl (Gen PP' gen0) (Gen PP' gen1).
Proof.
intros gen0 gen1 Hgen0 Hgen1.
unfold PP'; rewrite Gen_Nonempty; try easy; rewrite Gen_Nonempty; try easy.
now apply Gen_lub_alt.
Qed.
Lemma Gen_monot_Nonempty :
∀ gen0 gen1,
Nonempty gen0 → Incl gen0 gen1 → Incl (Gen PP' gen0) (Gen PP' gen1).
Proof.
intros gen0 gen1 Hgen0 H.
assert (Hgen1 : Nonempty gen1) by now apply Nonempty_Incl with gen0.
unfold PP'; rewrite Gen_Nonempty; try easy; rewrite Gen_Nonempty; try easy.
now apply Gen_monot.
Qed.
Lemma Gen_idem_Nonempty :
∀ calS,
Nonempty calS →
PP' calS ↔ Gen PP' calS = calS.
Proof.
intros calS HcalS.
unfold PP'; rewrite Gen_Nonempty; try easy.
rewrite NNonempty; try easy.
now apply Gen_idem.
Qed.
Lemma Gen_ext_Nonempty :
∀ gen0 gen1,
Nonempty gen0 → Nonempty gen1 →
Incl gen0 (Gen PP' gen1) →
Incl gen1 (Gen PP' gen0) →
Gen PP' gen0 = Gen PP' gen1.
Proof.
intros gen0 gen1 Hgen0 Hgen1.
unfold PP'; rewrite Gen_Nonempty; try easy; rewrite Gen_Nonempty; try easy.
now apply Gen_ext.
Qed.
Lemma Gen_union_eq_Nonempty :
∀ gen0 gen1,
Nonempty gen0 → Nonempty gen1 →
Incl gen1 (Gen PP' gen0) →
Gen PP' (union gen0 gen1) = Gen PP' gen0.
Proof.
intros gen0 gen1 Hgen0 Hgen1.
assert (Hgen01 : Nonempty (union gen0 gen1)).
apply Nonempty_Incl with gen0; try easy; apply union_ub_l.
unfold PP'; rewrite Gen_Nonempty; try easy; rewrite Gen_Nonempty; try easy.
now apply Gen_union_eq.
Qed.
Let QQ' := AAnd QQ Nonempty.
Hypothesis HQ : IInter_compat QQ.
Hypothesis HPQ : IIncl PP QQ.
Lemma Gen_monot_PP_Nonempty :
∀ gen,
Nonempty gen →
Incl (Gen QQ' gen) (Gen PP gen).
Proof.
intros gen Hgen.
unfold QQ'; rewrite Gen_Nonempty; try easy.
now apply Gen_monot_PP.
Qed.
Lemma Gen_comp_Nonempty :
∀ gen,
Nonempty gen →
Gen PP gen = Gen PP (Gen QQ' gen).
Proof.
intros gen Hgen.
unfold QQ'; rewrite Gen_Nonempty; try easy.
now apply Gen_comp.
Qed.
Hypothesis HPQR : IIncl (AAnd QQ RR) PP.
Lemma Gen_upgrade_Nonempty :
∀ gen,
Nonempty gen →
RR (Gen QQ gen) →
Incl (Gen PP gen) (Gen QQ' gen).
Proof.
intros gen Hgen.
unfold QQ'; rewrite Gen_Nonempty; try easy.
now apply Gen_upgrade.
Qed.
End Subset_system_Gen_Nonempty_Facts1.
Section Subset_system_Gen_Facts6.
Context {U1 U2 : Type}.
Variable PP : ∀ (U : Type), ((U → Prop) → Prop) → Prop.
Hypothesis PP_IInter_compat : ∀ U, IInter_compat (PP U).
Variable genU1 : (U1 → Prop) → Prop.
Variable genU2 : (U2 → Prop) → Prop.
Definition PP1 := PP U1.
Definition PP2 := PP U2.
Definition PP_prod := PP (U1 × U2).
Definition Product : (U1 × U2 → Prop) → Prop :=
fun A ⇒ ∃ (A1 : U1 → Prop) (A2 : U2 → Prop),
Gen PP1 genU1 A1 ∧ Gen PP2 genU2 A2 ∧
A = prod A1 A2.
Lemma Product_wFull :
(∀ U, IIncl (PP U) wFull) →
wFull Product.
Proof.
intros H; ∃ fullset; ∃ fullset; repeat split.
1,2: apply H; try now apply Gen_is_PP.
now rewrite prod_full.
Qed.
End Subset_system_Gen_Facts6.