blob: 56473adb9c7e5e2351bccea44dff9c39db4ba5c6 (
plain)
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
|
Require Import Nnat.
Require Import ArithRing.
Require Export Ring Field.
Require Import Rdefinitions.
Require Import Rpow_def.
Require Import Raxioms.
Open Local Scope R_scope.
Lemma RTheory : ring_theory 0 1 Rplus Rmult Rminus Ropp (eq (A:=R)).
Proof.
constructor.
intro; apply Rplus_0_l.
exact Rplus_comm.
symmetry in |- *; apply Rplus_assoc.
intro; apply Rmult_1_l.
exact Rmult_comm.
symmetry in |- *; apply Rmult_assoc.
intros m n p.
rewrite Rmult_comm in |- *.
rewrite (Rmult_comm n p) in |- *.
rewrite (Rmult_comm m p) in |- *.
apply Rmult_plus_distr_l.
reflexivity.
exact Rplus_opp_r.
Qed.
Lemma Rfield : field_theory 0 1 Rplus Rmult Rminus Ropp Rdiv Rinv (eq(A:=R)).
Proof.
constructor.
exact RTheory.
exact R1_neq_R0.
reflexivity.
exact Rinv_l.
Qed.
Lemma Rlt_n_Sn : forall x, x < x + 1.
Proof.
intro.
elim archimed with x; intros.
destruct H0.
apply Rlt_trans with (IZR (up x)); trivial.
replace (IZR (up x)) with (x + (IZR (up x) - x))%R.
apply Rplus_lt_compat_l; trivial.
unfold Rminus in |- *.
rewrite (Rplus_comm (IZR (up x)) (- x)) in |- *.
rewrite <- Rplus_assoc in |- *.
rewrite Rplus_opp_r in |- *.
apply Rplus_0_l.
elim H0.
unfold Rminus in |- *.
rewrite (Rplus_comm (IZR (up x)) (- x)) in |- *.
rewrite <- Rplus_assoc in |- *.
rewrite Rplus_opp_r in |- *.
rewrite Rplus_0_l in |- *; trivial.
Qed.
Notation Rset := (Eqsth R).
Notation Rext := (Eq_ext Rplus Rmult Ropp).
Lemma Rlt_0_2 : 0 < 2.
apply Rlt_trans with (0 + 1).
apply Rlt_n_Sn.
rewrite Rplus_comm in |- *.
apply Rplus_lt_compat_l.
replace 1 with (0 + 1).
apply Rlt_n_Sn.
apply Rplus_0_l.
Qed.
Lemma Rgen_phiPOS : forall x, InitialRing.gen_phiPOS1 1 Rplus Rmult x > 0.
unfold Rgt in |- *.
induction x; simpl in |- *; intros.
apply Rlt_trans with (1 + 0).
rewrite Rplus_comm in |- *.
apply Rlt_n_Sn.
apply Rplus_lt_compat_l.
rewrite <- (Rmul_0_l Rset Rext RTheory 2) in |- *.
rewrite Rmult_comm in |- *.
apply Rmult_lt_compat_l.
apply Rlt_0_2.
trivial.
rewrite <- (Rmul_0_l Rset Rext RTheory 2) in |- *.
rewrite Rmult_comm in |- *.
apply Rmult_lt_compat_l.
apply Rlt_0_2.
trivial.
replace 1 with (0 + 1).
apply Rlt_n_Sn.
apply Rplus_0_l.
Qed.
Lemma Rgen_phiPOS_not_0 :
forall x, InitialRing.gen_phiPOS1 1 Rplus Rmult x <> 0.
red in |- *; intros.
specialize (Rgen_phiPOS x).
rewrite H in |- *; intro.
apply (Rlt_asym 0 0); trivial.
Qed.
Lemma Zeq_bool_complete : forall x y,
InitialRing.gen_phiZ 0%R 1%R Rplus Rmult Ropp x =
InitialRing.gen_phiZ 0%R 1%R Rplus Rmult Ropp y ->
Zeq_bool x y = true.
Proof gen_phiZ_complete Rset Rext Rfield Rgen_phiPOS_not_0.
Lemma Rdef_pow_add : forall (x:R) (n m:nat), pow x (n + m) = pow x n * pow x m.
Proof.
intros x n; elim n; simpl in |- *; auto with real.
intros n0 H' m; rewrite H'; auto with real.
Qed.
Lemma R_power_theory : power_theory 1%R Rmult (eq (A:=R)) nat_of_N pow.
Proof.
constructor. destruct n. reflexivity.
simpl. induction p;simpl.
rewrite ZL6. rewrite Rdef_pow_add;rewrite IHp. reflexivity.
unfold nat_of_P;simpl;rewrite ZL6;rewrite Rdef_pow_add;rewrite IHp;trivial.
rewrite Rmult_comm;apply Rmult_1_l.
Qed.
Ltac Rpow_tac t :=
match isnatcst t with
| false => constr:(InitialRing.NotConstant)
| _ => constr:(N_of_nat t)
end.
Add Field RField : Rfield
(completeness Zeq_bool_complete, power_tac R_power_theory [Rpow_tac]).
|
