Library Lebesgue.subset_compl

This file is part of the Coq Numerical Analysis library
Copyright (C) Boldo, Clément, Faissole, Martin, Mayero
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.


From Requisite Require Import stdlib.

From Subsets Require Import Subsets_wDep.

Section FU_seq.


Context {E : Type}.
Variable A : nat E Prop.

Definition layers : nat E Prop :=
  fun nmatch n with
    | 0%natA 0%nat
    | S nfun xA (S n) x ¬ A n x
    end.

Lemma layers_incl : n x, layers n x A n x.
Proof.
intros n x; case n; now simpl.
Qed.

Lemma layers_union :
  ( n x, A n x A (S n) x)
   n x, A n x m, (m n)%nat layers m x.
Proof.
intros HA n x HASn.
induction n.
now 0%nat.
case (in_dec (A n) x); intros HAn.
  destruct IHn as [m [Hm HB]]; try easy; m; now split; [ lia | ].
  now (S n).
Qed.

Lemma layers_union_alt :
  ( n x, A n x A (S n) x)
   n x, ( m, (m n)%nat layers m x) A n x.
Proof.
intros HA n x.
induction n; intros [m [Hm HBn]].
apply layers_incl; replace m with 0%nat in HBn; [ easy | lia ].
case (le_lt_dec m n); intros Hm'.
  apply HA, IHn; now m.
  apply layers_incl; replace (S n) with m; [ easy | lia ].
Qed.

Lemma layers_union_countable :
  ( n x, A n x A (S n) x)
   x, ( n, A n x)
   n, layers n x.
Proof.
intros HA x [na HAn].
assert (HBm : n m, (m n)%nat layers m x).
   na; apply layers_union; try easy.
destruct HBm as [nb [mb [Hmb HBm]]]; now mb.
Qed.

Lemma layers_disjoint :
  ( n x, A n x A (S n) x)
   n m x, layers n x layers m x n = m.
