From 6b649aba925b6f7462da07599fe67ebb12a3460e Mon Sep 17 00:00:00 2001
From: Samuel Mimram <samuel.mimram@ens-lyon.org>
Date: Wed, 28 Jul 2004 21:54:47 +0000
Subject: Imported Upstream version 8.0pl1

---
 test-suite/success/Omega.v | 89 ++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 89 insertions(+)
 create mode 100644 test-suite/success/Omega.v

(limited to 'test-suite/success/Omega.v')

diff --git a/test-suite/success/Omega.v b/test-suite/success/Omega.v
new file mode 100644
index 00000000..c324919f
--- /dev/null
+++ b/test-suite/success/Omega.v
@@ -0,0 +1,89 @@
+
+Require Omega.
+
+(* Submitted by Xavier Urbain 18 Jan 2002 *)
+
+Lemma lem1 : (x,y:Z) 
+  `-5 < x < 5` ->
+  `-5 < y` ->
+  `-5 < x+y+5`.
+Proof.
+Intros x y.
+Omega.
+Qed.
+
+(* Proposed by Pierre Crégut *)
+
+Lemma lem2 : (x:Z) `x < 4` -> `x > 2` -> `x=3`.
+Intro.
+Omega.
+Qed.
+
+(* Proposed by Jean-Christophe Filliâtre *)
+
+Lemma lem3 : (x,y:Z) `x = y` -> `x+x = y+y`.
+Proof.
+Intros.
+Omega.
+Qed.
+
+(* Proposed by Jean-Christophe Filliâtre: confusion between an Omega *)
+(* internal variable and a section variable (June 2001) *)
+
+Section A.
+Variable x,y : Z.
+Hypothesis H : `x > y`.
+Lemma lem4 : `x > y`.
+Omega.
+Qed.
+End A.
+
+(* Proposed by Yves Bertot: because a section var, L was wrongly renamed L0 *)
+(* May 2002 *)
+
+Section B.
+Variables R1,R2,S1,S2,H,S:Z.
+Hypothesis I:`R1 < 0`->`R2 = R1+(2*S1-1)`.
+Hypothesis J:`R1 < 0`->`S2 = S1-1`.
+Hypothesis K:`R1 >= 0`->`R2 = R1`.
+Hypothesis L:`R1 >= 0`->`S2 = S1`.
+Hypothesis M:`H <= 2*S`.
+Hypothesis N:`S < H`.
+Lemma lem5 : `H > 0`.
+Omega.
+Qed.
+End B.
+
+(* From Nicolas Oury (bug #180): handling -> on Set (fixed Oct 2002) *)
+Lemma lem6: (A: Set) (i:Z) `i<= 0` -> (`i<= 0` -> A) -> `i<=0`.
+Intros.
+Omega.
+Qed.
+
+(* Adapted from an example in Nijmegen/FTA/ftc/RefSeparating (Oct 2002) *)
+Require Omega.
+Section C.
+Parameter g:(m:nat)~m=O->Prop.
+Parameter f:(m:nat)(H:~m=O)(g m H).
+Variable n:nat.
+Variable ap_n:~n=O.
+Local delta:=(f n ap_n).
+Lemma lem7 : n=n.
+Omega.
+Qed.
+End C.
+
+(* Problem of dependencies *)
+Require Omega.
+Lemma lem8 : (H:O=O->O=O) H=H -> O=O.
+Intros; Omega.
+Qed.
+
+(* Bug that what caused by the use of intro_using in Omega *)
+Require Omega.
+Lemma lem9 : (p,q:nat)
+  ~((le p q)/\(lt p q)\/(le q p)/\(lt p q))
+  -> (lt p p)\/(le p p).
+Intros; Omega.
+Qed.
+
-- 
cgit v1.2.3