Library LUB_spec_AX
Require Export Bridges_order2_AX.
Module lub_spec_AX (N:Num_w).
Import N.
Module Export XX:=mBridges2(N).
Axiom proof_irr :∀ A:Prop, ∀ x y:A, x=y.
Definition minA (x y:A) := if (A0_dec (x + -y)) then x else y.
Definition least_upper_bound (S:subset) (b:HRw) : Prop :=
(∀ s:HRw, (S s → (HRwge b s))) ∧
(∀ b':HRw, (HRwgt b b') → ∃ o:HRw, S o∧ HRwgt o b').
Definition has_least_upper_bound (s:subset) : Prop := ∃ b, least_upper_bound s b.
Lemma minA_lim : ∀ x y:A, ¬lim x → ¬lim y → ¬lim (minA x y).
Proof.
intros; unfold minA; destruct (A0_dec (x + - y)); assumption.
Qed.
Lemma minA_le : ∀ x y:A, 0≤ x → 0≤y → 0≤ minA x y.
Proof.
intros; unfold minA; destruct (A0_dec (x + - y)); assumption.
Qed.
Lemma HRwgt_1 : ∀ m, (m +w HRw1) >w m.
Proof.
intros m; unfold HRwgt; destruct m; unfold HRw1; simpl.
∃ a1.
split.
apply ANS1.
split.
apply lt_0_1.
ring_simplify.
apply le_refl.
Qed.
Lemma HRwgt_upper_bound : ∀ X:subset, ∀ m, upper_bound X m → upper_bound X (HRwplus m HRw1).
Proof.
unfold upper_bound; intros.
apply HRwgt_trans with m.
apply HRwgt_1.
apply H; assumption.
Qed.
Lemma HRwgt_upper_bound_2 : ∀ X:subset, ∀ x y, upper_bound X x → HRwgt y x → upper_bound X y.
Proof.
unfold upper_bound; intros.
apply HRwgt_trans with x.
assumption.
apply H; assumption.
Qed.
Parameter overspill_principle : ∀ P:A → Prop, (∀ n:A, lim n ∧ 0≤n → P n) →
(∃ v:A, ¬lim v ∧ 0<v ∧ (∀ m:A, 0≤m ∧ m ≤v → P m)).
Lemma ANS4_special : ∀ n k:A, (lim n ∧ 0≤n) → (0 ≤k ∧ k ≤ n) → lim k ∧ 0≤k.
Proof.
intros n k (Hlimn, Hlen) (Hlimk, Hlek).
split.
apply ANS4.
∃ n.
split.
assumption.
rewrite abs_pos_val by assumption.
rewrite abs_pos_val by assumption.
assumption.
assumption.
Qed.
Lemma H0 : lim 0 ∧0≤0.
Proof.
split; [apply lim0 | apply le_refl].
Qed.
Parameter ANS5 :
∀ P :A → Prop,
(∀ u : ∀ n:A, lim n ∧ 0 ≤ n → A,
P (u 0 H0) →
(∀ n:A, ∀ Hn : lim n ∧ 0 ≤ n,
(∀ k:A, ∀ Hk:0 ≤ k ∧ k ≤ n, ∀ Hn1 : lim (n+1)∧0<=(n+1), P (u k (ANS4_special n k Hn Hk))
→ P(u (plusA n 1) Hn1))) →
Module lub_spec_AX (N:Num_w).
Import N.
Module Export XX:=mBridges2(N).
Axiom proof_irr :∀ A:Prop, ∀ x y:A, x=y.
Definition minA (x y:A) := if (A0_dec (x + -y)) then x else y.
Definition least_upper_bound (S:subset) (b:HRw) : Prop :=
(∀ s:HRw, (S s → (HRwge b s))) ∧
(∀ b':HRw, (HRwgt b b') → ∃ o:HRw, S o∧ HRwgt o b').
Definition has_least_upper_bound (s:subset) : Prop := ∃ b, least_upper_bound s b.
Lemma minA_lim : ∀ x y:A, ¬lim x → ¬lim y → ¬lim (minA x y).
Proof.
intros; unfold minA; destruct (A0_dec (x + - y)); assumption.
Qed.
Lemma minA_le : ∀ x y:A, 0≤ x → 0≤y → 0≤ minA x y.
Proof.
intros; unfold minA; destruct (A0_dec (x + - y)); assumption.
Qed.
Lemma HRwgt_1 : ∀ m, (m +w HRw1) >w m.
Proof.
intros m; unfold HRwgt; destruct m; unfold HRw1; simpl.
∃ a1.
split.
apply ANS1.
split.
apply lt_0_1.
ring_simplify.
apply le_refl.
Qed.
Lemma HRwgt_upper_bound : ∀ X:subset, ∀ m, upper_bound X m → upper_bound X (HRwplus m HRw1).
Proof.
unfold upper_bound; intros.
apply HRwgt_trans with m.
apply HRwgt_1.
apply H; assumption.
Qed.
Lemma HRwgt_upper_bound_2 : ∀ X:subset, ∀ x y, upper_bound X x → HRwgt y x → upper_bound X y.
Proof.
unfold upper_bound; intros.
apply HRwgt_trans with x.
assumption.
apply H; assumption.
Qed.
Parameter overspill_principle : ∀ P:A → Prop, (∀ n:A, lim n ∧ 0≤n → P n) →
(∃ v:A, ¬lim v ∧ 0<v ∧ (∀ m:A, 0≤m ∧ m ≤v → P m)).
Lemma ANS4_special : ∀ n k:A, (lim n ∧ 0≤n) → (0 ≤k ∧ k ≤ n) → lim k ∧ 0≤k.
Proof.
intros n k (Hlimn, Hlen) (Hlimk, Hlek).
split.
apply ANS4.
∃ n.
split.
assumption.
rewrite abs_pos_val by assumption.
rewrite abs_pos_val by assumption.
assumption.
assumption.
Qed.
Lemma H0 : lim 0 ∧0≤0.
Proof.
split; [apply lim0 | apply le_refl].
Qed.
Parameter ANS5 :
∀ P :A → Prop,
(∀ u : ∀ n:A, lim n ∧ 0 ≤ n → A,
P (u 0 H0) →
(∀ n:A, ∀ Hn : lim n ∧ 0 ≤ n,
(∀ k:A, ∀ Hk:0 ≤ k ∧ k ≤ n, ∀ Hn1 : lim (n+1)∧0<=(n+1), P (u k (ANS4_special n k Hn Hk))
→ P(u (plusA n 1) Hn1))) →
{u:A->A | ... }
sigT(fun v ⇒ ∀ n:A, ∀ Hn:lim n ∧ 0≤ n,
∀ k:A, ∀ Hk:0 ≤ k ∧ k ≤ n, P (v k) ∧ v k = u k (ANS4_special n k Hn Hk))).
Definition extends (u:(∀ k:A, lim k ∧ 0≤ k → A)) : (A→A).
intros x.
elim
(ANS5 (fun x ⇒ True) u I (fun x y z t a b ⇒ I)).
intros v Hv.
exact (v x).
Defined.
Lemma extends_id : ∀ u:(∀ k:A, lim k ∧ 0≤k → A),
∀ n, ∀ H:lim n ∧ 0 ≤ n, u n H = (extends u) n.
Proof.
intros u n H.
unfold extends.
case (ANS5 (fun _ : A ⇒ True) u I
(fun (x : A) (_ : lim x ∧ 0 ≤ x) (z : A) (_ : 0 ≤ z ∧ z ≤ x) (_ : lim (x+1) ∧ 0 ≤ (x+1))
(_ : True) ⇒ I)).
simpl.
intros.
assert (Hk : 0 ≤ n ∧ n ≤ n).
split.
solve [intuition].
apply le_refl.
generalize (a n H n Hk) .
intros.
rewrite (proof_irr _ H (ANS4_special n n H Hk)).
solve [intuition].
Qed.
Parameter min_lim : A → (∀ k:A, lim k ∧ 0≤ k →A) → A.
Parameter min_lim_def :
∀ n:A, ∀ Hn : lim n∧0≤n,
∀ (b:∀ k:A, (lim k ∧ 0≤k) → A), ∀ k:A, ∀ Hk:0≤ k ∧ k ≤ n,
∀ Hk':lim k∧0≤k, min_lim n b ≤ b k Hk'.
Parameter min_lim_prop :
∀ P, ∀ n:A, ∀ b:∀ k:A, (lim k ∧ 0≤k) → A,
(∀ k:A, ∀ Hk:lim k∧0 ≤ k, k ≤ n → P(b k Hk )) → P (min_lim n b).
Parameter min : ∀ n:A, (A → A) → A.
Parameter min_def :
∀ n:A, ∀ b:A→ A, ∀ k:A, 0 ≤ k∧ k ≤ n → min n b ≤ b k.
Parameter min_prop :
∀ P, ∀ n:A, ∀ b:A→ A, (∀ k:A, 0 ≤ k∧ k ≤ n → P(b k)) → P (min n b).
Parameter min_def2 : ∀ (n m:A), ∀ b:A→ A, m≤n → min n b ≤ min m b.
Lemma lim_pos_P : ∀ x, lim x ∧ 0<x → P x.
Proof.
intros x (Hx1,Hx2).
unfold P.
∃ x.
split.
assumption.
split.
assumption.
rewrite abs_pos_val.
setoid_replace x with (x×1) at 1 by ring.
apply le_mult.
apply lt_le; assumption.
setoid_replace 1 with (0+1) by ring.
apply lt_le_2; apply Aw.
apply lt_le; assumption.
Qed.
Lemma has_limit :
∀ u:∀ n, lim n∧ 0≤n→ HRw, ∀ x:HRw, x >w HRw0 →
∀ eps : HRw, eps >w HRw0 →
(∀ n:A, ∀ Hn:lim n∧ 0≤n, (HRwequal (u n Hn) (HRwmult (power two_third n Hn) x))) →
∃ n:A, lim n∧0 ≤n ∧ ∀ H:lim n∧ 0 ≤ n, eps >w u n H.
Proof.
intros.
elim (power_lim two_third (proj1 two_third_prop) (proj2 two_third_prop) x H (eps) H1).
intros n Hn.
∃ n.
repeat split.
solve [intuition].
solve [intuition].
intros.
setoid_rewrite H2.
rewrite HRwmult_comm.
decompose [and] Hn.
apply H7.
Qed.
End lub_spec_AX.
∀ k:A, ∀ Hk:0 ≤ k ∧ k ≤ n, P (v k) ∧ v k = u k (ANS4_special n k Hn Hk))).
Definition extends (u:(∀ k:A, lim k ∧ 0≤ k → A)) : (A→A).
intros x.
elim
(ANS5 (fun x ⇒ True) u I (fun x y z t a b ⇒ I)).
intros v Hv.
exact (v x).
Defined.
Lemma extends_id : ∀ u:(∀ k:A, lim k ∧ 0≤k → A),
∀ n, ∀ H:lim n ∧ 0 ≤ n, u n H = (extends u) n.
Proof.
intros u n H.
unfold extends.
case (ANS5 (fun _ : A ⇒ True) u I
(fun (x : A) (_ : lim x ∧ 0 ≤ x) (z : A) (_ : 0 ≤ z ∧ z ≤ x) (_ : lim (x+1) ∧ 0 ≤ (x+1))
(_ : True) ⇒ I)).
simpl.
intros.
assert (Hk : 0 ≤ n ∧ n ≤ n).
split.
solve [intuition].
apply le_refl.
generalize (a n H n Hk) .
intros.
rewrite (proof_irr _ H (ANS4_special n n H Hk)).
solve [intuition].
Qed.
Parameter min_lim : A → (∀ k:A, lim k ∧ 0≤ k →A) → A.
Parameter min_lim_def :
∀ n:A, ∀ Hn : lim n∧0≤n,
∀ (b:∀ k:A, (lim k ∧ 0≤k) → A), ∀ k:A, ∀ Hk:0≤ k ∧ k ≤ n,
∀ Hk':lim k∧0≤k, min_lim n b ≤ b k Hk'.
Parameter min_lim_prop :
∀ P, ∀ n:A, ∀ b:∀ k:A, (lim k ∧ 0≤k) → A,
(∀ k:A, ∀ Hk:lim k∧0 ≤ k, k ≤ n → P(b k Hk )) → P (min_lim n b).
Parameter min : ∀ n:A, (A → A) → A.
Parameter min_def :
∀ n:A, ∀ b:A→ A, ∀ k:A, 0 ≤ k∧ k ≤ n → min n b ≤ b k.
Parameter min_prop :
∀ P, ∀ n:A, ∀ b:A→ A, (∀ k:A, 0 ≤ k∧ k ≤ n → P(b k)) → P (min n b).
Parameter min_def2 : ∀ (n m:A), ∀ b:A→ A, m≤n → min n b ≤ min m b.
Lemma lim_pos_P : ∀ x, lim x ∧ 0<x → P x.
Proof.
intros x (Hx1,Hx2).
unfold P.
∃ x.
split.
assumption.
split.
assumption.
rewrite abs_pos_val.
setoid_replace x with (x×1) at 1 by ring.
apply le_mult.
apply lt_le; assumption.
setoid_replace 1 with (0+1) by ring.
apply lt_le_2; apply Aw.
apply lt_le; assumption.
Qed.
Lemma has_limit :
∀ u:∀ n, lim n∧ 0≤n→ HRw, ∀ x:HRw, x >w HRw0 →
∀ eps : HRw, eps >w HRw0 →
(∀ n:A, ∀ Hn:lim n∧ 0≤n, (HRwequal (u n Hn) (HRwmult (power two_third n Hn) x))) →
∃ n:A, lim n∧0 ≤n ∧ ∀ H:lim n∧ 0 ≤ n, eps >w u n H.
Proof.
intros.
elim (power_lim two_third (proj1 two_third_prop) (proj2 two_third_prop) x H (eps) H1).
intros n Hn.
∃ n.
repeat split.
solve [intuition].
solve [intuition].
intros.
setoid_rewrite H2.
rewrite HRwmult_comm.
decompose [and] Hn.
apply H7.
Qed.
End lub_spec_AX.