Library sequences_AX

Require Export LUB_spec_AX.

Module seq(N:Num_w).

Import N.
Module Export XX:=lub_spec_AX(N).

Section section_sequences.
Variable S : subset.
Variable Hdec : alpha beta : HRw,
       beta >w alpha {s : HRw | S s s >w alpha} + {upper_bound S beta}.
Variables s0 b0 : HRw.
Variable Hs0 : S s0.
Variable Hb0S : upper_bound S b0.

Definition fs := fun (alpha beta : HRw) (Hab : beta >w alpha) (sn_1 : HRw) ⇒
      match Hdec alpha beta Hab with
      | inleft Hsproj1_sig Hs
      | inright _sn_1
      end.

Definition fb := fun (alpha beta : HRw) (Hab : beta >w alpha) (bn_1 : HRw) ⇒
      match Hdec alpha beta Hab with
      | inleft Hs(bn_1 +w proj1_sig Hs) +w (-w alpha)
      | inright _beta
      end.

Lemma s_b_alpha_beta_lemma :
(n : A)
(HlimH0 : lim n 0 n)
(sn : HRw)
(bn : HRw)
(Hbs : S sn upper_bound S bn)
(alphan : HRw)
(betan : HRw)
(Habn : betan >w alphan),
S (fs alphan betan Habn sn) upper_bound S (fb alphan betan Habn bn).
Proof.
intros.
unfold fs,fb; simpl.
elim (Hdec alphan betan Habn).
intros a; case a; simpl.
intros x (HSx, Hxa).
split.
assumption.
apply HRwgt_upper_bound_2 with bn.
abstract (solve [intuition]).
assert (Hr:(bn +w (x +w (-w alphan))) =w ((bn +w x) +w (-w alphan))) by ring.
setoid_rewrite <- Hr.
setoid_replace bn with (bn+w HRw0) at 2 by ring.
apply HRwgt_HRwplus_l.
apply HRwgt_HRwplus_inv_r with alphan.
ring_simplify; assumption.
abstract (intros;solve [intuition]).
Qed.

Definition Psb n HlimH0 sn bn :=
S sn upper_bound S bn (bn +w (-w sn)) =w (power two_third n HlimH0 ×w (b0 +w (-w s0))).

Lemma lemma :
(n : A)
(HlimH0 : lim n 0 n)
(alphan : HRw)
(betan : HRw)
(sn : HRw)
(bn : HRw)
(Hs : S sn)
(Hb : upper_bound S bn)
(Hpower : (bn +w (-w sn)) =w (power two_third n HlimH0 ×w (b0 +w (-w s0))))
(Habn : betan >w alphan)
(Halphan : alphan = ((two_third ×w sn) +w (one_third ×w bn)))
(Hbetan : betan = ((one_third ×w sn) +w (two_third ×w bn)))
(Hx0 : lim (n + 1) 0 (n + 1)),

S (fs alphan betan Habn sn)
upper_bound S (fb alphan betan Habn bn)
(fb alphan betan Habn bn +w (-w fs alphan betan Habn sn)) =w
(power two_third (n + 1) Hx0 ×w (b0 +w (-w s0))).
Proof.
intros.
assert (S (fs alphan betan Habn sn)
upper_bound S (fb alphan betan Habn bn)).

solve [eapply s_b_alpha_beta_lemma; eauto; intuition].
split.
intuition.
split.
intuition.

unfold fs, fb; elim (Hdec alphan betan Habn).
intros a; elim a; intros sa Hsa; simpl.

setoid_rewrite Halphan.
ring_simplify.
unfold HRwminus; setoid_replace (((-w bn) ×w one_third) +w bn) with (two_third ×w bn)
by (setoid_rewrite HRwplus_comm;setoid_rewrite (HRwmult_comm (-w bn)); setoid_rewrite <- HRwminus_one_third; ring_simplify; solve [trivial | apply HRwequal_refl]).
assert (Hr: ((two_third ×w bn) +w (-w (two_third ×w sn)))=w(two_third ×w (bn +w -w sn))) by ring.
setoid_rewrite Hr.
setoid_rewrite Hpower.
unfold power; rewrite nat_like_induction_r2 with (H:=HlimH0).
ring_simplify; unfold HRwminus.
apply HRwequal_refl.

