Library schutte.Critical

Add LoadPath "../prelude".
Add LoadPath "../hilbert".
Add LoadPath "../denumerable".

Notation Local "'inhabited' A" := A (at level 200, only parsing).

Require Import Arith.
Require Import Epsilon.
Require Import Ensembles.
Require Import Schutte.
Require Import Ordering_Functions.
Require Import PartialFun.
Require Import Denumerable.
Require Import "Plus".
Require Import AP.
Require Import Classical.
Require Import CNF.
Require Import PartialFix.
Require Import Well_Orders.
Require Import ProofIrrelevance.

Set Implicit Arguments.

Definition critical_fun : forall alpha : OT,
       (forall beta : Well_Orders.M ON, beta < alpha -> Ensemble OT) ->
       ordinal alpha -> OT -> Prop
:=
   fun (alpha :OT)
        (Cr : forall beta,
                beta < alpha ->
               Ensemble OT)
       (o_alpha :ordinal alpha)
       (x : OT) => ordinal x /\(
            (alpha = zero /\ AP x) \/
             (zero < alpha /\
              forall beta (H:beta < alpha), Cr beta H x /\
                 the_ordering_function (Cr beta H) x =x)).

Definition critical : forall alpha, (ordinal alpha) -> Ensemble OT :=
    (PFix ordinal lt_ordinal all_ord_acc
                  (fun (_:OT) => Ensemble OT) critical_fun).

Lemma critical_extensional : forall (x:OT)
          (f g : forall y : OT, y < x -> (fun _ : OT => Ensemble OT) y)
          (Ox : ordinal x),
         (forall (y : OT) (p : y < x), f y p = g y p) ->
          ((critical_fun x f Ox :Ensemble OT)=
            (critical_fun x g Ox:Ensemble OT)).
Proof.
 intros x f g H H0.
 apply Extensionality_Ensembles.
 split.
 unfold critical_fun;red.
 unfold In;intros.
 case H1;auto.
 intros.
 split.
 auto.
 case H3.
 auto.
 right.
 split.
 case H4;auto.
 intros.
 decompose [and] H4.
 rewrite <- (H0 beta H5).
 auto.
 unfold critical_fun;red.
 unfold In;intros.
 case H1;auto.
 intros.
 split.
 auto.
 case H3.
 auto.
 right.
 split.
 case H4;auto.
 intros.
 decompose [and] H4.

 rewrite (H0 beta H5).
 case (H7 beta H5).

 auto.
Qed.

Implicit Arguments critical [alpha].

Lemma critical_eq
     : forall (alpha : OT) (H : ordinal alpha),
       critical H =
       critical_fun alpha
         (fun (y : OT) (h : y < alpha) =>
          critical (lt_ordinal y alpha h))
         H.
Proof (PFix_eq ordinal lt_ordinal all_ord_acc
 (fun _ : OT => Ensemble OT) critical_fun critical_extensional
).

Lemma critical_e : forall alpha (Halpha: ordinal alpha),
                forall x,
                   critical Halpha x -> ordinal x /\(
                   (((alpha = zero) /\ (critical Halpha x <-> AP x)) \/
                   (zero < alpha /\
                                  (forall beta (H:beta < alpha),
                                         critical (lt_ordinal _ _ H) x /\
                                       the_ordering_function
                                         (critical (lt_ordinal _ _ H)) x =x)))).
Proof.
 intros alpha Halpha.
 intro x.
 rewrite (critical_eq alpha Halpha).
 unfold critical_fun at 1.
 intros.
 split.
 case H;auto.
 decompose [and] H.

 case H1;intros.
 clear H1.
  left.
split.
 case H2;auto.
 split.
 intro.
 case H2;auto.
 intro.
 red.
 split.
 auto.
 left;auto.
 right.
 auto.
Qed.

Lemma critical_ord : forall alpha (H:ordinal alpha) x,
                            critical H x -> ordinal x.
Proof.
 intros.
 case (critical_e _ H x).
 auto.
 auto.
Qed.

Lemma inh_ens_OT : inhabited (Ensemble OT).
Proof.
 exact (fun a : OT => False).
Qed.

Definition Cr (alpha : OT) : Ensemble OT :=
   fun beta =>
       exists H: ordinal alpha, critical H beta.

Lemma critical_zero : forall x (H:ordinal zero) , AP x -> critical H x.
Proof.
 intros.
 rewrite critical_eq.
 red.
  split.
  case H0;eauto with schutte.

left;auto.
Qed.

Lemma Cr_zero : forall x, AP x -> Cr zero x.
Proof.
 intros.
 exists ordinal_zero.
 apply critical_zero.
 auto.
Qed.

