Nouvelle preuve de times_convert pour nouvelle définition de times

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

1 files changed, 24 insertions, 27 deletions

diff --git a/theories/ZArith/fast_integer.v b/theories/ZArith/fast_integer.v
index 59ea036255..210e0846ba 100644
--- a/theories/ZArith/fast_integer.v
+++ b/theories/ZArith/fast_integer.v
@@ -1023,27 +1023,29 @@ Fixpoint times [x:positive] : positive -> positive:=
 Infix "*" times (at level 3, left associativity) : positive_scope.
 
 (** Correctness of multiplication on positive *)
-(*
 Theorem times_convert :
   (x,y:positive) (convert x*y) = (mult (convert x) (convert y)).
 Proof.
-NewInduction x as [ x' H | x' H | ]; [
-  Intro y; Simpl (mult (convert (xI x')) (convert y));
-  Rewrite ZL6; Rewrite convert_add; 
-  Rewrite H; Unfold 3 convert; Simpl; Rewrite ZL6;
-  Rewrite (mult_sym (convert x')); Do 2 Rewrite mult_plus_distr;
-  Rewrite (mult_sym (convert x')); Trivial with arith
-| Intro y; Simpl; Rewrite H; Unfold 2 3 convert; Simpl;
-  Do 2 Rewrite ZL6; Rewrite (mult_sym (convert x')); 
-  Do 2 Rewrite mult_plus_distr; Rewrite (mult_sym (convert x')); Auto with arith
-| Simpl; Intros;Rewrite <- plus_n_O; Trivial with arith ].
-Qed.
-*)
-Axiom times_convert :
-  (x,y:positive) (convert x*y) = (mult (convert x) (convert y)).
+Intros x y; NewInduction x as [ x' H | x' H | ]; [
+  Change (xI x')*y with (add y (xO x'*y)); Rewrite convert_add;
+  Unfold 2 3 convert; Simpl; Do 2 Rewrite ZL6; Rewrite H;
+  Rewrite -> mult_plus_distr; Reflexivity
+| Unfold 1 2 convert; Simpl; Do 2 Rewrite ZL6;
+  Rewrite H; Rewrite mult_plus_distr; Reflexivity
+| Simpl; Rewrite <- plus_n_O; Reflexivity ].
+Qed.
 
-Syntactic Definition times1 := times.
-Syntactic Definition times1_convert := times_convert.
+Theorem times_assoc :
+  ((x,y,z:positive) (times x (times y z))= (times (times x y) z)).
+Proof.
+Intros x y z;Apply convert_intro; Do 4 Rewrite times_convert;
+Apply mult_assoc_l.
+Qed.
+
+Theorem times_sym : (x,y:positive) (times x y) = (times y x).
+Proof.
+Intros x y; Apply convert_intro; Do 2 Rewrite times_convert; Apply mult_sym.
+Qed.
 
 (** Multiplication on integers *)
 Definition Zmult := [x,y:Z]
@@ -1063,17 +1065,9 @@ Definition Zmult := [x,y:Z]
              end
     end.
 
-Theorem times_assoc :
-  ((x,y,z:positive) (times x (times y z))= (times (times x y) z)).
-Proof.
-Intros x y z;Apply convert_intro; Do 4 Rewrite times_convert;
-Apply mult_assoc_l.
-Qed.
+Infix "*" Zmult (at level 3, left associativity) : Z_scope.
 
-Theorem times_sym : (x,y:positive) (times x y) = (times y x).
-Proof.
-Intros x y; Apply convert_intro; Do 2 Rewrite times_convert; Apply mult_sym.
-Qed.
+Open Scope Z_scope.
 
 Theorem Zmult_sym : (x,y:Z) (Zmult x y) = (Zmult y x).
 Proof.
@@ -1486,3 +1480,6 @@ Intros x y;Case x;Case y; [
   Simpl; Rewrite (ZC1 q p H); Trivial with arith].
 Qed.
 End fast_integers.
+
+Syntactic Definition times1 := times.
+Syntactic Definition times1_convert := times_convert.