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.

Brief description

Support for generated subset systems.

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 calSPP 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 calSPP 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.