diff options
Diffstat (limited to 'test-suite/success/Field.v')
| -rw-r--r-- | test-suite/success/Field.v | 63 |
1 files changed, 35 insertions, 28 deletions
diff --git a/test-suite/success/Field.v b/test-suite/success/Field.v index c203b739..9f4ec79a 100644 --- a/test-suite/success/Field.v +++ b/test-suite/success/Field.v @@ -6,66 +6,73 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: Field.v,v 1.1.16.1 2004/07/16 19:30:58 herbelin Exp $ *) +(* $Id: Field.v 7693 2005-12-21 23:50:17Z herbelin $ *) (**** Tests of Field with real numbers ****) -Require Reals. +Require Import Reals. (* Example 1 *) -Goal (eps:R)``eps*1/(2+2)+eps*1/(2+2) == eps*1/2``. +Goal +forall eps : R, +(eps * (1 / (2 + 2)) + eps * (1 / (2 + 2)))%R = (eps * (1 / 2))%R. Proof. - Intros. - Field. + intros. + field. Abort. (* Example 2 *) -Goal (f,g:(R->R); x0,x1: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)``. +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. Proof. - Intros. - Field. + intros. + field. Abort. (* Example 3 *) -Goal (a,b:R)``1/(a*b)*1/1/b == 1/a``. +Goal forall a b : R, (1 / (a * b) * (1 / 1 / b))%R = (1 / a)%R. Proof. - Intros. - Field. + intros. + field. Abort. (* Example 4 *) -Goal (a,b:R)``a <> 0``->``b <> 0``->``1/(a*b)/1/b == 1/a``. +Goal +forall a b : R, a <> 0%R -> b <> 0%R -> (1 / (a * b) / 1 / b)%R = (1 / a)%R. Proof. - Intros. - Field. + intros. + field. Abort. (* Example 5 *) -Goal (a:R)``1 == 1*1/a*a``. +Goal forall a : R, 1%R = (1 * (1 / a) * a)%R. Proof. - Intros. - Field. + intros. + field. Abort. (* Example 6 *) -Goal (a,b:R)``b == b*/a*a``. +Goal forall a b : R, b = (b * / a * a)%R. Proof. - Intros. - Field. + intros. + field. Abort. (* Example 7 *) -Goal (a,b:R)``b == b*1/a*a``. +Goal forall a b : R, b = (b * (1 / a) * a)%R. Proof. - Intros. - Field. + intros. + field. Abort. (* Example 8 *) -Goal (x,y:R)``x*((1/x)+x/(x+y)) == -(1/y)*y*(-(x*x/(x+y))-1)``. +Goal +forall x y : R, +(x * (1 / x + x / (x + y)))%R = +(- (1 / y) * y * (- (x * (x / (x + y))) - 1))%R. Proof. - Intros. - Field. + intros. + field. Abort. |