diff options
Diffstat (limited to 'test-suite/success/OmegaPre.v')
| -rw-r--r-- | test-suite/success/OmegaPre.v | 43 |
1 files changed, 21 insertions, 22 deletions
diff --git a/test-suite/success/OmegaPre.v b/test-suite/success/OmegaPre.v index 0223255067..32bc99621a 100644 --- a/test-suite/success/OmegaPre.v +++ b/test-suite/success/OmegaPre.v @@ -1,4 +1,4 @@ -Require Import ZArith Nnat Omega. +Require Import ZArith Nnat Lia. Open Scope Z_scope. (** Test of the zify preprocessor for (R)Omega *) @@ -16,112 +16,111 @@ Open Scope Z_scope. Goal forall a:Z, Z.max a a = a. intros. -zify; omega. +lia. Qed. Goal forall a b:Z, Z.max a b = Z.max b a. intros. -zify; omega. +lia. Qed. Goal forall a b c:Z, Z.max a (Z.max b c) = Z.max (Z.max a b) c. intros. -zify; omega. +lia. Qed. Goal forall a b:Z, Z.max a b + Z.min a b = a + b. intros. -zify; omega. +lia. Qed. Goal forall a:Z, (Z.abs a)*(Z.sgn a) = a. intros. -zify. -intuition; subst; zify; omega. (* pure multiplication: zify; omega alone can't do it *) +intuition; subst; lia. Qed. Goal forall a:Z, Z.abs a = a -> a >= 0. intros. -zify; omega. +lia. Qed. Goal forall a:Z, Z.sgn a = a -> a = 1 \/ a = 0 \/ a = -1. intros. -zify; omega. +lia. Qed. (* zify_nat *) Goal forall m: nat, (m<2)%nat -> (0<= m+m <=2)%nat. intros. -zify; omega. +lia. Qed. Goal forall m:nat, (m<1)%nat -> (m=0)%nat. intros. -zify; omega. +lia. Qed. Goal forall m: nat, (m<=100)%nat -> (0<= m+m <=200)%nat. intros. -zify; omega. +lia. Qed. (* 2000 instead of 200: works, but quite slow *) Goal forall m: nat, (m*m>=0)%nat. intros. -zify; omega. +lia. Qed. (* zify_positive *) Goal forall m: positive, (m<2)%positive -> (2 <= m+m /\ m+m <= 2)%positive. intros. -zify; omega. +lia. Qed. Goal forall m:positive, (m<2)%positive -> (m=1)%positive. intros. -zify; omega. +lia. Qed. Goal forall m: positive, (m<=1000)%positive -> (2<=m+m/\m+m <=2000)%positive. intros. -zify; omega. +lia. Qed. Goal forall m: positive, (m*m>=1)%positive. intros. -zify; omega. +lia. Qed. (* zify_N *) Goal forall m:N, (m<2)%N -> (0 <= m+m /\ m+m <= 2)%N. intros. -zify; omega. +lia. Qed. Goal forall m:N, (m<1)%N -> (m=0)%N. intros. -zify; omega. +lia. Qed. Goal forall m:N, (m<=1000)%N -> (0<=m+m/\m+m <=2000)%N. intros. -zify; omega. +lia. Qed. Goal forall m:N, (m*m>=0)%N. intros. -zify; omega. +lia. Qed. (* mix of datatypes *) Goal forall p, Z.of_N (N.of_nat (N.to_nat (Npos p))) = Zpos p. intros. -zify; omega. +lia. Qed. |