Proof of Uac_Ifc_wF_is_Open.

WIP: Open_equiv.

Lebesgue/Set_theory/Set_system/Set_system_any.v

@@ -15,6 +15,7 @@ COPYING file for more details.
 *)
 
 From Coq Require Import ClassicalChoice.
+From Coq Require Import Lia.
 
 Require Import Set_system_base Set_system_def.
 
@@ -350,7 +351,7 @@ Lemma is_Open_is_Closed_complp_any_equiv :
 Proof.
 intros; rewrite is_Open_equiv, is_Closed_equiv.
 rewrite <- wFull_wEmpty_complp_any, <- wEmpty_wFull_complp_any,
-    <- Inter_Union_complp_any, Interf_any_complp_any_equiv; easy.
+    Union_complp_any_equiv, Interf_any_complp_any_equiv; easy.
 Qed.
 
 Lemma is_Closed_is_Open_complp_any_equiv :
@@ -491,42 +492,81 @@ Section Basis_Facts3.
 Context {U : Type}.
 Variable genU : set_system U.
 
-Definition Uac_Ifc : set_system U := Union_any_closure (Inter_finite_closure genU).
+Definition Uac_Ifc_wF : set_system U := Union_any_closure (Inter_finite_closure_wF genU).
 
-Lemma Uac_Ifc_Gen : Incl genU Uac_Ifc.
+Lemma Uac_Ifc_wF_Gen : Incl genU Uac_Ifc_wF.
 Proof.
-intros A HA.
-rewrite <- unionp_any_singleton; apply Uac; intros B HB; induction HB.
-rewrite <- (inter_finite_cst A 0); apply Ifc; intros; easy.
+apply Incl_trans with (Union_any_closure (Inter_finite_closure genU)).
+apply Incl_trans with (Inter_finite_closure genU).
+apply Inter_finite_closure_Gen.
+apply Union_any_closure_Gen.
+apply Union_any_closure_monot, incl_add_r.
+Qed.
+
+(*
+Lemma Uac_Ifc_wFull :
+  wFull genU -> Uac_Ifc_wF = Union_any_closure (Inter_finite_closure genU).
+Proof.
+intros H; unfold Uac_Ifc_wF; f_equal; apply Ext_equiv; split; intros A HA.
+destruct HA as [HA | HA]; try easy;
+    rewrite HA; apply Inter_finite_closure_Gen; easy.
+apply incl_add_r; easy.
 Qed.
+*)
 
-Lemma Uac_Ifc_is_Open : is_Open Uac_Ifc.
+Lemma Uac_Ifc_wF_is_Open : is_Open Uac_Ifc_wF.
 Proof.
 apply Union_any_closure_is_Open.
-apply unionp_any_full, Ifc_full.
-intros C D [ | A N HA] [ | B M HB]; clear C D.
-1,2 : rewrite inter_fullset_l.
-3: rewrite inter_fullset_r.
-4: rewrite inter_inter_finite_distr.
+apply unionp_any_full; right; easy.
+intros A B [HA | HA] [HB | HB].
+(* *)
+induction HA as [A N HA], HB as [B M HB].
+rewrite inter_inter_finite_distr.
+exists (singletonp_any (inter_finite (append A B N) (S N + M))); split.
+intros C HC; induction HC; left; apply Ifc;
+    intros; apply append_in with M; try lia; easy.
+symmetry; apply unionp_any_singleton.
+(* *)
+induction HA as [A N HA]; rewrite HB.
+rewrite inter_fullset_r.
+exists (singletonp_any (inter_finite A N)); split.
+intros C HC; induction HC; left; easy.
+symmetry; apply unionp_any_singleton.
 (* *)
+rewrite HA; induction HB as [B M HB].
+rewrite inter_fullset_l.
+exists (singletonp_any (inter_finite B M)); split.
+intros C HC; induction HC; left; easy.
+symmetry; apply unionp_any_singleton.
+(* *)
+rewrite HA, HB, inter_fullset_r.
 exists (singletonp_any fullset); split.
-intros A HA; induction HA; apply Ifc_full.
-
-
-
-
-Admitted.
+intros C HC; induction HC; right; easy.
+symmetry; apply unionp_any_singleton.
+Qed.
 
-Lemma Open_equiv : wFull genU -> Open genU = Uac_Ifc.
+Lemma Open_equiv : Open genU = Uac_Ifc_wF.
 Proof.
-intros H.
 apply Ext_equiv; split; intros A HA.
 (* *)
 induction HA as [A HA | | | A N HA1 HA2 | Idx fA HIdx HfA1 HfA2].
-apply Uac_Ifc_Gen; easy.
+apply Uac_Ifc_wF_Gen; easy.
 rewrite <- unionp_any_nullary; apply Uac; easy.
+apply Union_any_closure_Gen; right; easy.
+(* . *)
+destruct (choice (fun (i : {n | n < S N}) QB =>
+    Incl QB (Inter_finite_closure_wF genU) /\
+    A (proj1_sig i) = unionp_any QB)) as [QB HQB].
+  intros [n Hn]; simpl; induction (HA2 n Hn) as [QB HQB].
+  exists QB; repeat split; easy.
+assert (HA3 : inter_finite A N = unionp_any (interf_any QB)).
+  admit.
+rewrite HA3; apply Uac.
+intros C HC.
+
+
+Search incl interf_any.
 
-apply Uac_Ifc_Gen; easy.
 
 admit.
 
@@ -541,7 +581,11 @@ destruct (empty_dec Q) as [HQ2 | HQ2].
 rewrite empty_equiv in HQ2; rewrite HQ2, unionp_any_nullary; apply Open_wEmpty.
 apply Open_Union_any; try easy.
 apply Incl_trans with (Inter_finite_closure genU); try easy.
-intros A HA; induction HA; apply Open_Inter_finite.
+intros A HA.
+
+
+
+; induction HA; apply Open_Inter_finite.
 intros; apply Open_Gen; auto.
 Admitted.