← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to contrib/setoid_ring/RealField.v

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
contrib/setoid_ring/RealField.v
 
1
Require Import Nnat.
 
2
Require Import ArithRing. 
 
3
Require Export Ring Field.
 
4
Require Import Rdefinitions.
 
5
Require Import Rpow_def.
 
6
Require Import Raxioms.
 
7
 
 
8
Open Local Scope R_scope.
 
9
 
 
10
Lemma RTheory : ring_theory 0 1 Rplus Rmult Rminus Ropp (eq (A:=R)).
 
11
Proof.
 
12
constructor.
 
13
 intro; apply Rplus_0_l.
 
14
 exact Rplus_comm.
 
15
 symmetry  in |- *; apply Rplus_assoc.
 
16
 intro; apply Rmult_1_l.
 
17
 exact Rmult_comm.
 
18
 symmetry  in |- *; apply Rmult_assoc.
 
19
 intros m n p.
 
20
   rewrite Rmult_comm in |- *.
 
21
   rewrite (Rmult_comm n p) in |- *.
 
22
   rewrite (Rmult_comm m p) in |- *.
 
23
   apply Rmult_plus_distr_l.
 
24
 reflexivity.
 
25
 exact Rplus_opp_r.
 
26
Qed.
 
27
 
 
28
Lemma Rfield : field_theory 0 1 Rplus Rmult Rminus Ropp Rdiv Rinv (eq(A:=R)).
 
29
Proof.
 
30
constructor.
 
31
 exact RTheory.
 
32
 exact R1_neq_R0.
 
33
 reflexivity.
 
34
 exact Rinv_l.
 
35
Qed.
 
36
 
 
37
Lemma Rlt_n_Sn : forall x, x < x + 1.
 
38
Proof.
 
39
intro.
 
40
elim archimed with x; intros.
 
41
destruct H0.
 
42
 apply Rlt_trans with (IZR (up x)); trivial.
 
43
    replace (IZR (up x)) with (x + (IZR (up x) - x))%R.
 
44
  apply Rplus_lt_compat_l; trivial.
 
45
  unfold Rminus in |- *.
 
46
    rewrite (Rplus_comm (IZR (up x)) (- x)) in |- *.
 
47
    rewrite <- Rplus_assoc in |- *.
 
48
    rewrite Rplus_opp_r in |- *.
 
49
    apply Rplus_0_l.
 
50
 elim H0.
 
51
   unfold Rminus in |- *.
 
52
   rewrite (Rplus_comm (IZR (up x)) (- x)) in |- *.
 
53
   rewrite <- Rplus_assoc in |- *.
 
54
   rewrite Rplus_opp_r in |- *.
 
55
   rewrite Rplus_0_l in |- *; trivial.
 
56
Qed.
 
57
 
 
58
Notation Rset := (Eqsth R).
 
59
Notation Rext := (Eq_ext Rplus Rmult Ropp).
 
60
 
 
61
Lemma Rlt_0_2 : 0 < 2.
 
62
apply Rlt_trans with (0 + 1).
 
63
 apply Rlt_n_Sn.
 
64
 rewrite Rplus_comm in |- *.
 
65
   apply Rplus_lt_compat_l.
 
66
    replace 1 with (0 + 1).
 
67
  apply Rlt_n_Sn.
 
68
  apply Rplus_0_l.
 
69
Qed.
 
70
 
 
71
Lemma Rgen_phiPOS : forall x, InitialRing.gen_phiPOS1 1 Rplus Rmult x > 0.
 
72
unfold Rgt in |- *.
 
73
induction x; simpl in |- *; intros.
 
74
 apply Rlt_trans with (1 + 0).
 
75
  rewrite Rplus_comm in |- *.
 
76
    apply Rlt_n_Sn.
 
77
  apply Rplus_lt_compat_l.
 
78
    rewrite <- (Rmul_0_l Rset Rext RTheory 2) in |- *.
 
79
    rewrite Rmult_comm in |- *.
 
80
    apply Rmult_lt_compat_l.
 
81
   apply Rlt_0_2.
 
82
   trivial.
 
83
 rewrite <- (Rmul_0_l Rset Rext RTheory 2) in |- *.
 
84
   rewrite Rmult_comm in |- *.
 
85
   apply Rmult_lt_compat_l.
 
86
  apply Rlt_0_2.
 
87
  trivial.
 
88
  replace 1 with (0 + 1).
 
89
  apply Rlt_n_Sn.
 
90
  apply Rplus_0_l.
 
91
Qed.
 
92
 
 
93
 
 
94
Lemma Rgen_phiPOS_not_0 :
 
95
  forall x, InitialRing.gen_phiPOS1 1 Rplus Rmult x <> 0.
 
96
red in |- *; intros.
 
97
specialize (Rgen_phiPOS x).
 
98
rewrite H in |- *; intro.
 
99
apply (Rlt_asym 0 0); trivial.
 
100
Qed.
 
101
 
 
102
Lemma Zeq_bool_complete : forall x y, 
 
103
  InitialRing.gen_phiZ 0%R 1%R Rplus Rmult Ropp x =
 
104
  InitialRing.gen_phiZ 0%R 1%R Rplus Rmult Ropp y ->
 
105
  Zeq_bool x y = true.
 
106
Proof gen_phiZ_complete Rset Rext Rfield Rgen_phiPOS_not_0.
 
107
 
 
108
Lemma Rdef_pow_add : forall (x:R) (n m:nat), pow x  (n + m) = pow x n * pow x m.
 
109
Proof.
 
110
  intros x n; elim n; simpl in |- *; auto with real.
 
111
  intros n0 H' m; rewrite H'; auto with real.
 
112
Qed.
 
113
 
 
114
Lemma R_power_theory : power_theory 1%R Rmult (eq (A:=R))  nat_of_N pow.
 
115
Proof.
 
116
 constructor. destruct n. reflexivity.
 
117
 simpl. induction p;simpl. 
 
118
 rewrite ZL6. rewrite Rdef_pow_add;rewrite IHp. reflexivity.
 
119
 unfold nat_of_P;simpl;rewrite ZL6;rewrite Rdef_pow_add;rewrite IHp;trivial.
 
120
 rewrite Rmult_comm;apply Rmult_1_l.
 
121
Qed.
 
122
 
 
123
Ltac Rpow_tac t := 
 
124
  match isnatcst t with
 
125
  | false => constr:(InitialRing.NotConstant)
 
126
  | _ => constr:(N_of_nat t)
 
127
  end. 
 
128
 
 
129
Add Field RField : Rfield  
 
130
   (completeness Zeq_bool_complete, power_tac R_power_theory [Rpow_tac]).
 
131
 
 
132
 
 
133
 
 
134