diff options
Diffstat (limited to 'theories7/ZArith/fast_integer.v')
| -rw-r--r-- | theories7/ZArith/fast_integer.v | 191 |
1 files changed, 191 insertions, 0 deletions
diff --git a/theories7/ZArith/fast_integer.v b/theories7/ZArith/fast_integer.v new file mode 100644 index 00000000..7e3fe306 --- /dev/null +++ b/theories7/ZArith/fast_integer.v @@ -0,0 +1,191 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: fast_integer.v,v 1.1.2.1 2004/07/16 19:31:44 herbelin Exp $ i*) + +(***********************************************************) +(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *) +(***********************************************************) + +Require BinPos. +Require BinNat. +Require BinInt. +Require Zcompare. +Require Mult. + +V7only [ +(* Defs and ppties on positive, entier and Z, previously in fast_integer *) +(* For v7 compatibility *) +Notation positive := positive. +Notation xO := xO. +Notation xI := xI. +Notation xH := xH. +Notation add_un := add_un. +Notation add := add. +Notation convert := convert. +Notation convert_add_un := convert_add_un. +Notation cvt_carry := cvt_carry. +Notation convert_add := convert_add. +Notation positive_to_nat := positive_to_nat. +Notation anti_convert := anti_convert. +Notation double_moins_un := double_moins_un. +Notation sub_un := sub_un. +Notation positive_mask := positive_mask. +Notation Un_suivi_de_mask := Un_suivi_de_mask. +Notation Zero_suivi_de_mask := Zero_suivi_de_mask. +Notation double_moins_deux := double_moins_deux. +Notation sub_pos := sub_pos. +Notation true_sub := true_sub. +Notation times := times. +Notation relation := relation. +Notation SUPERIEUR := SUPERIEUR. +Notation INFERIEUR := INFERIEUR. +Notation EGAL := EGAL. +Notation Op := Op. +Notation compare := compare. +Notation compare_convert1 := compare_convert1. +Notation compare_convert_EGAL := compare_convert_EGAL. +Notation ZLSI := ZLSI. +Notation ZLIS := ZLIS. +Notation ZLII := ZLII. +Notation ZLSS := ZLSS. +Notation Dcompare := Dcompare. +Notation convert_compare_EGAL := convert_compare_EGAL. +Notation ZL0 := ZL0. +Notation ZL11 := ZL11. +Notation xI_add_un_xO := xI_add_un_xO. +Notation is_double_moins_un := is_double_moins_un. +Notation double_moins_un_add_un_xI := double_moins_un_add_un_xI. +Notation ZL1 := ZL1. +Notation add_un_not_un := add_un_not_un. +Notation sub_add_one := sub_add_one. +Notation add_sub_one := add_sub_one. +Notation add_un_inj := add_un_inj. +Notation ZL12 := ZL12. +Notation ZL12bis := ZL12bis. +Notation ZL13 := ZL13. +Notation add_sym := add_sym. +Notation ZL14 := ZL14. +Notation ZL14bis := ZL14bis. +Notation ZL15 := ZL15. +Notation add_no_neutral := add_no_neutral. +Notation add_carry_not_add_un := add_carry_not_add_un. +Notation add_carry_add := add_carry_add. +Notation simpl_add_r := simpl_add_r. +Notation simpl_add_carry_r := simpl_add_carry_r. +Notation simpl_add_l := simpl_add_l. +Notation simpl_add_carry_l := simpl_add_carry_l. +Notation add_assoc := add_assoc. +Notation add_xI_double_moins_un := add_xI_double_moins_un. +Notation add_x_x := add_x_x. +Notation ZS := ZS. +Notation US := US. +Notation USH := USH. +Notation ZSH := ZSH. +Notation sub_pos_x_x := sub_pos_x_x. +Notation ZL10 := ZL10. +Notation sub_pos_SUPERIEUR := sub_pos_SUPERIEUR. +Notation sub_add := sub_add. +Notation convert_add_carry := convert_add_carry. +Notation add_verif := add_verif. +Notation ZL2 := ZL2. +Notation ZL6 := ZL6. +Notation positive_to_nat_mult := positive_to_nat_mult. +Notation times_convert := times_convert. +Notation compare_positive_to_nat_O := compare_positive_to_nat_O. +Notation compare_convert_O := compare_convert_O. +Notation convert_xH := convert_xH. +Notation convert_xO := convert_xO. +Notation convert_xI := convert_xI. +Notation bij1 := bij1. +Notation ZL3 := ZL3. +Notation ZL4 := ZL4. +Notation ZL5 := ZL5. +Notation bij2 := bij2. +Notation bij3 := bij3. +Notation ZL7 := ZL7. +Notation ZL8 := ZL8. +Notation compare_convert_INFERIEUR := compare_convert_INFERIEUR. +Notation compare_convert_SUPERIEUR := compare_convert_SUPERIEUR. +Notation convert_compare_INFERIEUR := convert_compare_INFERIEUR. +Notation convert_compare_SUPERIEUR := convert_compare_SUPERIEUR. +Notation ZC1 := ZC1. +Notation ZC2 := ZC2. +Notation ZC3 := ZC3. +Notation ZC4 := ZC4. +Notation true_sub_convert := true_sub_convert. +Notation convert_intro := convert_intro. +Notation ZL16 := ZL16. +Notation ZL17 := ZL17. +Notation compare_true_sub_right := compare_true_sub_right. +Notation compare_true_sub_left := compare_true_sub_left. +Notation times_x_ := times_x_1. +Notation times_x_double := times_x_double. +Notation times_x_double_plus_one := times_x_double_plus_one. +Notation times_sym := times_sym. +Notation times_add_distr := times_add_distr. +Notation times_add_distr_l := times_add_distr_l. +Notation times_assoc := times_assoc. +Notation times_true_sub_distr := times_true_sub_distr. +Notation times_discr_xO_xI := times_discr_xO_xI. +Notation times_discr_xO := times_discr_xO. +Notation simpl_times_r := simpl_times_r. +Notation simpl_times_l := simpl_times_l. +Notation iterate_add := iterate_add. +Notation entier := entier. +Notation Nul := Nul. +Notation Pos := Pos. +Notation Un_suivi_de := Un_suivi_de. +Notation Zero_suivi_de := Zero_suivi_de. +Notation times1 := + [x:positive;_:positive->positive;y:positive](times x y). +Notation times1_convert := + [x,y:positive;_:positive->positive](times_convert x y). + +Notation Z := Z. +Notation POS := POS. +Notation NEG := NEG. +Notation ZERO := ZERO. +Notation Zero_left := Zero_left. +Notation Zopp_Zopp := Zopp_Zopp. +Notation Zero_right := Zero_right. +Notation Zplus_inverse_r := Zplus_inverse_r. +Notation Zopp_Zplus := Zopp_Zplus. +Notation Zplus_sym := Zplus_sym. +Notation Zplus_inverse_l := Zplus_inverse_l. +Notation Zopp_intro := Zopp_intro. +Notation Zopp_NEG := Zopp_NEG. +Notation weak_assoc := weak_assoc. +Notation Zplus_assoc := Zplus_assoc. +Notation Zplus_simpl := Zplus_simpl. +Notation Zmult_sym := Zmult_sym. +Notation Zmult_assoc := Zmult_assoc. +Notation Zmult_one := Zmult_one. +Notation lt_mult_left := lt_mult_left. (* Mult*) +Notation Zero_mult_left := Zero_mult_left. +Notation Zero_mult_right := Zero_mult_right. +Notation Zopp_Zmult := Zopp_Zmult. +Notation Zmult_Zopp_Zopp := Zmult_Zopp_Zopp. +Notation weak_Zmult_plus_distr_r := weak_Zmult_plus_distr_r. +Notation Zmult_plus_distr_r := Zmult_plus_distr_r. +Notation Zcompare_EGAL := Zcompare_EGAL. +Notation Zcompare_ANTISYM := Zcompare_ANTISYM. +Notation le_minus := le_minus. +Notation Zcompare_Zopp := Zcompare_Zopp. +Notation weaken_Zcompare_Zplus_compatible := weaken_Zcompare_Zplus_compatible. +Notation weak_Zcompare_Zplus_compatible := weak_Zcompare_Zplus_compatible. +Notation Zcompare_Zplus_compatible := Zcompare_Zplus_compatible. +Notation Zcompare_trans_SUPERIEUR := Zcompare_trans_SUPERIEUR. +Notation SUPERIEUR_POS := SUPERIEUR_POS. +Export Datatypes. +Export BinPos. +Export BinNat. +Export BinInt. +Export Zcompare. +Export Mult. +]. |