Evening train...

Lebesgue/measurable.v

@@ -21,6 +21,7 @@ COPYING file for more details.
  of sigma-algebras from the file Subset_system.v where "measurable" is used
  instead of "Sigma_algebra" in almost all lemma names and statements. *)
 
+From Coq Require Import ClassicalChoice.
 From Coq Require Import Lia.
 From Coquelicot Require Import Hierarchy.
 
@@ -260,34 +261,44 @@ Section measurable_gen_Image_Facts.
 Context {E F : Type}. (* Universes. *)
 
 Variable f : E -> F.
-Variable PE1 PE2 : (E -> Prop) -> Prop. (* Subset systems. *)
-Variable PF1 PF2 : (F -> Prop) -> Prop. (* Subset systems. *)
 
-Lemma Image_monot : Incl PE1 PE2 -> Incl (Image f PE1) (Image f PE2).
+Lemma Image_monot :
+  forall PE1 PE2, Incl PE1 PE2 -> Incl (Image f PE1) (Image f PE2).
 Proof.
-intros H B HB; apply H; easy.
+intros PE1 PE2 H B HB; apply H; easy.
 Qed.
 
-Lemma Preimage_monot : Incl PF1 PF2 -> Incl (Preimage f PF1) (Preimage f PF2).
+Lemma Preimage_monot :
+  forall PF1 PF2, Incl PF1 PF2 -> Incl (Preimage f PF1) (Preimage f PF2).
 Proof.
 apply image_monot.
 Qed.
 
-Lemma Preimage_of_Image : Incl (Preimage f (Image f PE1)) PE1.
+Lemma Preimage_of_Image : forall PE, Incl (Preimage f (Image f PE)) PE.
 Proof.
-intros A [B [HB1 HB2]]; rewrite HB2; easy.
+intros PE A [B [HB1 HB2]]; rewrite HB2; easy.
 Qed.
 
-Lemma Image_of_Preimage : Incl PF1 (Image f (Preimage f PF1)).
+Lemma Image_of_Preimage : forall PF, Incl PF (Image f (Preimage f PF)).
 Proof.
-intros B HB; exists B; easy.
+intros PF B HB; exists B; easy.
 Qed.
 
-Lemma toto : Incl PF1 (Image f PE1) -> Incl (Preimage f PF1) PE1.
+Lemma Incl_Image_Preimage_Incl :
+  forall PE PF, Incl PF (Image f PE) -> Incl (Preimage f PF) PE.
 Proof.
-intros; apply Incl_trans with (Preimage f (Image f PE1)).
-(*apply Preimage_monot.*)
-Admitted.
+intros PE PF H; apply Incl_trans with (Preimage f (Image f PE)).
+apply Preimage_monot; easy.
+apply Preimage_of_Image.
+Qed.
+
+Lemma Preimage_Incl_Incl_Image :
+  forall PE PF, Incl (Preimage f PF) PE -> Incl PF (Image f PE).
+Proof.
+intros PE PF H; apply Incl_trans with (Image f (Preimage f PF)).
+apply Image_of_Preimage.
+apply Image_monot; easy.
+Qed.
 
 End measurable_gen_Image_Facts.
 
@@ -323,7 +334,7 @@ rewrite preimage_compl; f_equal; easy.
 (* *)
 intros A HA.
 unfold image in HA.
-destruct (ClassicalChoice.choice
+destruct (choice
     (fun n Bn => measurable genF Bn /\ A n = preimage f Bn) HA) as [B HB].
 exists (union_seq B); split.
 apply measurable_union_seq; intros n; apply HB.
@@ -332,6 +343,17 @@ apply subset_seq_ext.
 intros n; rewrite (proj2 (HB n)); easy.
 Qed.
 
+End measurable_gen_Facts2.
+
+
+Section measurable_gen_Facts3.
+
+Context {E F : Type}. (* Universes. *)
+Variable genE : (E -> Prop) -> Prop. (* Generator. *)
+Variable genF : (F -> Prop) -> Prop. (* Generator. *)
+
+Variable f : E -> F.
+
 Lemma measurable_gen_Preimage :
   measurable (Preimage f genF) = Preimage f (measurable genF).
 Proof.
@@ -340,14 +362,12 @@ apply Ext_equiv; split.
 rewrite <- is_Sigma_algebra_Preimage.
 apply measurable_gen_monot, Preimage_monot, measurable_gen.
 (* *)
+apply Incl_Image_Preimage_Incl, measurable_gen_lub_alt.
+apply is_Sigma_algebra_Image.
+apply Preimage_Incl_Incl_Image, measurable_gen.
+Qed.
 
-
-
-
-
-Admitted.
-
-End measurable_gen_Facts2.
+End measurable_gen_Facts3.
 
 
 Section measurable_correct.

Lebesgue/nat_compl.v

@@ -14,7 +14,9 @@ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
 COPYING file for more details.
 *)
 
+From Coq Require Import Classical.
 From Coq Require Import Arith Nat Lia.
+From Coquelicot Require Import Coquelicot.
 
 
 Section Order_compl.
@@ -79,22 +81,41 @@ End Even_compl.
 
 Section Select_in_pred.
 
+Variable P : nat -> Prop. (* Predicate on natural numbers. *)
+
+Definition useful_finite : (nat -> nat) -> nat -> Prop :=
+  fun phi N =>
+    (forall n, n < S N -> P (phi n)) /\
+    (forall p, P p -> exists n, n < S N /\ p = phi n).
+
+Definition useful_seq : (nat -> nat) -> Prop :=
+  fun phi =>
+    (forall n, P (phi n)) /\
+    (forall p, P p -> exists n, p = phi n).
+
 Lemma keep_useful :
-  forall (P : nat -> Prop), exists (phi : nat -> nat) (optN : option nat),
+  exists (phi : nat -> nat) (optN : option nat),
     (forall n1 n2, n1 < n2 -> phi n1 < phi n2) /\ (* phi injective would be fine too. *)
     match optN with
-    | Some N =>
-        (forall n, n < S N -> P (phi n)) /\
-        (forall p, P p -> exists n, n < S N /\ p = phi n)
-    | None =>
-        (forall n, P (phi n)) /\
-        (forall p, P p -> exists n, p = phi n)
+    | Some N => useful_finite phi N
+    | None => useful_seq phi
     end.
 Proof.
+destruct (LPO (fun N => forall n, N < n -> ~ P n)) as [[N HN] | H].
+intros; apply classic.
+(* *)
+
+
+
+
+
+
+
 Admitted.
 
 Definition get_useful :
-    forall {T : Type}, (nat -> T) -> T -> (nat -> nat) -> option nat -> nat -> T :=
+    forall {T : Type},
+      (nat -> T) -> T -> (nat -> nat) -> option nat -> nat -> T :=
   fun T f f0 phi optN n =>
     match optN with
     | Some N => match (lt_dec n (S N)) with