Library schutte.CNF
Add LoadPath "../prelude".
Add LoadPath "../hilbert".
Add LoadPath "../denumerable".
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.
Set Implicit Arguments.
Inductive Olist : Type :=
nil : Olist
| cons : OT -> Olist -> Olist.
Fixpoint eval (ol : Olist) : OT :=
match ol with nil => zero
| (cons alpha ol') => phi0 alpha + eval ol'
end.
Inductive sorted : Olist -> Prop :=
| sorted0 : sorted nil
| sorted1 :forall alpha, ordinal alpha -> sorted (cons alpha nil)
| sortedn : forall alpha beta ol, beta <= alpha ->
sorted (cons beta ol) ->
sorted (cons alpha (cons beta ol)).
Hint Constructors sorted.
Inductive o_forall (P : OT -> Prop) : Olist -> Prop :=
nil_forall : o_forall P nil
|cons_forall : forall ol alpha, P alpha -> o_forall P ol ->
o_forall P (cons alpha ol).
Definition o_bounded (alpha: OT) :=
o_forall (fun beta => beta < alpha).
Definition o_bounded_leq (alpha : OT) :=
o_forall (fun beta => beta <= alpha).
Lemma eval_bounded : forall alpha ol, ordinal alpha -> o_bounded alpha ol ->
eval ol < phi0 alpha.
Proof.
induction 2.
simpl.
apply phi0_positive.
auto.
simpl.
apply AP_plus_closed.
apply AP_phi0; ordi.
apply phi0_mono;auto.
auto.
Qed.
Lemma sorted_tail : forall alpha ol, sorted (cons alpha ol) ->
sorted ol.
inversion 1.
constructor.
auto.
Qed.
Lemma eval_ordinal : forall ol, sorted ol ->
ordinal (eval ol).
Proof.
induction ol;simpl.
eauto with schutte.
intro.
apply ordinal_plus.
apply ordinal_phi0.
inversion H;eauto with schutte.
apply IHol.
eapply sorted_tail;eauto.
Qed.
Inductive cnf_of (alpha : OT)(ol : Olist) : Prop :=
mk_cnf_of : sorted ol -> alpha = eval ol -> cnf_of alpha ol.
Lemma has_cnf_ordinal : forall alpha ol, cnf_of alpha ol ->
ordinal alpha.
Proof.
inversion 1.
subst alpha; apply eval_ordinal;auto.
Qed.
Lemma nf_bounded : forall beta, ordinal beta -> forall o alpha,
alpha <= phi0 beta ->
cnf_of alpha o -> o_bounded_leq beta o.
intros beta Obeta o ; elim o.
constructor.
intros.
right.
case H1;intros.
simpl in H3.
subst alpha.
apply phi0_mono_R_weak.
inversion H2;ordi.
auto.
apply le_trans with (phi0 o0 + eval o1);auto.
apply le_plus_l.
apply ordinal_phi0.
inversion H2;ordi.
apply eval_ordinal.
eapply sorted_tail;eauto.
apply H with (eval o1).
case H1.
intros.
simpl in H3.
apply le_trans with alpha.
subst alpha.
apply le_plus_r.
apply ordinal_phi0.
inversion H2;ordi.
apply eval_ordinal.
eapply sorted_tail;eauto.
auto.
split.
case H1.
intros; eapply sorted_tail;eauto.
auto.
Qed.
Hint Resolve has_cnf_ordinal eval_ordinal : schutte.
Lemma cnf_of_ap : forall alpha, AP alpha -> exists ol, cnf_of alpha ol.
Proof.
intros.
case phi0_ordering.
destruct 2.
decompose [and] H2.
case (H5 alpha H).
intros x (Hx,Ex);subst alpha.
exists (cons x nil).
constructor;auto.
simpl.
rewrite alpha_plus_zero;auto.
ordi.
Qed.
Lemma sorted_lt_lt : forall o' , forall l o, sorted (cons o l) ->
o < o' ->
eval (cons o l) < phi0 o'.
Proof.
induction l.
simpl.
inversion_clear 1.
intro;apply AP_plus_closed.
apply AP_phi0;eauto with schutte.
apply phi0_mono;eauto with schutte.
apply phi0_positive.
ordi.
inversion 1.
simpl.
simpl in IHl.
intro.
apply AP_plus_closed.
apply AP_phi0;eauto with schutte.
apply phi0_mono;eauto with schutte.
apply IHl.
eapply sorted_tail;eauto.
eauto with schutte.
Qed.
Lemma sorted_lt_lt_2 : forall l o, sorted (cons o l) ->
eval (cons o l) < phi0 (succ o).
Proof.
intros;apply sorted_lt_lt.
auto.
inversion H;intros;eauto with schutte.
Qed.
Lemma cnf_head_eq : forall alpha beta ol ol',
sorted (cons alpha ol) ->
sorted (cons beta ol') ->
eval (cons alpha ol) = eval (cons beta ol') ->
alpha = beta.
intros.
tricho alpha beta H2.
inversion H;ordi.
inversion H0;ordi.
generalize (sorted_lt_lt _ H H2).
intro.
case (lt_irr (eval (cons alpha ol))).
apply lt_le_trans with (phi0 beta).
auto.
rewrite H1.
simpl.
apply le_plus_l.
ordi.
apply eval_ordinal.
inversion H0;auto.
auto.
generalize (sorted_lt_lt _ H0 H2).
intro.
case (lt_irr (eval (cons beta ol'))).
apply lt_le_trans with (phi0 alpha).
auto.
rewrite <- H1.
simpl.
apply le_plus_l.
ordi.
apply eval_ordinal.
inversion H;auto.
Qed.
Lemma cnf_eq : forall alpha beta ol ol',
sorted (cons alpha ol) ->
sorted (cons beta ol') ->
eval (cons alpha ol) = eval (cons beta ol') ->
alpha = beta /\ eval ol = eval ol'.
Proof.
intros.
generalize (cnf_head_eq H H0 H1).
split;auto.
simpl in H1.
subst beta.
eapply plus_reg_r with (phi0 alpha).
inversion H0;ordi.
inversion H;ordi.
apply eval_ordinal;auto.
inversion H0;auto.
auto.
Qed.
Lemma cnf_plus1 : forall ol, sorted ol ->
forall alpha, ordinal alpha ->
exists ol',
cnf_of (phi0 alpha + eval ol) ol'.
Proof.
induction ol.
inversion_clear 1 .
intros.
simpl.
exists (cons alpha nil).
split.
constructor.
auto.
simpl.
auto.
intros.
simpl.
tricho alpha o H1.
inversion H;ordi.
exists (cons o ol).
split.
auto.
rewrite plus_assoc.
rewrite phi0_alpha_phi0_beta.
simpl;auto.
auto.
ordi.
ordi.
apply eval_ordinal.
inversion H;auto.
subst o; exists (cons alpha (cons alpha ol)).
split.
constructor; eauto with schutte.
simpl.
auto.
exists (cons alpha (cons o ol)).
split.
constructor;auto.
auto with schutte.
simpl.
auto.
Qed.
Lemma cnf_plus2 : forall ol, sorted ol ->
forall ol', sorted ol' ->
exists ol'', cnf_of (eval ol + eval ol') ol''.
Proof.
induction ol.
simpl.
intros; rewrite zero_plus_alpha;auto.
exists ol';split;auto.
apply eval_ordinal;auto.
intros.
simpl.
assert (sorted ol).
inversion H;auto.
case (IHol H1 _ H0).
intros.
case H2;intros.
case (cnf_plus1 H3 o).
inversion H;ordi.
intros; exists x0.
rewrite <- H4 in H5.
rewrite plus_assoc in H5;auto.
apply ordinal_phi0.
inversion H;auto.
ordi.
apply eval_ordinal;auto.
apply eval_ordinal;auto.
Qed.
Lemma cnf_plus : forall ol alpha,
cnf_of alpha ol -> forall ol' beta, cnf_of beta ol' ->
exists ol'', cnf_of (alpha+beta) ol''.
Proof.
destruct 1.
destruct 1.
rewrite H0;rewrite H2.
apply cnf_plus2;auto.
Qed.
Theorem cnf_exists : forall alpha, ordinal alpha ->
exists nf, cnf_of alpha nf.
Proof.
intros alpha H;case (le_eq_or_lt (le_zero _ H)).
exists nil.
split.
constructor.
simpl;auto.
intro.
generalize H0; pattern alpha.
apply Induction;auto.
red.
intros.
case (classic (AP a)).
intros.
apply cnf_of_ap; auto.
intros.
case (not_AP_inv2 H3 H4).
intros.
case H5;intros z (H4',(H5',H6)).
case (H2 x);ordi.
case H6;auto.
auto.
intros.
case (H2 z);ordi.
case H6;auto.
destruct 2;auto.
auto.
intros.
decompose [and] H6.
subst a.
case (cnf_plus H7 H8).
intros;exists x2;auto.
Qed.
Lemma sorted_lt : forall ol alpha, sorted (cons alpha ol) ->
eval ol < phi0 alpha + eval ol.
induction ol.
inversion 1.
simpl.
rewrite alpha_plus_zero.
apply phi0_positive;auto.
ordi.
inversion 1.
simpl.
rewrite plus_assoc.
generalize (IHol _ H4).
intro.
apply le_lt_trans with (phi0 alpha + eval ol).
apply plus_mono_weak_l.
apply eval_ordinal.
inversion H4;auto.
apply phi0_mono_weak.
auto.
rewrite <- plus_assoc. apply plus_mono_r.
ordi.
auto.
ordi.
ordi.
apply eval_ordinal.
inversion H4;auto.
ordi.
ordi.
apply eval_ordinal.
inversion H4;auto.
Qed.
Lemma cnf_of_AP : forall ol, sorted ol ->
AP (eval ol) -> exists beta, ordinal beta /\
ol = cons beta nil.
Proof.
destruct ol.
simpl.
destruct 2.
case (lt_irr zero);auto.
case ol.
exists o;split;auto.
inversion H.
auto.
clear ol.
intros.
simpl in H0.
case (AP_to_phi0 H0).
intros x (Hx,Hx').
assert (zero < (phi0 o0 + eval o1)).
apply lt_le_trans with (phi0 o0).
apply phi0_positive.
inversion H.
ordi.
apply le_plus_l.
inversion H;intros;ordi.
apply eval_ordinal;auto.
inversion H.
inversion H5;auto.
assert (ordinal o).
inversion H;auto.
ordi.
case (AP_plus_AP _ _ _ H2 H1 Hx Hx').
intros.
generalize (sorted_lt H).
intros.
rewrite <- Hx' in H4.
simpl in H5.
rewrite <- H4 in H5.
case (lt_irr (phi0 o0 + eval o1)).
auto.
Qed.
Lemma cnf_unicity : forall ol alpha, cnf_of alpha ol -> forall ol',
cnf_of alpha ol' -> ol=ol'.
Proof.
induction ol.
destruct 1.
simpl in H0.
subst alpha.
destruct ol'.
auto.
destruct 1.
simpl in H1.
case (lt_irr zero).
pattern zero at 2;rewrite H1.
apply lt_le_trans with (phi0 o);auto with schutte.
apply phi0_positive.
inversion H0;ordi.
apply le_plus_l;auto.
inversion H0;auto.
ordi.
inversion H0;ordi.
apply eval_ordinal.
eapply sorted_tail;eauto.
destruct ol'.
intro.
case H;case H0;intros.
simpl in H2;simpl in H4.
rewrite H2 in H4.
assert (ordinal o).
inversion H3;ordi.
case (lt_irr zero).
pattern zero at 2; rewrite H4.
apply lt_le_trans with (phi0 o);auto.
apply phi0_positive.
auto.
apply le_plus_l;auto.
inversion H3;ordi.
apply eval_ordinal;auto.
eapply sorted_tail;eauto.
intro.
case H; case H0;intros.
rewrite H4 in H2.
case (cnf_eq H3 H1 H2).
intros; subst o0.
replace ol' with ol;auto.
apply IHol with (eval ol).
split;auto.
eapply sorted_tail;eauto.
rewrite H6;split;auto.
eapply sorted_tail;eauto.
Qed.