diff options
| author | herbelin | 2002-12-06 14:23:12 +0000 |
|---|---|---|
| committer | herbelin | 2002-12-06 14:23:12 +0000 |
| commit | 07f73dacfb68f36a366141d9545524d7afce4e9a (patch) | |
| tree | ae22ddc2b8ed8312e0764bcdd7fbd30be7448dcb | |
| parent | 3430da144df39077064e28e0fa15204db76ad9b9 (diff) | |
Un axiome en attendant la mise a jour de la preuve de times_convert
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3386 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | theories/ZArith/fast_integer.v | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/theories/ZArith/fast_integer.v b/theories/ZArith/fast_integer.v index 8069d686b3..8f0b381ad0 100644 --- a/theories/ZArith/fast_integer.v +++ b/theories/ZArith/fast_integer.v @@ -1011,6 +1011,7 @@ Intros; Elim H; Elim H0; Auto with arith. Qed. (** Addition on positive numbers *) + Fixpoint times [x:positive] : positive -> positive:= [y:positive] Cases x of @@ -1022,11 +1023,13 @@ 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; Rewrite ZL6; Rewrite convert_add; + 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 @@ -1035,6 +1038,9 @@ NewInduction x as [ x' H | x' H | ]; [ 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)). (** Multiplication on integers *) Definition Zmult := [x,y:Z] |