1
<html xmlns="http://www.w3.org/1999/xhtml">
3
<meta http-equiv="Content-Type" content="text/html; charset="><link rel="stylesheet" href="style.css" type="text/css"><title>Coq.Reals.DiscrR</title>
8
<h1>Library Coq.Reals.DiscrR</h1>
11
<code class="keyword">Require</code> <code class="keyword">Import</code> RIneq.<br/>
12
<code class="keyword">Require</code> <code class="keyword">Import</code> Omega. Open <code class="keyword">Local</code> Scope R_scope.<br/>
15
<code class="keyword">Lemma</code> <a name="Rlt_R0_R2"></a>Rlt_R0_R2 : 0 < 2.<br/>
16
replace 2 with (<a href="Coq.Reals.Raxioms.html#INR">INR</a> 2); [ apply lt_INR_0; apply lt_O_Sn | reflexivity ].<br/>
17
<code class="keyword">Qed</code>.<br/>
20
<code class="keyword">Lemma</code> <a name="Rplus_lt_pos"></a>Rplus_lt_pos : forall x y:<a href="Coq.Reals.Rdefinitions.html#R">R</a>, 0 < x -> 0 < y -> 0 < x + y.<br/>
22
apply <a href="Coq.Reals.Raxioms.html#Rlt_trans">Rlt_trans</a> with x.<br/>
24
pattern x at 1 in |- *; rewrite <- <a href="Coq.Reals.RIneq.html#Rplus_0_r">Rplus_0_r</a>.<br/>
25
apply <a href="Coq.Reals.Raxioms.html#Rplus_lt_compat_l">Rplus_lt_compat_l</a>.<br/>
27
<code class="keyword">Qed</code>.<br/>
30
<code class="keyword">Lemma</code> <a name="IZR_eq"></a>IZR_eq : forall z1 z2:<a href="Coq.ZArith.BinInt.html#Z">Z</a>, z1 = z2 -> <a href="Coq.Reals.Raxioms.html#IZR">IZR</a> z1 = <a href="Coq.Reals.Raxioms.html#IZR">IZR</a> z2.<br/>
31
intros; rewrite H; reflexivity.<br/>
32
<code class="keyword">Qed</code>.<br/>
35
<code class="keyword">Lemma</code> <a name="IZR_neq"></a>IZR_neq : forall z1 z2:<a href="Coq.ZArith.BinInt.html#Z">Z</a>, z1 <> z2 -> <a href="Coq.Reals.Raxioms.html#IZR">IZR</a> z1 <> <a href="Coq.Reals.Raxioms.html#IZR">IZR</a> z2.<br/>
36
intros; red in |- *; intro; elim H; apply <a href="Coq.Reals.RIneq.html#eq_IZR">eq_IZR</a>; assumption.<br/>
37
<code class="keyword">Qed</code>.<br/>
40
<code class="keyword">Ltac</code> discrR :=<br/>
42
match goal with<br/>
43
| |- (?X1 <> ?X2) =><br/>
44
replace 2 with (<a href="Coq.Reals.Raxioms.html#IZR">IZR</a> 2);<br/>
45
[ replace 1 with (<a href="Coq.Reals.Raxioms.html#IZR">IZR</a> 1);<br/>
46
[ replace 0 with (<a href="Coq.Reals.Raxioms.html#IZR">IZR</a> 0);<br/>
47
[ repeat
48
rewrite <- plus_IZR ||
49
rewrite <- mult_IZR ||
50
rewrite <- Ropp_Ropp_IZR || rewrite Z_R_minus;
51
apply IZR_neq; try discriminate
53
| reflexivity ]<br/>
54
| reflexivity ]<br/>
55
end.<br/>
58
<code class="keyword">Ltac</code> prove_sup0 :=<br/>
59
match goal with<br/>
60
| |- (0 < 1) => apply <a href="Coq.Reals.RIneq.html#Rlt_0_1">Rlt_0_1</a><br/>
61
| |- (0 < ?X1) =><br/>
62
repeat<br/>
63
(apply <a href="Coq.Reals.RIneq.html#Rmult_lt_0_compat">Rmult_lt_0_compat</a> || apply <a href="Coq.Reals.DiscrR.html#Rplus_lt_pos">Rplus_lt_pos</a>;<br/>
64
try apply <a href="Coq.Reals.RIneq.html#Rlt_0_1">Rlt_0_1</a> || apply <a href="Coq.Reals.DiscrR.html#Rlt_R0_R2">Rlt_R0_R2</a>)<br/>
65
| |- (?X1 > 0) => change (0 < X1) in |- *; prove_sup0<br/>
69
<code class="keyword">Ltac</code> omega_sup :=<br/>
70
replace 2 with (<a href="Coq.Reals.Raxioms.html#IZR">IZR</a> 2);<br/>
71
[ replace 1 with (<a href="Coq.Reals.Raxioms.html#IZR">IZR</a> 1);<br/>
72
[ replace 0 with (<a href="Coq.Reals.Raxioms.html#IZR">IZR</a> 0);<br/>
73
[ repeat
74
rewrite <- plus_IZR ||
75
rewrite <- mult_IZR ||
76
rewrite <- Ropp_Ropp_IZR || rewrite Z_R_minus;
79
| reflexivity ]<br/>
80
| reflexivity ].<br/>
82
<code class="keyword">Ltac</code> prove_sup :=<br/>
83
match goal with<br/>
84
| |- (?X1 > ?X2) => change (X2 < X1) in |- *; prove_sup<br/>
85
| |- (0 < ?X1) => prove_sup0<br/>
86
| |- (- ?X1 < 0) => rewrite <- <a href="Coq.Reals.RIneq.html#Ropp_0">Ropp_0</a>; prove_sup<br/>
87
| |- (- ?X1 < - ?X2) => apply <a href="Coq.Reals.RIneq.html#Ropp_lt_gt_contravar">Ropp_lt_gt_contravar</a>; prove_sup<br/>
88
| |- (- ?X1 < ?X2) => apply <a href="Coq.Reals.Raxioms.html#Rlt_trans">Rlt_trans</a> with 0; prove_sup<br/>
89
| |- (?X1 < ?X2) => omega_sup<br/>
90
| _ => idtac<br/>
94
<code class="keyword">Ltac</code> Rcompute :=<br/>
95
replace 2 with (<a href="Coq.Reals.Raxioms.html#IZR">IZR</a> 2);<br/>
96
[ replace 1 with (<a href="Coq.Reals.Raxioms.html#IZR">IZR</a> 1);<br/>
97
[ replace 0 with (<a href="Coq.Reals.Raxioms.html#IZR">IZR</a> 0);<br/>
98
[ repeat
99
rewrite <- plus_IZR ||
100
rewrite <- mult_IZR ||
101
rewrite <- Ropp_Ropp_IZR || rewrite Z_R_minus;
102
apply IZR_eq; try reflexivity
104
| reflexivity ]<br/>
105
| reflexivity ].</code>
106
<hr/><a href="index.html">Index</a><hr/><font size="-1">This page has been generated by <a href="http://www.lri.fr/~filliatr/coqdoc/">coqdoc</a></font>
b'\\ No newline at end of file'
added
removed
library/Coq.Reals.DiscrR.html
