← Back to branch summary

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

« back to all changes in this revision

Viewing changes to test-suite/success/ROmega0.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:
test-suite/success/ROmega0.v
 
1
Require Import ZArith ROmega.
 
2
Open Scope Z_scope.
 
3
 
 
4
(* Pierre L: examples gathered while debugging romega. *)
 
5
 
 
6
Lemma test_romega_0 : 
 
7
 forall m m', 
 
8
  0<= m <= 1 -> 0<= m' <= 1 -> (0 < m <-> 0 < m') -> m = m'.
 
9
Proof.
 
10
intros.
 
11
romega.
 
12
Qed.
 
13
 
 
14
Lemma test_romega_0b : 
 
15
 forall m m', 
 
16
  0<= m <= 1 -> 0<= m' <= 1 -> (0 < m <-> 0 < m') -> m = m'.
 
17
Proof.
 
18
intros m m'.
 
19
romega.
 
20
Qed.
 
21
 
 
22
Lemma test_romega_1 : 
 
23
 forall (z z1 z2 : Z), 
 
24
    z2 <= z1 ->
 
25
    z1 <= z2 ->
 
26
    z1 >= 0 ->
 
27
    z2 >= 0 ->
 
28
    z1 >= z2 /\ z = z1 \/ z1 <= z2 /\ z = z2 ->
 
29
    z >= 0.
 
30
Proof.
 
31
intros.
 
32
romega.
 
33
Qed.
 
34
 
 
35
Lemma test_romega_1b : 
 
36
 forall (z z1 z2 : Z), 
 
37
    z2 <= z1 ->
 
38
    z1 <= z2 ->
 
39
    z1 >= 0 ->
 
40
    z2 >= 0 ->
 
41
    z1 >= z2 /\ z = z1 \/ z1 <= z2 /\ z = z2 ->
 
42
    z >= 0.
 
43
Proof.
 
44
intros z z1 z2.
 
45
romega.
 
46
Qed.
 
47
 
 
48
Lemma test_romega_2 : forall a b c:Z, 
 
49
 0<=a-b<=1 -> b-c<=2 -> a-c<=3.
 
50
Proof.
 
51
intros.
 
52
romega.
 
53
Qed.
 
54
 
 
55
Lemma test_romega_2b : forall a b c:Z, 
 
56
 0<=a-b<=1 -> b-c<=2 -> a-c<=3.
 
57
Proof.
 
58
intros a b c.
 
59
romega.
 
60
Qed.
 
61
 
 
62
Lemma test_romega_3 : forall a b h hl hr ha hb, 
 
63
 0 <= ha - hl <= 1 -> 
 
64
 -2 <= hl - hr <= 2 ->
 
65
 h =b+1 ->
 
66
 (ha >= hr /\ a = ha \/ ha <= hr /\ a = hr) ->
 
67
 (hl >= hr /\ b = hl \/ hl <= hr /\ b = hr) ->
 
68
 (-3 <= ha -hr <=3 -> 0 <= hb - a <= 1) ->
 
69
 (-2 <= ha-hr <=2 -> hb = a  + 1) -> 
 
70
 0 <= hb - h <= 1.
 
71
Proof.
 
72
intros.
 
73
romega.
 
74
Qed.
 
75
 
 
76
Lemma test_romega_3b : forall a b h hl hr ha hb, 
 
77
 0 <= ha - hl <= 1 -> 
 
78
 -2 <= hl - hr <= 2 ->
 
79
 h =b+1 ->
 
80
 (ha >= hr /\ a = ha \/ ha <= hr /\ a = hr) ->
 
81
 (hl >= hr /\ b = hl \/ hl <= hr /\ b = hr) ->
 
82
 (-3 <= ha -hr <=3 -> 0 <= hb - a <= 1) ->
 
83
 (-2 <= ha-hr <=2 -> hb = a  + 1) -> 
 
84
 0 <= hb - h <= 1.
 
85
Proof.
 
86
intros a b h hl hr ha hb.
 
87
romega.
 
88
Qed.
 
89
 
 
90
 
 
91
Lemma test_romega_4 : forall hr ha, 
 
92
 ha = 0 ->
 
93
 (ha = 0 -> hr =0) -> 
 
94
 hr = 0.
 
95
Proof.
 
96
intros hr ha.
 
97
romega.
 
98
Qed.
 
99
 
 
100
Lemma test_romega_5 : forall hr ha, 
 
101
 ha = 0 ->
 
102
 (~ha = 0 \/ hr =0) -> 
 
103
 hr = 0.
 
104
Proof.
 
105
intros hr ha.
 
106
romega.
 
107
Qed.
 
108
 
 
109
Lemma test_romega_6 : forall z, z>=0 -> 0>z+2 -> False.
 
110
Proof.
 
111
intros.
 
112
romega.
 
113
Qed.
 
114
 
 
115
Lemma test_romega_6b : forall z, z>=0 -> 0>z+2 -> False.
 
116
Proof.
 
117
intros z.
 
118
romega.
 
119
Qed.
 
120
 
 
121
Lemma test_romega_7 : forall z, 
 
122
  0>=0 /\ z=0 \/ 0<=0 /\ z =0 -> 1 = z+1.
 
123
Proof.
 
124
intros.
 
125
romega.
 
126
Qed.
 
127
 
 
128
Lemma test_romega_7b : forall z, 
 
129
  0>=0 /\ z=0 \/ 0<=0 /\ z =0 -> 1 = z+1.
 
130
Proof.
 
131
intros.
 
132
romega.
 
133
Qed.
 
134
 
 
135
(* Magaud #240 *)
 
136
 
 
137
Lemma test_romega_8 : forall x y:Z, x*x<y*y-> ~ y*y <= x*x.
 
138
intros.
 
139
romega.
 
140
Qed.
 
141
 
 
142
Lemma test_romega_8b : forall x y:Z, x*x<y*y-> ~ y*y <= x*x.
 
143
intros x y.
 
144
romega.
 
145
Qed.
 
146
 
 
147
(* Besson #1298 *)
 
148
 
 
149
Lemma test_romega9 : forall z z':Z, z<>z' -> z'=z -> False.
 
150
intros.
 
151
romega.
 
152
Qed.