Library w_2n
Require Export LaugwitzSchmieden.
Module LS2n <: Num_w.
Include LS.
Fixpoint power2 (n:nat) : Z :=
match n with
| O ⇒ 1%Z
| S p ⇒ (2 × (power2 p))%Z
end.
Lemma power2_pos : ∀ n:nat, (0 < power2 n)%Z.
Proof.
induction n.
unfold power2; omega.
change (0 < 2 × (power2 n))%Z.
omega.
Qed.
Lemma n_power : ∀ n, (Z_of_nat n < power2 n)%Z.
Proof.
induction n.
simpl; omega.
change (Z.of_nat (S n) < 2× power2 n)%Z.
setoid_replace (Z.of_nat (S n)) with ((Z.of_nat n)+1)%Z
by (rewrite Nat2Z.inj_succ; unfold Z.succ; reflexivity).
omega.
Qed.
Definition w :A := fun (n:nat) ⇒ power2 n.
Lemma beta_w : leA beta w.
Proof.
unfold beta, w; unfold_intros.
∃ 0%nat.
intros.
generalize (n_power n); intros; omega.
Qed.
Lemma Aw : 0 <A w.
Proof.
unfold ltA.
∃ 0%nat.
intros; apply power2_pos.
Qed.
Lemma lim_lt_w : ∀ a, lim a∧ leA 0 a → ltA a w.
intros.
apply lt_le_trans with beta.
apply lim_lt_beta.
assumption.
apply beta_w.
Qed.
Lemma div_modw2 : ∀ a, w*(a/w) =A a + - (a mod% w).
Proof.
intros.
apply div_mod2.
left; apply Aw.
Qed.
Lemma div_modw3 : ∀ a, |(a mod% w)| <A w.
Proof.
intros.
apply div_mod3.
apply Aw.
Qed.
Lemma ANS3 : ¬ lim w.
Proof.
intro H; unfold lim in ×.
elim H; clear H; intros p (Hstdp,(Hle0p,Hwp)).
unfold ltA,a0 in ×.
elim Hstdp.
intros b Hb.
elim Hwp.
intros a Ha.
elim Hle0p.
intros c Hc.
pose (px:=p (a+b+c+1)%nat).
assert (0≤ px)%Z.
apply Hc.
omega.
pose (x:=((Zabs_nat px)+a+b+c+1)%nat).
assert ((|w |) (x) < p (x))%Z.
apply Ha.
unfold px,x in ×.
omega.
assert ((|w |) (x) ≥ p (x))%Z.
apply Zle_ge.
apply Zle_trans with (((|fun n ⇒ Z_of_nat n|) (x))%Z).
unfold absA in ×.
unfold w.
unfold x.
replace (p (Zabs_nat px + a + b + c + 1)%nat)%Z with
(p (a+b+c+1)%nat)%Z.
rewrite Zabs_eq.
replace (Zabs_nat px + a + b + c + 1)%nat with (Zabs_nat (px + (Z_of_nat (a + b + c + 1))))%nat.
rewrite inj_Zabs_nat.
rewrite Zabs_eq.
unfold px.
omega.
omega.
rewrite Zabs_nat_Zplus.
rewrite Zabs_nat_Z_of_nat.
ring.
unfold px; apply Hc.
omega.
solve [auto with zarith].
solve [auto with zarith].
apply Hb.
omega.
omega.
unfold w, absA.
rewrite Z.abs_eq.
rewrite Z.abs_eq.
assert (Z.of_nat x < power2 x)%Z.
apply n_power.
omega.
generalize (power2_pos x); intros; omega.
apply Zle_0_nat.
omega.
Qed.
End LS2n.
Module LS2n <: Num_w.
Include LS.
Fixpoint power2 (n:nat) : Z :=
match n with
| O ⇒ 1%Z
| S p ⇒ (2 × (power2 p))%Z
end.
Lemma power2_pos : ∀ n:nat, (0 < power2 n)%Z.
Proof.
induction n.
unfold power2; omega.
change (0 < 2 × (power2 n))%Z.
omega.
Qed.
Lemma n_power : ∀ n, (Z_of_nat n < power2 n)%Z.
Proof.
induction n.
simpl; omega.
change (Z.of_nat (S n) < 2× power2 n)%Z.
setoid_replace (Z.of_nat (S n)) with ((Z.of_nat n)+1)%Z
by (rewrite Nat2Z.inj_succ; unfold Z.succ; reflexivity).
omega.
Qed.
Definition w :A := fun (n:nat) ⇒ power2 n.
Lemma beta_w : leA beta w.
Proof.
unfold beta, w; unfold_intros.
∃ 0%nat.
intros.
generalize (n_power n); intros; omega.
Qed.
Lemma Aw : 0 <A w.
Proof.
unfold ltA.
∃ 0%nat.
intros; apply power2_pos.
Qed.
Lemma lim_lt_w : ∀ a, lim a∧ leA 0 a → ltA a w.
intros.
apply lt_le_trans with beta.
apply lim_lt_beta.
assumption.
apply beta_w.
Qed.
Lemma div_modw2 : ∀ a, w*(a/w) =A a + - (a mod% w).
Proof.
intros.
apply div_mod2.
left; apply Aw.
Qed.
Lemma div_modw3 : ∀ a, |(a mod% w)| <A w.
Proof.
intros.
apply div_mod3.
apply Aw.
Qed.
Lemma ANS3 : ¬ lim w.
Proof.
intro H; unfold lim in ×.
elim H; clear H; intros p (Hstdp,(Hle0p,Hwp)).
unfold ltA,a0 in ×.
elim Hstdp.
intros b Hb.
elim Hwp.
intros a Ha.
elim Hle0p.
intros c Hc.
pose (px:=p (a+b+c+1)%nat).
assert (0≤ px)%Z.
apply Hc.
omega.
pose (x:=((Zabs_nat px)+a+b+c+1)%nat).
assert ((|w |) (x) < p (x))%Z.
apply Ha.
unfold px,x in ×.
omega.
assert ((|w |) (x) ≥ p (x))%Z.
apply Zle_ge.
apply Zle_trans with (((|fun n ⇒ Z_of_nat n|) (x))%Z).
unfold absA in ×.
unfold w.
unfold x.
replace (p (Zabs_nat px + a + b + c + 1)%nat)%Z with
(p (a+b+c+1)%nat)%Z.
rewrite Zabs_eq.
replace (Zabs_nat px + a + b + c + 1)%nat with (Zabs_nat (px + (Z_of_nat (a + b + c + 1))))%nat.
rewrite inj_Zabs_nat.
rewrite Zabs_eq.
unfold px.
omega.
omega.
rewrite Zabs_nat_Zplus.
rewrite Zabs_nat_Z_of_nat.
ring.
unfold px; apply Hc.
omega.
solve [auto with zarith].
solve [auto with zarith].
apply Hb.
omega.
omega.
unfold w, absA.
rewrite Z.abs_eq.
rewrite Z.abs_eq.
assert (Z.of_nat x < power2 x)%Z.
apply n_power.
omega.
generalize (power2_pos x); intros; omega.
apply Zle_0_nat.
omega.
Qed.
End LS2n.