diff options
Diffstat (limited to 'theories/Numbers/Natural')
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NAdd.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NAddOrder.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NBase.v | 26 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NBits.v | 85 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NDiv.v | 6 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NGcd.v | 10 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NLcm.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NMaxMin.v | 56 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NOrder.v | 26 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NParity.v | 8 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NPow.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NSub.v | 23 |
12 files changed, 126 insertions, 122 deletions
diff --git a/theories/Numbers/Natural/Abstract/NAdd.v b/theories/Numbers/Natural/Abstract/NAdd.v index 8c4d072114..55c4b193a5 100644 --- a/theories/Numbers/Natural/Abstract/NAdd.v +++ b/theories/Numbers/Natural/Abstract/NAdd.v @@ -58,7 +58,7 @@ Qed. Theorem succ_add_discr : forall n m, m ~= S (n + m). Proof. -intro n; induct m. +intros n m; induct m. apply neq_sym. apply neq_succ_0. intros m IH H. apply succ_inj in H. rewrite add_succ_r in H. unfold not in IH; now apply IH. diff --git a/theories/Numbers/Natural/Abstract/NAddOrder.v b/theories/Numbers/Natural/Abstract/NAddOrder.v index 7c74de6364..d0ef94d1a4 100644 --- a/theories/Numbers/Natural/Abstract/NAddOrder.v +++ b/theories/Numbers/Natural/Abstract/NAddOrder.v @@ -19,7 +19,7 @@ Include NOrderProp N. Theorem le_add_r : forall n m, n <= n + m. Proof. -intro n; induct m. +intros n m; induct m. rewrite add_0_r; now apply eq_le_incl. intros m IH. rewrite add_succ_r; now apply le_le_succ_r. Qed. diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v index a141cb7c0d..185a5974c2 100644 --- a/theories/Numbers/Natural/Abstract/NBase.v +++ b/theories/Numbers/Natural/Abstract/NBase.v @@ -39,7 +39,7 @@ Qed. Theorem le_0_l : forall n, 0 <= n. Proof. -nzinduct n. +intro n; nzinduct n. now apply eq_le_incl. intro n; split. apply le_le_succ_r. @@ -79,21 +79,21 @@ Proof. intro H; apply (neq_succ_0 0). apply H. Qed. -Theorem neq_0_r : forall n, n ~= 0 <-> exists m, n == S m. +Theorem neq_0_r n : n ~= 0 <-> exists m, n == S m. Proof. cases n. split; intro H; [now elim H | destruct H as [m H]; symmetry in H; false_hyp H neq_succ_0]. intro n; split; intro H; [now exists n | apply neq_succ_0]. Qed. -Theorem zero_or_succ : forall n, n == 0 \/ exists m, n == S m. +Theorem zero_or_succ n : n == 0 \/ exists m, n == S m. Proof. cases n. now left. intro n; right; now exists n. Qed. -Theorem eq_pred_0 : forall n, P n == 0 <-> n == 0 \/ n == 1. +Theorem eq_pred_0 n : P n == 0 <-> n == 0 \/ n == 1. Proof. cases n. rewrite pred_0. now split; [left|]. @@ -103,16 +103,16 @@ intros [H|H]. elim (neq_succ_0 _ H). apply succ_inj_wd. now rewrite <- one_succ. Qed. -Theorem succ_pred : forall n, n ~= 0 -> S (P n) == n. +Theorem succ_pred n : n ~= 0 -> S (P n) == n. Proof. cases n. intro H; exfalso; now apply H. intros; now rewrite pred_succ. Qed. -Theorem pred_inj : forall n m, n ~= 0 -> m ~= 0 -> P n == P m -> n == m. +Theorem pred_inj n m : n ~= 0 -> m ~= 0 -> P n == P m -> n == m. Proof. -intros n m; cases n. +cases n. intros H; exfalso; now apply H. intros n _; cases m. intros H; exfalso; now apply H. @@ -134,7 +134,7 @@ Proof. rewrite one_succ. intros until 3. assert (D : forall n, A n /\ A (S n)); [ |intro n; exact (proj1 (D n))]. -induct n; [ | intros n [IH1 IH2]]; auto. +intro n; induct n; [ | intros n [IH1 IH2]]; auto. Qed. End PairInduction. @@ -151,10 +151,10 @@ Theorem two_dim_induction : (forall n m, R n m -> R n (S m)) -> (forall n, (forall m, R n m) -> R (S n) 0) -> forall n m, R n m. Proof. -intros H1 H2 H3. induct n. -induct m. +intros H1 H2 H3. intro n; induct n. +intro m; induct m. exact H1. exact (H2 0). -intros n IH. induct m. +intros n IH. intro m; induct m. now apply H3. exact (H2 (S n)). Qed. @@ -171,8 +171,8 @@ Theorem double_induction : (forall n, R (S n) 0) -> (forall n m, R n m -> R (S n) (S m)) -> forall n m, R n m. Proof. -intros H1 H2 H3; induct n; auto. -intros n H; cases m; auto. +intros H1 H2 H3 n; induct n; auto. +intros n H m; cases m; auto. Qed. End DoubleInduction. diff --git a/theories/Numbers/Natural/Abstract/NBits.v b/theories/Numbers/Natural/Abstract/NBits.v index 6e557a567e..313b9adfd1 100644 --- a/theories/Numbers/Natural/Abstract/NBits.v +++ b/theories/Numbers/Natural/Abstract/NBits.v @@ -190,7 +190,7 @@ Qed. Lemma bit0_odd : forall a, a.[0] = odd a. Proof. - intros. symmetry. + intros a. symmetry. destruct (exists_div2 a) as (a' & b & EQ). rewrite EQ, testbit_0_r, add_comm, odd_add_mul_2. destruct b; simpl; apply odd_1 || apply odd_0. @@ -272,14 +272,14 @@ Qed. Lemma mul_pow2_bits_high : forall a n m, n<=m -> (a*2^n).[m] = a.[m-n]. Proof. - intros. + intros a n m ?. rewrite <- (sub_add n m) at 1 by order'. now rewrite mul_pow2_bits_add. Qed. Lemma mul_pow2_bits_low : forall a n m, m<n -> (a*2^n).[m] = false. Proof. - intros. apply testbit_false. + intros a n m H. apply testbit_false. rewrite <- (sub_add m n) by order'. rewrite pow_add_r, mul_assoc. rewrite div_mul by order_nz. rewrite <- (succ_pred (n-m)). rewrite pow_succ_r. @@ -370,7 +370,10 @@ Qed. Hint Rewrite lxor_spec lor_spec land_spec ldiff_spec bits_0 : bitwise. -Ltac bitwise := apply bits_inj; intros ?m; autorewrite with bitwise. +Tactic Notation "bitwise" "as" simple_intropattern(m) + := apply bits_inj; intros m; autorewrite with bitwise. + +Ltac bitwise := bitwise as ?m. (** The streams of bits that correspond to a natural numbers are exactly the ones that are always 0 after some point *) @@ -418,7 +421,7 @@ Qed. Lemma shiftl_mul_pow2 : forall a n, a << n == a * 2^n. Proof. - intros. bitwise. + intros a n. bitwise as m. destruct (le_gt_cases n m) as [H|H]. now rewrite shiftl_spec_high', mul_pow2_bits_high. now rewrite shiftl_spec_low, mul_pow2_bits_low. @@ -455,7 +458,7 @@ Qed. Lemma shiftr_shiftl_l : forall a n m, m<=n -> (a << n) >> m == a << (n-m). Proof. - intros. + intros a n m ?. rewrite shiftr_div_pow2, !shiftl_mul_pow2. rewrite <- (sub_add m n) at 1 by trivial. now rewrite pow_add_r, mul_assoc, div_mul by order_nz. @@ -464,7 +467,7 @@ Qed. Lemma shiftr_shiftl_r : forall a n m, n<=m -> (a << n) >> m == a >> (m-n). Proof. - intros. + intros a n m ?. rewrite !shiftr_div_pow2, shiftl_mul_pow2. rewrite <- (sub_add n m) at 1 by trivial. rewrite pow_add_r, (mul_comm (2^(m-n))). @@ -630,7 +633,7 @@ Qed. Lemma lor_eq_0_l : forall a b, lor a b == 0 -> a == 0. Proof. - intros a b H. bitwise. + intros a b H. bitwise as m. apply (orb_false_iff a.[m] b.[m]). now rewrite <- lor_spec, H, bits_0. Qed. @@ -638,7 +641,7 @@ Qed. Lemma lor_eq_0_iff : forall a b, lor a b == 0 <-> a == 0 /\ b == 0. Proof. intros a b. split. - split. now apply lor_eq_0_l in H. + intro H; split. now apply lor_eq_0_l in H. rewrite lor_comm in H. now apply lor_eq_0_l in H. intros (EQ,EQ'). now rewrite EQ, lor_0_l. Qed. @@ -751,13 +754,13 @@ Proof. unfold clearbit. solve_proper. Qed. Lemma pow2_bits_true : forall n, (2^n).[n] = true. Proof. - intros. rewrite <- (mul_1_l (2^n)). rewrite <- (add_0_l n) at 2. + intros n. rewrite <- (mul_1_l (2^n)). rewrite <- (add_0_l n) at 2. now rewrite mul_pow2_bits_add, bit0_odd, odd_1. Qed. Lemma pow2_bits_false : forall n m, n~=m -> (2^n).[m] = false. Proof. - intros. + intros n m ?. rewrite <- (mul_1_l (2^n)). destruct (le_gt_cases n m). rewrite mul_pow2_bits_high; trivial. @@ -768,7 +771,7 @@ Qed. Lemma pow2_bits_eqb : forall n m, (2^n).[m] = eqb n m. Proof. - intros. apply eq_true_iff_eq. rewrite eqb_eq. split. + intros n m. apply eq_true_iff_eq. rewrite eqb_eq. split. destruct (eq_decidable n m) as [H|H]. trivial. now rewrite (pow2_bits_false _ _ H). intros EQ. rewrite EQ. apply pow2_bits_true. @@ -813,7 +816,7 @@ Qed. Lemma clearbit_eq : forall a n, (clearbit a n).[n] = false. Proof. - intros. rewrite clearbit_eqb, (proj2 (eqb_eq _ _) (eq_refl n)). + intros a n. rewrite clearbit_eqb, (proj2 (eqb_eq _ _) (eq_refl n)). apply andb_false_r. Qed. @@ -830,7 +833,7 @@ Qed. Lemma shiftl_lxor : forall a b n, (lxor a b) << n == lxor (a << n) (b << n). Proof. - intros. bitwise. + intros a b n. bitwise as m. destruct (le_gt_cases n m). now rewrite !shiftl_spec_high', lxor_spec. now rewrite !shiftl_spec_low. @@ -845,7 +848,7 @@ Qed. Lemma shiftl_land : forall a b n, (land a b) << n == land (a << n) (b << n). Proof. - intros. bitwise. + intros a b n. bitwise as m. destruct (le_gt_cases n m). now rewrite !shiftl_spec_high', land_spec. now rewrite !shiftl_spec_low. @@ -860,7 +863,7 @@ Qed. Lemma shiftl_lor : forall a b n, (lor a b) << n == lor (a << n) (b << n). Proof. - intros. bitwise. + intros a b n. bitwise as m. destruct (le_gt_cases n m). now rewrite !shiftl_spec_high', lor_spec. now rewrite !shiftl_spec_low. @@ -875,7 +878,7 @@ Qed. Lemma shiftl_ldiff : forall a b n, (ldiff a b) << n == ldiff (a << n) (b << n). Proof. - intros. bitwise. + intros a b n. bitwise as m. destruct (le_gt_cases n m). now rewrite !shiftl_spec_high', ldiff_spec. now rewrite !shiftl_spec_low. @@ -944,7 +947,7 @@ Qed. Lemma ones_spec_high : forall n m, n<=m -> (ones n).[m] = false. Proof. - intros. + intros n m ?. destruct (eq_0_gt_0_cases n) as [EQ|LT]; rewrite ones_equiv. now rewrite EQ, pow_0_r, one_succ, pred_succ, bits_0. apply bits_above_log2. @@ -973,7 +976,7 @@ Qed. Lemma lnot_involutive : forall a n, lnot (lnot a n) n == a. Proof. - intros a n. bitwise. + intros a n. bitwise as m. destruct (le_gt_cases n m). now rewrite 2 lnot_spec_high. now rewrite 2 lnot_spec_low, negb_involutive. @@ -994,7 +997,7 @@ Qed. Lemma lor_ones_low : forall a n, log2 a < n -> lor a (ones n) == ones n. Proof. - intros a n H. bitwise. destruct (le_gt_cases n m). + intros a n H. bitwise as m. destruct (le_gt_cases n m). rewrite ones_spec_high, bits_above_log2; trivial. now apply lt_le_trans with n. now rewrite ones_spec_low, orb_true_r. @@ -1002,7 +1005,7 @@ Qed. Lemma land_ones : forall a n, land a (ones n) == a mod 2^n. Proof. - intros a n. bitwise. destruct (le_gt_cases n m). + intros a n. bitwise as m. destruct (le_gt_cases n m). now rewrite ones_spec_high, mod_pow2_bits_high, andb_false_r. now rewrite ones_spec_low, mod_pow2_bits_low, andb_true_r. Qed. @@ -1017,7 +1020,7 @@ Qed. Lemma ldiff_ones_r : forall a n, ldiff a (ones n) == (a >> n) << n. Proof. - intros a n. bitwise. destruct (le_gt_cases n m). + intros a n. bitwise as m. destruct (le_gt_cases n m). rewrite ones_spec_high, shiftl_spec_high', shiftr_spec'; trivial. rewrite sub_add; trivial. apply andb_true_r. now rewrite ones_spec_low, shiftl_spec_low, andb_false_r. @@ -1026,7 +1029,7 @@ Qed. Lemma ldiff_ones_r_low : forall a n, log2 a < n -> ldiff a (ones n) == 0. Proof. - intros a n H. bitwise. destruct (le_gt_cases n m). + intros a n H. bitwise as m. destruct (le_gt_cases n m). rewrite ones_spec_high, bits_above_log2; trivial. now apply lt_le_trans with n. now rewrite ones_spec_low, andb_false_r. @@ -1035,7 +1038,7 @@ Qed. Lemma ldiff_ones_l_low : forall a n, log2 a < n -> ldiff (ones n) a == lnot a n. Proof. - intros a n H. bitwise. destruct (le_gt_cases n m). + intros a n H. bitwise as m. destruct (le_gt_cases n m). rewrite ones_spec_high, lnot_spec_high, bits_above_log2; trivial. now apply lt_le_trans with n. now rewrite ones_spec_low, lnot_spec_low. @@ -1044,7 +1047,7 @@ Qed. Lemma lor_lnot_diag : forall a n, lor a (lnot a n) == lor a (ones n). Proof. - intros a n. bitwise. + intros a n. bitwise as m. destruct (le_gt_cases n m). rewrite lnot_spec_high, ones_spec_high; trivial. now destruct a.[m]. rewrite lnot_spec_low, ones_spec_low; trivial. now destruct a.[m]. @@ -1059,7 +1062,7 @@ Qed. Lemma land_lnot_diag : forall a n, land a (lnot a n) == ldiff a (ones n). Proof. - intros a n. bitwise. + intros a n. bitwise as m. destruct (le_gt_cases n m). rewrite lnot_spec_high, ones_spec_high; trivial. now destruct a.[m]. rewrite lnot_spec_low, ones_spec_low; trivial. now destruct a.[m]. @@ -1074,7 +1077,7 @@ Qed. Lemma lnot_lor_low : forall a b n, log2 a < n -> log2 b < n -> lnot (lor a b) n == land (lnot a n) (lnot b n). Proof. - intros a b n Ha Hb. bitwise. destruct (le_gt_cases n m). + intros a b n Ha Hb. bitwise as m. destruct (le_gt_cases n m). rewrite !lnot_spec_high, lor_spec, !bits_above_log2; trivial. now apply lt_le_trans with n. now apply lt_le_trans with n. @@ -1084,7 +1087,7 @@ Qed. Lemma lnot_land_low : forall a b n, log2 a < n -> log2 b < n -> lnot (land a b) n == lor (lnot a n) (lnot b n). Proof. - intros a b n Ha Hb. bitwise. destruct (le_gt_cases n m). + intros a b n Ha Hb. bitwise as m. destruct (le_gt_cases n m). rewrite !lnot_spec_high, land_spec, !bits_above_log2; trivial. now apply lt_le_trans with n. now apply lt_le_trans with n. @@ -1094,7 +1097,7 @@ Qed. Lemma ldiff_land_low : forall a b n, log2 a < n -> ldiff a b == land a (lnot b n). Proof. - intros a b n Ha. bitwise. destruct (le_gt_cases n m). + intros a b n Ha. bitwise as m. destruct (le_gt_cases n m). rewrite (bits_above_log2 a m). trivial. now apply lt_le_trans with n. rewrite !lnot_spec_low; trivial. @@ -1103,7 +1106,7 @@ Qed. Lemma lnot_ldiff_low : forall a b n, log2 a < n -> log2 b < n -> lnot (ldiff a b) n == lor (lnot a n) b. Proof. - intros a b n Ha Hb. bitwise. destruct (le_gt_cases n m). + intros a b n Ha Hb. bitwise as m. destruct (le_gt_cases n m). rewrite !lnot_spec_high, ldiff_spec, !bits_above_log2; trivial. now apply lt_le_trans with n. now apply lt_le_trans with n. @@ -1113,7 +1116,7 @@ Qed. Lemma lxor_lnot_lnot : forall a b n, lxor (lnot a n) (lnot b n) == lxor a b. Proof. - intros a b n. bitwise. destruct (le_gt_cases n m). + intros a b n. bitwise as m. destruct (le_gt_cases n m). rewrite !lnot_spec_high; trivial. rewrite !lnot_spec_low, xorb_negb_negb; trivial. Qed. @@ -1121,7 +1124,7 @@ Qed. Lemma lnot_lxor_l : forall a b n, lnot (lxor a b) n == lxor (lnot a n) b. Proof. - intros a b n. bitwise. destruct (le_gt_cases n m). + intros a b n. bitwise as m. destruct (le_gt_cases n m). rewrite !lnot_spec_high, lxor_spec; trivial. rewrite !lnot_spec_low, lxor_spec, negb_xorb_l; trivial. Qed. @@ -1129,7 +1132,7 @@ Qed. Lemma lnot_lxor_r : forall a b n, lnot (lxor a b) n == lxor a (lnot b n). Proof. - intros a b n. bitwise. destruct (le_gt_cases n m). + intros a b n. bitwise as m. destruct (le_gt_cases n m). rewrite !lnot_spec_high, lxor_spec; trivial. rewrite !lnot_spec_low, lxor_spec, negb_xorb_r; trivial. Qed. @@ -1137,7 +1140,7 @@ Qed. Lemma lxor_lor : forall a b, land a b == 0 -> lxor a b == lor a b. Proof. - intros a b H. bitwise. + intros a b H. bitwise as m. assert (a.[m] && b.[m] = false) by now rewrite <- land_spec, H, bits_0. now destruct a.[m], b.[m]. @@ -1264,7 +1267,7 @@ Qed. Lemma add_carry_div2 : forall a b (c0:bool), (a + b + c0)/2 == a/2 + b/2 + nextcarry a.[0] b.[0] c0. Proof. - intros. + intros a b c0. rewrite <- add3_bits_div2. rewrite (add_comm ((a/2)+_)). rewrite <- div_add by order'. @@ -1312,7 +1315,7 @@ Proof. apply div_lt_upper_bound; trivial. order'. now rewrite <- pow_succ_r'. exists (c0 + 2*c). repeat split. (* - add *) - bitwise. + bitwise as m. destruct (zero_or_succ m) as [EQ|[m' EQ]]; rewrite EQ; clear EQ. now rewrite add_b2n_double_bit0, add3_bit0, b2n_bit0. rewrite <- !div2_bits, <- 2 lxor_spec. @@ -1320,7 +1323,7 @@ Proof. rewrite add_b2n_double_div2, <- IH1. apply add_carry_div2. (* - carry *) rewrite add_b2n_double_div2. - bitwise. + bitwise as m. destruct (zero_or_succ m) as [EQ|[m' EQ]]; rewrite EQ; clear EQ. now rewrite add_b2n_double_bit0. rewrite <- !div2_bits, IH2. autorewrite with bitwise. @@ -1356,7 +1359,7 @@ Proof. symmetry in H. now apply lor_eq_0_l in H. intros EQ. rewrite EQ, lor_0_l in H. apply bits_inj_0. - induct n. trivial. + intro n; induct n. trivial. intros n IH. rewrite <- div2_bits, H. autorewrite with bitwise. @@ -1381,7 +1384,7 @@ Lemma ldiff_le : forall a b, ldiff a b == 0 -> a <= b. Proof. cut (forall n a b, a < 2^n -> ldiff a b == 0 -> a <= b). intros H a b. apply (H a), pow_gt_lin_r; order'. - induct n. + intro n; induct n. intros a b Ha _. rewrite pow_0_r, one_succ, lt_succ_r in Ha. assert (Ha' : a == 0) by (generalize (le_0_l a); order'). rewrite Ha'. apply le_0_l. @@ -1410,7 +1413,7 @@ Proof. rewrite sub_add. symmetry. rewrite add_nocarry_lxor. - bitwise. + bitwise as m. apply bits_inj_iff in H. specialize (H m). rewrite ldiff_spec, bits_0 in H. now destruct a.[m], b.[m]. @@ -1454,7 +1457,7 @@ Lemma add_nocarry_mod_lt_pow2 : forall a b n, land a b == 0 -> Proof. intros a b n H. apply add_nocarry_lt_pow2. - bitwise. + bitwise as m. destruct (le_gt_cases n m). now rewrite mod_pow2_bits_high. now rewrite !mod_pow2_bits_low, <- land_spec, H, bits_0. diff --git a/theories/Numbers/Natural/Abstract/NDiv.v b/theories/Numbers/Natural/Abstract/NDiv.v index 9c50d5ca58..bb2f32935f 100644 --- a/theories/Numbers/Natural/Abstract/NDiv.v +++ b/theories/Numbers/Natural/Abstract/NDiv.v @@ -39,15 +39,15 @@ Qed. Theorem div_mod_unique : forall b q1 q2 r1 r2, r1<b -> r2<b -> b*q1+r1 == b*q2+r2 -> q1 == q2 /\ r1 == r2. -Proof. intros. apply div_mod_unique with b; auto'. Qed. +Proof. intros b q1 q2 r1 r2 ? ? ?. apply div_mod_unique with b; auto'. Qed. Theorem div_unique: forall a b q r, r<b -> a == b*q + r -> q == a/b. -Proof. intros; apply div_unique with r; auto'. Qed. +Proof. intros a b q r ? ?; apply div_unique with r; auto'. Qed. Theorem mod_unique: forall a b q r, r<b -> a == b*q + r -> r == a mod b. -Proof. intros. apply mod_unique with q; auto'. Qed. +Proof. intros a b q r ? ?. apply mod_unique with q; auto'. Qed. Theorem div_unique_exact: forall a b q, b~=0 -> a == b*q -> q == a/b. Proof. intros. apply div_unique_exact; auto'. Qed. diff --git a/theories/Numbers/Natural/Abstract/NGcd.v b/theories/Numbers/Natural/Abstract/NGcd.v index a80ae8dc45..c1d8308e34 100644 --- a/theories/Numbers/Natural/Abstract/NGcd.v +++ b/theories/Numbers/Natural/Abstract/NGcd.v @@ -53,7 +53,7 @@ Definition divide_gcd_iff' n m := divide_gcd_iff n m (le_0_l n). Lemma gcd_add_mult_diag_r : forall n m p, gcd n (m+p*n) == gcd n m. Proof. - intros. apply gcd_unique_alt'. + intros n m p. apply gcd_unique_alt'. intros. rewrite gcd_divide_iff. split; intros (U,V); split; trivial. apply divide_add_r; trivial. now apply divide_mul_r. apply divide_add_cancel_r with (p*n); trivial. @@ -98,11 +98,11 @@ Lemma gcd_bezout_pos_pos : forall n, 0<n -> forall m, 0<m -> Bezout n m (gcd n m) /\ Bezout m n (gcd n m). Proof. intros n Hn. rewrite <- le_succ_l, <- one_succ in Hn. - pattern n. apply strong_right_induction with (z:=1); trivial. + pattern n. apply (fun H => strong_right_induction _ H 1); trivial. unfold Bezout. solve_proper. clear n Hn. intros n Hn IHn. intros m Hm. rewrite <- le_succ_l, <- one_succ in Hm. - pattern m. apply strong_right_induction with (z:=1); trivial. + pattern m. apply (fun H => strong_right_induction _ H 1); trivial. unfold Bezout. solve_proper. clear m Hm. intros m Hm IHm. destruct (lt_trichotomy n m) as [LT|[EQ|LT]]. @@ -156,7 +156,7 @@ Qed. Theorem bezout_comm : forall a b g, b ~= 0 -> Bezout a b g -> Bezout b a g. Proof. - intros * Hbz (u & v & Huv). + intros a b g Hbz (u & v & Huv). destruct (eq_0_gt_0_cases a) as [Haz| Haz]. -rewrite Haz in Huv |-*. rewrite mul_0_r in Huv; symmetry in Huv. @@ -260,7 +260,7 @@ Qed. Lemma gcd_mul_mono_r : forall n m p, gcd (n*p) (m*p) == gcd n m * p. Proof. - intros. rewrite !(mul_comm _ p). apply gcd_mul_mono_l. + intros n m p. rewrite !(mul_comm _ p). apply gcd_mul_mono_l. Qed. Lemma gauss : forall n m p, (n | m * p) -> gcd n m == 1 -> (n | p). diff --git a/theories/Numbers/Natural/Abstract/NLcm.v b/theories/Numbers/Natural/Abstract/NLcm.v index 3a9cf34b25..b75b4521df 100644 --- a/theories/Numbers/Natural/Abstract/NLcm.v +++ b/theories/Numbers/Natural/Abstract/NLcm.v @@ -169,7 +169,7 @@ Qed. Lemma lcm_divide_iff : forall n m p, (lcm n m | p) <-> (n | p) /\ (m | p). Proof. - intros. split. split. + intros n m p. split. split. transitivity (lcm n m); trivial using divide_lcm_l. transitivity (lcm n m); trivial using divide_lcm_r. intros (H,H'). now apply lcm_least. diff --git a/theories/Numbers/Natural/Abstract/NMaxMin.v b/theories/Numbers/Natural/Abstract/NMaxMin.v index ad6e2d65f0..3a41a2a560 100644 --- a/theories/Numbers/Natural/Abstract/NMaxMin.v +++ b/theories/Numbers/Natural/Abstract/NMaxMin.v @@ -42,95 +42,95 @@ Qed. (** Succ *) -Lemma succ_max_distr : forall n m, S (max n m) == max (S n) (S m). +Lemma succ_max_distr n m : S (max n m) == max (S n) (S m). Proof. - intros. destruct (le_ge_cases n m); + destruct (le_ge_cases n m); [rewrite 2 max_r | rewrite 2 max_l]; now rewrite <- ?succ_le_mono. Qed. -Lemma succ_min_distr : forall n m, S (min n m) == min (S n) (S m). +Lemma succ_min_distr n m : S (min n m) == min (S n) (S m). Proof. - intros. destruct (le_ge_cases n m); + destruct (le_ge_cases n m); [rewrite 2 min_l | rewrite 2 min_r]; now rewrite <- ?succ_le_mono. Qed. (** Add *) -Lemma add_max_distr_l : forall n m p, max (p + n) (p + m) == p + max n m. +Lemma add_max_distr_l n m p : max (p + n) (p + m) == p + max n m. Proof. - intros. destruct (le_ge_cases n m); + destruct (le_ge_cases n m); [rewrite 2 max_r | rewrite 2 max_l]; now rewrite <- ?add_le_mono_l. Qed. -Lemma add_max_distr_r : forall n m p, max (n + p) (m + p) == max n m + p. +Lemma add_max_distr_r n m p : max (n + p) (m + p) == max n m + p. Proof. - intros. destruct (le_ge_cases n m); + destruct (le_ge_cases n m); [rewrite 2 max_r | rewrite 2 max_l]; now rewrite <- ?add_le_mono_r. Qed. -Lemma add_min_distr_l : forall n m p, min (p + n) (p + m) == p + min n m. +Lemma add_min_distr_l n m p : min (p + n) (p + m) == p + min n m. Proof. - intros. destruct (le_ge_cases n m); + destruct (le_ge_cases n m); [rewrite 2 min_l | rewrite 2 min_r]; now rewrite <- ?add_le_mono_l. Qed. -Lemma add_min_distr_r : forall n m p, min (n + p) (m + p) == min n m + p. +Lemma add_min_distr_r n m p : min (n + p) (m + p) == min n m + p. Proof. - intros. destruct (le_ge_cases n m); + destruct (le_ge_cases n m); [rewrite 2 min_l | rewrite 2 min_r]; now rewrite <- ?add_le_mono_r. Qed. (** Mul *) -Lemma mul_max_distr_l : forall n m p, max (p * n) (p * m) == p * max n m. +Lemma mul_max_distr_l n m p : max (p * n) (p * m) == p * max n m. Proof. - intros. destruct (le_ge_cases n m); + destruct (le_ge_cases n m); [rewrite 2 max_r | rewrite 2 max_l]; try order; now apply mul_le_mono_l. Qed. -Lemma mul_max_distr_r : forall n m p, max (n * p) (m * p) == max n m * p. +Lemma mul_max_distr_r n m p : max (n * p) (m * p) == max n m * p. Proof. - intros. destruct (le_ge_cases n m); + destruct (le_ge_cases n m); [rewrite 2 max_r | rewrite 2 max_l]; try order; now apply mul_le_mono_r. Qed. -Lemma mul_min_distr_l : forall n m p, min (p * n) (p * m) == p * min n m. +Lemma mul_min_distr_l n m p : min (p * n) (p * m) == p * min n m. Proof. - intros. destruct (le_ge_cases n m); + destruct (le_ge_cases n m); [rewrite 2 min_l | rewrite 2 min_r]; try order; now apply mul_le_mono_l. Qed. -Lemma mul_min_distr_r : forall n m p, min (n * p) (m * p) == min n m * p. +Lemma mul_min_distr_r n m p : min (n * p) (m * p) == min n m * p. Proof. - intros. destruct (le_ge_cases n m); + destruct (le_ge_cases n m); [rewrite 2 min_l | rewrite 2 min_r]; try order; now apply mul_le_mono_r. Qed. (** Sub *) -Lemma sub_max_distr_l : forall n m p, max (p - n) (p - m) == p - min n m. +Lemma sub_max_distr_l n m p : max (p - n) (p - m) == p - min n m. Proof. - intros. destruct (le_ge_cases n m). + destruct (le_ge_cases n m). rewrite min_l by trivial. apply max_l. now apply sub_le_mono_l. rewrite min_r by trivial. apply max_r. now apply sub_le_mono_l. Qed. -Lemma sub_max_distr_r : forall n m p, max (n - p) (m - p) == max n m - p. +Lemma sub_max_distr_r n m p : max (n - p) (m - p) == max n m - p. Proof. - intros. destruct (le_ge_cases n m); + destruct (le_ge_cases n m); [rewrite 2 max_r | rewrite 2 max_l]; try order; now apply sub_le_mono_r. Qed. -Lemma sub_min_distr_l : forall n m p, min (p - n) (p - m) == p - max n m. +Lemma sub_min_distr_l n m p : min (p - n) (p - m) == p - max n m. Proof. - intros. destruct (le_ge_cases n m). + destruct (le_ge_cases n m). rewrite max_r by trivial. apply min_r. now apply sub_le_mono_l. rewrite max_l by trivial. apply min_l. now apply sub_le_mono_l. Qed. -Lemma sub_min_distr_r : forall n m p, min (n - p) (m - p) == min n m - p. +Lemma sub_min_distr_r n m p : min (n - p) (m - p) == min n m - p. Proof. - intros. destruct (le_ge_cases n m); + destruct (le_ge_cases n m); [rewrite 2 min_l | rewrite 2 min_r]; try order; now apply sub_le_mono_r. Qed. diff --git a/theories/Numbers/Natural/Abstract/NOrder.v b/theories/Numbers/Natural/Abstract/NOrder.v index 9a9a882239..ccdac104a3 100644 --- a/theories/Numbers/Natural/Abstract/NOrder.v +++ b/theories/Numbers/Natural/Abstract/NOrder.v @@ -46,19 +46,19 @@ Qed. Theorem lt_0_succ : forall n, 0 < S n. Proof. -induct n; [apply lt_succ_diag_r | intros n H; now apply lt_lt_succ_r]. +intro n; induct n; [apply lt_succ_diag_r | intros n H; now apply lt_lt_succ_r]. Qed. Theorem neq_0_lt_0 : forall n, n ~= 0 <-> 0 < n. Proof. -cases n. +intro n; cases n. split; intro H; [now elim H | intro; now apply lt_irrefl with 0]. intro n; split; intro H; [apply lt_0_succ | apply neq_succ_0]. Qed. Theorem eq_0_gt_0_cases : forall n, n == 0 \/ 0 < n. Proof. -cases n. +intro n; cases n. now left. intro; right; apply lt_0_succ. Qed. @@ -66,8 +66,8 @@ Qed. Theorem zero_one : forall n, n == 0 \/ n == 1 \/ 1 < n. Proof. setoid_rewrite one_succ. -induct n. now left. -cases n. intros; right; now left. +intro n; induct n. now left. +intro n; cases n. intros; right; now left. intros n IH. destruct IH as [H | [H | H]]. false_hyp H neq_succ_0. right; right. rewrite H. apply lt_succ_diag_r. @@ -77,7 +77,7 @@ Qed. Theorem lt_1_r : forall n, n < 1 <-> n == 0. Proof. setoid_rewrite one_succ. -cases n. +intro n; cases n. split; intro; [reflexivity | apply lt_succ_diag_r]. intros n. rewrite <- succ_lt_mono. split; intro H; [false_hyp H nlt_0_r | false_hyp H neq_succ_0]. @@ -86,7 +86,7 @@ Qed. Theorem le_1_r : forall n, n <= 1 <-> n == 0 \/ n == 1. Proof. setoid_rewrite one_succ. -cases n. +intro n; cases n. split; intro; [now left | apply le_succ_diag_r]. intro n. rewrite <- succ_le_mono, le_0_r, succ_inj_wd. split; [intro; now right | intros [H | H]; [false_hyp H neq_succ_0 | assumption]]. @@ -101,7 +101,7 @@ Qed. Theorem lt_1_l' : forall n m p, n < m -> m < p -> 1 < p. Proof. -intros. apply lt_1_l with m; auto. +intros n m p H H0. apply lt_1_l with m; auto. apply le_lt_trans with n; auto. now apply le_0_l. Qed. @@ -117,7 +117,7 @@ Theorem le_ind_rel : (forall n m, n <= m -> R n m -> R (S n) (S m)) -> forall n m, n <= m -> R n m. Proof. -intros Base Step; induct n. +intros Base Step n; induct n. intros; apply Base. intros n IH m H. elim H using le_ind. solve_proper. @@ -130,7 +130,7 @@ Theorem lt_ind_rel : (forall n m, n < m -> R n m -> R (S n) (S m)) -> forall n m, n < m -> R n m. Proof. -intros Base Step; induct n. +intros Base Step n; induct n. intros m H. apply lt_exists_pred in H; destruct H as [m' [H _]]. rewrite H; apply Base. intros n IH m H. elim H using lt_ind. @@ -151,14 +151,14 @@ Qed. Theorem le_pred_l : forall n, P n <= n. Proof. -cases n. +intro n; cases n. rewrite pred_0; now apply eq_le_incl. intros; rewrite pred_succ; apply le_succ_diag_r. Qed. Theorem lt_pred_l : forall n, n ~= 0 -> P n < n. Proof. -cases n. +intro n; cases n. intro H; exfalso; now apply H. intros; rewrite pred_succ; apply lt_succ_diag_r. Qed. @@ -176,7 +176,7 @@ Qed. Theorem lt_le_pred : forall n m, n < m -> n <= P m. (* Converse is false for n == m == 0 *) Proof. -intro n; cases m. +intros n m; cases m. intro H; false_hyp H nlt_0_r. intros m IH. rewrite pred_succ; now apply lt_succ_r. Qed. diff --git a/theories/Numbers/Natural/Abstract/NParity.v b/theories/Numbers/Natural/Abstract/NParity.v index 58bc1499e1..4bb465c93c 100644 --- a/theories/Numbers/Natural/Abstract/NParity.v +++ b/theories/Numbers/Natural/Abstract/NParity.v @@ -16,19 +16,19 @@ Module Type NParityProp (Import N : NAxiomsSig')(Import NP : NSubProp N). Include NZParityProp N N NP. -Lemma odd_pred : forall n, n~=0 -> odd (P n) = even n. +Lemma odd_pred n : n~=0 -> odd (P n) = even n. Proof. intros. rewrite <- (succ_pred n) at 2 by trivial. symmetry. apply even_succ. Qed. -Lemma even_pred : forall n, n~=0 -> even (P n) = odd n. +Lemma even_pred n : n~=0 -> even (P n) = odd n. Proof. intros. rewrite <- (succ_pred n) at 2 by trivial. symmetry. apply odd_succ. Qed. -Lemma even_sub : forall n m, m<=n -> even (n-m) = Bool.eqb (even n) (even m). +Lemma even_sub n m : m<=n -> even (n-m) = Bool.eqb (even n) (even m). Proof. intros. case_eq (even n); case_eq (even m); @@ -56,7 +56,7 @@ Proof. rewrite add_1_r in Hm,Hn. order. Qed. -Lemma odd_sub : forall n m, m<=n -> odd (n-m) = xorb (odd n) (odd m). +Lemma odd_sub n m : m<=n -> odd (n-m) = xorb (odd n) (odd m). Proof. intros. rewrite <- !negb_even. rewrite even_sub by trivial. now destruct (even n), (even m). diff --git a/theories/Numbers/Natural/Abstract/NPow.v b/theories/Numbers/Natural/Abstract/NPow.v index 0b7720fd57..b49b6bf03c 100644 --- a/theories/Numbers/Natural/Abstract/NPow.v +++ b/theories/Numbers/Natural/Abstract/NPow.v @@ -55,7 +55,7 @@ Proof. wrap pow_mul_r. Qed. (** Power and nullity *) Lemma pow_eq_0 : forall a b, b~=0 -> a^b == 0 -> a == 0. -Proof. intros. apply (pow_eq_0 a b); trivial. auto'. Qed. +Proof. intros a b ? ?. apply (pow_eq_0 a b); trivial. auto'. Qed. Lemma pow_nonzero : forall a b, a~=0 -> a^b ~= 0. Proof. wrap pow_nonzero. Qed. diff --git a/theories/Numbers/Natural/Abstract/NSub.v b/theories/Numbers/Natural/Abstract/NSub.v index e06604db53..b939352144 100644 --- a/theories/Numbers/Natural/Abstract/NSub.v +++ b/theories/Numbers/Natural/Abstract/NSub.v @@ -17,21 +17,21 @@ Include NMulOrderProp N. Theorem sub_0_l : forall n, 0 - n == 0. Proof. -induct n. +intro n; induct n. apply sub_0_r. intros n IH; rewrite sub_succ_r; rewrite IH. now apply pred_0. Qed. Theorem sub_succ : forall n m, S n - S m == n - m. Proof. -intro n; induct m. +intros n m; induct m. rewrite sub_succ_r. do 2 rewrite sub_0_r. now rewrite pred_succ. intros m IH. rewrite sub_succ_r. rewrite IH. now rewrite sub_succ_r. Qed. Theorem sub_diag : forall n, n - n == 0. Proof. -induct n. apply sub_0_r. intros n IH; rewrite sub_succ; now rewrite IH. +intro n; induct n. apply sub_0_r. intros n IH; rewrite sub_succ; now rewrite IH. Qed. Theorem sub_gt : forall n m, n > m -> n - m ~= 0. @@ -96,7 +96,7 @@ Qed. Theorem sub_add_distr : forall n m p, n - (m + p) == (n - m) - p. Proof. -intros n m; induct p. +intros n m p; induct p. rewrite add_0_r; now rewrite sub_0_r. intros p IH. rewrite add_succ_r; do 2 rewrite sub_succ_r. now rewrite IH. Qed. @@ -113,7 +113,7 @@ Qed. Theorem le_sub_l : forall n m, n - m <= n. Proof. -intro n; induct m. +intros n m; induct m. rewrite sub_0_r; now apply eq_le_incl. intros m IH. rewrite sub_succ_r. apply le_trans with (n - m); [apply le_pred_l | assumption]. @@ -121,7 +121,7 @@ Qed. Theorem sub_0_le : forall n m, n - m == 0 <-> n <= m. Proof. -double_induct n m. +intros n m; double_induct n m. intro m; split; intro; [apply le_0_l | apply sub_0_l]. intro m; rewrite sub_0_r; split; intro H; [false_hyp H neq_succ_0 | false_hyp H nle_succ_0]. @@ -130,7 +130,7 @@ Qed. Theorem sub_add_le : forall n m, n <= n - m + m. Proof. -intros. +intros n m. destruct (le_ge_cases n m) as [LE|GE]. rewrite <- sub_0_le in LE. rewrite LE; nzsimpl. now rewrite <- sub_0_le. @@ -216,12 +216,13 @@ Qed. Lemma sub_le_mono_r : forall n m p, n <= m -> n-p <= m-p. Proof. - intros. rewrite le_sub_le_add_r. transitivity m. assumption. apply sub_add_le. + intros n m p. rewrite le_sub_le_add_r. + transitivity m. assumption. apply sub_add_le. Qed. Lemma sub_le_mono_l : forall n m p, n <= m -> p-m <= p-n. Proof. - intros. rewrite le_sub_le_add_r. + intros n m p. rewrite le_sub_le_add_r. transitivity (p-n+n); [ apply sub_add_le | now apply add_le_mono_l]. Qed. @@ -264,14 +265,14 @@ Definition lt_alt n m := exists p, S p + n == m. Lemma le_equiv : forall n m, le_alt n m <-> n <= m. Proof. -split. +intros n m; split. intros (p,H). rewrite <- H, add_comm. apply le_add_r. intro H. exists (m-n). now apply sub_add. Qed. Lemma lt_equiv : forall n m, lt_alt n m <-> n < m. Proof. -split. +intros n m; split. intros (p,H). rewrite <- H, add_succ_l, lt_succ_r, add_comm. apply le_add_r. intro H. exists (m-S n). rewrite add_succ_l, <- add_succ_r. apply sub_add. now rewrite le_succ_l. |