(* This program 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 2.1   *)
(* of the License, or (at your option) any later version.             *)
(*                                                                    *)
(* This program 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      *)
(* GNU General Public License for more details.                       *)
(*                                                                    *)
(* You should have received a copy of the GNU Lesser General Public   *)
(* License along with this program; if not, write to the Free         *)
(* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *)
(* 02110-1301 USA                                                     *)


(* Contribution to the Coq Library   V6.3 (July 1999)                    *)

(****************************************************************************)
(* This contribution was updated for Coq V5.10 by the COQ workgroup.        *)
(* January 1995                                                             *)
(****************************************************************************)
(*                                                                          *)
(*                      Rem Theorem in Baire space                          *)
(*                                                                          *)
(*                           Henk Barendregt                                *)
(*                                                                          *)
(*                           Bastad, June 1993                              *)
(*                               Coq V5.8                                   *)
(*                                                                          *)
(*                                                                          *)
(****************************************************************************)
(*                                  Rem.v                                   *)
(****************************************************************************)

(* Needs classical logic *)

Require Import Classical.


(* Baire Space *)
Definition B := nat -> nat.

Definition Top := B -> Prop.

Definition inclusion (X Y : Top) := forall z : B, X z -> Y z.
Definition equal (X Y : Top) := inclusion X Y /\ inclusion Y X.
Definition complement (X : Top) (z : B) := ~ X z.
Definition union (X Y : Top) (z : B) := X z \/ Y z.
Definition inter (X Y : Top) (z : B) := X z /\ Y z.

Definition neighbour (f : B) (n : nat) (g : B) :=
  forall m : nat, m <= n -> f m = g m.
Definition open (X : Top) :=
  forall f : B, X f -> exists n : nat, inclusion (neighbour f n) X.
Definition closed (X : Top) := open (complement X).
Definition dense (X : Top) :=
  forall (f : B) (n : nat), exists g : B, X g /\ neighbour f n g.
Definition closure (X : Top) (f : B) :=
  forall n : nat, exists g : B, X g /\ neighbour f n g.

Lemma refl_neighbour : forall (n : nat) (x : B), neighbour x n x.
(* Goal: forall (n : nat) (x : B), neighbour x n x *)
unfold neighbour in |- *; auto.
Qed.
Hint Resolve refl_neighbour.

Lemma trans_neighbour :
 forall (n : nat) (f g h : B),
 neighbour f n g -> neighbour g n h -> neighbour f n h.
(* Goal: forall (n : nat) (f g h : B) (_ : neighbour f n g) (_ : neighbour g n h), neighbour f n h *)
unfold neighbour in |- *.
(* Goal: forall (n : nat) (f g h : B) (_ : forall (m : nat) (_ : le m n), @eq nat (f m) (g m)) (_ : forall (m : nat) (_ : le m n), @eq nat (g m) (h m)) (m : nat) (_ : le m n), @eq nat (f m) (h m) *)
intros.
(* Goal: @eq nat (f m) (h m) *)
rewrite (H m); trivial.
(* Goal: @eq nat (g m) (h m) *)
apply H0; trivial.
Qed.

Lemma closedc_clX : forall X : Top, closed (closure X).
(* Goal: forall X : Top, closed (closure X) *)
unfold closed, closure in |- *.
(* Goal: forall X : Top, open (complement (fun f : B => forall n : nat, @ex B (fun g : B => and (X g) (neighbour f n g)))) *)
unfold open, complement in |- *.
(* Goal: forall (X : Top) (f : B) (_ : not (forall n : nat, @ex B (fun g : B => and (X g) (neighbour f n g)))), @ex nat (fun n : nat => inclusion (neighbour f n) (fun z : B => not (forall n0 : nat, @ex B (fun g : B => and (X g) (neighbour z n0 g))))) *)
intros X f complement_clX.
generalize
 (not_all_ex_not nat (fun n : nat => exists g : B, X g /\ neighbour f n g)
    complement_clX). 
