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.