diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
commit | a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (patch) | |
tree | 26dd9c4aa142597ee09c887ef161d5f0fa5077b6 /theories/Numbers/Natural | |
parent | 164c6861860e6b52818c031f901ffeff91fca16a (diff) |
Imported Upstream version 8.6upstream/8.6
Diffstat (limited to 'theories/Numbers/Natural')
-rw-r--r-- | theories/Numbers/Natural/BigN/BigN.v | 26 | ||||
-rw-r--r-- | theories/Numbers/Natural/BigN/NMake.v | 2 | ||||
-rw-r--r-- | theories/Numbers/Natural/BigN/NMake_gen.ml | 2 | ||||
-rw-r--r-- | theories/Numbers/Natural/Peano/NPeano.v | 84 |
4 files changed, 97 insertions, 17 deletions
diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v index 29a1145e..e8ff516f 100644 --- a/theories/Numbers/Natural/BigN/BigN.v +++ b/theories/Numbers/Natural/BigN/BigN.v @@ -110,7 +110,7 @@ intros NEQ. generalize (BigN.spec_div_eucl a b). generalize (Z_div_mod_full [a] [b] NEQ). destruct BigN.div_eucl as (q,r), Z.div_eucl as (q',r'). -intros (EQ,_). injection 1. intros EQr EQq. +intros (EQ,_). injection 1 as EQr EQq. BigN.zify. rewrite EQr, EQq; auto. Qed. @@ -119,10 +119,10 @@ Qed. Ltac isStaticWordCst t := match t with - | W0 => constr:true + | W0 => constr:(true) | WW ?t1 ?t2 => match isStaticWordCst t1 with - | false => constr:false + | false => constr:(false) | true => isStaticWordCst t2 end | _ => isInt31cst t @@ -139,30 +139,30 @@ Ltac isBigNcst t := | BigN.N6 ?t => isStaticWordCst t | BigN.Nn ?n ?t => match isnatcst n with | true => isStaticWordCst t - | false => constr:false + | false => constr:(false) end - | BigN.zero => constr:true - | BigN.one => constr:true - | BigN.two => constr:true - | _ => constr:false + | BigN.zero => constr:(true) + | BigN.one => constr:(true) + | BigN.two => constr:(true) + | _ => constr:(false) end. Ltac BigNcst t := match isBigNcst t with - | true => constr:t - | false => constr:NotConstant + | true => constr:(t) + | false => constr:(NotConstant) end. Ltac BigN_to_N t := match isBigNcst t with | true => eval vm_compute in (BigN.to_N t) - | false => constr:NotConstant + | false => constr:(NotConstant) end. Ltac Ncst t := match isNcst t with - | true => constr:t - | false => constr:NotConstant + | true => constr:(t) + | false => constr:(NotConstant) end. (** Registration for the "ring" tactic *) diff --git a/theories/Numbers/Natural/BigN/NMake.v b/theories/Numbers/Natural/BigN/NMake.v index 98949736..1425041a 100644 --- a/theories/Numbers/Natural/BigN/NMake.v +++ b/theories/Numbers/Natural/BigN/NMake.v @@ -338,7 +338,7 @@ Module Make (W0:CyclicType) <: NType. Proof. apply eq_iff_eq_true. rewrite Z.leb_le. unfold Z.le, leb. rewrite spec_compare. - destruct Z.compare; split; try easy. now destruct 1. + now destruct Z.compare; split. Qed. Definition min (n m : t) : t := match compare n m with Gt => m | _ => n end. diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml index 601fa108..5177fae6 100644 --- a/theories/Numbers/Natural/BigN/NMake_gen.ml +++ b/theories/Numbers/Natural/BigN/NMake_gen.ml @@ -147,7 +147,7 @@ pr pr " Local Notation Size := (SizePlus O)."; pr ""; - pr " Tactic Notation \"do_size\" tactic(t) := do %i t." (size+1); + pr " Tactic Notation (at level 3) \"do_size\" tactic3(t) := do %i t." (size+1); pr ""; pr " Definition dom_t n := match n with"; diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v index 58b1b018..d0168bd9 100644 --- a/theories/Numbers/Natural/Peano/NPeano.v +++ b/theories/Numbers/Natural/Peano/NPeano.v @@ -8,8 +8,88 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -Require Import PeanoNat NAxioms. +Require Import PeanoNat Even NAxioms. -(** * [PeanoNat.Nat] already implements [NAxiomSig] *) +(** This file is DEPRECATED ! Use [PeanoNat] (or [Arith]) instead. *) + +(** [PeanoNat.Nat] already implements [NAxiomSig] *) Module Nat <: NAxiomsSig := Nat. + +(** Compat notations for stuff that used to be at the beginning of NPeano. *) + +Notation leb := Nat.leb (compat "8.4"). +Notation ltb := Nat.ltb (compat "8.4"). +Notation leb_le := Nat.leb_le (compat "8.4"). +Notation ltb_lt := Nat.ltb_lt (compat "8.4"). +Notation pow := Nat.pow (compat "8.4"). +Notation pow_0_r := Nat.pow_0_r (compat "8.4"). +Notation pow_succ_r := Nat.pow_succ_r (compat "8.4"). +Notation square := Nat.square (compat "8.4"). +Notation square_spec := Nat.square_spec (compat "8.4"). +Notation Even := Nat.Even (compat "8.4"). +Notation Odd := Nat.Odd (compat "8.4"). +Notation even := Nat.even (compat "8.4"). +Notation odd := Nat.odd (compat "8.4"). +Notation even_spec := Nat.even_spec (compat "8.4"). +Notation odd_spec := Nat.odd_spec (compat "8.4"). + +Lemma Even_equiv n : Even n <-> Even.even n. +Proof. symmetry. apply Even.even_equiv. Qed. +Lemma Odd_equiv n : Odd n <-> Even.odd n. +Proof. symmetry. apply Even.odd_equiv. Qed. + +Notation divmod := Nat.divmod (compat "8.4"). +Notation div := Nat.div (compat "8.4"). +Notation modulo := Nat.modulo (compat "8.4"). +Notation divmod_spec := Nat.divmod_spec (compat "8.4"). +Notation div_mod := Nat.div_mod (compat "8.4"). +Notation mod_bound_pos := Nat.mod_bound_pos (compat "8.4"). +Notation sqrt_iter := Nat.sqrt_iter (compat "8.4"). +Notation sqrt := Nat.sqrt (compat "8.4"). +Notation sqrt_iter_spec := Nat.sqrt_iter_spec (compat "8.4"). +Notation sqrt_spec := Nat.sqrt_spec (compat "8.4"). +Notation log2_iter := Nat.log2_iter (compat "8.4"). +Notation log2 := Nat.log2 (compat "8.4"). +Notation log2_iter_spec := Nat.log2_iter_spec (compat "8.4"). +Notation log2_spec := Nat.log2_spec (compat "8.4"). +Notation log2_nonpos := Nat.log2_nonpos (compat "8.4"). +Notation gcd := Nat.gcd (compat "8.4"). +Notation divide := Nat.divide (compat "8.4"). +Notation gcd_divide := Nat.gcd_divide (compat "8.4"). +Notation gcd_divide_l := Nat.gcd_divide_l (compat "8.4"). +Notation gcd_divide_r := Nat.gcd_divide_r (compat "8.4"). +Notation gcd_greatest := Nat.gcd_greatest (compat "8.4"). +Notation testbit := Nat.testbit (compat "8.4"). +Notation shiftl := Nat.shiftl (compat "8.4"). +Notation shiftr := Nat.shiftr (compat "8.4"). +Notation bitwise := Nat.bitwise (compat "8.4"). +Notation land := Nat.land (compat "8.4"). +Notation lor := Nat.lor (compat "8.4"). +Notation ldiff := Nat.ldiff (compat "8.4"). +Notation lxor := Nat.lxor (compat "8.4"). +Notation double_twice := Nat.double_twice (compat "8.4"). +Notation testbit_0_l := Nat.testbit_0_l (compat "8.4"). +Notation testbit_odd_0 := Nat.testbit_odd_0 (compat "8.4"). +Notation testbit_even_0 := Nat.testbit_even_0 (compat "8.4"). +Notation testbit_odd_succ := Nat.testbit_odd_succ (compat "8.4"). +Notation testbit_even_succ := Nat.testbit_even_succ (compat "8.4"). +Notation shiftr_spec := Nat.shiftr_spec (compat "8.4"). +Notation shiftl_spec_high := Nat.shiftl_spec_high (compat "8.4"). +Notation shiftl_spec_low := Nat.shiftl_spec_low (compat "8.4"). +Notation div2_bitwise := Nat.div2_bitwise (compat "8.4"). +Notation odd_bitwise := Nat.odd_bitwise (compat "8.4"). +Notation div2_decr := Nat.div2_decr (compat "8.4"). +Notation testbit_bitwise_1 := Nat.testbit_bitwise_1 (compat "8.4"). +Notation testbit_bitwise_2 := Nat.testbit_bitwise_2 (compat "8.4"). +Notation land_spec := Nat.land_spec (compat "8.4"). +Notation ldiff_spec := Nat.ldiff_spec (compat "8.4"). +Notation lor_spec := Nat.lor_spec (compat "8.4"). +Notation lxor_spec := Nat.lxor_spec (compat "8.4"). + +Infix "<=?" := Nat.leb (at level 70) : nat_scope. +Infix "<?" := Nat.ltb (at level 70) : nat_scope. +Infix "^" := Nat.pow : nat_scope. +Infix "/" := Nat.div : nat_scope. +Infix "mod" := Nat.modulo (at level 40, no associativity) : nat_scope. +Notation "( x | y )" := (Nat.divide x y) (at level 0) : nat_scope. |