summaryrefslogtreecommitdiff
path: root/test-suite
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite')
-rw-r--r--test-suite/bugs/closed/2319.v13
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1507.v2
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2145.v4
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2262.v11
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2303.v4
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2347.v10
-rw-r--r--test-suite/output/Notations.out28
-rw-r--r--test-suite/output/Notations.v39
-rw-r--r--test-suite/output/Notations2.out15
-rw-r--r--test-suite/output/Notations2.v41
-rw-r--r--test-suite/output/Search.out18
-rw-r--r--test-suite/output/SearchPattern.out18
-rw-r--r--test-suite/success/Field.v2
-rw-r--r--test-suite/success/Nsatz.v132
-rw-r--r--test-suite/success/Nsatz_domain.v274
-rw-r--r--test-suite/success/Tauto.v2
-rw-r--r--test-suite/success/Typeclasses.v6
17 files changed, 270 insertions, 349 deletions
diff --git a/test-suite/bugs/closed/2319.v b/test-suite/bugs/closed/2319.v
new file mode 100644
index 00000000..e06fb975
--- /dev/null
+++ b/test-suite/bugs/closed/2319.v
@@ -0,0 +1,13 @@
+Section S.
+
+ CoInductive A (X: Type) := mkA: A X -> A X.
+ Variable T : Type.
+
+ (* This used to loop (bug #2319) *)
+ Timeout 5 Eval vm_compute in cofix s : A T := mkA T s.
+
+ CoFixpoint s : A T := mkA T s
+ with t : A unit := mkA unit (mkA unit t).
+ Timeout 5 Eval vm_compute in s.
+
+End S. \ No newline at end of file
diff --git a/test-suite/bugs/closed/shouldsucceed/1507.v b/test-suite/bugs/closed/shouldsucceed/1507.v
index f1872a2b..ea72ba89 100644
--- a/test-suite/bugs/closed/shouldsucceed/1507.v
+++ b/test-suite/bugs/closed/shouldsucceed/1507.v
@@ -2,7 +2,7 @@
Implementing reals a la Stolzenberg
Danko Ilik, March 2007
- svn revision: $Id$
+ svn revision: $Id: 1507.v 12337 2009-09-17 15:58:14Z glondu $
XField.v -- (unfinished) axiomatisation of the theories of real and
rational intervals.
diff --git a/test-suite/bugs/closed/shouldsucceed/2145.v b/test-suite/bugs/closed/shouldsucceed/2145.v
index b6c5da65..4dc0de74 100644
--- a/test-suite/bugs/closed/shouldsucceed/2145.v
+++ b/test-suite/bugs/closed/shouldsucceed/2145.v
@@ -1,7 +1,7 @@
(* Test robustness of Groebner tactic in presence of disequalities *)
Require Export Reals.
-Require Export NsatzR.
+Require Export Nsatz.
Open Scope R_scope.
@@ -15,6 +15,6 @@ Lemma essai :
Proof.
intros.
(* clear H. groebner used not to work when H was not cleared *)
-nsatzR.
+nsatz.
Qed.
diff --git a/test-suite/bugs/closed/shouldsucceed/2262.v b/test-suite/bugs/closed/shouldsucceed/2262.v
new file mode 100644
index 00000000..b61f18b8
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2262.v
@@ -0,0 +1,11 @@
+
+
+Generalizable Variables A.
+Class Test A := { test : A }.
+
+Lemma mylemma : forall `{Test A}, test = test.
+Admitted. (* works fine *)
+
+Definition mylemma' := forall `{Test A}, test = test.
+About mylemma'.
+
diff --git a/test-suite/bugs/closed/shouldsucceed/2303.v b/test-suite/bugs/closed/shouldsucceed/2303.v
new file mode 100644
index 00000000..e614b9b5
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2303.v
@@ -0,0 +1,4 @@
+Class A := a: unit.
+Class B (x: unit).
+Axiom H: forall x: A, @B x -> x = x -> unit.
+Definition Field (z: A) (m: @B z) x := (@H _ _ x) = z.
diff --git a/test-suite/bugs/closed/shouldsucceed/2347.v b/test-suite/bugs/closed/shouldsucceed/2347.v
new file mode 100644
index 00000000..e433f158
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2347.v
@@ -0,0 +1,10 @@
+Require Import EquivDec List.
+Generalizable All Variables.
+
+Program Definition list_eqdec `(eqa : EqDec A eq) : EqDec (list A) eq :=
+ (fun (x y : list A) => _).
+Admit Obligations of list_eqdec.
+
+Program Definition list_eqdec' `(eqa : EqDec A eq) : EqDec (list A) eq :=
+ (fun _ : nat => (fun (x y : list A) => _)) 0.
+Admit Obligations of list_eqdec'.
diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
index 924030ba..215d9b68 100644
--- a/test-suite/output/Notations.out
+++ b/test-suite/output/Notations.out
@@ -46,6 +46,32 @@ fun x : nat => ifn x is succ n then n else 0
: bool
-4
: Z
+The command has indeed failed with message:
+=> Error: x should not be bound in a recursive pattern of the right-hand side.
+The command has indeed failed with message:
+=> Error: in the right-hand side, y and z should appear in
+ term position as part of a recursive pattern.
+The command has indeed failed with message:
+=> Error: The reference w was not found in the current environment.
+The command has indeed failed with message:
+=> Error: x is unbound in the right-hand side.
+The command has indeed failed with message:
+=> Error: in the right-hand side, y and z should appear in
+ term position as part of a recursive pattern.
+The command has indeed failed with message:
+=> Error: z is expected to occur in binding position in the right-hand side.
+The command has indeed failed with message:
+=> Error: as y is a non-closed binder, no such "," is allowed to occur.
+The command has indeed failed with message:
+=> Error: Cannot find where the recursive pattern starts.
+The command has indeed failed with message:
+=> Error: Cannot find where the recursive pattern starts.
+The command has indeed failed with message:
+=> Error: Cannot find where the recursive pattern starts.
+The command has indeed failed with message:
+=> Error: Cannot find where the recursive pattern starts.
+The command has indeed failed with message:
+=> Error: Both ends of the recursive pattern are the same.
SUM (nat * nat) nat
: Set
FST (0; 1)
@@ -59,6 +85,8 @@ Defining 'I' as keyword
: Prop
[|1, 2, 3; 4, 5, 6|]
: Z * Z * Z * (Z * Z * Z)
+[|0 * (1, 2, 3); (4, 5, 6) * false|]
+ : Z * Z * (Z * Z) * (Z * Z) * (Z * bool * (Z * bool) * (Z * bool))
fun f : Z -> Z -> Z -> Z => {|f; 0; 1; 2|}:Z
: (Z -> Z -> Z -> Z) -> Z
plus
diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v
index f041b9b7..b8f8f48f 100644
--- a/test-suite/output/Notations.v
+++ b/test-suite/output/Notations.v
@@ -121,6 +121,39 @@ Notation "- 4" := (-2 + -2).
Check -4.
(**********************************************************************)
+(* Check ill-formed recursive notations *)
+
+(* Recursive variables not part of a recursive pattern *)
+Fail Notation "( x , y , .. , z )" := (pair x .. (pair y z) ..).
+
+(* No recursive notation *)
+Fail Notation "( x , y , .. , z )" := (pair x (pair y z)).
+
+(* Left-unbound variable *)
+Fail Notation "( x , y , .. , z )" := (pair x .. (pair y w) ..).
+
+(* Right-unbound variable *)
+Fail Notation "( x , y , .. , z )" := (pair y .. (pair z 0) ..).
+
+(* Not the right kind of recursive pattern *)
+Fail Notation "( x , y , .. , z )" := (ex (fun z => .. (ex (fun y => x)) ..)).
+Fail Notation "( x -- y , .. , z )" := (pair y .. (pair z 0) ..)
+ (y closed binder, z closed binder).
+
+(* No separator allowed with open binders *)
+Fail Notation "( x -- y , .. , z )" := (ex (fun z => .. (ex (fun y => x)) ..))
+ (y binder, z binder).
+
+(* Ends of pattern do not match *)
+Fail Notation "( x , y , .. , z )" := (pair y .. (pair (plus z) 0) ..).
+Fail Notation "( x , y , .. , z )" := (pair y .. (plus z 0) ..).
+Fail Notation "( x1 , x2 , y , .. , z )" := (y y .. (x2 z 0) ..).
+Fail Notation "( x1 , x2 , y , .. , z )" := (x1 y .. (x2 z 0) ..).
+
+(* Ends of pattern are the same *)
+Fail Notation "( x , y , .. , z )" := (pair .. (pair (pair y z) x) .. x).
+
+(**********************************************************************)
(* Check preservation of scopes at printing time *)
Notation SUM := sum.
@@ -163,6 +196,12 @@ Notation "[| x , y , .. , z ; a , b , .. , c |]" :=
(pair (pair .. (pair x y) .. z) (pair .. (pair a b) .. c)).
Check [|1,2,3;4,5,6|].
+Notation "[| t * ( x , y , .. , z ) ; ( a , b , .. , c ) * u |]" :=
+ (pair (pair .. (pair (pair t x) (pair t y)) .. (pair t z))
+ (pair .. (pair (pair a u) (pair b u)) .. (pair c u)))
+ (t at level 39).
+Check [|0*(1,2,3);(4,5,6)*false|].
+
(**********************************************************************)
(* Test recursive notations involving applications *)
(* Caveat: does not work for applied constant because constants are *)
diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out
index 20d20d82..6731d505 100644
--- a/test-suite/output/Notations2.out
+++ b/test-suite/output/Notations2.out
@@ -10,3 +10,18 @@ end
: nat
let '(a, _, _) := (2, 3, 4) in a
: nat
+∃ n p : nat, n + p = 0
+ : Prop
+∀ n p : nat, n + p = 0
+ : Prop
+λ n p : nat, n + p = 0
+ : nat -> nat -> Prop
+λ (A : Type) (n p : A), n = p
+ : ∀ A : Type, A -> A -> Prop
+λ A : Type, ∃ n p : A, n = p
+ : Type -> Prop
+λ A : Type, ∀ n p : A, n = p
+ : Type -> Prop
+Defining 'let'' as keyword
+let' f (x y z : nat) (_ : bool) := x + y + z + 1 in f 0 1 2
+ : bool -> nat
diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v
index 2e136edf..57d8ebbc 100644
--- a/test-suite/output/Notations2.v
+++ b/test-suite/output/Notations2.v
@@ -24,3 +24,44 @@ Check forall (A: Set) (le: A -> A -> Prop) (x y: A), le x y \/ le y x.
Remove Printing Let prod.
Check match (0,0,0) with (x,y,z) => x+y+z end.
Check let '(a,b,c) := ((2,3),4) in a.
+
+(* Test notations with binders *)
+
+Notation "∃ x .. y , P":=
+ (ex (fun x => .. (ex (fun y => P)) ..)) (x binder, y binder, at level 200).
+
+Check (∃ n p, n+p=0).
+
+Notation "∀ x .. y , P":= (forall x, .. (forall y, P) ..)
+ (x binder, at level 200, right associativity).
+
+Check (∀ n p, n+p=0).
+
+Notation "'λ' x .. y , P":= (fun x, .. (fun y, P) ..)
+ (y binder, at level 200, right associativity).
+
+Check (λ n p, n+p=0).
+
+Generalizable Variable A.
+
+Check `(λ n p : A, n=p).
+Check `(∃ n p : A, n=p).
+Check `(∀ n p : A, n=p).
+
+Notation "'let'' f x .. y := t 'in' u":=
+ (let f := fun x => .. (fun y => t) .. in u)
+ (f ident, x closed binder, y closed binder, at level 200,
+ right associativity).
+
+Check let' f x y z (a:bool) := x+y+z+1 in f 0 1 2.
+
+(* This one is not fully satisfactory because binders in the same type
+ are re-factorized and parentheses are needed even for atomic binder
+
+Notation "'mylet' f [ x ; .. ; y ] := t 'in' u":=
+ (let f := fun x => .. (fun y => t) .. in u)
+ (f ident, x closed binder, y closed binder, at level 200,
+ right associativity).
+
+Check mylet f [x;y;z;(a:bool)] := x+y+z+1 in f 0 1 2.
+*)
diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out
index 99e736dd..154d9cdd 100644
--- a/test-suite/output/Search.out
+++ b/test-suite/output/Search.out
@@ -2,29 +2,11 @@ le_S: forall n m : nat, n <= m -> n <= S m
le_n: forall n : nat, n <= n
false: bool
true: bool
-sumor_beq:
- forall (A : Type) (B : Prop),
- (A -> A -> bool) -> (B -> B -> bool) -> A + {B} -> A + {B} -> bool
-sumbool_beq:
- forall A B : Prop,
- (A -> A -> bool) -> (B -> B -> bool) -> {A} + {B} -> {A} + {B} -> bool
xorb: bool -> bool -> bool
-sum_beq:
- forall A B : Type,
- (A -> A -> bool) -> (B -> B -> bool) -> A + B -> A + B -> bool
-prod_beq:
- forall A B : Type,
- (A -> A -> bool) -> (B -> B -> bool) -> A * B -> A * B -> bool
orb: bool -> bool -> bool
-option_beq: forall A : Type, (A -> A -> bool) -> option A -> option A -> bool
negb: bool -> bool
-nat_beq: nat -> nat -> bool
-list_beq: forall A : Type, (A -> A -> bool) -> list A -> list A -> bool
implb: bool -> bool -> bool
-comparison_beq: comparison -> comparison -> bool
-bool_beq: bool -> bool -> bool
andb: bool -> bool -> bool
-Empty_set_beq: Empty_set -> Empty_set -> bool
pred_Sn: forall n : nat, n = pred (S n)
plus_n_Sm: forall n m : nat, S (n + m) = n + S m
plus_n_O: forall n : nat, n = n + 0
diff --git a/test-suite/output/SearchPattern.out b/test-suite/output/SearchPattern.out
index 1a87f4cc..c87eaadc 100644
--- a/test-suite/output/SearchPattern.out
+++ b/test-suite/output/SearchPattern.out
@@ -1,28 +1,10 @@
false: bool
true: bool
-sumor_beq:
- forall (A : Type) (B : Prop),
- (A -> A -> bool) -> (B -> B -> bool) -> A + {B} -> A + {B} -> bool
-sumbool_beq:
- forall A B : Prop,
- (A -> A -> bool) -> (B -> B -> bool) -> {A} + {B} -> {A} + {B} -> bool
xorb: bool -> bool -> bool
-sum_beq:
- forall A B : Type,
- (A -> A -> bool) -> (B -> B -> bool) -> A + B -> A + B -> bool
-prod_beq:
- forall A B : Type,
- (A -> A -> bool) -> (B -> B -> bool) -> A * B -> A * B -> bool
orb: bool -> bool -> bool
-option_beq: forall A : Type, (A -> A -> bool) -> option A -> option A -> bool
negb: bool -> bool
-nat_beq: nat -> nat -> bool
-list_beq: forall A : Type, (A -> A -> bool) -> list A -> list A -> bool
implb: bool -> bool -> bool
-comparison_beq: comparison -> comparison -> bool
-bool_beq: bool -> bool -> bool
andb: bool -> bool -> bool
-Empty_set_beq: Empty_set -> Empty_set -> bool
S: nat -> nat
O: nat
pred: nat -> nat
diff --git a/test-suite/success/Field.v b/test-suite/success/Field.v
index b5fba17b..cb90e742 100644
--- a/test-suite/success/Field.v
+++ b/test-suite/success/Field.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
+(* $Id: Field.v 13323 2010-07-24 15:57:30Z herbelin $ *)
(**** Tests of Field with real numbers ****)
diff --git a/test-suite/success/Nsatz.v b/test-suite/success/Nsatz.v
index fde9f470..518d22e9 100644
--- a/test-suite/success/Nsatz.v
+++ b/test-suite/success/Nsatz.v
@@ -1,4 +1,74 @@
-Require Import NsatzR ZArith Reals List Ring_polynom.
+Require Import Nsatz ZArith Reals List Ring_polynom.
+
+(* Example with a generic domain *)
+
+Variable A: Type.
+Variable Ad: Domain A.
+
+Definition Ari : Ring A:= (@domain_ring A Ad).
+Existing Instance Ari.
+
+Existing Instance ring_setoid.
+Existing Instance ring_plus_comp.
+Existing Instance ring_mult_comp.
+Existing Instance ring_sub_comp.
+Existing Instance ring_opp_comp.
+
+Add Ring Ar: (@ring_ring A (@domain_ring A Ad)).
+
+Instance zero_ring2 : Zero A := {zero := ring0}.
+Instance one_ring2 : One A := {one := ring1}.
+Instance addition_ring2 : Addition A := {addition x y := ring_plus x y}.
+Instance multiplication_ring2 : Multiplication A := {multiplication x y := ring_mult x y}.
+Instance subtraction_ring2 : Subtraction A := {subtraction x y := ring_sub x y}.
+Instance opposite_ring2 : Opposite A := {opposite x := ring_opp x}.
+
+Infix "==" := ring_eq (at level 70, no associativity).
+
+Ltac nsatzA := simpl; unfold Ari; nsatz_domain.
+
+Goal forall x y:A, x == y -> x+0 == y*1+0.
+nsatzA.
+Qed.
+
+Lemma example3 : forall x y z,
+ x+y+z==0 ->
+ x*y+x*z+y*z==0->
+ x*y*z==0 -> x*x*x==0.
+Proof.
+Time nsatzA.
+Admitted.
+
+Lemma example4 : forall x y z u,
+ x+y+z+u==0 ->
+ x*y+x*z+x*u+y*z+y*u+z*u==0->
+ x*y*z+x*y*u+x*z*u+y*z*u==0->
+ x*y*z*u==0 -> x*x*x*x==0.
+Proof.
+Time nsatzA.
+Qed.
+
+Lemma example5 : forall x y z u v,
+ x+y+z+u+v==0 ->
+ x*y+x*z+x*u+x*v+y*z+y*u+y*v+z*u+z*v+u*v==0->
+ x*y*z+x*y*u+x*y*v+x*z*u+x*z*v+x*u*v+y*z*u+y*z*v+y*u*v+z*u*v==0->
+ x*y*z*u+y*z*u*v+z*u*v*x+u*v*x*y+v*x*y*z==0 ->
+ x*y*z*u*v==0 -> x*x*x*x*x ==0.
+Proof.
+Time nsatzA.
+Qed.
+
+Goal forall x y:Z, x = y -> (x+0)%Z = (y*1+0)%Z.
+nsatz.
+Qed.
+
+Goal forall x y:R, x = y -> (x+0)%R = (y*1+0)%R.
+nsatz.
+Qed.
+
+Goal forall a b c x:R, a = b -> b = c -> (a*a)%R = (c*c)%R.
+nsatz.
+Qed.
Section Examples.
@@ -16,12 +86,12 @@ Lemma example1 : forall x y,
x*y=0 ->
x^2=0.
Proof.
- nsatzR.
+ nsatz.
Qed.
Lemma example2 : forall x, x^2=0 -> x=0.
Proof.
- nsatzR.
+ nsatz.
Qed.
(*
@@ -29,12 +99,12 @@ Notation X := (PEX Z 3).
Notation Y := (PEX Z 2).
Notation Z_ := (PEX Z 1).
*)
-Lemma example3 : forall x y z,
+Lemma example3b : forall x y z,
x+y+z=0 ->
x*y+x*z+y*z=0->
x*y*z=0 -> x^3=0.
Proof.
-Time nsatzR.
+Time nsatz.
Qed.
(*
@@ -43,13 +113,13 @@ Notation Y := (PEX Z 3).
Notation Z_ := (PEX Z 2).
Notation U := (PEX Z 1).
*)
-Lemma example4 : forall x y z u,
+Lemma example4b : forall x y z u,
x+y+z+u=0 ->
x*y+x*z+x*u+y*z+y*u+z*u=0->
x*y*z+x*y*u+x*z*u+y*z*u=0->
x*y*z*u=0 -> x^4=0.
Proof.
-Time nsatzR.
+Time nsatz.
Qed.
(*
@@ -64,20 +134,20 @@ Notation "x :: y" := (List.app x y)
(at level 60, right associativity, format "x :: y").
*)
-Lemma example5 : forall x y z u v,
+Lemma example5b : forall x y z u v,
x+y+z+u+v=0 ->
x*y+x*z+x*u+x*v+y*z+y*u+y*v+z*u+z*v+u*v=0->
x*y*z+x*y*u+x*y*v+x*z*u+x*z*v+x*u*v+y*z*u+y*z*v+y*u*v+z*u*v=0->
x*y*z*u+y*z*u*v+z*u*v*x+u*v*x*y+v*x*y*z=0 ->
x*y*z*u*v=0 -> x^5=0.
Proof.
-Time nsatzR.
+Time nsatz.
Qed.
End Examples.
Section Geometry.
-Require Export Reals NsatzR.
+
Open Scope R_scope.
Record point:Type:={
@@ -169,6 +239,7 @@ Ltac geo_begin:=
(* Examples *)
+
Lemma Thales: forall O A B C D:point,
collinear O A C -> collinear O B D ->
parallel A B C D ->
@@ -176,26 +247,7 @@ Lemma Thales: forall O A B C D:point,
/\ distance2 O B * distance2 C D = distance2 O D * distance2 A B)
\/ collinear O A B.
repeat geo_begin.
-(*
Time nsatz.
-*)
-Time nsatz without sugar.
-(*
-Time nsatz with lexico sugar.
-Time nsatz with lexico.
-*)
-(*
-Time nsatzRpv 1%N 1%Z (@nil R) (@nil R). (* revlex, sugar, no div *)
-(*Finished transaction in 1. secs (0.479927u,0.s)*)
-Time nsatzRpv 1%N 0%Z (@nil R) (@nil R). (* revlex, no sugar, no div *)
-(*Finished transaction in 0. secs (0.543917u,0.s)*)
-Time nsatzRpv 1%N 2%Z (@nil R) (@nil R). (* lex, no sugar, no div *)
-(*Finished transaction in 0. secs (0.586911u,0.s)*)
-Time nsatzRpv 1%N 3%Z (@nil R) (@nil R). (* lex, sugar, no div *)
-(*Finished transaction in 0. secs (0.481927u,0.s)*)
-Time nsatzRpv 1%N 5%Z (@nil R) (@nil R). (* revlex, sugar, div *)
-(*Finished transaction in 1. secs (0.601909u,0.s)*)
-*)
Time nsatz.
Qed.
@@ -209,8 +261,26 @@ Lemma hauteurs:forall A B C A1 B1 C1 H:point,
\/ collinear A B C.
geo_begin.
-Time nsatz.
-(*Finished transaction in 3. secs (2.43263u,0.010998s)*)
+
+(* Time nsatzRpv 2%N 1%Z (@nil R) (@nil R).*)
+(*Finished transaction in 3. secs (2.363641u,0.s)*)
+(*Time nsatz_domainR. trop long! *)
+Time
+ let lv := constr:(Y A1
+ :: X A1
+ :: Y B1
+ :: X B1
+ :: Y A0
+ :: Y B
+ :: X B
+ :: X A0
+ :: X H
+ :: Y C
+ :: Y C1 :: Y H :: X C1 :: X C :: (@Datatypes.nil R)) in
+ nsatz_domainpv ltac:pretacR 2%N 1%Z (@Datatypes.nil R) lv ltac:simplR Rdi;
+ discrR.
+(* Finished transaction in 6. secs (5.579152u,0.001s) *)
Qed.
End Geometry.
+
diff --git a/test-suite/success/Nsatz_domain.v b/test-suite/success/Nsatz_domain.v
deleted file mode 100644
index 8a30b47f..00000000
--- a/test-suite/success/Nsatz_domain.v
+++ /dev/null
@@ -1,274 +0,0 @@
-Require Import Nsatz_domain ZArith Reals List Ring_polynom.
-
-Variable A: Type.
-Variable Ad: Domain A.
-
-Add Ring Ar1: (@ring_ring A (@domain_ring _ Ad)).
-
-Instance Ari : Ring A := {
- ring0 := @ring0 A (@domain_ring _ Ad);
- ring1 := @ring1 A (@domain_ring _ Ad);
- ring_plus := @ring_plus A (@domain_ring _ Ad);
- ring_mult := @ring_mult A (@domain_ring _ Ad);
- ring_sub := @ring_sub A (@domain_ring _ Ad);
- ring_opp := @ring_opp A (@domain_ring _ Ad);
- ring_ring := @ring_ring A (@domain_ring _ Ad)}.
-
-Instance Adi : Domain A := {
- domain_ring := Ari;
- domain_axiom_product := @domain_axiom_product A Ad;
- domain_axiom_one_zero := @domain_axiom_one_zero A Ad}.
-
-Instance zero_ring2 : Zero A := {zero := ring0}.
-Instance one_ring2 : One A := {one := ring1}.
-Instance addition_ring2 : Addition A := {addition x y := ring_plus x y}.
-Instance multiplication_ring2 : Multiplication A := {multiplication x y := ring_mult x y}.
-Instance subtraction_ring2 : Subtraction A := {subtraction x y := ring_sub x y}.
-Instance opposite_ring2 : Opposite A := {opposite x := ring_opp x}.
-
-Goal forall x y:A, x = y -> x+0 = y*1+0.
-nsatz_domain.
-Qed.
-
-Goal forall a b c:A, a = b -> b = c -> c = a.
-nsatz_domain.
-Qed.
-
-Goal forall a b c:A, a = b -> b = c -> a = c.
-nsatz_domain.
-Qed.
-
-Goal forall a b c x:A, a = b -> b = c -> a*a = c*c.
-nsatz_domain.
-Qed.
-
-Goal forall x y:Z, x = y -> (x+0)%Z = (y*1+0)%Z.
-nsatz_domainZ.
-Qed.
-
-Goal forall x y:R, x = y -> (x+0)%R = (y*1+0)%R.
-nsatz_domainR.
-Qed.
-
-Goal forall a b c x:R, a = b -> b = c -> (a*a)%R = (c*c)%R.
-nsatz_domainR.
-Qed.
-
-Section Examples.
-
-Delimit Scope PE_scope with PE.
-Infix "+" := PEadd : PE_scope.
-Infix "*" := PEmul : PE_scope.
-Infix "-" := PEsub : PE_scope.
-Infix "^" := PEpow : PE_scope.
-Notation "[ n ]" := (@PEc Z n) (at level 0).
-
-Open Scope R_scope.
-
-Lemma example1 : forall x y,
- x+y=0 ->
- x*y=0 ->
- x^2=0.
-Proof.
- nsatz_domainR.
-Qed.
-
-Lemma example2 : forall x, x^2=0 -> x=0.
-Proof.
- nsatz_domainR.
-Qed.
-
-(*
-Notation X := (PEX Z 3).
-Notation Y := (PEX Z 2).
-Notation Z_ := (PEX Z 1).
-*)
-Lemma example3 : forall x y z,
- x+y+z=0 ->
- x*y+x*z+y*z=0->
- x*y*z=0 -> x^3=0.
-Proof.
-Time nsatz_domainR.
-simpl.
-discrR.
-Qed.
-
-(*
-Notation X := (PEX Z 4).
-Notation Y := (PEX Z 3).
-Notation Z_ := (PEX Z 2).
-Notation U := (PEX Z 1).
-*)
-Lemma example4 : forall x y z u,
- x+y+z+u=0 ->
- x*y+x*z+x*u+y*z+y*u+z*u=0->
- x*y*z+x*y*u+x*z*u+y*z*u=0->
- x*y*z*u=0 -> x^4=0.
-Proof.
-Time nsatz_domainR.
-Qed.
-
-(*
-Notation x_ := (PEX Z 5).
-Notation y_ := (PEX Z 4).
-Notation z_ := (PEX Z 3).
-Notation u_ := (PEX Z 2).
-Notation v_ := (PEX Z 1).
-Notation "x :: y" := (List.cons x y)
-(at level 60, right associativity, format "'[hv' x :: '/' y ']'").
-Notation "x :: y" := (List.app x y)
-(at level 60, right associativity, format "x :: y").
-*)
-
-Lemma example5 : forall x y z u v,
- x+y+z+u+v=0 ->
- x*y+x*z+x*u+x*v+y*z+y*u+y*v+z*u+z*v+u*v=0->
- x*y*z+x*y*u+x*y*v+x*z*u+x*z*v+x*u*v+y*z*u+y*z*v+y*u*v+z*u*v=0->
- x*y*z*u+y*z*u*v+z*u*v*x+u*v*x*y+v*x*y*z=0 ->
- x*y*z*u*v=0 -> x^5=0.
-Proof.
-Time nsatz_domainR.
-Qed.
-
-End Examples.
-
-Section Geometry.
-
-Open Scope R_scope.
-
-Record point:Type:={
- X:R;
- Y:R}.
-
-Definition collinear(A B C:point):=
- (X A - X B)*(Y C - Y B)-(Y A - Y B)*(X C - X B)=0.
-
-Definition parallel (A B C D:point):=
- ((X A)-(X B))*((Y C)-(Y D))=((Y A)-(Y B))*((X C)-(X D)).
-
-Definition notparallel (A B C D:point)(x:R):=
- x*(((X A)-(X B))*((Y C)-(Y D))-((Y A)-(Y B))*((X C)-(X D)))=1.
-
-Definition orthogonal (A B C D:point):=
- ((X A)-(X B))*((X C)-(X D))+((Y A)-(Y B))*((Y C)-(Y D))=0.
-
-Definition equal2(A B:point):=
- (X A)=(X B) /\ (Y A)=(Y B).
-
-Definition equal3(A B:point):=
- ((X A)-(X B))^2+((Y A)-(Y B))^2 = 0.
-
-Definition nequal2(A B:point):=
- (X A)<>(X B) \/ (Y A)<>(Y B).
-
-Definition nequal3(A B:point):=
- not (((X A)-(X B))^2+((Y A)-(Y B))^2 = 0).
-
-Definition middle(A B I:point):=
- 2*(X I)=(X A)+(X B) /\ 2*(Y I)=(Y A)+(Y B).
-
-Definition distance2(A B:point):=
- (X B - X A)^2 + (Y B - Y A)^2.
-
-(* AB = CD *)
-Definition samedistance2(A B C D:point):=
- (X B - X A)^2 + (Y B - Y A)^2 = (X D - X C)^2 + (Y D - Y C)^2.
-Definition determinant(A O B:point):=
- (X A - X O)*(Y B - Y O) - (Y A - Y O)*(X B - X O).
-Definition scalarproduct(A O B:point):=
- (X A - X O)*(X B - X O) + (Y A - Y O)*(Y B - Y O).
-Definition norm2(A O B:point):=
- ((X A - X O)^2+(Y A - Y O)^2)*((X B - X O)^2+(Y B - Y O)^2).
-
-
-Lemma a1:forall A B C:Prop, ((A\/B)/\(A\/C)) -> (A\/(B/\C)).
-intuition.
-Qed.
-
-Lemma a2:forall A B C:Prop, ((A\/C)/\(B\/C)) -> ((A/\B)\/C).
-intuition.
-Qed.
-
-Lemma a3:forall a b c d:R, (a-b)*(c-d)=0 -> (a=b \/ c=d).
-intros.
-assert ( (a-b = 0) \/ (c-d = 0)).
-apply Rmult_integral.
-trivial.
-destruct H0.
-left; nsatz_domainR.
-right; nsatz_domainR.
-Qed.
-
-Ltac geo_unfold :=
- unfold collinear; unfold parallel; unfold notparallel; unfold orthogonal;
- unfold equal2; unfold equal3; unfold nequal2; unfold nequal3;
- unfold middle; unfold samedistance2;
- unfold determinant; unfold scalarproduct; unfold norm2; unfold distance2.
-
-Ltac geo_end :=
- repeat (
- repeat (match goal with h:_/\_ |- _ => decompose [and] h; clear h end);
- repeat (apply a1 || apply a2 || apply a3);
- repeat split).
-
-Ltac geo_rewrite_hyps:=
- repeat (match goal with
- | h:X _ = _ |- _ => rewrite h in *; clear h
- | h:Y _ = _ |- _ => rewrite h in *; clear h
- end).
-
-Ltac geo_begin:=
- geo_unfold;
- intros;
- geo_rewrite_hyps;
- geo_end.
-
-(* Examples *)
-
-Lemma Thales: forall O A B C D:point,
- collinear O A C -> collinear O B D ->
- parallel A B C D ->
- (distance2 O B * distance2 O C = distance2 O D * distance2 O A
- /\ distance2 O B * distance2 C D = distance2 O D * distance2 A B)
- \/ collinear O A B.
-repeat geo_begin.
-
-Time nsatz_domainR.
-simpl;discrR.
-Time nsatz_domainR.
-simpl;discrR.
-Qed.
-
-Require Import NsatzR.
-
-Lemma hauteurs:forall A B C A1 B1 C1 H:point,
- collinear B C A1 -> orthogonal A A1 B C ->
- collinear A C B1 -> orthogonal B B1 A C ->
- collinear A B C1 -> orthogonal C C1 A B ->
- collinear A A1 H -> collinear B B1 H ->
-
- collinear C C1 H
- \/ collinear A B C.
-
-geo_begin.
-(* Time nsatzRpv 2%N 1%Z (@nil R) (@nil R).*)
-(*Finished transaction in 3. secs (2.363641u,0.s)*)
-(*Time nsatz_domainR. trop long! *)
-(* en fait nsatz_domain ne tient pas encore compte de la liste des variables! ;-) *)
-Time
- let lv := constr:(Y A1
- :: X A1
- :: Y B1
- :: X B1
- :: Y A0
- :: Y B
- :: X B
- :: X A0
- :: X H
- :: Y C
- :: Y C1 :: Y H :: X C1 :: X C ::nil) in
- nsatz_domainpv 2%N 1%Z (@List.nil R) lv ltac:simplR Rdi.
-(* Finished transaction in 6. secs (5.579152u,0.001s) *)
-Qed.
-
-End Geometry.
diff --git a/test-suite/success/Tauto.v b/test-suite/success/Tauto.v
index b9326c64..6322ed2b 100644
--- a/test-suite/success/Tauto.v
+++ b/test-suite/success/Tauto.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
+(* $Id: Tauto.v 13323 2010-07-24 15:57:30Z herbelin $ *)
(**** Tactics Tauto and Intuition ****)
diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v
index 55351a47..30a2a742 100644
--- a/test-suite/success/Typeclasses.v
+++ b/test-suite/success/Typeclasses.v
@@ -8,9 +8,9 @@ Reserved Notation "x >>= y" (at level 65, left associativity).
Record Monad {m : Type -> Type} := {
- unit : Π {α}, α -> m α where "'return' t" := (unit t) ;
- bind : Π {α β}, m α -> (α -> m β) -> m β where "x >>= y" := (bind x y) ;
- bind_unit_left : Π {α β} (a : α) (f : α -> m β), return a >>= f = f a }.
+ unit : forall {α}, α -> m α where "'return' t" := (unit t) ;
+ bind : forall {α β}, m α -> (α -> m β) -> m β where "x >>= y" := (bind x y) ;
+ bind_unit_left : forall {α β} (a : α) (f : α -> m β), return a >>= f = f a }.
Print Visibility.
Print unit.