diff options
Diffstat (limited to 'theories/Numbers/Natural/Abstract')
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NAdd.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NBase.v | 10 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NDefOps.v | 15 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NMulOrder.v | 4 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NOrder.v | 3 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NParity.v | 22 |
6 files changed, 28 insertions, 28 deletions
diff --git a/theories/Numbers/Natural/Abstract/NAdd.v b/theories/Numbers/Natural/Abstract/NAdd.v index 96d60c9979..fbe71a4c70 100644 --- a/theories/Numbers/Natural/Abstract/NAdd.v +++ b/theories/Numbers/Natural/Abstract/NAdd.v @@ -45,7 +45,7 @@ Qed. Theorem eq_add_1 : forall n m, n + m == 1 -> n == 1 /\ m == 0 \/ n == 0 /\ m == 1. Proof. -intros n m H. +intros n m. rewrite one_succ. intro H. assert (H1 : exists p, n + m == S p) by now exists 0. apply -> eq_add_succ in H1. destruct H1 as [[n' H1] | [m' H1]]. left. rewrite H1 in H; rewrite add_succ_l in H; apply succ_inj in H. diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v index e9ec6a823e..7ed563be5e 100644 --- a/theories/Numbers/Natural/Abstract/NBase.v +++ b/theories/Numbers/Natural/Abstract/NBase.v @@ -94,12 +94,11 @@ Qed. Theorem eq_pred_0 : forall n, P n == 0 <-> n == 0 \/ n == 1. Proof. cases n. -rewrite pred_0. setoid_replace (0 == 1) with False using relation iff. tauto. -split; intro H; [symmetry in H; false_hyp H neq_succ_0 | elim H]. +rewrite pred_0. now split; [left|]. intro n. rewrite pred_succ. -setoid_replace (S n == 0) with False using relation iff by - (apply -> neg_false; apply neq_succ_0). -rewrite succ_inj_wd. tauto. +split. intros H; right. now rewrite H, one_succ. +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. @@ -130,6 +129,7 @@ Theorem pair_induction : A 0 -> A 1 -> (forall n, A n -> A (S n) -> A (S (S n))) -> forall n, A n. 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. diff --git a/theories/Numbers/Natural/Abstract/NDefOps.v b/theories/Numbers/Natural/Abstract/NDefOps.v index c1bac7165a..8d11b5ce33 100644 --- a/theories/Numbers/Natural/Abstract/NDefOps.v +++ b/theories/Numbers/Natural/Abstract/NDefOps.v @@ -308,7 +308,7 @@ Qed. Theorem half_1 : half 1 == 0. Proof. -unfold half. rewrite half_aux_succ, half_aux_0; simpl; auto with *. +unfold half. rewrite one_succ, half_aux_succ, half_aux_0; simpl; auto with *. Qed. Theorem half_double : forall n, @@ -346,9 +346,8 @@ assert (LE : 0 <= half n) by apply le_0_l. le_elim LE; auto. destruct (half_double n) as [E|E]; rewrite <- LE, mul_0_r, ?add_0_r in E; rewrite E in LT. -destruct (nlt_0_r _ LT). -rewrite <- succ_lt_mono in LT. -destruct (nlt_0_r _ LT). +order'. +order. Qed. Theorem half_decrease : forall n, 0 < n -> half n < n. @@ -359,11 +358,11 @@ destruct (half_double n) as [E|E]; rewrite E at 2; rewrite <- add_0_l at 1. rewrite <- add_lt_mono_r. assert (LE : 0 <= half n) by apply le_0_l. -le_elim LE; auto. +nzsimpl. le_elim LE; auto. rewrite <- LE, mul_0_r in E. rewrite E in LT. destruct (nlt_0_r _ LT). rewrite <- add_0_l at 1. rewrite <- add_lt_mono_r. -rewrite add_succ_l. apply lt_0_succ. +nzsimpl. apply lt_0_succ. Qed. @@ -437,7 +436,7 @@ destruct (n<<2) as [ ]_eqn:H. auto with *. apply succ_wd, E, half_decrease. rewrite <- not_true_iff_false, ltb_lt, nlt_ge, le_succ_l in H. -apply lt_succ_l; auto. +order'. Qed. Hint Resolve log_good_step. @@ -468,7 +467,7 @@ intros n IH k Hk1 Hk2. destruct (lt_ge_cases k 2) as [LT|LE]. (* base *) rewrite log_init, pow_0 by auto. -rewrite <- le_succ_l in Hk2. +rewrite <- le_succ_l, <- one_succ in Hk2. le_elim Hk2. rewrite <- nle_gt, le_succ_l in LT. destruct LT; auto. rewrite <- Hk2. diff --git a/theories/Numbers/Natural/Abstract/NMulOrder.v b/theories/Numbers/Natural/Abstract/NMulOrder.v index f6c6ad5428..6ecdef9ef0 100644 --- a/theories/Numbers/Natural/Abstract/NMulOrder.v +++ b/theories/Numbers/Natural/Abstract/NMulOrder.v @@ -65,10 +65,10 @@ Proof. intros n m. split; [| intros [H1 H2]; now rewrite H1, H2, mul_1_l]. intro H; destruct (lt_trichotomy n 1) as [H1 | [H1 | H1]]. -apply -> lt_1_r in H1. rewrite H1, mul_0_l in H. false_hyp H neq_0_succ. +apply -> lt_1_r in H1. rewrite H1, mul_0_l in H. order'. rewrite H1, mul_1_l in H; now split. destruct (eq_0_gt_0_cases m) as [H2 | H2]. -rewrite H2, mul_0_r in H; false_hyp H neq_0_succ. +rewrite H2, mul_0_r in H. order'. apply -> (mul_lt_mono_pos_r m) in H1; [| assumption]. rewrite mul_1_l in H1. assert (H3 : 1 < n * m) by now apply (lt_1_l m). rewrite H in H3; false_hyp H3 lt_irrefl. diff --git a/theories/Numbers/Natural/Abstract/NOrder.v b/theories/Numbers/Natural/Abstract/NOrder.v index fa855f2105..2816af7c47 100644 --- a/theories/Numbers/Natural/Abstract/NOrder.v +++ b/theories/Numbers/Natural/Abstract/NOrder.v @@ -63,6 +63,7 @@ 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. intros n IH. destruct IH as [H | [H | H]]. @@ -73,6 +74,7 @@ Qed. Theorem lt_1_r : forall n, n < 1 <-> n == 0. Proof. +setoid_rewrite one_succ. cases n. split; intro; [reflexivity | apply lt_succ_diag_r]. intros n. rewrite <- succ_lt_mono. @@ -81,6 +83,7 @@ Qed. Theorem le_1_r : forall n, n <= 1 <-> n == 0 \/ n == 1. Proof. +setoid_rewrite one_succ. cases n. split; intro; [now left | apply le_succ_diag_r]. intro n. rewrite <- succ_le_mono, le_0_r, succ_inj_wd. diff --git a/theories/Numbers/Natural/Abstract/NParity.v b/theories/Numbers/Natural/Abstract/NParity.v index e815f9ee6a..bd65886867 100644 --- a/theories/Numbers/Natural/Abstract/NParity.v +++ b/theories/Numbers/Natural/Abstract/NParity.v @@ -40,17 +40,17 @@ Proof. intros x. intros [(y,H)|(y,H)]. right. exists y. rewrite H. now nzsimpl. - left. exists (S y). rewrite H. now nzsimpl. + left. exists (S y). rewrite H. now nzsimpl'. Qed. Lemma double_below : forall n m, n<=m -> 2*n < 2*m+1. Proof. - intros. nzsimpl. apply lt_succ_r. now apply add_le_mono. + intros. nzsimpl'. apply lt_succ_r. now apply add_le_mono. Qed. Lemma double_above : forall n m, n<m -> 2*n+1 < 2*m. Proof. - intros. nzsimpl. + intros. nzsimpl'. rewrite <- le_succ_l, <- add_succ_l, <- add_succ_r. apply add_le_mono; now apply le_succ_l. Qed. @@ -91,7 +91,7 @@ Qed. Lemma odd_1 : odd 1 = true. Proof. - rewrite odd_spec. exists 0. now nzsimpl. + rewrite odd_spec. exists 0. now nzsimpl'. Qed. Lemma Odd_succ_Even : forall n, Odd (S n) <-> Even n. @@ -138,7 +138,7 @@ Proof. exists (n'+m'). now rewrite mul_add_distr_l, Hn, Hm. exists (n'+m'). now rewrite mul_add_distr_l, Hn, Hm, add_assoc. exists (n'+m'). now rewrite mul_add_distr_l, Hn, Hm, add_shuffle0. - exists (n'+m'+1). rewrite Hm,Hn. nzsimpl. now rewrite add_shuffle1. + exists (n'+m'+1). rewrite Hm,Hn. nzsimpl'. now rewrite add_shuffle1. Qed. Lemma odd_add : forall n m, odd (n+m) = xorb (odd n) (odd m). @@ -176,19 +176,17 @@ Proof. exists (n'-m'). now rewrite mul_sub_distr_l, Hn, Hm. exists (n'-m'-1). rewrite !mul_sub_distr_l, Hn, Hm, sub_add_distr, mul_1_r. - rewrite <- (add_1_l 1) at 5. rewrite sub_add_distr. + rewrite two_succ at 5. rewrite <- (add_1_l 1). rewrite sub_add_distr. symmetry. apply sub_add. apply le_add_le_sub_l. - rewrite add_1_l, <- (mul_1_r 2) at 1. - rewrite <- mul_sub_distr_l. rewrite <- mul_le_mono_pos_l. - rewrite le_succ_l. rewrite <- lt_add_lt_sub_l, add_0_r. + rewrite add_1_l, <- two_succ, <- (mul_1_r 2) at 1. + rewrite <- mul_sub_distr_l. rewrite <- mul_le_mono_pos_l by order'. + rewrite one_succ, le_succ_l. rewrite <- lt_add_lt_sub_l, add_0_r. destruct (le_gt_cases n' m') as [LE|GT]; trivial. generalize (double_below _ _ LE). order. - apply lt_succ_r, le_0_1. exists (n'-m'). rewrite mul_sub_distr_l, Hn, Hm. apply add_sub_swap. - apply mul_le_mono_pos_l. - apply lt_succ_r, le_0_1. + apply mul_le_mono_pos_l; try order'. destruct (le_gt_cases m' n') as [LE|GT]; trivial. generalize (double_above _ _ GT). order. exists (n'-m'). rewrite Hm,Hn, mul_sub_distr_l. |