diff options
Diffstat (limited to 'test-suite/success/Omega.v')
| -rw-r--r-- | test-suite/success/Omega.v | 95 |
1 files changed, 51 insertions, 44 deletions
diff --git a/test-suite/success/Omega.v b/test-suite/success/Omega.v index c324919f..2d29a835 100644 --- a/test-suite/success/Omega.v +++ b/test-suite/success/Omega.v @@ -1,40 +1,38 @@ -Require Omega. +Require Import Omega. (* Submitted by Xavier Urbain 18 Jan 2002 *) -Lemma lem1 : (x,y:Z) - `-5 < x < 5` -> - `-5 < y` -> - `-5 < x+y+5`. +Lemma lem1 : + forall x y : Z, (-5 < x < 5)%Z -> (-5 < y)%Z -> (-5 < x + y + 5)%Z. Proof. -Intros x y. -Omega. +intros x y. + omega. Qed. (* Proposed by Pierre Crégut *) -Lemma lem2 : (x:Z) `x < 4` -> `x > 2` -> `x=3`. -Intro. -Omega. +Lemma lem2 : forall x : Z, (x < 4)%Z -> (x > 2)%Z -> x = 3%Z. +intro. + omega. Qed. (* Proposed by Jean-Christophe Filliâtre *) -Lemma lem3 : (x,y:Z) `x = y` -> `x+x = y+y`. +Lemma lem3 : forall x y : Z, x = y -> (x + x)%Z = (y + y)%Z. Proof. -Intros. -Omega. +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. +Variable x y : Z. +Hypothesis H : (x > y)%Z. +Lemma lem4 : (x > y)%Z. + omega. Qed. End A. @@ -42,48 +40,57 @@ End A. (* 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. +Variable R1 R2 S1 S2 H S : Z. +Hypothesis I : (R1 < 0)%Z -> R2 = (R1 + (2 * S1 - 1))%Z. +Hypothesis J : (R1 < 0)%Z -> S2 = (S1 - 1)%Z. +Hypothesis K : (R1 >= 0)%Z -> R2 = R1. +Hypothesis L : (R1 >= 0)%Z -> S2 = S1. +Hypothesis M : (H <= 2 * S)%Z. +Hypothesis N : (S < H)%Z. +Lemma lem5 : (H > 0)%Z. + 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. +Lemma lem6 : + forall (A : Set) (i : Z), (i <= 0)%Z -> ((i <= 0)%Z -> A) -> (i <= 0)%Z. +intros. + omega. Qed. (* Adapted from an example in Nijmegen/FTA/ftc/RefSeparating (Oct 2002) *) -Require Omega. +Require Import 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. +Parameter g : forall m : nat, m <> 0 -> Prop. +Parameter f : forall (m : nat) (H : m <> 0), g m H. +Variable n : nat. +Variable ap_n : n <> 0. +Let 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. +Require Import Omega. +Lemma lem8 : forall H : 0 = 0 -> 0 = 0, H = H -> 0 = 0. +intros; omega. Qed. (* Bug that what caused by the use of intro_using in Omega *) +Require Import Omega. +Lemma lem9 : + forall p q : nat, ~ (p <= q /\ p < q \/ q <= p /\ p < q) -> p < p \/ p <= p. +intros; omega. +Qed. + +(* Check that the interpretation of mult on nat enforces its positivity *) +(* Submitted by Hubert Thierry (bug #743) *) +(* Postponed... problem with goals of the form "(n*m=0)%nat -> (n*m=0)%Z" 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). +Lemma lem10 : (n, m : nat) (le n (plus n (mult n m))). +Proof. Intros; Omega. Qed. - +*) |