diff options
Diffstat (limited to 'test-suite/success/Field.v')
| -rw-r--r-- | test-suite/success/Field.v | 43 |
1 files changed, 28 insertions, 15 deletions
diff --git a/test-suite/success/Field.v b/test-suite/success/Field.v index 9f4ec79a..b4c06c7b 100644 --- a/test-suite/success/Field.v +++ b/test-suite/success/Field.v @@ -6,62 +6,75 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: Field.v 7693 2005-12-21 23:50:17Z herbelin $ *) +(* $Id: Field.v 9197 2006-10-02 15:55:52Z barras $ *) (**** 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. |