diff options
Diffstat (limited to 'theories/Numbers')
| -rw-r--r-- | theories/Numbers/AltBinNotations.v | 10 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/Abstract/CyclicAxioms.v | 8 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/Abstract/DoubleType.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/Int31/Int31.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/Int63/Cyclic63.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/Int63/Int63.v | 199 | ||||
| -rw-r--r-- | theories/Numbers/NatInt/NZAdd.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/NatInt/NZBase.v | 4 | ||||
| -rw-r--r-- | theories/Numbers/NatInt/NZDiv.v | 50 | ||||
| -rw-r--r-- | theories/Numbers/NatInt/NZGcd.v | 10 | ||||
| -rw-r--r-- | theories/Numbers/NatInt/NZLog.v | 8 | ||||
| -rw-r--r-- | theories/Numbers/NatInt/NZMul.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/NatInt/NZMulOrder.v | 8 | ||||
| -rw-r--r-- | theories/Numbers/NatInt/NZOrder.v | 18 | ||||
| -rw-r--r-- | theories/Numbers/NatInt/NZParity.v | 14 | ||||
| -rw-r--r-- | theories/Numbers/NatInt/NZPow.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/NatInt/NZSqrt.v | 6 |
17 files changed, 187 insertions, 160 deletions
diff --git a/theories/Numbers/AltBinNotations.v b/theories/Numbers/AltBinNotations.v index 5585f478b3..7c846571a7 100644 --- a/theories/Numbers/AltBinNotations.v +++ b/theories/Numbers/AltBinNotations.v @@ -8,12 +8,12 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -(** * Alternative Binary Numeral Notations *) +(** * Alternative Binary Number Notations *) (** Faster but less safe parsers and printers of [positive], [N], [Z]. *) (** By default, literals in types [positive], [N], [Z] are parsed and - printed via the [Numeral Notation] command, by conversion from/to + printed via the [Number Notation] command, by conversion from/to the [Decimal.int] representation. When working with numbers with thousands of digits and more, conversion from/to [Decimal.int] can become significantly slow. If that becomes a problem for your @@ -43,7 +43,7 @@ Definition pos_of_z z := Definition pos_to_z p := Zpos p. -Numeral Notation positive pos_of_z pos_to_z : positive_scope. +Number Notation positive pos_of_z pos_to_z : positive_scope. (** [N] *) @@ -60,10 +60,10 @@ Definition n_to_z n := | Npos p => Zpos p end. -Numeral Notation N n_of_z n_to_z : N_scope. +Number Notation N n_of_z n_to_z : N_scope. (** [Z] *) Definition z_of_z (z:Z) := z. -Numeral Notation Z z_of_z z_of_z : Z_scope. +Number Notation Z z_of_z z_of_z : Z_scope. diff --git a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v index 6470cd6c81..e3e8f532b3 100644 --- a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v +++ b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v @@ -99,7 +99,7 @@ Module ZnZ. lxor : t -> t -> t }. Section Specs. - Context {t : Type}{ops : Ops t}. + Context {t : Set}{ops : Ops t}. Notation "[| x |]" := (to_Z x) (at level 0, x at level 99). @@ -221,7 +221,7 @@ Module ZnZ. Section WW. - Context {t : Type}{ops : Ops t}{specs : Specs ops}. + Context {t : Set}{ops : Ops t}{specs : Specs ops}. Let wB := base digits. @@ -284,7 +284,7 @@ Module ZnZ. Section Of_Z. - Context {t : Type}{ops : Ops t}{specs : Specs ops}. + Context {t : Set}{ops : Ops t}{specs : Specs ops}. Notation "[| x |]" := (to_Z x) (at level 0, x at level 99). @@ -325,7 +325,7 @@ End ZnZ. (** A modular specification grouping the earlier records. *) Module Type CyclicType. - Parameter t : Type. + Parameter t : Set. Declare Instance ops : ZnZ.Ops t. Declare Instance specs : ZnZ.Specs ops. End CyclicType. diff --git a/theories/Numbers/Cyclic/Abstract/DoubleType.v b/theories/Numbers/Cyclic/Abstract/DoubleType.v index 3232e3afe0..165f9893ca 100644 --- a/theories/Numbers/Cyclic/Abstract/DoubleType.v +++ b/theories/Numbers/Cyclic/Abstract/DoubleType.v @@ -54,7 +54,7 @@ Arguments W0 {znz}. (if depth = n). *) -Fixpoint word (w:Type) (n:nat) : Type := +Fixpoint word (w:Set) (n:nat) : Set := match n with | O => w | S n => zn2z (word w n) diff --git a/theories/Numbers/Cyclic/Int31/Int31.v b/theories/Numbers/Cyclic/Int31/Int31.v index cd814091a1..d3528ce87c 100644 --- a/theories/Numbers/Cyclic/Int31/Int31.v +++ b/theories/Numbers/Cyclic/Int31/Int31.v @@ -477,4 +477,4 @@ Definition tail031 (i:int31) := end) i On. -Numeral Notation int31 phi_inv_nonneg phi : int31_scope. +Number Notation int31 phi_inv_nonneg phi : int31_scope. diff --git a/theories/Numbers/Cyclic/Int63/Cyclic63.v b/theories/Numbers/Cyclic/Int63/Cyclic63.v index 5f903c41cb..2a26b6b12a 100644 --- a/theories/Numbers/Cyclic/Int63/Cyclic63.v +++ b/theories/Numbers/Cyclic/Int63/Cyclic63.v @@ -48,7 +48,7 @@ Definition mulc_WW x y := Notation "n '*c' m" := (mulc_WW n m) (at level 40, no associativity) : int63_scope. Definition pos_mod p x := - if p <= digits then + if p <=? digits then let p := digits - p in (x << p) >> p else x. diff --git a/theories/Numbers/Cyclic/Int63/Int63.v b/theories/Numbers/Cyclic/Int63/Int63.v index 2c112c3469..383c0aff3a 100644 --- a/theories/Numbers/Cyclic/Int63/Int63.v +++ b/theories/Numbers/Cyclic/Int63/Int63.v @@ -31,56 +31,61 @@ Declare Scope int63_scope. Definition id_int : int -> int := fun x => x. Declare ML Module "int63_syntax_plugin". +Module Import Int63NotationsInternalA. Delimit Scope int63_scope with int63. Bind Scope int63_scope with int. +End Int63NotationsInternalA. (* Logical operations *) Primitive lsl := #int63_lsl. -Infix "<<" := lsl (at level 30, no associativity) : int63_scope. Primitive lsr := #int63_lsr. -Infix ">>" := lsr (at level 30, no associativity) : int63_scope. Primitive land := #int63_land. -Infix "land" := land (at level 40, left associativity) : int63_scope. Primitive lor := #int63_lor. -Infix "lor" := lor (at level 40, left associativity) : int63_scope. Primitive lxor := #int63_lxor. -Infix "lxor" := lxor (at level 40, left associativity) : int63_scope. (* Arithmetic modulo operations *) Primitive add := #int63_add. -Notation "n + m" := (add n m) : int63_scope. Primitive sub := #int63_sub. -Notation "n - m" := (sub n m) : int63_scope. Primitive mul := #int63_mul. -Notation "n * m" := (mul n m) : int63_scope. Primitive mulc := #int63_mulc. Primitive div := #int63_div. -Notation "n / m" := (div n m) : int63_scope. Primitive mod := #int63_mod. -Notation "n '\%' m" := (mod n m) (at level 40, left associativity) : int63_scope. (* Comparisons *) Primitive eqb := #int63_eq. -Notation "m '==' n" := (eqb m n) (at level 70, no associativity) : int63_scope. Primitive ltb := #int63_lt. -Notation "m < n" := (ltb m n) : int63_scope. Primitive leb := #int63_le. -Notation "m <= n" := (leb m n) : int63_scope. -Notation "m ≤ n" := (leb m n) (at level 70, no associativity) : int63_scope. Local Open Scope int63_scope. +Module Import Int63NotationsInternalB. +Infix "<<" := lsl (at level 30, no associativity) : int63_scope. +Infix ">>" := lsr (at level 30, no associativity) : int63_scope. +Infix "land" := land (at level 40, left associativity) : int63_scope. +Infix "lor" := lor (at level 40, left associativity) : int63_scope. +Infix "lxor" := lxor (at level 40, left associativity) : int63_scope. +Infix "+" := add : int63_scope. +Infix "-" := sub : int63_scope. +Infix "*" := mul : int63_scope. +Infix "/" := div : int63_scope. +Infix "mod" := mod (at level 40, no associativity) : int63_scope. +Infix "=?" := eqb (at level 70, no associativity) : int63_scope. +Infix "<?" := ltb (at level 70, no associativity) : int63_scope. +Infix "<=?" := leb (at level 70, no associativity) : int63_scope. +Infix "≤?" := leb (at level 70, no associativity) : int63_scope. +End Int63NotationsInternalB. + (** The number of digits as a int *) Definition digits := 63. @@ -89,16 +94,16 @@ Definition max_int := Eval vm_compute in 0 - 1. Register Inline max_int. (** Access to the nth digits *) -Definition get_digit x p := (0 < (x land (1 << p))). +Definition get_digit x p := (0 <? (x land (1 << p))). Definition set_digit x p (b:bool) := - if if 0 <= p then p < digits else false then + if if 0 <=? p then p <? digits else false then if b then x lor (1 << p) else x land (max_int lxor (1 << p)) else x. (** Equality to 0 *) -Definition is_zero (i:int) := i == 0. +Definition is_zero (i:int) := i =? 0. Register Inline is_zero. (** Parity *) @@ -113,7 +118,6 @@ Definition bit i n := negb (is_zero ((i >> n) << (digits - 1))). (** Extra modulo operations *) Definition opp (i:int) := 0 - i. Register Inline opp. -Notation "- x" := (opp x) : int63_scope. Definition oppcarry i := max_int - i. Register Inline oppcarry. @@ -134,29 +138,27 @@ Register Inline subcarry. Definition addc_def x y := let r := x + y in - if r < x then C1 r else C0 r. + if r <? x then C1 r else C0 r. (* the same but direct implementation for efficiency *) Primitive addc := #int63_addc. -Notation "n '+c' m" := (addc n m) (at level 50, no associativity) : int63_scope. Definition addcarryc_def x y := let r := addcarry x y in - if r <= x then C1 r else C0 r. + if r <=? x then C1 r else C0 r. (* the same but direct implementation for efficiency *) Primitive addcarryc := #int63_addcarryc. Definition subc_def x y := - if y <= x then C0 (x - y) else C1 (x - y). + if y <=? x then C0 (x - y) else C1 (x - y). (* the same but direct implementation for efficiency *) Primitive subc := #int63_subc. -Notation "n '-c' m" := (subc n m) (at level 50, no associativity) : int63_scope. Definition subcarryc_def x y := - if y < x then C0 (x - y - 1) else C1 (x - y - 1). + if y <? x then C0 (x - y - 1) else C1 (x - y - 1). (* the same but direct implementation for efficiency *) Primitive subcarryc := #int63_subcarryc. -Definition diveucl_def x y := (x/y, x\%y). +Definition diveucl_def x y := (x/y, x mod y). (* the same but direct implementation for efficiency *) Primitive diveucl := #int63_diveucl. @@ -166,6 +168,12 @@ Definition addmuldiv_def p x y := (x << p) lor (y >> (digits - p)). Primitive addmuldiv := #int63_addmuldiv. +Module Import Int63NotationsInternalC. +Notation "- x" := (opp x) : int63_scope. +Notation "n '+c' m" := (addc n m) (at level 50, no associativity) : int63_scope. +Notation "n '-c' m" := (subc n m) (at level 50, no associativity) : int63_scope. +End Int63NotationsInternalC. + Definition oppc (i:int) := 0 -c i. Register Inline oppc. @@ -177,11 +185,10 @@ Register Inline predc. (** Comparison *) Definition compare_def x y := - if x < y then Lt - else if (x == y) then Eq else Gt. + if x <? y then Lt + else if (x =? y) then Eq else Gt. Primitive compare := #int63_compare. -Notation "n ?= m" := (compare n m) (at level 70, no associativity) : int63_scope. Import Bool ZArith. (** Translation to Z *) @@ -194,8 +201,6 @@ Fixpoint to_Z_rec (n:nat) (i:int) := Definition to_Z := to_Z_rec size. -Notation "'φ' x" := (to_Z x) (at level 0) : int63_scope. - Fixpoint of_pos_rec (n:nat) (p:positive) := match n, p with | O, _ => 0 @@ -215,8 +220,12 @@ Definition of_Z z := Definition wB := (2 ^ (Z.of_nat size))%Z. +Module Import Int63NotationsInternalD. +Notation "n ?= m" := (compare n m) (at level 70, no associativity) : int63_scope. +Notation "'φ' x" := (to_Z x) (at level 0) : int63_scope. Notation "'Φ' x" := (zn2z_to_Z wB to_Z x) (at level 0) : int63_scope. +End Int63NotationsInternalD. Lemma to_Z_rec_bounded size : forall x, (0 <= to_Z_rec size x < 2 ^ Z.of_nat size)%Z. Proof. @@ -347,16 +356,16 @@ Axiom mulc_spec : forall x y, φ x * φ y = φ (fst (mulc x y)) * wB + φ (snd ( Axiom div_spec : forall x y, φ (x / y) = φ x / φ y. -Axiom mod_spec : forall x y, φ (x \% y) = φ x mod φ y. +Axiom mod_spec : forall x y, φ (x mod y) = φ x mod φ y. (* Comparisons *) -Axiom eqb_correct : forall i j, (i == j)%int63 = true -> i = j. +Axiom eqb_correct : forall i j, (i =? j)%int63 = true -> i = j. -Axiom eqb_refl : forall x, (x == x)%int63 = true. +Axiom eqb_refl : forall x, (x =? x)%int63 = true. -Axiom ltb_spec : forall x y, (x < y)%int63 = true <-> φ x < φ y. +Axiom ltb_spec : forall x y, (x <? y)%int63 = true <-> φ x < φ y. -Axiom leb_spec : forall x y, (x <= y)%int63 = true <-> φ x <= φ y. +Axiom leb_spec : forall x y, (x <=? y)%int63 = true <-> φ x <= φ y. (** Exotic operations *) @@ -397,7 +406,7 @@ Local Open Scope int63_scope. Definition sqrt_step (rec: int -> int -> int) (i j: int) := let quo := i / j in - if quo < j then rec i ((j + quo) >> 1) + if quo <? j then rec i ((j + quo) >> 1) else j. Definition iter_sqrt := @@ -421,9 +430,9 @@ Definition high_bit := 1 << (digits - 1). Definition sqrt2_step (rec: int -> int -> int -> int) (ih il j: int) := - if ih < j then + if ih <? j then let (quo,_) := diveucl_21 ih il j in - if quo < j then + if quo <? j then match j +c quo with | C0 m1 => rec ih il (m1 >> 1) | C1 m1 => rec ih il ((m1 >> 1) + high_bit) @@ -448,48 +457,48 @@ Definition sqrt2 ih il := let (ih1, il1) := mulc s s in match il -c il1 with | C0 il2 => - if ih1 < ih then (s, C1 il2) else (s, C0 il2) + if ih1 <? ih then (s, C1 il2) else (s, C0 il2) | C1 il2 => - if ih1 < (ih - 1) then (s, C1 il2) else (s, C0 il2) + if ih1 <? (ih - 1) then (s, C1 il2) else (s, C0 il2) end. (** Gcd **) Fixpoint gcd_rec (guard:nat) (i j:int) {struct guard} := match guard with | O => 1 - | S p => if j == 0 then i else gcd_rec p j (i \% j) + | S p => if j =? 0 then i else gcd_rec p j (i mod j) end. Definition gcd := gcd_rec (2*size). (** equality *) -Lemma eqb_complete : forall x y, x = y -> (x == y) = true. +Lemma eqb_complete : forall x y, x = y -> (x =? y) = true. Proof. intros x y H; rewrite -> H, eqb_refl;trivial. Qed. -Lemma eqb_spec : forall x y, (x == y) = true <-> x = y. +Lemma eqb_spec : forall x y, (x =? y) = true <-> x = y. Proof. split;auto using eqb_correct, eqb_complete. Qed. -Lemma eqb_false_spec : forall x y, (x == y) = false <-> x <> y. +Lemma eqb_false_spec : forall x y, (x =? y) = false <-> x <> y. Proof. intros;rewrite <- not_true_iff_false, eqb_spec;split;trivial. Qed. -Lemma eqb_false_complete : forall x y, x <> y -> (x == y) = false. +Lemma eqb_false_complete : forall x y, x <> y -> (x =? y) = false. Proof. intros x y;rewrite eqb_false_spec;trivial. Qed. -Lemma eqb_false_correct : forall x y, (x == y) = false -> x <> y. +Lemma eqb_false_correct : forall x y, (x =? y) = false -> x <> y. Proof. intros x y;rewrite eqb_false_spec;trivial. Qed. Definition eqs (i j : int) : {i = j} + { i <> j } := - (if i == j as b return ((b = true -> i = j) -> (b = false -> i <> j) -> {i=j} + {i <> j} ) + (if i =? j as b return ((b = true -> i = j) -> (b = false -> i <> j) -> {i=j} + {i <> j} ) then fun (Heq : true = true -> i = j) _ => left _ (Heq (eq_refl true)) else fun _ (Hdiff : false = false -> i <> j) => right _ (Hdiff (eq_refl false))) (eqb_correct i j) @@ -503,7 +512,7 @@ Qed. (* Extra function on equality *) Definition cast i j := - (if i == j as b return ((b = true -> i = j) -> option (forall P : int -> Type, P i -> P j)) + (if i =? j as b return ((b = true -> i = j) -> option (forall P : int -> Type, P i -> P j)) then fun Heq : true = true -> i = j => Some (fun (P : int -> Type) (Hi : P i) => @@ -520,14 +529,14 @@ Proof. rewrite (Eqdep_dec.eq_proofs_unicity eq_dec (e (eq_refl true)) (eq_refl i));trivial. Qed. -Lemma cast_diff : forall i j, i == j = false -> cast i j = None. +Lemma cast_diff : forall i j, i =? j = false -> cast i j = None. Proof. intros;unfold cast;intros; generalize (eqb_correct i j). rewrite H;trivial. Qed. Definition eqo i j := - (if i == j as b return ((b = true -> i = j) -> option (i=j)) + (if i =? j as b return ((b = true -> i = j) -> option (i=j)) then fun Heq : true = true -> i = j => Some (Heq (eq_refl true)) else fun _ : false = true -> i = j => None) (eqb_correct i j). @@ -540,7 +549,7 @@ Proof. rewrite (Eqdep_dec.eq_proofs_unicity eq_dec (e (eq_refl true)) (eq_refl i));trivial. Qed. -Lemma eqo_diff : forall i j, i == j = false -> eqo i j = None. +Lemma eqo_diff : forall i j, i =? j = false -> eqo i j = None. Proof. unfold eqo;intros; generalize (eqb_correct i j). rewrite H;trivial. @@ -548,13 +557,13 @@ Qed. (** Comparison *) -Lemma eqbP x y : reflect (φ x = φ y ) (x == y). +Lemma eqbP x y : reflect (φ x = φ y ) (x =? y). Proof. apply iff_reflect; rewrite eqb_spec; split; [ apply to_Z_inj | apply f_equal ]. Qed. -Lemma ltbP x y : reflect (φ x < φ y )%Z (x < y). +Lemma ltbP x y : reflect (φ x < φ y )%Z (x <? y). Proof. apply iff_reflect; symmetry; apply ltb_spec. Qed. -Lemma lebP x y : reflect (φ x <= φ y )%Z (x ≤ y). +Lemma lebP x y : reflect (φ x <= φ y )%Z (x ≤? y). Proof. apply iff_reflect; symmetry; apply leb_spec. Qed. Lemma compare_spec x y : compare x y = (φ x ?= φ y)%Z. @@ -742,7 +751,7 @@ Proof. Qed. Lemma add_le_r m n: - if (n <= m + n)%int63 then (φ m + φ n < wB)%Z else (wB <= φ m + φ n)%Z. + if (n <=? m + n)%int63 then (φ m + φ n < wB)%Z else (wB <= φ m + φ n)%Z. Proof. case (to_Z_bounded m); intros H1m H2m. case (to_Z_bounded n); intros H1n H2n. @@ -753,11 +762,11 @@ Proof. rewrite -> Zplus_mod, Z_mod_same_full, Zplus_0_r, !Zmod_small; auto with zarith. rewrite !Zmod_small; auto with zarith. apply f_equal2 with (f := Zmod); auto with zarith. - case_eq (n <= m + n)%int63; auto. + case_eq (n <=? m + n)%int63; auto. rewrite leb_spec, H1; auto with zarith. assert (H1: (φ (m + n) = φ m + φ n)%Z). rewrite add_spec, Zmod_small; auto with zarith. - replace (n <= m + n)%int63 with true; auto. + replace (n <=? m + n)%int63 with true; auto. apply sym_equal; rewrite leb_spec, H1; auto with zarith. Qed. @@ -783,7 +792,7 @@ Proof. apply to_Z_inj; rewrite lsr_spec; reflexivity. Qed. Lemma lsr_0_r i: i >> 0 = i. Proof. apply to_Z_inj; rewrite lsr_spec, Zdiv_1_r; exact eq_refl. Qed. -Lemma lsr_1 n : 1 >> n = (n == 0). +Lemma lsr_1 n : 1 >> n = (n =? 0)%int63. Proof. case eqbP. intros h; rewrite (to_Z_inj _ _ h), lsr_0_r; reflexivity. @@ -798,12 +807,12 @@ Proof. lia. Qed. -Lemma lsr_add i m n: ((i >> m) >> n = if n <= m + n then i >> (m + n) else 0)%int63. +Lemma lsr_add i m n: ((i >> m) >> n = if n <=? m + n then i >> (m + n) else 0)%int63. Proof. case (to_Z_bounded m); intros H1m H2m. case (to_Z_bounded n); intros H1n H2n. case (to_Z_bounded i); intros H1i H2i. - generalize (add_le_r m n); case (n <= m + n)%int63; intros H. + generalize (add_le_r m n); case (n <=? m + n)%int63; intros H. apply to_Z_inj; rewrite -> !lsr_spec, Zdiv_Zdiv, <- Zpower_exp; auto with zarith. rewrite add_spec, Zmod_small; auto with zarith. apply to_Z_inj; rewrite -> !lsr_spec, Zdiv_Zdiv, <- Zpower_exp; auto with zarith. @@ -833,7 +842,7 @@ Proof. apply f_equal2 with (f := Zmod); auto with zarith. Qed. -Lemma lsr_M_r x i (H: (digits <= i = true)%int63) : x >> i = 0%int63. +Lemma lsr_M_r x i (H: (digits <=? i = true)%int63) : x >> i = 0%int63. Proof. apply to_Z_inj. rewrite lsr_spec, to_Z_0. @@ -889,22 +898,22 @@ Proof. Qed. Lemma bit_lsr x i j : - (bit (x >> i) j = if j <= i + j then bit x (i + j) else false)%int63. + (bit (x >> i) j = if j <=? i + j then bit x (i + j) else false)%int63. Proof. - unfold bit; rewrite lsr_add; case (_ ≤ _); auto. + unfold bit; rewrite lsr_add; case (_ ≤? _); auto. Qed. -Lemma bit_b2i (b: bool) i : bit b i = (i == 0) && b. +Lemma bit_b2i (b: bool) i : bit b i = (i =? 0)%int63 && b. Proof. case b; unfold bit; simpl b2i. - rewrite lsr_1; case (i == 0); auto. + rewrite lsr_1; case (i =? 0)%int63; auto. rewrite lsr0, lsl0, andb_false_r; auto. Qed. -Lemma bit_1 n : bit 1 n = (n == 0). +Lemma bit_1 n : bit 1 n = (n =? 0)%int63. Proof. unfold bit; rewrite lsr_1. - case (_ == _); simpl; auto. + case (_ =? _)%int63; simpl; auto. Qed. Local Hint Resolve Z.lt_gt Z.div_pos : zarith. @@ -929,14 +938,14 @@ Proof. case bit; discriminate. Qed. -Lemma bit_M i n (H: (digits <= n = true)%int63): bit i n = false. +Lemma bit_M i n (H: (digits <=? n = true)%int63): bit i n = false. Proof. unfold bit; rewrite lsr_M_r; auto. Qed. -Lemma bit_half i n (H: (n < digits = true)%int63) : bit (i>>1) n = bit i (n+1). +Lemma bit_half i n (H: (n <? digits = true)%int63) : bit (i>>1) n = bit i (n+1). Proof. unfold bit. rewrite lsr_add. - case_eq (n <= (1 + n))%int63. + case_eq (n <=? (1 + n))%int63. replace (1+n)%int63 with (n+1)%int63; [auto|idtac]. apply to_Z_inj; rewrite !add_spec, Zplus_comm; auto. intros H1; assert (H2: n = max_int). @@ -968,10 +977,10 @@ Proof. Qed. Lemma bit_lsl x i j : bit (x << i) j = -(if (j < i) || (digits <= j) then false else bit x (j - i))%int63. +(if (j <? i) || (digits <=? j) then false else bit x (j - i))%int63. Proof. assert (F1: 1 >= 0) by discriminate. - case_eq (digits <= j)%int63; intros H. + case_eq (digits <=? j)%int63; intros H. rewrite orb_true_r, bit_M; auto. set (d := φ digits). case (Zle_or_lt d (φ j)); intros H1. @@ -1039,10 +1048,10 @@ Lemma lor_lsr i1 i2 i: (i1 lor i2) >> i = (i1 >> i) lor (i2 >> i). Proof. apply bit_ext; intros n. rewrite -> lor_spec, !bit_lsr, lor_spec. - case (_ <= _)%int63; auto. + case (_ <=? _)%int63; auto. Qed. -Lemma lor_le x y : (y <= x lor y)%int63 = true. +Lemma lor_le x y : (y <=? x lor y)%int63 = true. Proof. generalize x y (to_Z_bounded x) (to_Z_bounded y); clear x y. unfold wB; elim size. @@ -1092,7 +1101,7 @@ Proof. rewrite lsr_spec, Z.pow_1_r; split; auto with zarith. apply Zdiv_lt_upper_bound; auto with zarith. intros m H1 H2. - case_eq (digits <= m)%int63; [idtac | rewrite <- not_true_iff_false]; + case_eq (digits <=? m)%int63; [idtac | rewrite <- not_true_iff_false]; intros Heq. rewrite bit_M in H1; auto; discriminate. rewrite leb_spec in Heq. @@ -1131,7 +1140,7 @@ Proof. rewrite lsr_spec, to_Z_1, Z.pow_1_r; split; auto with zarith. apply Zdiv_lt_upper_bound; auto with zarith. intros _ HH m; case (to_Z_bounded m); intros H1m H2m. - case_eq (digits <= m)%int63. + case_eq (digits <=? m)%int63. intros Hlm; rewrite bit_M; auto; discriminate. rewrite <- not_true_iff_false, leb_spec; intros Hlm. case (Zle_lt_or_eq 0 φ m); auto; intros Hm. @@ -1177,11 +1186,11 @@ Proof. rewrite (fun x y => Zmod_small (x - y)); auto with zarith. intros n; rewrite -> bit_lsl, bit_lsr. generalize (add_le_r (digits - p) n). - case (_ ≤ _); try discriminate. + case (_ ≤? _); try discriminate. rewrite -> sub_spec, Zmod_small; auto with zarith; intros H1. - case_eq (n < p)%int63; try discriminate. + case_eq (n <? p)%int63; try discriminate. rewrite <- not_true_iff_false, ltb_spec; intros H2. - case (_ ≤ _); try discriminate. + case (_ ≤? _); try discriminate. intros _; rewrite bit_M; try discriminate. rewrite -> leb_spec, add_spec, Zmod_small, sub_spec, Zmod_small; auto with zarith. rewrite -> sub_spec, Zmod_small; auto with zarith. @@ -1196,7 +1205,7 @@ Proof. apply bit_ext; intros n. rewrite bit_b2i, land_spec, bit_1. generalize (eqb_spec n 0). - case (n == 0); auto. + case (n =? 0)%int63; auto. intros(H,_); rewrite andb_true_r, H; auto. rewrite andb_false_r; auto. Qed. @@ -1373,9 +1382,9 @@ Qed. (* sqrt2 *) Lemma sqrt2_step_def rec ih il j: sqrt2_step rec ih il j = - if (ih < j)%int63 then + if (ih <? j)%int63 then let quo := fst (diveucl_21 ih il j) in - if (quo < j)%int63 then + if (quo <? j)%int63 then let m := match j +c quo with | C0 m1 => m1 >> 1 @@ -1453,7 +1462,7 @@ Proof. apply Zmult_lt_0_compat; auto with zarith. refine (Z.lt_le_trans _ _ _ _ Hih); auto with zarith. } cbv zeta. - case_eq (ih < j)%int63;intros Heq. + case_eq (ih <? j)%int63;intros Heq. rewrite -> ltb_spec in Heq. 2: rewrite <-not_true_iff_false, ltb_spec in Heq. 2: split; auto. @@ -1462,7 +1471,7 @@ Proof. 2: assert (0 <= φ il/φ j) by (apply Z_div_pos; auto with zarith). 2: rewrite Zmult_comm, Z_div_plus_full_l; unfold base; auto with zarith. case (Zle_or_lt (2^(Z_of_nat size -1)) φ j); intros Hjj. - case_eq (fst (diveucl_21 ih il j) < j)%int63;intros Heq0. + case_eq (fst (diveucl_21 ih il j) <? j)%int63;intros Heq0. 2: rewrite <-not_true_iff_false, ltb_spec, (div2_phi _ _ _ Hjj Heq) in Heq0. 2: split; auto; apply sqrt_test_true; auto with zarith. rewrite -> ltb_spec, (div2_phi _ _ _ Hjj Heq) in Heq0. @@ -1557,7 +1566,7 @@ Lemma sqrt2_spec : forall x y, generalize (subc_spec il il1). case subc; intros il2 Hil2. simpl interp_carry in Hil2. - case_eq (ih1 < ih)%int63; [idtac | rewrite <- not_true_iff_false]; + case_eq (ih1 <? ih)%int63; [idtac | rewrite <- not_true_iff_false]; rewrite ltb_spec; intros Heq. unfold interp_carry; rewrite Zmult_1_l. rewrite -> Z.pow_2_r, Hihl1, Hil2. @@ -1602,7 +1611,7 @@ Lemma sqrt2_spec : forall x y, case (to_Z_bounded ih); intros H1 H2. split; auto with zarith. apply Z.le_trans with (wB/4 - 1); auto with zarith. - case_eq (ih1 < ih - 1)%int63; [idtac | rewrite <- not_true_iff_false]; + case_eq (ih1 <? ih - 1)%int63; [idtac | rewrite <- not_true_iff_false]; rewrite ltb_spec, Hsih; intros Heq. rewrite Z.pow_2_r, Hihl1. case (Zle_lt_or_eq (φ ih1 + 2) φ ih); auto with zarith. @@ -1927,3 +1936,21 @@ Qed. Lemma lxor0_r i : i lxor 0 = i. Proof. rewrite lxorC; exact (lxor0 i). Qed. + +Module Export Int63Notations. + Local Open Scope int63_scope. + #[deprecated(since="8.13",note="use infix mod instead")] + Notation "a \% m" := (a mod m) (at level 40, left associativity) : int63_scope. + #[deprecated(since="8.13",note="use infix =? instead")] + Notation "m '==' n" := (m =? n) (at level 70, no associativity) : int63_scope. + #[deprecated(since="8.13",note="use infix <? instead")] + Notation "m < n" := (m <? n) : int63_scope. + #[deprecated(since="8.13",note="use infix <=? instead")] + Notation "m <= n" := (m <=? n) : int63_scope. + #[deprecated(since="8.13",note="use infix ≤? instead")] + Notation "m ≤ n" := (m <=? n) (at level 70, no associativity) : int63_scope. + Export Int63NotationsInternalA. + Export Int63NotationsInternalB. + Export Int63NotationsInternalC. + Export Int63NotationsInternalD. +End Int63Notations. diff --git a/theories/Numbers/NatInt/NZAdd.v b/theories/Numbers/NatInt/NZAdd.v index 7982411bdd..66cbba9e08 100644 --- a/theories/Numbers/NatInt/NZAdd.v +++ b/theories/Numbers/NatInt/NZAdd.v @@ -22,7 +22,7 @@ Ltac nzsimpl' := autorewrite with nz nz'. Theorem add_0_r : forall n, n + 0 == n. Proof. - nzinduct n. + intro n; nzinduct n. - now nzsimpl. - intro. nzsimpl. now rewrite succ_inj_wd. Qed. diff --git a/theories/Numbers/NatInt/NZBase.v b/theories/Numbers/NatInt/NZBase.v index 8bc393bbad..d4f70adbc5 100644 --- a/theories/Numbers/NatInt/NZBase.v +++ b/theories/Numbers/NatInt/NZBase.v @@ -74,7 +74,7 @@ Proof. intros z Base Step; revert Base; pattern z; apply bi_induction. - solve_proper. - intro; now apply bi_induction. -- intro; pose proof (Step n); tauto. +- intro n; pose proof (Step n); tauto. Qed. End CentralInduction. @@ -83,7 +83,7 @@ Tactic Notation "nzinduct" ident(n) := induction_maker n ltac:(apply bi_induction). Tactic Notation "nzinduct" ident(n) constr(u) := - induction_maker n ltac:(apply central_induction with (z := u)). + induction_maker n ltac:(apply (fun A A_wd => central_induction A A_wd u)). End NZBaseProp. diff --git a/theories/Numbers/NatInt/NZDiv.v b/theories/Numbers/NatInt/NZDiv.v index 1c45aa440f..e6249be8df 100644 --- a/theories/Numbers/NatInt/NZDiv.v +++ b/theories/Numbers/NatInt/NZDiv.v @@ -116,7 +116,7 @@ Qed. Theorem div_small: forall a b, 0<=a<b -> a/b == 0. Proof. -intros. symmetry. +intros a b ?. symmetry. apply div_unique with a; intuition; try order. now nzsimpl. Qed. @@ -149,7 +149,7 @@ Qed. Lemma mod_1_r: forall a, 0<=a -> a mod 1 == 0. Proof. -intros. symmetry. +intros a ?. symmetry. apply mod_unique with a; try split; try order; try apply lt_0_1. now nzsimpl. Qed. @@ -173,7 +173,7 @@ Qed. Lemma mod_mul : forall a b, 0<=a -> 0<b -> (a*b) mod b == 0. Proof. -intros; symmetry. +intros a b ? ?; symmetry. apply mod_unique with a; try split; try order. - apply mul_nonneg_nonneg; order. - nzsimpl; apply mul_comm. @@ -186,7 +186,7 @@ Qed. Theorem mod_le: forall a b, 0<=a -> 0<b -> a mod b <= a. Proof. -intros. destruct (le_gt_cases b a). +intros a b ? ?. destruct (le_gt_cases b a). - apply le_trans with b; auto. apply lt_le_incl. destruct (mod_bound_pos a b); auto. - rewrite lt_eq_cases; right. @@ -198,7 +198,7 @@ Qed. Lemma div_pos: forall a b, 0<=a -> 0<b -> 0 <= a/b. Proof. -intros. +intros a b ? ?. rewrite (mul_le_mono_pos_l _ _ b); auto; nzsimpl. rewrite (add_le_mono_r _ _ (a mod b)). rewrite <- div_mod by order. @@ -247,7 +247,7 @@ Qed. Lemma div_lt : forall a b, 0<a -> 1<b -> a/b < a. Proof. -intros. +intros a b ? ?. assert (0 < b) by (apply lt_trans with 1; auto using lt_0_1). destruct (lt_ge_cases a b). - rewrite div_small; try split; order. @@ -284,7 +284,7 @@ Qed. Lemma mul_div_le : forall a b, 0<=a -> 0<b -> b*(a/b) <= a. Proof. -intros. +intros a b ? ?. rewrite (add_le_mono_r _ _ (a mod b)), <- div_mod by order. rewrite <- (add_0_r a) at 1. rewrite <- add_le_mono_l. destruct (mod_bound_pos a b); order. @@ -292,7 +292,7 @@ Qed. Lemma mul_succ_div_gt : forall a b, 0<=a -> 0<b -> a < b*(S (a/b)). Proof. -intros. +intros a b ? ?. rewrite (div_mod a b) at 1 by order. rewrite (mul_succ_r). rewrite <- add_lt_mono_l. @@ -304,7 +304,7 @@ Qed. Lemma div_exact : forall a b, 0<=a -> 0<b -> (a == b*(a/b) <-> a mod b == 0). Proof. -intros. rewrite (div_mod a b) at 1 by order. +intros a b ? ?. rewrite (div_mod a b) at 1 by order. rewrite <- (add_0_r (b*(a/b))) at 2. apply add_cancel_l. Qed. @@ -314,7 +314,7 @@ Qed. Theorem div_lt_upper_bound: forall a b q, 0<=a -> 0<b -> a < b*q -> a/b < q. Proof. -intros. +intros a b q ? ? ?. rewrite (mul_lt_mono_pos_l b) by order. apply le_lt_trans with a; auto. apply mul_div_le; auto. @@ -323,7 +323,7 @@ Qed. Theorem div_le_upper_bound: forall a b q, 0<=a -> 0<b -> a <= b*q -> a/b <= q. Proof. -intros. +intros a b q ? ? ?. rewrite (mul_le_mono_pos_l _ _ b) by order. apply le_trans with a; auto. apply mul_div_le; auto. @@ -362,7 +362,7 @@ Qed. Lemma mod_add : forall a b c, 0<=a -> 0<=a+b*c -> 0<c -> (a + b * c) mod c == a mod c. Proof. - intros. + intros a b c ? ? ?. symmetry. apply mod_unique with (a/c+b); auto. - apply mod_bound_pos; auto. @@ -373,7 +373,7 @@ Qed. Lemma div_add : forall a b c, 0<=a -> 0<=a+b*c -> 0<c -> (a + b * c) / c == a / c + b. Proof. - intros. + intros a b c ? ? ?. apply (mul_cancel_l _ _ c); try order. apply (add_cancel_r _ _ ((a+b*c) mod c)). rewrite <- div_mod, mod_add by order. @@ -393,7 +393,7 @@ Qed. Lemma div_mul_cancel_r : forall a b c, 0<=a -> 0<b -> 0<c -> (a*c)/(b*c) == a/b. Proof. - intros. + intros a b c ? ? ?. symmetry. apply div_unique with ((a mod b)*c). - apply mul_nonneg_nonneg; order. @@ -409,13 +409,13 @@ Qed. Lemma div_mul_cancel_l : forall a b c, 0<=a -> 0<b -> 0<c -> (c*a)/(c*b) == a/b. Proof. - intros. rewrite !(mul_comm c); apply div_mul_cancel_r; auto. + intros a b c ? ? ?. rewrite !(mul_comm c); apply div_mul_cancel_r; auto. Qed. Lemma mul_mod_distr_l: forall a b c, 0<=a -> 0<b -> 0<c -> (c*a) mod (c*b) == c * (a mod b). Proof. - intros. + intros a b c ? ? ?. rewrite <- (add_cancel_l _ _ ((c*b)* ((c*a)/(c*b)))). rewrite <- div_mod. - rewrite div_mul_cancel_l; auto. @@ -427,7 +427,7 @@ Qed. Lemma mul_mod_distr_r: forall a b c, 0<=a -> 0<b -> 0<c -> (a*c) mod (b*c) == (a mod b) * c. Proof. - intros. rewrite !(mul_comm _ c); now rewrite mul_mod_distr_l. + intros a b c ? ? ?. rewrite !(mul_comm _ c); now rewrite mul_mod_distr_l. Qed. (** Operations modulo. *) @@ -435,7 +435,7 @@ Qed. Theorem mod_mod: forall a n, 0<=a -> 0<n -> (a mod n) mod n == a mod n. Proof. - intros. destruct (mod_bound_pos a n); auto. now rewrite mod_small_iff. + intros a n ? ?. destruct (mod_bound_pos a n); auto. now rewrite mod_small_iff. Qed. Lemma mul_mod_idemp_l : forall a b n, 0<=a -> 0<=b -> 0<n -> @@ -454,13 +454,14 @@ Qed. Lemma mul_mod_idemp_r : forall a b n, 0<=a -> 0<=b -> 0<n -> (a*(b mod n)) mod n == (a*b) mod n. Proof. - intros. rewrite !(mul_comm a). apply mul_mod_idemp_l; auto. + intros a b n ? ? ?. rewrite !(mul_comm a). apply mul_mod_idemp_l; auto. Qed. Theorem mul_mod: forall a b n, 0<=a -> 0<=b -> 0<n -> (a * b) mod n == ((a mod n) * (b mod n)) mod n. Proof. - intros. rewrite mul_mod_idemp_l, mul_mod_idemp_r; trivial. - reflexivity. + intros a b n ? ? ?. rewrite mul_mod_idemp_l, mul_mod_idemp_r; trivial. + - reflexivity. - now destruct (mod_bound_pos b n). Qed. @@ -478,13 +479,14 @@ Qed. Lemma add_mod_idemp_r : forall a b n, 0<=a -> 0<=b -> 0<n -> (a+(b mod n)) mod n == (a+b) mod n. Proof. - intros. rewrite !(add_comm a). apply add_mod_idemp_l; auto. + intros a b n ? ? ?. rewrite !(add_comm a). apply add_mod_idemp_l; auto. Qed. Theorem add_mod: forall a b n, 0<=a -> 0<=b -> 0<n -> (a+b) mod n == (a mod n + b mod n) mod n. Proof. - intros. rewrite add_mod_idemp_l, add_mod_idemp_r; trivial. - reflexivity. + intros a b n ? ? ?. rewrite add_mod_idemp_l, add_mod_idemp_r; trivial. + - reflexivity. - now destruct (mod_bound_pos b n). Qed. @@ -525,7 +527,7 @@ Qed. Theorem div_mul_le: forall a b c, 0<=a -> 0<b -> 0<=c -> c*(a/b) <= (c*a)/b. Proof. - intros. + intros a b c ? ? ?. apply div_le_lower_bound; auto. - apply mul_nonneg_nonneg; auto. - rewrite mul_assoc, (mul_comm b c), <- mul_assoc. @@ -538,7 +540,7 @@ Qed. Lemma mod_divides : forall a b, 0<=a -> 0<b -> (a mod b == 0 <-> exists c, a == b*c). Proof. - split. + intros a b ? ?; split. - intros. exists (a/b). rewrite div_exact; auto. - intros (c,Hc). rewrite Hc, mul_comm. apply mod_mul; auto. rewrite (mul_le_mono_pos_l _ _ b); auto. nzsimpl. order. diff --git a/theories/Numbers/NatInt/NZGcd.v b/theories/Numbers/NatInt/NZGcd.v index 63cc725aec..c542c3fc2c 100644 --- a/theories/Numbers/NatInt/NZGcd.v +++ b/theories/Numbers/NatInt/NZGcd.v @@ -147,7 +147,7 @@ Qed. Lemma mul_divide_cancel_r : forall n m p, p ~= 0 -> ((n * p | m * p) <-> (n | m)). Proof. - intros. rewrite 2 (mul_comm _ p). now apply mul_divide_cancel_l. + intros n m p ?. rewrite 2 (mul_comm _ p). now apply mul_divide_cancel_l. Qed. Lemma divide_add_r : forall n m p, (n | m) -> (n | p) -> (n | m + p). @@ -215,7 +215,7 @@ Qed. Lemma gcd_divide_iff : forall n m p, (p | gcd n m) <-> (p | n) /\ (p | m). Proof. - intros. split. - split. + intros n m p. split. - split. + transitivity (gcd n m); trivial using gcd_divide_l. + transitivity (gcd n m); trivial using gcd_divide_r. - intros (H,H'). now apply gcd_greatest. @@ -273,18 +273,18 @@ Qed. Lemma gcd_eq_0_l : forall n m, gcd n m == 0 -> n == 0. Proof. - intros. + intros n m H. generalize (gcd_divide_l n m). rewrite H. apply divide_0_l. Qed. Lemma gcd_eq_0_r : forall n m, gcd n m == 0 -> m == 0. Proof. - intros. apply gcd_eq_0_l with n. now rewrite gcd_comm. + intros n m ?. apply gcd_eq_0_l with n. now rewrite gcd_comm. Qed. Lemma gcd_eq_0 : forall n m, gcd n m == 0 <-> n == 0 /\ m == 0. Proof. - intros. split. + intros n m. split. - split. + now apply gcd_eq_0_l with m. + now apply gcd_eq_0_r with n. diff --git a/theories/Numbers/NatInt/NZLog.v b/theories/Numbers/NatInt/NZLog.v index 5491d7ab04..526af2f9df 100644 --- a/theories/Numbers/NatInt/NZLog.v +++ b/theories/Numbers/NatInt/NZLog.v @@ -335,7 +335,7 @@ Qed. Lemma log2_succ_or : forall a, log2 (S a) == S (log2 a) \/ log2 (S a) == log2 a. Proof. - intros. + intros a. destruct (le_gt_cases (log2 (S a)) (log2 a)) as [H|H]. - right. generalize (log2_le_mono _ _ (le_succ_diag_r a)); order. - left. apply le_succ_l in H. generalize (log2_succ_le a); order. @@ -601,7 +601,7 @@ Lemma log2_log2_up_exact : Proof. intros a Ha. split. - - intros. exists (log2 a). + - intros H. exists (log2 a). generalize (log2_log2_up_spec a Ha). rewrite <-H. destruct 1; order. - intros (b,Hb). rewrite Hb. @@ -806,8 +806,8 @@ Qed. Lemma log2_up_succ_or : forall a, log2_up (S a) == S (log2_up a) \/ log2_up (S a) == log2_up a. Proof. - intros. - destruct (le_gt_cases (log2_up (S a)) (log2_up a)). + intros a. + destruct (le_gt_cases (log2_up (S a)) (log2_up a)) as [H|H]. - right. generalize (log2_up_le_mono _ _ (le_succ_diag_r a)); order. - left. apply le_succ_l in H. generalize (log2_up_succ_le a); order. Qed. diff --git a/theories/Numbers/NatInt/NZMul.v b/theories/Numbers/NatInt/NZMul.v index 9ddf7cb0eb..3d6465191d 100644 --- a/theories/Numbers/NatInt/NZMul.v +++ b/theories/Numbers/NatInt/NZMul.v @@ -17,7 +17,7 @@ Include NZAddProp NZ NZBase. Theorem mul_0_r : forall n, n * 0 == 0. Proof. -nzinduct n; intros; now nzsimpl. +intro n; nzinduct n; intros; now nzsimpl. Qed. Theorem mul_succ_r : forall n m, n * (S m) == n * m + n. diff --git a/theories/Numbers/NatInt/NZMulOrder.v b/theories/Numbers/NatInt/NZMulOrder.v index 46749504a9..c67bbe38d8 100644 --- a/theories/Numbers/NatInt/NZMulOrder.v +++ b/theories/Numbers/NatInt/NZMulOrder.v @@ -46,7 +46,7 @@ Qed. Theorem mul_lt_mono_neg_l : forall p n m, p < 0 -> (n < m <-> p * m < p * n). Proof. -nzord_induct p. +intro p; nzord_induct p. - order. - intros p Hp _ n m Hp'. apply lt_succ_l in Hp'. order. - intros p Hp IH n m _. apply le_succ_l in Hp. @@ -196,7 +196,7 @@ Qed. Theorem mul_nonneg_nonneg : forall n m, 0 <= n -> 0 <= m -> 0 <= n*m. Proof. -intros. rewrite <- (mul_0_l m). apply mul_le_mono_nonneg; order. +intros n m Hn Hm. rewrite <- (mul_0_l m). apply mul_le_mono_nonneg; order. Qed. Theorem mul_pos_cancel_l : forall n m, 0 < n -> (0 < n*m <-> 0 < m). @@ -343,7 +343,7 @@ Qed. Lemma square_nonneg : forall a, 0 <= a * a. Proof. - intros. rewrite <- (mul_0_r a). destruct (le_gt_cases a 0). + intro a. rewrite <- (mul_0_r a). destruct (le_gt_cases a 0). - now apply mul_le_mono_nonpos_l. - apply mul_le_mono_nonneg_l; order. Qed. @@ -391,7 +391,7 @@ Qed. Lemma quadmul_le_squareadd : forall a b, 0<=a -> 0<=b -> 2*2*a*b <= (a+b)*(a+b). Proof. - intros. + intros a b Ha Hb. nzsimpl'. rewrite !mul_add_distr_l, !mul_add_distr_r. rewrite (add_comm _ (b*b)), add_assoc. diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v index d576902c5c..68bb974c5d 100644 --- a/theories/Numbers/NatInt/NZOrder.v +++ b/theories/Numbers/NatInt/NZOrder.v @@ -65,7 +65,7 @@ Qed. Theorem le_succ_l : forall n m, S n <= m <-> n < m. Proof. -intro n; nzinduct m n. +intros n m; nzinduct m n. - split; intro H. + false_hyp H nle_succ_diag_l. + false_hyp H lt_irrefl. - intro m. rewrite (lt_eq_cases (S n) (S m)), !lt_succ_r, (lt_eq_cases n m), succ_inj_wd. @@ -362,7 +362,7 @@ induction does not go through, so we need to use strong Lemma lt_exists_pred_strong : forall z n m, z < m -> m <= n -> exists k, m == S k /\ z <= k. Proof. -intro z; nzinduct n z. +intros z n; nzinduct n z. - order. - intro n; split; intros IH m H1 H2. + apply le_succ_r in H2. destruct H2 as [H2 | H2]. @@ -373,7 +373,7 @@ Qed. Theorem lt_exists_pred : forall z n, z < n -> exists k, n == S k /\ z <= k. Proof. -intros z n H; apply lt_exists_pred_strong with (z := z) (n := n). +intros z n H; apply (lt_exists_pred_strong z n). - assumption. - apply le_refl. Qed. @@ -428,12 +428,12 @@ Qed. Lemma A'A_right : (forall n, A' n) -> forall n, z <= n -> A n. Proof. -intros H1 n H2. apply H1 with (n := S n); [assumption | apply lt_succ_diag_r]. +intros H1 n H2. apply (H1 (S n)); [assumption | apply lt_succ_diag_r]. Qed. Theorem strong_right_induction: right_step' -> forall n, z <= n -> A n. Proof. -intro RS'; apply A'A_right; unfold A'; nzinduct n z; +intro RS'; apply A'A_right; unfold A'; intro n; nzinduct n z; [apply rbase | apply rs'_rs''; apply RS']. Qed. @@ -504,7 +504,7 @@ Qed. Theorem strong_left_induction: left_step' -> forall n, n <= z -> A n. Proof. -intro LS'; apply A'A_left; unfold A'; nzinduct n (S z); +intro LS'; apply A'A_left; unfold A'; intro n; nzinduct n (S z); [apply lbase | apply ls'_ls''; apply LS']. Qed. @@ -629,8 +629,7 @@ Qed. Theorem lt_wf : well_founded Rlt. Proof. unfold well_founded. -apply strong_right_induction' with (z := z). -- auto with typeclass_instances. +apply (strong_right_induction' _ _ z). - intros n H; constructor; intros y [H1 H2]. apply nle_gt in H2. elim H2. now apply le_trans with z. - intros n H1 H2; constructor; intros m [H3 H4]. now apply H2. @@ -639,8 +638,7 @@ Qed. Theorem gt_wf : well_founded Rgt. Proof. unfold well_founded. -apply strong_left_induction' with (z := z). -- auto with typeclass_instances. +apply (strong_left_induction' _ _ z). - intros n H; constructor; intros y [H1 H2]. apply nle_gt in H2. + elim H2. diff --git a/theories/Numbers/NatInt/NZParity.v b/theories/Numbers/NatInt/NZParity.v index ee6f4014f0..07a33e3f67 100644 --- a/theories/Numbers/NatInt/NZParity.v +++ b/theories/Numbers/NatInt/NZParity.v @@ -47,7 +47,7 @@ Qed. Lemma Even_or_Odd : forall x, Even x \/ Odd x. Proof. - nzinduct x. + intro x; nzinduct x. - left. exists 0. now nzsimpl. - intros x. split; intros [(y,H)|(y,H)]. @@ -86,7 +86,7 @@ Qed. Lemma orb_even_odd : forall n, orb (even n) (odd n) = true. Proof. - intros. + intros n. destruct (Even_or_Odd n) as [H|H]. - rewrite <- even_spec in H. now rewrite H. - rewrite <- odd_spec in H. now rewrite H, orb_true_r. @@ -94,7 +94,7 @@ Qed. Lemma negb_odd : forall n, negb (odd n) = even n. Proof. - intros. + intros n. generalize (Even_or_Odd n) (Even_Odd_False n). rewrite <- even_spec, <- odd_spec. destruct (odd n), (even n) ; simpl; intuition. @@ -188,7 +188,7 @@ Qed. Lemma even_add : forall n m, even (n+m) = Bool.eqb (even n) (even m). Proof. - intros. + intros n m. case_eq (even n); case_eq (even m); rewrite <- ?negb_true_iff, ?negb_even, ?odd_spec, ?even_spec; intros (m',Hm) (n',Hn). @@ -200,7 +200,7 @@ Qed. Lemma odd_add : forall n m, odd (n+m) = xorb (odd n) (odd m). Proof. - intros. rewrite <- !negb_even. rewrite even_add. + intros n m. rewrite <- !negb_even. rewrite even_add. now destruct (even n), (even m). Qed. @@ -208,7 +208,7 @@ Qed. Lemma even_mul : forall n m, even (mul n m) = even n || even m. Proof. - intros. + intros n m. case_eq (even n); simpl; rewrite ?even_spec. - intros (n',Hn). exists (n'*m). now rewrite Hn, mul_assoc. - case_eq (even m); simpl; rewrite ?even_spec. @@ -222,7 +222,7 @@ Qed. Lemma odd_mul : forall n m, odd (mul n m) = odd n && odd m. Proof. - intros. rewrite <- !negb_even. rewrite even_mul. + intros n m. rewrite <- !negb_even. rewrite even_mul. now destruct (even n), (even m). Qed. diff --git a/theories/Numbers/NatInt/NZPow.v b/theories/Numbers/NatInt/NZPow.v index 01a15686e0..3b2a496229 100644 --- a/theories/Numbers/NatInt/NZPow.v +++ b/theories/Numbers/NatInt/NZPow.v @@ -238,7 +238,7 @@ Qed. Lemma pow_le_mono : forall a b c d, 0<a<=c -> b<=d -> a^b <= c^d. Proof. - intros. transitivity (a^d). + intros a b c d ? ?. transitivity (a^d). - apply pow_le_mono_r; intuition order. - apply pow_le_mono_l; intuition order. Qed. diff --git a/theories/Numbers/NatInt/NZSqrt.v b/theories/Numbers/NatInt/NZSqrt.v index 446ed07b53..4122632603 100644 --- a/theories/Numbers/NatInt/NZSqrt.v +++ b/theories/Numbers/NatInt/NZSqrt.v @@ -58,7 +58,7 @@ Qed. Lemma sqrt_nonneg : forall a, 0<=√a. Proof. - intros. destruct (lt_ge_cases a 0) as [Ha|Ha]. + intros a. destruct (lt_ge_cases a 0) as [Ha|Ha]. - now rewrite (sqrt_neg _ Ha). - apply sqrt_spec_nonneg. destruct (sqrt_spec a Ha). order. Qed. @@ -429,7 +429,7 @@ Qed. Lemma sqrt_up_nonneg : forall a, 0<=√°a. Proof. - intros. destruct (le_gt_cases a 0) as [Ha|Ha]. + intros a. destruct (le_gt_cases a 0) as [Ha|Ha]. - now rewrite sqrt_up_eqn0. - rewrite sqrt_up_eqn; trivial. apply le_le_succ_r, sqrt_nonneg. Qed. @@ -527,7 +527,7 @@ Lemma sqrt_sqrt_up_exact : forall a, 0<=a -> (√a == √°a <-> exists b, 0<=b /\ a == b²). Proof. intros a Ha. - split. - intros. exists √a. + split. - intros H. exists √a. split. + apply sqrt_nonneg. + generalize (sqrt_sqrt_up_spec a Ha). rewrite <-H. destruct 1; order. - intros (b & Hb & Hb'). rewrite Hb'. |