diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-10-02 15:55:52 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-10-02 15:55:52 +0000 |
| commit | 83c7941f909ebe5150868b1242669c7f4502b528 (patch) | |
| tree | 1a98d6724ff5155de35c93633a669046e01e87e2 /test-suite/success/Field.v | |
| parent | 08ac8a40c8bfde21889196519883718b8c5ea521 (diff) | |
nouveau ring/field
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9197 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/success/Field.v')
| -rw-r--r-- | test-suite/success/Field.v | 41 |
1 files changed, 27 insertions, 14 deletions
diff --git a/test-suite/success/Field.v b/test-suite/success/Field.v index 310dfb620..6fb922b0f 100644 --- a/test-suite/success/Field.v +++ b/test-suite/success/Field.v @@ -10,58 +10,71 @@ (**** Tests of Field with real numbers ****) -Require Import Reals. +Require Import Reals RealField. +Open Scope R_scope. (* Example 1 *) Goal forall eps : R, -(eps * (1 / (2 + 2)) + eps * (1 / (2 + 2)))%R = (eps * (1 / 2))%R. +eps * (1 / (2 + 2)) + eps * (1 / (2 + 2)) = eps * (1 / 2). Proof. intros. field. -Abort. +Qed. (* Example 2 *) Goal forall (f g : R -> R) (x0 x1 : R), -((f x1 - f x0) * (1 / (x1 - x0)) + (g x1 - g x0) * (1 / (x1 - x0)))%R = -((f x1 + g x1 - (f x0 + g x0)) * (1 / (x1 - x0)))%R. +(f x1 - f x0) * (1 / (x1 - x0)) + (g x1 - g x0) * (1 / (x1 - x0)) = +(f x1 + g x1 - (f x0 + g x0)) * (1 / (x1 - x0)). Proof. intros. field. Abort. (* Example 3 *) -Goal forall a b : R, (1 / (a * b) * (1 / 1 / b))%R = (1 / a)%R. +Goal forall a b : R, 1 / (a * b) * (1 / (1 / b)) = 1 / a. Proof. intros. field. Abort. + +Goal forall a b : R, 1 / (a * b) * (1 / 1 / b) = 1 / a. +Proof. + intros. + field_simplify_eq. +Abort. +Goal forall a b : R, 1 / (a * b) * (1 / 1 / b) = 1 / a. +Proof. + intros. + field_simplify (1 / (a * b) * (1 / 1 / b)). +Abort. + (* Example 4 *) Goal -forall a b : R, a <> 0%R -> b <> 0%R -> (1 / (a * b) / 1 / b)%R = (1 / a)%R. +forall a b : R, a <> 0 -> b <> 0 -> 1 / (a * b) / (1 / b) = 1 / a. Proof. intros. - field. -Abort. + field; auto. +Qed. (* Example 5 *) -Goal forall a : R, 1%R = (1 * (1 / a) * a)%R. +Goal forall a : R, 1 = 1 * (1 / a) * a. Proof. intros. field. Abort. (* Example 6 *) -Goal forall a b : R, b = (b * / a * a)%R. +Goal forall a b : R, b = b * / a * a. Proof. intros. field. Abort. (* Example 7 *) -Goal forall a b : R, b = (b * (1 / a) * a)%R. +Goal forall a b : R, b = b * (1 / a) * a. Proof. intros. field. @@ -70,8 +83,8 @@ Abort. (* Example 8 *) Goal forall x y : R, -(x * (1 / x + x / (x + y)))%R = -(- (1 / y) * y * (- (x * (x / (x + y))) - 1))%R. +x * (1 / x + x / (x + y)) = +- (1 / y) * y * (- (x * (x / (x + y))) - 1). Proof. intros. field. |