(* Goal: forall _ : @ex nat (fun n : nat => not (@ex B (fun g : B => and (X g) (neighbour f n g)))), @ex nat (fun n : nat => inclusion (neighbour f n) (fun z : B => not (forall n0 : nat, @ex B (fun g : B => and (X g) (neighbour z n0 g))))) *)
simple induction 1; intros n H1.
(* Goal: @ex nat (fun n0 : nat => inclusion (fun g0 : B => forall (m : nat) (_ : le m n0), @eq nat (g m) (g0 m)) (fun z : B => not (forall (m : nat) (_ : le m n), @eq nat (f m) (z m)))) *)
exists n.
(* Goal: inclusion (neighbour f n) (fun z : B => not (forall n : nat, @ex B (fun g : B => and (X g) (neighbour z n g)))) *)
unfold inclusion in |- *; intros g fng.
(* Goal: not (forall n : nat, @ex B (fun g0 : B => and (X g0) (neighbour g n g0))) *)
unfold not in |- *; intro H2.
(* Goal: False *)
apply H1.
(* Goal: @ex B (fun g : B => and (X g) (neighbour f n g)) *)
elim (H2 n).
(* Goal: forall (n : nat) (f g h : B) (_ : forall (m : nat) (_ : le m n), @eq nat (f m) (g m)) (_ : forall (m : nat) (_ : le m n), @eq nat (g m) (h m)) (m : nat) (_ : le m n), @eq nat (f m) (h m) *)
simple induction 1; intros.
(* Goal: @ex B (fun g : B => and (X g) (neighbour f n g)) *)
exists x; split; trivial.
(* Goal: neighbour f n x *)
apply trans_neighbour with g; trivial.
Qed.
Hint Resolve closedc_clX.

Lemma Xinc_clX : forall X : Top, inclusion X (closure X).
(* Goal: forall X : Top, inclusion X (closure X) *)
unfold inclusion in |- *; intros X f Xf.
(* Goal: closure X f *)
unfold closure in |- *; intro n.
(* Goal: @ex B (fun g : B => and (X g) (neighbour f n g)) *)
exists f; split; trivial.
Qed.

Lemma Lemma1 :
 forall X : Top,
 equal X (inter (closure X) (union X (complement (closure X)))).
(* Goal: forall X : Top, equal X (inter (closure X) (union X (complement (closure X)))) *)
unfold equal, inclusion in |- *; intro X; split.
(* Goal: forall (n : nat) (f g h : B) (_ : forall (m : nat) (_ : le m n), @eq nat (f m) (g m)) (_ : forall (m : nat) (_ : le m n), @eq nat (g m) (h m)) (m : nat) (_ : le m n), @eq nat (f m) (h m) *)
unfold inter, union, closure in |- *; intros.
(* Goal: and (open (nbh f n)) (closed (nbh f n)) *)
split.
(* Goal: forall n : nat, @ex B (fun g : B => and (X g) (neighbour z n g)) *)
(* Goal: or (X z) (complement (fun f : B => forall n : nat, @ex B (fun g : B => and (X g) (neighbour f n g))) z) *)
(* Goal: forall (z : B) (_ : inter (closure X) (union X (complement (closure X))) z), X z *)
intro n; exists z; split; auto.
(* Goal: or (X x) (complement (closure X) x) *)
(* Goal: forall _ : not (closure X f), @ex B (fun g : B => and (union X (complement (closure X)) g) (neighbour f n g)) *)
left; trivial.
(* Goal: forall (n : nat) (f g h : B) (_ : forall (m : nat) (_ : le m n), @eq nat (f m) (g m)) (_ : forall (m : nat) (_ : le m n), @eq nat (g m) (h m)) (m : nat) (_ : le m n), @eq nat (f m) (h m) *)
unfold inter, union, closure in |- *; intros.
(* Goal: forall (n : nat) (f g h : B) (_ : forall (m : nat) (_ : le m n), @eq nat (f m) (g m)) (_ : forall (m : nat) (_ : le m n), @eq nat (g m) (h m)) (m : nat) (_ : le m n), @eq nat (f m) (h m) *)
elim H; intros.
(* Goal: X z *)
elim H1; trivial.
(* Goal: forall (n : nat) (f g h : B) (_ : forall (m : nat) (_ : le m n), @eq nat (f m) (g m)) (_ : forall (m : nat) (_ : le m n), @eq nat (g m) (h m)) (m : nat) (_ : le m n), @eq nat (f m) (h m) *)
unfold complement in |- *; intros.
(* Goal: X z *)
elim (H2 H0).
Qed.