Lemma critical_pos : forall alpha (Oalpha:ordinal alpha),
   zero < alpha ->
    forall x, ordinal x ->
   (forall beta (H:beta < alpha), (critical (lt_ordinal _ _ H) x) /\
         the_ordering_function (critical (lt_ordinal _ _ H)) x =x) ->
   critical Oalpha x.
 intros.
 rewrite critical_eq.
 red.
  split.
 auto.
right.
 split;auto.
Qed.

Lemma Cr_rw : forall alpha (H:ordinal alpha), Cr alpha = critical H.
Proof.
 intros.
 apply Extensionality_Ensembles.
 unfold Cr.
 split.
 intros beta Hbeta.
 red in Hbeta.
 case Hbeta.
 intro p.

 rewrite (proof_irrelevance( ordinal alpha) H p).
 auto.
 red.
 intros x Hx.
 generalize (critical_ord alpha H x Hx).
 intro.
 red.
 exists H.
 auto.
Qed.

Lemma Cr_pos : forall alpha, zero < alpha ->
                      forall x, ordinal x ->
   (forall beta ,beta < alpha -> (Cr beta x) /\
         the_ordering_function (Cr beta) x =x) ->
   Cr alpha x.
Proof.
 intros.
 assert (ordinal alpha).
 ordi.
 exists H2.
 apply critical_pos;auto.
 intros.
 case (H1 beta H3);intros.
 split;auto.
 rewrite <- Cr_rw;auto.
  rewrite <- Cr_rw;auto.
Qed.



Lemma critical_zero_inv : forall x, critical ordinal_zero x -> AP x.
Proof.
 intros.
 case (critical_e _ ordinal_zero x H).
 destruct 2.

tauto.
 case H1.
 intros.
 case (lt_irr zero).
 auto.
Qed.

Lemma Cr_zero_AP : Cr zero = AP.
Proof.
 apply Extensionality_Ensembles.
 rewrite (Cr_rw zero ordinal_zero).
 split.
 red;intros;red;apply critical_zero_inv;auto.
 red;intros.
 red.
 apply critical_zero;auto.
Qed.


Lemma critical_pos_inv : forall alpha (Oalpha:ordinal alpha),
   zero < alpha ->
    forall x,
   critical Oalpha x ->
   (forall beta (H:beta < alpha), (critical (lt_ordinal _ _ H)) x /\
         the_ordering_function (critical (lt_ordinal _ _ H)) x =x).

 intros.
 case (critical_e _ Oalpha x H0).
 destruct 2.
 decompose [and] H3.
subst alpha.

 case (not_lt_zero beta).
 auto.
 case H3.
 intros.
  auto.

Qed.

Lemma critical_lt : forall alpha beta (H:ordinal alpha)
                                      (H0:ordinal beta),
   beta < alpha -> forall x, critical H x -> critical H0 x.
Proof.
 intros.
 case (critical_e alpha H x);auto.
 intros Hx [[H3 H4]| [H3 H4]].
 subst alpha.
 case (not_lt_zero beta);auto.
 case (H4 beta H1).
 intros.
 rewrite (proof_irrelevance( ordinal beta) H0 (lt_ordinal beta alpha H1)).
 auto.
Qed.

Lemma Critical_incl : forall alpha beta (H :beta <= alpha)
    (Ha : ordinal alpha)(Hb : ordinal beta),
    Included (critical Ha) (critical Hb).
Proof.
 intros.
 case (le_disj H).

 intro;subst beta.
rewrite (proof_irrelevance _ Ha Hb).
 auto.
 intro.
 assert (zero < alpha).
 eauto with schutte.
 red;unfold In;intro.
 intro.
 generalize (critical_pos_inv _ (gt_ordinal _ _ H1) H1 x ).
 intros.
 rewrite (proof_irrelevance _ Hb (lt_ordinal beta alpha H0)).
rewrite (proof_irrelevance _ Ha (gt_ordinal zero alpha H1)) in H2.
generalize (H3 H2).
 intro.
 generalize (H4 _ H0).
 intro.
 case H5;auto.
Qed.

Lemma Cr_incl : forall alpha beta ,beta <= alpha ->
    Included (Cr alpha) (Cr beta).
Proof.
 intros.
  rewrite (Cr_rw _ (ge_ordinal H)).
 rewrite (Cr_rw _ (le_ordinal H)).

 apply Critical_incl;auto.
Qed.

Ltac unfold_CR alpha := let H := fresh in
                      (assert(ordinal alpha);[try ordi | rewrite (Cr_rw alpha H)]).

Lemma Cr_incl' : forall alpha beta ,beta <= alpha ->
    Included (Cr alpha) (Cr beta).
Proof.
 intros.
 unfold_CR alpha.
 unfold_CR beta.
 apply Critical_incl;auto.
Qed.