intros Hup.
setoid_rewrite Hbetan.
ring_simplify; unfold HRwminus.
assert (Hr:((one_third ×w sn) +w (-w sn))=w (-w two_third ×w sn)).
assert (Hr2:((-w two_third) ×w sn)=w(-w (two_third ×w sn))) by ring.
setoid_rewrite Hr2.
setoid_rewrite <- HRwminus_one_third; ring_simplify; solve [trivial | apply HRwequal_refl].
setoid_rewrite Hr.
assert (Hr2:(((-w two_third) ×w sn) +w (two_third ×w bn))=w(two_third ×w (bn +w -w sn))) by ring.
setoid_rewrite Hr2.
setoid_rewrite Hpower.
unfold power; rewrite nat_like_induction_r2 with (H:=HlimH0).
ring_simplify; unfold HRwminus.
apply HRwequal_refl.
Qed.

Definition def_s_b_alpha_beta :
     k:A, Hk:(lim k 0 k),
{sn:HRw & {bn:HRw & Psb k Hk sn bn}}.
Proof.
intros k HlimkH0k.
apply (nat_like_induction
 (fun (x:A) ⇒ ( Hx:lim x 0x, {sn:HRw & {bn:HRw & Psb x Hx sn bn}}))).
clear HlimkH0k k.
intros.
s0.
b0.

abstract (
split; [assumption |idtac];
split; [assumption |idtac];
unfold power; rewrite nat_like_induction_r1; ring
) using aproof1.

clear HlimkH0k k.
intros n HlimH0 Hx.

generalize (Hx HlimH0) ; clear Hx.
intros
 (sn,(bn, (Hs, (Hb,Hpower)))).

pose (alphan:=((two_third ×w sn)) +w (one_third ×w bn)).
pose (betan:=((one_third ×w sn) +w (two_third ×w bn))).

assert (Habn:(HRwgt betan alphan)) by (clear HlimH0 Hpower; abstract (apply step_thirds; intuition) using aproof2).

(fs alphan betan Habn sn).
(fb alphan betan Habn bn).
abstract (eapply lemma; eapply Hpower || intuition) using aproof3.

apply HlimkH0k.
Defined.

Lemma Hsn_increasing_aux :
ssA, HssA : ssA = (fun k0 Hk0proj1_sig(projT1 (def_s_b_alpha_beta k0 Hk0))),
bbA, HbbA : bbA = (fun k0 Hk0proj1_sig (projT1 (projT2 (def_s_b_alpha_beta k0 Hk0)))),
n, Hn, Hn1, ssA n Hn ssA (n+1) Hn1.
Proof.
intros ssA HssA bbA HbbA n Hn.
rewrite HssA.
unfold def_s_b_alpha_beta at 2.
intros.
rewrite nat_like_induction_r2 with (H:=Hn).
unfold def_s_b_alpha_beta.