Lemma density : forall X : Top, dense (union X (complement (closure X))).
(* Goal: forall X : Top, dense (union X (complement (closure X))) *)
unfold dense in |- *; intros X f n.
(* Goal: @ex B (fun g : B => and (union X (complement (closure X)) g) (neighbour f n g)) *)
elim (classic (closure X f)).
(* Goal: forall _ : closure X f, @ex B (fun g : B => and (union X (complement (closure X)) g) (neighbour f n g)) *)
(* Goal: forall _ : not (closure X f), @ex B (fun g : B => and (union X (complement (closure X)) g) (neighbour f n g)) *)
intro clXf.
(* Goal: @ex B (fun g : B => and (union X (complement (closure X)) g) (neighbour f n g)) *)
(* Goal: forall _ : not (closure X f), @ex B (fun g : B => and (union X (complement (closure X)) g) (neighbour f n g)) *)
elim (clXf n).
(* Goal: forall (x : B) (_ : and (X x) (neighbour f n x)), @ex B (fun g : B => and (union X (complement (closure X)) g) (neighbour f n g)) *)
(* Goal: forall _ : not (closure X f), @ex B (fun g : B => and (union X (complement (closure X)) g) (neighbour f n g)) *)
simple induction 1.
(* Goal: forall (_ : X x) (_ : neighbour f n x), @ex B (fun g : B => and (union X (complement (closure X)) g) (neighbour f n g)) *)
(* Goal: forall _ : not (closure X f), @ex B (fun g : B => and (union X (complement (closure X)) g) (neighbour f n g)) *)
intros; exists x.
(* Goal: and (union X (complement (closure X)) f) (neighbour f n f) *)
split; trivial.
(* Goal: union X (complement (closure X)) f *)
unfold union in |- *.
(* Goal: or (X x) (complement (closure X) x) *)
(* Goal: forall _ : not (closure X f), @ex B (fun g : B => and (union X (complement (closure X)) g) (neighbour f n g)) *)
left; trivial.
(* Goal: forall _ : not (closure X f), @ex B (fun g : B => and (union X (complement (closure X)) g) (neighbour f n g)) *)
intro notclXf. 
(* Goal: forall (n : nat) (f g h : B) (_ : forall (m : nat) (_ : le m n), @eq nat (f m) (g m)) (_ : forall (m : nat) (_ : le m n), @eq nat (g m) (h m)) (m : nat) (_ : le m n), @eq nat (f m) (h m) *)
exists f; intros.
(* Goal: and (union X (complement (closure X)) f) (neighbour f n f) *)
split; trivial.
(* Goal: union X (complement (closure X)) f *)
unfold union in |- *.
(* Goal: or (X f) (complement (closure X) f) *)
right; trivial.
Qed.
Hint Resolve density.

Theorem Rem :
 forall X : Top,
 exists Y : Top, (exists Z : Top, closed Y /\ dense Z /\ equal X (inter Y Z)).
(* Goal: forall X : Top, @ex Top (fun Y : Top => @ex Top (fun Z : Top => and (closed Y) (and (dense Z) (equal X (inter Y Z))))) *)
intro X; exists (closure X).
(* Goal: @ex Top (fun Z : Top => and (closed (closure X)) (and (dense Z) (equal X (inter (closure X) Z)))) *)
exists (union X (complement (closure X))).
(* Goal: and (dense (union X (complement (closure X)))) (equal X (inter (closure X) (union X (complement (closure X))))) *)
split; auto.
(* Goal: and (dense (union X (complement (closure X)))) (equal X (inter (closure X) (union X (complement (closure X))))) *)
split; auto.
(* Goal: equal X (inter (closure X) (union X (complement (closure X)))) *)
apply Lemma1.
Qed.
Require Import Lt.

Definition nbh := neighbour.
Definition clopen (X : Top) := open X /\ closed X.

