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.