1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(*i $Id: ArithProp.v,v 1.1.2.1 2004/07/16 19:31:31 herbelin Exp $ i*)
Require Rbase.
Require Rbasic_fun.
Require Even.
Require Div2.
V7only [ Import nat_scope. Import Z_scope. Import R_scope. ].
Open Local Scope Z_scope.
Open Local Scope R_scope.
Lemma minus_neq_O : (n,i:nat) (lt i n) -> ~(minus n i)=O.
Intros; Red; Intro.
Cut (n,m:nat) (le m n) -> (minus n m)=O -> n=m.
Intro; Assert H2 := (H1 ? ? (lt_le_weak ? ? H) H0); Rewrite H2 in H; Elim (lt_n_n ? H).
Pose R := [n,m:nat](le m n)->(minus n m)=(0)->n=m.
Cut ((n,m:nat)(R n m)) -> ((n0,m:nat)(le m n0)->(minus n0 m)=(0)->n0=m).
Intro; Apply H1.
Apply nat_double_ind.
Unfold R; Intros; Inversion H2; Reflexivity.
Unfold R; Intros; Simpl in H3; Assumption.
Unfold R; Intros; Simpl in H4; Assert H5 := (le_S_n ? ? H3); Assert H6 := (H2 H5 H4); Rewrite H6; Reflexivity.
Unfold R; Intros; Apply H1; Assumption.
Qed.
Lemma le_minusni_n : (n,i:nat) (le i n)->(le (minus n i) n).
Pose R := [m,n:nat] (le n m) -> (le (minus m n) m).
Cut ((m,n:nat)(R m n)) -> ((n,i:nat)(le i n)->(le (minus n i) n)).
Intro; Apply H.
Apply nat_double_ind.
Unfold R; Intros; Simpl; Apply le_n.
Unfold R; Intros; Simpl; Apply le_n.
Unfold R; Intros; Simpl; Apply le_trans with n.
Apply H0; Apply le_S_n; Assumption.
Apply le_n_Sn.
Unfold R; Intros; Apply H; Assumption.
Qed.
Lemma lt_minus_O_lt : (m,n:nat) (lt m n) -> (lt O (minus n m)).
Intros n m; Pattern n m; Apply nat_double_ind; [
Intros; Rewrite <- minus_n_O; Assumption
| Intros; Elim (lt_n_O ? H)
| Intros; Simpl; Apply H; Apply lt_S_n; Assumption].
Qed.
Lemma even_odd_cor : (n:nat) (EX p : nat | n=(mult (2) p)\/n=(S (mult (2) p))).
Intro.
Assert H := (even_or_odd n).
Exists (div2 n).
Assert H0 := (even_odd_double n).
Elim H0; Intros.
Elim H1; Intros H3 _.
Elim H2; Intros H4 _.
Replace (mult (2) (div2 n)) with (Div2.double (div2 n)).
Elim H; Intro.
Left.
Apply H3; Assumption.
Right.
Apply H4; Assumption.
Unfold Div2.double; Ring.
Qed.
(* 2m <= 2n => m<=n *)
Lemma le_double : (m,n:nat) (le (mult (2) m) (mult (2) n)) -> (le m n).
Intros; Apply INR_le.
Assert H1 := (le_INR ? ? H).
Do 2 Rewrite mult_INR in H1.
Apply Rle_monotony_contra with ``(INR (S (S O)))``.
Replace (INR (S (S O))) with ``2``; [Sup0 | Reflexivity].
Assumption.
Qed.
(* Here, we have the euclidian division *)
(* This lemma is used in the proof of sin_eq_0 : (sin x)=0<->x=kPI *)
Lemma euclidian_division : (x,y:R) ``y<>0`` -> (EXT k:Z | (EXT r : R | ``x==(IZR k)*y+r``/\``0<=r<(Rabsolu y)``)).
Intros.
Pose k0 := Cases (case_Rabsolu y) of
(leftT _) => (Zminus `1` (up ``x/-y``))
| (rightT _) => (Zminus (up ``x/y``) `1`) end.
Exists k0.
Exists ``x-(IZR k0)*y``.
Split.
Ring.
Unfold k0; Case (case_Rabsolu y); Intro.
Assert H0 := (archimed ``x/-y``); Rewrite <- Z_R_minus; Simpl; Unfold Rminus.
Replace ``-((1+ -(IZR (up (x/( -y)))))*y)`` with ``((IZR (up (x/-y)))-1)*y``; [Idtac | Ring].
Split.
Apply Rle_monotony_contra with ``/-y``.
Apply Rlt_Rinv; Apply Rgt_RO_Ropp; Exact r.
Rewrite Rmult_Or; Rewrite (Rmult_sym ``/-y``); Rewrite Rmult_Rplus_distrl; Rewrite <- Ropp_Rinv; [Idtac | Assumption].
Rewrite Rmult_assoc; Repeat Rewrite Ropp_mul3; Rewrite <- Rinv_r_sym; [Rewrite Rmult_1r | Assumption].
Apply Rle_anti_compatibility with ``(IZR (up (x/( -y))))-x/( -y)``.
Rewrite Rplus_Or; Unfold Rdiv; Pattern 4 ``/-y``; Rewrite <- Ropp_Rinv; [Idtac | Assumption].
Replace ``(IZR (up (x*/ -y)))-x* -/y+( -(x*/y)+ -((IZR (up (x*/ -y)))-1))`` with R1; [Idtac | Ring].
Elim H0; Intros _ H1; Unfold Rdiv in H1; Exact H1.
Rewrite (Rabsolu_left ? r); Apply Rlt_monotony_contra with ``/-y``.
Apply Rlt_Rinv; Apply Rgt_RO_Ropp; Exact r.
Rewrite <- Rinv_l_sym.
Rewrite (Rmult_sym ``/-y``); Rewrite Rmult_Rplus_distrl; Rewrite <- Ropp_Rinv; [Idtac | Assumption].
Rewrite Rmult_assoc; Repeat Rewrite Ropp_mul3; Rewrite <- Rinv_r_sym; [Rewrite Rmult_1r | Assumption]; Apply Rlt_anti_compatibility with ``((IZR (up (x/( -y))))-1)``.
Replace ``(IZR (up (x/( -y))))-1+1`` with ``(IZR (up (x/( -y))))``; [Idtac | Ring].
Replace ``(IZR (up (x/( -y))))-1+( -(x*/y)+ -((IZR (up (x/( -y))))-1))`` with ``-(x*/y)``; [Idtac | Ring].
Rewrite <- Ropp_mul3; Rewrite (Ropp_Rinv ? H); Elim H0; Unfold Rdiv; Intros H1 _; Exact H1.
Apply Ropp_neq; Assumption.
Assert H0 := (archimed ``x/y``); Rewrite <- Z_R_minus; Simpl; Cut ``0<y``.
Intro; Unfold Rminus; Replace ``-(((IZR (up (x/y)))+ -1)*y)`` with ``(1-(IZR (up (x/y))))*y``; [Idtac | Ring].
Split.
Apply Rle_monotony_contra with ``/y``.
Apply Rlt_Rinv; Assumption.
Rewrite Rmult_Or; Rewrite (Rmult_sym ``/y``); Rewrite Rmult_Rplus_distrl; Rewrite Rmult_assoc; Rewrite <- Rinv_r_sym; [Rewrite Rmult_1r | Assumption]; Apply Rle_anti_compatibility with ``(IZR (up (x/y)))-x/y``; Rewrite Rplus_Or; Unfold Rdiv; Replace ``(IZR (up (x*/y)))-x*/y+(x*/y+(1-(IZR (up (x*/y)))))`` with R1; [Idtac | Ring]; Elim H0; Intros _ H2; Unfold Rdiv in H2; Exact H2.
Rewrite (Rabsolu_right ? r); Apply Rlt_monotony_contra with ``/y``.
Apply Rlt_Rinv; Assumption.
Rewrite <- (Rinv_l_sym ? H); Rewrite (Rmult_sym ``/y``); Rewrite Rmult_Rplus_distrl; Rewrite Rmult_assoc; Rewrite <- Rinv_r_sym; [Rewrite Rmult_1r | Assumption]; Apply Rlt_anti_compatibility with ``((IZR (up (x/y)))-1)``; Replace ``(IZR (up (x/y)))-1+1`` with ``(IZR (up (x/y)))``; [Idtac | Ring]; Replace ``(IZR (up (x/y)))-1+(x*/y+(1-(IZR (up (x/y)))))`` with ``x*/y``; [Idtac | Ring]; Elim H0; Unfold Rdiv; Intros H2 _; Exact H2.
Case (total_order_T R0 y); Intro.
Elim s; Intro.
Assumption.
Elim H; Symmetry; Exact b.
Assert H1 := (Rle_sym2 ? ? r); Elim (Rlt_antirefl ? (Rle_lt_trans ? ? ? H1 r0)).
Qed.
Lemma tech8 : (n,i:nat) (le n (plus (S n) i)).
Intros; Induction i.
Replace (plus (S n) O) with (S n); [Apply le_n_Sn | Ring].
Replace (plus (S n) (S i)) with (S (plus (S n) i)).
Apply le_S; Assumption.
Apply INR_eq; Rewrite S_INR; Do 2 Rewrite plus_INR; Do 2 Rewrite S_INR; Ring.
Qed.
|
