diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-12-21 23:50:17 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-12-21 23:50:17 +0000 |
| commit | 4d4f08acb5e5f56d38289e5629173bc1b8b5fd57 (patch) | |
| tree | c160d442d54dbd15cbd0ab3500cdf94d0a6da74e /test-suite/success/Field.v | |
| parent | 960859c0c10e029f9768d0d70addeca8f6b6d784 (diff) | |
Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7693 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/success/Field.v')
| -rw-r--r-- | test-suite/success/Field.v | 61 |
1 files changed, 34 insertions, 27 deletions
diff --git a/test-suite/success/Field.v b/test-suite/success/Field.v index aa51e0577..310dfb620 100644 --- a/test-suite/success/Field.v +++ b/test-suite/success/Field.v @@ -10,62 +10,69 @@ (**** 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. |