pose (NLI :=
(nat_like_induction
        (fun x : A
          Hx : lim x 0 x, {sn : HRw & {bn : HRw & Psb x Hx sn bn}})
        (fun Hx : lim 0 0 0 ⇒
         existT (fun sn : HRw{bn : HRw & Psb 0 Hx sn bn}) s0
           (existT (fun bn : HRwPsb 0 Hx s0 bn) b0 (aproof1 Hx)))
        (fun (n0 : A) (HlimH0 : lim n0 0 n0)
           (Hx : Hx : lim n0 0 n0,
                 {sn : HRw & {bn : HRw & Psb n0 Hx sn bn}}) ⇒
         let (sn, s) := Hx HlimH0 in
         let (bn, p) := s in
         match p with
         | conj Hs (conj Hb Hpower) ⇒
             fun Hx0 : lim (n0 + 1) 0 n0 + 1 ⇒
             existT (fun sn0 : HRw{bn0 : HRw & Psb (n0 + 1) Hx0 sn0 bn0})
               (fs ((two_third ×w sn) +w (one_third ×w bn))
                  ((one_third ×w sn) +w (two_third ×w bn))
                  (aproof2 n0 sn bn Hs Hb) sn)
               (existT
                  (fun bn0 : HRw
                   Psb (n0 + 1) Hx0
                     (fs ((two_third ×w sn) +w (one_third ×w bn))
                        ((one_third ×w sn) +w (two_third ×w bn))
                        (aproof2 n0 sn bn Hs Hb) sn) bn0)
                  (fb ((two_third ×w sn) +w (one_third ×w bn))
                     ((one_third ×w sn) +w (two_third ×w bn))
                     (aproof2 n0 sn bn Hs Hb) bn)
                  (aproof3 n0 HlimH0 sn bn Hs Hb Hpower
                     (aproof2 n0 sn bn Hs Hb) Hx0))
         end) n Hn Hn)).

change (
(proj1_sig
  (projT1
     NLI)
proj1_sig
  (projT1
     ((let (sn, s) := NLI in
       let (bn, p) := s in
       match p with
       | conj Hs (conj Hb Hpower) ⇒
           fun Hx : lim (n + 1) 0 n + 1 ⇒
           existT (fun sn0 : HRw{bn0 : HRw & Psb (n + 1) Hx sn0 bn0})
             (fs ((two_third ×w sn) +w (one_third ×w bn))
                ((one_third ×w sn) +w (two_third ×w bn))
                (aproof2 n sn bn Hs Hb) sn)
             (existT
                (fun bn0 : HRw
                 Psb (n + 1) Hx
                   (fs ((two_third ×w sn) +w (one_third ×w bn))
                      ((one_third ×w sn) +w (two_third ×w bn))
                      (aproof2 n sn bn Hs Hb) sn) bn0)
                (fb ((two_third ×w sn) +w (one_third ×w bn))
                   ((one_third ×w sn) +w (two_third ×w bn))
                   (aproof2 n sn bn Hs Hb) bn)
                (aproof3 n Hn sn bn Hs Hb Hpower (aproof2 n sn bn Hs Hb) Hx))
       end) Hn1))
)).
destruct NLI.
destruct s.
destruct p.
destruct a.

replace
  (projT1
     (existT (fun sn : HRw{bn : HRw & Psb n Hn sn bn}) x
        (existT (fun bn : HRwPsb n Hn x bn) x0 (conj s (conj u h))))) with x by auto.

replace
(projT1
     (existT (fun sn0 : HRw{bn0 : HRw & Psb (n + 1) Hn1 sn0 bn0})
        (fs ((two_third ×w x) +w (one_third ×w x0))
           ((one_third ×w x) +w (two_third ×w x0)) (aproof2 n x x0 s u) x)
        (existT
           (fun bn0 : HRw
            Psb (n + 1) Hn1
              (fs ((two_third ×w x) +w (one_third ×w x0))
                 ((one_third ×w x) +w (two_third ×w x0)) (aproof2 n x x0 s u)
                 x) bn0)
           (fb ((two_third ×w x) +w (one_third ×w x0))
              ((one_third ×w x) +w (two_third ×w x0)) (aproof2 n x x0 s u) x0)
           (aproof3 n Hn x x0 s u h (aproof2 n x x0 s u) Hn1))))
with
(fs ((two_third ×w x) +w (one_third ×w x0))
           ((one_third ×w x) +w (two_third ×w x0)) (aproof2 n x x0 s u) x)
by auto.

unfold fs.
destruct (Hdec ((two_third ×w x) +w (one_third ×w x0))
      ((one_third ×w x) +w (two_third ×w x0)) (aproof2 n x x0 s u)).
