diff options
Diffstat (limited to 'theories/Init/Peano.v')
| -rw-r--r-- | theories/Init/Peano.v | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v index 98fd52f351..fb2a7a57fe 100644 --- a/theories/Init/Peano.v +++ b/theories/Init/Peano.v @@ -37,6 +37,7 @@ Local Notation "0" := O. Definition eq_S := f_equal S. Definition f_equal_nat := f_equal (A:=nat). +#[global] Hint Resolve f_equal_nat: core. (** The predecessor function *) @@ -53,12 +54,14 @@ Qed. (** Injectivity of successor *) Definition eq_add_S n m (H: S n = S m): n = m := f_equal pred H. +#[global] Hint Immediate eq_add_S: core. Theorem not_eq_S : forall n m:nat, n <> m -> S n <> S m. Proof. red; auto. Qed. +#[global] Hint Resolve not_eq_S: core. Definition IsSucc (n:nat) : Prop := @@ -73,12 +76,14 @@ Theorem O_S : forall n:nat, 0 <> S n. Proof. discriminate. Qed. +#[global] Hint Resolve O_S: core. Theorem n_Sn : forall n:nat, n <> S n. Proof. intro n; induction n; auto. Qed. +#[global] Hint Resolve n_Sn: core. (** Addition *) @@ -88,6 +93,7 @@ Infix "+" := Nat.add : nat_scope. Definition f_equal2_plus := f_equal2 plus. Definition f_equal2_nat := f_equal2 (A1:=nat) (A2:=nat). +#[global] Hint Resolve f_equal2_nat: core. Lemma plus_n_O : forall n:nat, n = n + 0. @@ -95,7 +101,9 @@ Proof. intro n; induction n; simpl; auto. Qed. +#[global] Remove Hints eq_refl : core. +#[global] Hint Resolve plus_n_O eq_refl: core. (* We want eq_refl to have higher priority than plus_n_O *) Lemma plus_O_n : forall n:nat, 0 + n = n. @@ -107,6 +115,7 @@ Lemma plus_n_Sm : forall n m:nat, S (n + m) = n + S m. Proof. intros n m; induction n; simpl; auto. Qed. +#[global] Hint Resolve plus_n_Sm: core. Lemma plus_Sn_m : forall n m:nat, S n + m = S (n + m). @@ -125,12 +134,14 @@ Notation mult := Nat.mul (only parsing). Infix "*" := Nat.mul : nat_scope. Definition f_equal2_mult := f_equal2 mult. +#[global] Hint Resolve f_equal2_mult: core. Lemma mult_n_O : forall n:nat, 0 = n * 0. Proof. intro n; induction n; simpl; auto. Qed. +#[global] Hint Resolve mult_n_O: core. Lemma mult_n_Sm : forall n m:nat, n * m + n = n * S m. @@ -139,6 +150,7 @@ Proof. destruct H; rewrite <- plus_n_Sm; apply eq_S. pattern m at 1 3; elim m; simpl; auto. Qed. +#[global] Hint Resolve mult_n_Sm: core. (** Standard associated names *) @@ -162,20 +174,24 @@ where "n <= m" := (le n m) : nat_scope. Register le_n as num.nat.le_n. +#[global] Hint Constructors le: core. (*i equivalent to : "Hints Resolve le_n le_S : core." i*) Definition lt (n m:nat) := S n <= m. +#[global] Hint Unfold lt: core. Infix "<" := lt : nat_scope. Definition ge (n m:nat) := m <= n. +#[global] Hint Unfold ge: core. Infix ">=" := ge : nat_scope. Definition gt (n m:nat) := m < n. +#[global] Hint Unfold gt: core. Infix ">" := gt : nat_scope. |