Lemma clopenbasis : forall (f : B) (n : nat), clopen (nbh f n).
(* Goal: forall (f : B) (n : nat), clopen (nbh f n) *)
intros f n.
(* Goal: clopen (nbh f n) *)
unfold clopen in |- *.
(* Goal: and (open (nbh f n)) (closed (nbh f n)) *)
split.
(* Goal: open (nbh f n) *)
(* Goal: closed (nbh f n) *)
unfold open in |- *; intro g.
(* Goal: forall _ : nbh f n g, @ex nat (fun n0 : nat => inclusion (neighbour g n0) (nbh f n)) *)
(* Goal: closed (nbh f n) *)
intro Ofng.
(* Goal: @ex nat (fun n0 : nat => inclusion (neighbour g n0) (nbh f n)) *)
(* Goal: closed (nbh f n) *)
exists (S n).
(* Goal: inclusion (fun g0 : B => forall (m : nat) (_ : le m n), @eq nat (g m) (g0 m)) (fun z : B => not (forall (m : nat) (_ : le m n), @eq nat (f m) (z m))) *)
unfold inclusion in |- *.
(* Goal: forall (z : B) (_ : neighbour g (S n) z), nbh f n z *)
(* Goal: closed (nbh f n) *)
intros h OhSnz.
(* Goal: forall (n : nat) (f g h : B) (_ : neighbour f n g) (_ : neighbour g n h), neighbour f n h *)
unfold nbh in |- *; unfold neighbour in |- *.
(* Goal: forall (m : nat) (_ : le m n), @eq nat (f m) (h m) *)
(* Goal: closed (nbh f n) *)
intros m lemn.
(* Goal: @eq nat (f m) (h m) *)
(* Goal: closed (nbh f n) *)
unfold neighbour in OhSnz.
(* Goal: @eq nat (f m) (h m) *)
(* Goal: closed (nbh f n) *)
unfold nbh in Ofng; unfold neighbour in Ofng.
(* Goal: @eq nat (f m) (h m) *)
(* Goal: closed (nbh f n) *)
generalize (Ofng m lemn).
(* Goal: forall _ : @eq nat (f m) (g m), @eq nat (f m) (h m) *)
(* Goal: closed (nbh f n) *)
intro E; rewrite E.
(* Goal: @eq nat (g m) (h m) *)
(* Goal: closed (nbh f n) *)
auto.
(* Goal: closed (nbh f n) *)
unfold closed, nbh in |- *.
(* Goal: open (complement (neighbour f n)) *)
unfold open, complement, neighbour in |- *.
(* Goal: forall (f0 : B) (_ : not (forall (m : nat) (_ : le m n), @eq nat (f m) (f0 m))), @ex nat (fun n0 : nat => inclusion (fun g : B => forall (m : nat) (_ : le m n0), @eq nat (f0 m) (g m)) (fun z : B => not (forall (m : nat) (_ : le m n), @eq nat (f m) (z m)))) *)
intro g.
(* Goal: forall _ : not (forall (m : nat) (_ : le m n), @eq nat (f m) (g m)), @ex nat (fun n0 : nat => inclusion (fun g0 : B => forall (m : nat) (_ : le m n0), @eq nat (g m) (g0 m)) (fun z : B => not (forall (m : nat) (_ : le m n), @eq nat (f m) (z m)))) *)
intro notgfn.
(* Goal: @ex nat (fun n0 : nat => inclusion (fun g0 : B => forall (m : nat) (_ : le m n0), @eq nat (g m) (g0 m)) (fun z : B => not (forall (m : nat) (_ : le m n), @eq nat (f m) (z m)))) *)
exists n.
(* Goal: inclusion (fun g0 : B => forall (m : nat) (_ : le m n), @eq nat (g m) (g0 m)) (fun z : B => not (forall (m : nat) (_ : le m n), @eq nat (f m) (z m))) *)
unfold inclusion in |- *.
(* Goal: forall (z : B) (_ : forall (m : nat) (_ : le m n), @eq nat (g m) (z m)), not (forall (m : nat) (_ : le m n), @eq nat (f m) (z m)) *)
intro h.
(* Goal: forall _ : forall (m : nat) (_ : le m n), @eq nat (g m) (h m), not (forall (m : nat) (_ : le m n), @eq nat (f m) (h m)) *)
intro hgn.
(* Goal: not (forall (m : nat) (_ : le m n), @eq nat (f m) (h m)) *)
unfold not in |- *; intros fhn.
(* Goal: False *)
apply notgfn.
(* Goal: forall (m : nat) (_ : le m n), @eq nat (f m) (g m) *)
intros p psn.
(* Goal: @eq nat (f p) (g p) *)
rewrite (fhn p psn).
(* Goal: @eq nat (h p) (g p) *)
rewrite (hgn p psn); trivial.
Qed.


