← Back to branch summary

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

« back to all changes in this revision

Viewing changes to test-suite/success/OmegaPre.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/OmegaPre.v
 
1
Require Import ZArith Nnat Omega.
 
2
Open Scope Z_scope.
 
3
 
 
4
(** Test of the zify preprocessor for (R)Omega *)
 
5
 
 
6
(* More details in file PreOmega.v
 
7
 
 
8
   (r)omega with Z        : starts with zify_op
 
9
   (r)omega with nat      : starts with zify_nat
 
10
   (r)omega with positive : starts with zify_positive
 
11
   (r)omega with N        : starts with uses zify_N
 
12
   (r)omega with *        : starts zify (a saturation of the others)
 
13
*)
 
14
 
 
15
(* zify_op *)
 
16
 
 
17
Goal forall a:Z, Zmax a a = a.
 
18
intros.
 
19
omega with *.
 
20
Qed.
 
21
 
 
22
Goal forall a b:Z, Zmax a b = Zmax b a.
 
23
intros.
 
24
omega with *.
 
25
Qed.
 
26
 
 
27
Goal forall a b c:Z, Zmax a (Zmax b c) = Zmax (Zmax a b) c.
 
28
intros.
 
29
omega with *.
 
30
Qed.
 
31
 
 
32
Goal forall a b:Z, Zmax a b + Zmin a b = a + b.
 
33
intros.
 
34
omega with *.
 
35
Qed.
 
36
 
 
37
Goal forall a:Z, (Zabs a)*(Zsgn a) = a.
 
38
intros.
 
39
zify.
 
40
intuition; subst; omega. (* pure multiplication: omega alone can't do it *)
 
41
Qed.
 
42
 
 
43
Goal forall a:Z, Zabs a = a -> a >= 0.
 
44
intros.
 
45
omega with *.
 
46
Qed.
 
47
 
 
48
Goal forall a:Z, Zsgn a = a -> a = 1 \/ a = 0 \/ a = -1.
 
49
intros.
 
50
omega with *.
 
51
Qed.
 
52
 
 
53
(* zify_nat *)
 
54
 
 
55
Goal forall m: nat, (m<2)%nat -> (0<= m+m <=2)%nat.
 
56
intros.
 
57
omega with *.
 
58
Qed.
 
59
 
 
60
Goal forall m:nat, (m<1)%nat -> (m=0)%nat.
 
61
intros.
 
62
omega with *.
 
63
Qed.
 
64
 
 
65
Goal forall m: nat, (m<=100)%nat -> (0<= m+m <=200)%nat.
 
66
intros.
 
67
omega with *.
 
68
Qed.
 
69
(* 2000 instead of 200: works, but quite slow *)
 
70
 
 
71
Goal forall m: nat, (m*m>=0)%nat.
 
72
intros.
 
73
omega with *.
 
74
Qed.
 
75
 
 
76
(* zify_positive *)
 
77
 
 
78
Goal forall m: positive, (m<2)%positive -> (2 <= m+m /\ m+m <= 2)%positive.
 
79
intros.
 
80
omega with *.
 
81
Qed.
 
82
 
 
83
Goal forall m:positive, (m<2)%positive -> (m=1)%positive.
 
84
intros.
 
85
omega with *.
 
86
Qed.
 
87
 
 
88
Goal forall m: positive, (m<=1000)%positive -> (2<=m+m/\m+m <=2000)%positive.
 
89
intros.
 
90
omega with *.
 
91
Qed.
 
92
 
 
93
Goal forall m: positive, (m*m>=1)%positive.
 
94
intros.
 
95
omega with *.
 
96
Qed.
 
97
 
 
98
(* zify_N *)
 
99
 
 
100
Goal forall m:N, (m<2)%N -> (0 <= m+m /\ m+m <= 2)%N.
 
101
intros.
 
102
omega with *.
 
103
Qed.
 
104
 
 
105
Goal forall m:N, (m<1)%N -> (m=0)%N.
 
106
intros.
 
107
omega with *.
 
108
Qed.
 
109
 
 
110
Goal forall m:N, (m<=1000)%N -> (0<=m+m/\m+m <=2000)%N.
 
111
intros.
 
112
omega with *.
 
113
Qed.
 
114
 
 
115
Goal forall m:N, (m*m>=0)%N.
 
116
intros.
 
117
omega with *.
 
118
Qed.
 
119
 
 
120
(* mix of datatypes *)
 
121
 
 
122
Goal forall p, Z_of_N (N_of_nat (nat_of_N (Npos p))) = Zpos p.
 
123
intros.
 
124
omega with *.
 
125
Qed.
 
126
 
 
127