generalize s1; intros (sn1, (hsn1a,hsn1b)).
simpl.
assert (HRwgt sn1 x).
assert (t:=two_thirds_one_third x).
setoid_rewrite t.
eapply HRwgt_trans.
apply hsn1b.
setoid_rewrite (HRwplus_comm (two_third ×w x)).
apply R2_4.
apply HRw1_3.
apply u; apply s.
apply lt_le; apply HRwgt_Zgt; assumption.
apply le_refl.
Qed.

Definition Q:A Prop := fun (a:A) ⇒ lim a leA a0 a.

Instance Q_morph : Proper (equalA ==> Basics.impl) Q.
Proof.
repeat red.
unfold Q.
intros x y Heq H'.
destruct H'.
split; rewrite <- Heq; assumption.
Qed.

Definition R: ssA: a, Q aA, x, a, Q aProp :=
fun (ssA: a, Q aA) (x:A) (a:A) (h:Q a) ⇒ leA (ssA a h) x.

Definition allDep (Q: A Prop) (R: x, a, Q aProp) (x:A) (a:A):=
  p:(Q a), (R x a p).

Parameter ssA_args_id :
   ssA: a, Q aA, ( x y, equalA x y p:Q x, q:Q y, equalA (ssA x p) (ssA y q)).

Instance allDep_morph (ssA: a, Q aA)(v:A) : Proper (equalA ==> iff) (@allDep Q (R ssA) v).
Proof.
repeat red; unfold allDep, R.
intros x y H.
split.
intros.
assert (Q x) by (rewrite H; assumption).
rewrite <- (ssA_args_id ssA x y H).
eapply H1.

unfold allDep ,R; intros.
assert (Q y) by (rewrite <- H; assumption).
rewrite (ssA_args_id ssA).
eapply H1.
assumption.
Existential 1:= H2.
Existential 1 := H2.
Qed.

Lemma thm_Hsn_increasing :
ssA, HssA : ssA = (fun k0 Hk0proj1_sig (projT1 (def_s_b_alpha_beta k0 Hk0))),
bbA, HbbA : bbA = (fun k0 Hk0proj1_sig (projT1 (projT2 (def_s_b_alpha_beta k0 Hk0)))),
n, Hn:lim n0 n, m, (Hm:lim m0 m),
  m n ssA m Hm ssA n Hn.
Proof.
intros ssA HssA bbA HbbA n Hn m Hm.
apply (nat_like_induction
  (fun x:A Hx:lim x 0x,
  m x ssA m Hm ssA x Hx)).
intros.
assert (m==0) by (apply le_id; solve [intuition]).
generalize Hm.
assert (HallDep: (allDep Q (R ssA) (ssA 0 Hx) m)).
rewrite H1.
unfold allDep, Q, R; intros.
rewrite (proof_irr _ Hx p).
apply le_refl.
apply HallDep.
intros n0 Hn0 IH Hx Hmn0.
elim (A0_dec (m + - (n0+1))). intros Hdec'; elim Hdec'.
intros.
apply le_trans with (ssA n0 Hn0).
assert (m n0).
apply le_plus_inv with (- (n0+1) +1).
rewrite plus_assoc.
setoid_replace (n0 + (-(n0+1) +1)) with 0 by ring.
apply lt_le_2.
assumption.
apply IH.
assumption.
apply Hsn_increasing_aux with (bbA:=bbA); solve [assumption].

intros.
assert (m==n0+1).
setoid_replace (n0+1) with (0+(n0+1)) by ring.
setoid_replace m with ((m + - (n0 + 1)) + (n0 +1 )) by ring.
rewrite b.
reflexivity.

generalize Hm.
assert (HallDep: (allDep Q (R ssA) (ssA (n0+1) Hx) m)).
rewrite H.
unfold allDep, Q, R; intros.
rewrite (proof_irr _ Hx p).
apply le_refl.
apply HallDep.

intros.
assert (Hf:False).
apply contradict_lt_le with (s:=0) (x:=m + - (n0+1)).
assumption.
apply le_plus_inv with (n0+1).
ring_simplify.
assumption.
solve [intuition].
assumption.
Qed.

End section_sequences.

End seq.