nstaz pour les anneaux integres et les setoides, R Z et Q

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13336 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 59 insertions, 47 deletions

diff --git a/test-suite/success/Nsatz_domain.v b/test-suite/success/Nsatz_domain.v
index a5a6a223c..dd190e3b8 100644
--- a/test-suite/success/Nsatz_domain.v
+++ b/test-suite/success/Nsatz_domain.v
@@ -1,23 +1,20 @@
 Require Import Nsatz_domain ZArith Reals List Ring_polynom.
 
+(* Example with a generic domain *)
+
 Variable A: Type.
 Variable Ad: Domain A.
 
-Add Ring Ar1: (@ring_ring A (@domain_ring _ Ad)).
+Definition Ari : Ring A:= (@domain_ring A Ad).
+Existing Instance Ari.
 
-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)}.
+Existing Instance ring_setoid.
+Existing Instance ring_plus_comp.
+Existing Instance ring_mult_comp.
+Existing Instance ring_sub_comp.
+Existing Instance ring_opp_comp.
 
-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}.
+Add Ring Ar: (@ring_ring A (@domain_ring A Ad)).
 
 Instance zero_ring2 : Zero A := {zero := ring0}.
 Instance one_ring2 : One A := {one := ring1}.
@@ -26,32 +23,51 @@ Instance multiplication_ring2 : Multiplication A := {multiplication x y := ring_
 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.
+Infix "==" := ring_eq (at level 70, no associativity).
+
+Ltac nsatzA := simpl; unfold Ari; nsatz_domain.
 
-Goal forall a b c:A, a = b -> b = c -> c = a.
-nsatz_domain.
+Goal forall x y:A,  x == y -> x+0 == y*1+0.
+nsatzA.
 Qed.
 
-Goal forall a b c:A, a = b -> b = c -> a = c.
-nsatz_domain.
+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.
 
-Goal forall a b c x:A, a = b -> b = c -> a*a = c*c.
-nsatz_domain.
+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_domainZ.
+nsatz.
 Qed.
 
 Goal forall x y:R,  x = y -> (x+0)%R = (y*1+0)%R.
-nsatz_domainR.
+nsatz.
 Qed.
 
 Goal forall a b c x:R, a = b -> b = c -> (a*a)%R = (c*c)%R.
-nsatz_domainR.
+nsatz.
 Qed.
 
 Section Examples.
@@ -70,12 +86,12 @@ Lemma example1 : forall x y,
   x*y=0 ->
   x^2=0.
 Proof.
- nsatz_domainR.
+ nsatz.
 Qed.
 
 Lemma example2 : forall x, x^2=0 -> x=0.
 Proof.
- nsatz_domainR.
+ nsatz.
 Qed.
 
 (*
@@ -83,14 +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 nsatz_domainR.
-simpl.
-discrR.
+Time nsatz. 
 Qed.
 
 (*
@@ -99,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 nsatz_domainR.
+Time nsatz.
 Qed.
 
 (*
@@ -120,14 +134,14 @@ 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 nsatz_domainR.
+Time nsatz.
 Qed.
 
 End Examples.
@@ -195,8 +209,8 @@ assert ( (a-b = 0) \/ (c-d = 0)).
 apply Rmult_integral.
 trivial.
 destruct H0.
-left; nsatz_domainR.
-right; nsatz_domainR.
+left; nsatz.
+right; nsatz.
 Qed.
 
 Ltac geo_unfold :=
@@ -225,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 ->
@@ -232,15 +247,10 @@ 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_domainR.
-simpl;discrR.
-Time nsatz_domainR.
-simpl;discrR.
+Time nsatz.
+Time nsatz.
 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 -> 
@@ -251,10 +261,10 @@ Lemma hauteurs:forall A B C A1 B1 C1 H:point,
   \/ 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
@@ -266,9 +276,11 @@ Time
                    :: 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.
+                            :: 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.
+