← Back to branch summary

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

« back to all changes in this revision

Viewing changes to test-suite/success/ROmega.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/ROmega.v
 
1
 
 
2
Require Import ZArith ROmega.
 
3
 
 
4
(* Submitted by Xavier Urbain 18 Jan 2002 *)
 
5
 
 
6
Lemma lem1 :
 
7
 forall x y : Z, (-5 < x < 5)%Z -> (-5 < y)%Z -> (-5 < x + y + 5)%Z.
 
8
Proof.
 
9
intros x y.
 
10
romega.
 
11
Qed.
 
12
 
 
13
(* Proposed by Pierre Crégut *)
 
14
 
 
15
Lemma lem2 : forall x : Z, (x < 4)%Z -> (x > 2)%Z -> x = 3%Z.
 
16
intro.
 
17
 romega.
 
18
Qed.
 
19
 
 
20
(* Proposed by Jean-Christophe Filliâtre *)
 
21
 
 
22
Lemma lem3 : forall x y : Z, x = y -> (x + x)%Z = (y + y)%Z.
 
23
Proof.
 
24
intros.
 
25
romega. 
 
26
Qed.
 
27
 
 
28
(* Proposed by Jean-Christophe Filliâtre: confusion between an Omega *)
 
29
(* internal variable and a section variable (June 2001) *)
 
30
 
 
31
Section A.
 
32
Variable x y : Z.
 
33
Hypothesis H : (x > y)%Z.
 
34
Lemma lem4 : (x > y)%Z.
 
35
 romega.
 
36
Qed.
 
37
End A.
 
38
 
 
39
(* Proposed by Yves Bertot: because a section var, L was wrongly renamed L0 *)
 
40
(* May 2002 *)
 
41
 
 
42
Section B.
 
43
Variable R1 R2 S1 S2 H S : Z.
 
44
Hypothesis I : (R1 < 0)%Z -> R2 = (R1 + (2 * S1 - 1))%Z.
 
45
Hypothesis J : (R1 < 0)%Z -> S2 = (S1 - 1)%Z.
 
46
Hypothesis K : (R1 >= 0)%Z -> R2 = R1.
 
47
Hypothesis L : (R1 >= 0)%Z -> S2 = S1.
 
48
Hypothesis M : (H <= 2 * S)%Z.
 
49
Hypothesis N : (S < H)%Z.
 
50
Lemma lem5 : (H > 0)%Z.
 
51
 romega.
 
52
Qed.
 
53
End B.
 
54
 
 
55
(* From Nicolas Oury (bug #180): handling -> on Set (fixed Oct 2002) *)
 
56
Lemma lem6 :
 
57
 forall (A : Set) (i : Z), (i <= 0)%Z -> ((i <= 0)%Z -> A) -> (i <= 0)%Z.
 
58
intros.
 
59
 romega.
 
60
Qed.
 
61
 
 
62
(* Adapted from an example in Nijmegen/FTA/ftc/RefSeparating (Oct 2002) *)
 
63
Require Import Omega.
 
64
Section C.
 
65
Parameter g : forall m : nat, m <> 0 -> Prop.
 
66
Parameter f : forall (m : nat) (H : m <> 0), g m H.
 
67
Variable n : nat.
 
68
Variable ap_n : n <> 0.
 
69
Let delta := f n ap_n.
 
70
Lemma lem7 : n = n.
 
71
 romega with nat.
 
72
Qed.
 
73
End C.
 
74
 
 
75
(* Problem of dependencies *)
 
76
Require Import Omega.
 
77
Lemma lem8 : forall H : 0 = 0 -> 0 = 0, H = H -> 0 = 0.
 
78
intros.
 
79
romega with nat.
 
80
Qed.
 
81
 
 
82
(* Bug that what caused by the use of intro_using in Omega *)
 
83
Require Import Omega.
 
84
Lemma lem9 :
 
85
 forall p q : nat, ~ (p <= q /\ p < q \/ q <= p /\ p < q) -> p < p \/ p <= p.
 
86
intros.
 
87
romega with nat.
 
88
Qed.
 
89
 
 
90
(* Check that the interpretation of mult on nat enforces its positivity *)
 
91
(* Submitted by Hubert Thierry (bug #743) *)
 
92
(* Postponed... problem with goals of the form "(n*m=0)%nat -> (n*m=0)%Z" *)
 
93
Lemma lem10 : forall n m : nat, le n (plus n (mult n m)).
 
94
Proof.
 
95
intros; romega with nat.
 
96
Qed.