Proof.
intros HA.
assert (HA' : n m x, (n < m)%nat A n x A m x).
  intros n m x Hnm HAn.
  induction m; try lia.
  apply HA.
  destruct (ifflr (Nat.lt_eq_cases n m)) as [nltm | ->]; try easy.
  now apply Nat.lt_succ_r.
  now apply IHm.
assert (HBA' : n x, layers (S n) x A n x False).
  intros n x HBSn HAn; now unfold layers in HBSn.
assert (HBA'' : n m x,
    (n < m)%nat layers m x A n x False).
  intros n m x Hnm HAn HBm.
  apply HBA' with (pred m) x.
  replace (S (pred m)) with m; [ easy | lia ].
  case (ifflr (Nat.lt_eq_cases n (pred m))); try lia; intros Hn.
    apply HA' with n; try easy.
    now replace (pred m) with n.
assert (HB : n m x,
    (n < m)%nat layers n x layers m x False).
  intros n m x Hnm HBn HBm.
  apply HBA'' with n m x; try easy.
  now apply layers_incl.
intros n m x HBn HBm.
case (Nat.lt_total n m); intros Hnm.
exfalso; now apply HB with n m x.
destruct Hnm; try easy.
exfalso; now apply HB with m n x.
Qed.

Definition layers_from_above : nat nat E Prop :=
  fun n0 n xA n0 x ¬ A (n0 + n)%nat x.

Lemma layers_from_above_incr :
   n0,
    ( n x, A (S n) x A n x)
     n x, layers_from_above n0 n x layers_from_above n0 (S n) x.
Proof.
intros n0 HA.
induction n; intros x [HB HB'].
destruct HB'; replace (n0 + 0)%nat with n0; [easy|ring].
split; try easy.
intros H; destruct HB'; apply HA.
replace (S (n0 + S n)) with (n0 + S (S n))%nat; [easy|ring].
Qed.

Lemma layers_from_above_union :
   n0,
    ( n x, A (S n) x A n x)
     x,
      ( n1, layers_from_above n0 n1 x)
      (A n0 x ¬ ( n, A (n0 + n)%nat x)).
Proof.
intros n0 HA x; split.
intros [n1 [HA0 HA0']]; split; try easy; intros HA0''; now destruct HA0'.
intros [HA0 HA0']; apply not_all_ex_not in HA0';
  destruct HA0' as [n HA0n]; now n.
Qed.

Lemma subset_decr_shift :
  ( n x, A (S n) x A n x)
   n0 n x , A (n0 + n)%nat x A n0 x.
Proof.
intros HAn n0 n x; induction n; intros H.
replace n0 with (n0 + 0)%nat; [easy|ring].
apply IHn, HAn; replace (S (n0 + n)) with (n0 + S n)%nat; [easy|ring].
Qed.

Definition partial_union : nat E Prop :=
  fun n x m, (m n)%nat A m x.

Lemma partial_union_nondecr :
   n x, partial_union n x partial_union (S n) x.
Proof.
intros n x HAn.
case (in_dec (A (S n)) x); intros HAn'.
  now (S n).
  destruct HAn as [m [Hm HAm]]; m; split; [ lia | easy ].
Qed.

Lemma partial_union_union :
   x, ( n, A n x) ( n, partial_union n x).
Proof.
intros x; split; intros [n HAn].
n; now n.
destruct HAn as [m [Hm HAm]]; now m.
Qed.

End FU_seq.

Section DU_seq.


Context {E : Type}.

Definition DU : (nat E Prop) nat E Prop :=
  fun A n x
    match n with
    | 0%natA 0%nat x
    | S nA (S n) x ¬ ( p, (p n)%nat A p x)
    end.

Lemma DU_incl :
   (A : nat E Prop) n x,
    DU A n x A n x.
Proof.
intros A; induction n; try easy.
now intros x [Hn _].
Qed.

Lemma DU_disjoint_alt :
   (A : nat E Prop) n p x,
    (p < n)%nat DU A n x ¬ DU A p x.
Proof.
intros A n p x H Hn Hp.
case_eq n; try lia.
intros n' Hn'.
rewrite Hn' in H, Hn; clear Hn' n.
destruct Hn as [H1 H2].
apply DU_incl in Hp.
contradict H2.
p; split; [lia | easy].
Qed.

Lemma DU_disjoint :
   (A : nat E Prop) n p x,
    DU A n x DU A p x n = p.
Proof.
intros A n p x Hn Hp.
case (lt_eq_lt_dec n p); [intros [H | H] | intros H].
contradict Hn; now apply DU_disjoint_alt with (n := p).
easy.
contradict Hp; now apply DU_disjoint_alt with (n := n).
Qed.

Lemma DU_union_alt :
   (A : nat E Prop) n x,
    ( p, (p n)%nat DU A p x)
    ( p, (p n)%nat A p x).
Proof.
intros A; induction n; intros x [p [Hp Hpx]];
   p; split; try easy; now apply DU_incl.
Qed.

Lemma DU_union :
   (A : nat E Prop) n x,
    ( p, (p n)%nat A p x)
    ( p, (p n)%nat DU A p x).
Proof.
assert (H : (A B : E Prop) x, A x B x A x B x ¬ A x).
intros A B x.
case (in_dec A x).
intros H _; now left.
intros H [H' | H'].
contradiction.
right; now split.
intros A n x; induction n; intros [p [Hp Hpx]].
p; split; try easy.
rewrite Nat.le_0_r in Hp; rewrite Hp in Hpx; now rewrite Hp.
destruct H
    with (A := fun x p, (p n)%nat A p x)
         (B := fun xA (S n) x) (x := x) as [H' | H'].
  case (le_lt_eq_dec p (S n)); try easy; clear Hp; intros Hp.
  left; p; split; [lia | easy].
  right; now rewrite Hp in Hpx.
destruct H' as [p' Hp'].
destruct IHn as [i [Hi Hix]].
now p'.
i; split; [lia | easy].
now (S n).
Qed.

Lemma DU_union_countable :
   (A : nat E Prop) x,
    ( n, DU A n x) ( n, A n x).
Proof.
intros A x; split; intros [n Hn].
destruct (DU_union_alt A n x) as [p Hp].
n; split; [lia | easy].
now p.
destruct (DU_union A n x) as [p Hp].
n; split; [lia | easy].
now p.
Qed.

Lemma DU_equiv :
   (A : nat E Prop) n x,
    DU A n x A n x ( p, (p < n)%nat ¬ A p x).
Proof.
intros A n x; destruct n; try easy.
split; intros [HSn Hn]; split; try easy.
intros p Hp Hp'; apply (Nat.lt_succ_r) in Hp; apply Hn.
     p; split; try easy.
    now apply Nat.succ_le_mono, Nat.succ_le_mono.
intros Hp; destruct Hp as [p [plen HA]]; apply (Hn p); try easy.
now apply Nat.succ_le_mono in plen.
Qed.

End DU_seq.