diff options
Diffstat (limited to 'theories/NArith/Nnat.v')
| -rw-r--r-- | theories/NArith/Nnat.v | 46 |
1 files changed, 28 insertions, 18 deletions
diff --git a/theories/NArith/Nnat.v b/theories/NArith/Nnat.v index ccf1e9dc6..133d4c23b 100644 --- a/theories/NArith/Nnat.v +++ b/theories/NArith/Nnat.v @@ -15,20 +15,25 @@ Module N2Nat. (** [N.to_nat] is a bijection between [N] and [nat], with [Pos.of_nat] as reciprocal. - See [Nat2N.bij] below for the dual equation. *) + See [Nat2N.id] below for the dual equation. *) -Lemma bij a : N.of_nat (N.to_nat a) = a. +Lemma id a : N.of_nat (N.to_nat a) = a. Proof. destruct a as [| p]; simpl; trivial. destruct (Pos2Nat.is_succ p) as (n,H). rewrite H. simpl. f_equal. - apply Pos2Nat.inj. rewrite H. apply SuccNat2Pos.bij. + apply Pos2Nat.inj. rewrite H. apply SuccNat2Pos.id_succ. Qed. (** [N.to_nat] is hence injective *) Lemma inj a a' : N.to_nat a = N.to_nat a' -> a = a'. Proof. - intro H. rewrite <- (bij a), <- (bij a'). now f_equal. + intro H. rewrite <- (id a), <- (id a'). now f_equal. +Qed. + +Lemma inj_iff a a' : N.to_nat a = N.to_nat a' <-> a = a'. +Proof. + split. apply inj. intros; now subst. Qed. (** Interaction of this translation and usual operations. *) @@ -85,7 +90,7 @@ Proof. Qed. Lemma inj_compare a a' : - N.compare a a' = nat_compare (N.to_nat a) (N.to_nat a'). + (a ?= a')%N = nat_compare (N.to_nat a) (N.to_nat a'). Proof. destruct a, a'; simpl; trivial. now destruct (Pos2Nat.is_succ p) as (n,->). @@ -118,7 +123,7 @@ End N2Nat. Hint Rewrite N2Nat.inj_double N2Nat.inj_succ_double N2Nat.inj_succ N2Nat.inj_add N2Nat.inj_mul N2Nat.inj_sub N2Nat.inj_pred N2Nat.inj_div2 N2Nat.inj_max N2Nat.inj_min - N2Nat.bij + N2Nat.id : Nnat. @@ -126,23 +131,28 @@ Hint Rewrite N2Nat.inj_double N2Nat.inj_succ_double Module Nat2N. -(** [N.of_nat] is a bijection between [nat] and [N], +(** [N.of_nat] is an bijection between [nat] and [N], with [Pos.to_nat] as reciprocal. - See [N2Nat.bij] above for the dual equation. *) + See [N2Nat.id] above for the dual equation. *) -Lemma bij n : N.to_nat (N.of_nat n) = n. +Lemma id n : N.to_nat (N.of_nat n) = n. Proof. - induction n; simpl; trivial. apply SuccNat2Pos.bij. + induction n; simpl; trivial. apply SuccNat2Pos.id_succ. Qed. -Hint Rewrite bij : Nnat. +Hint Rewrite id : Nnat. Ltac nat2N := apply N2Nat.inj; now autorewrite with Nnat. (** [N.of_nat] is hence injective *) Lemma inj n n' : N.of_nat n = N.of_nat n' -> n = n'. Proof. - intros H. rewrite <- (bij n), <- (bij n'). now f_equal. + intros H. rewrite <- (id n), <- (id n'). now f_equal. +Qed. + +Lemma inj_iff n n' : N.of_nat n = N.of_nat n' <-> n = n'. +Proof. + split. apply inj. intros; now subst. Qed. (** Interaction of this translation and usual operations. *) @@ -172,8 +182,8 @@ Lemma inj_div2 n : N.of_nat (div2 n) = N.div2 (N.of_nat n). Proof. nat2N. Qed. Lemma inj_compare n n' : - nat_compare n n' = N.compare (N.of_nat n) (N.of_nat n'). -Proof. now rewrite N2Nat.inj_compare, !bij. Qed. + nat_compare n n' = (N.of_nat n ?= N.of_nat n')%N. +Proof. now rewrite N2Nat.inj_compare, !id. Qed. Lemma inj_min n n' : N.of_nat (min n n') = N.min (N.of_nat n) (N.of_nat n'). @@ -185,16 +195,16 @@ Proof. nat2N. Qed. Lemma inj_iter n {A} (f:A->A) (x:A) : nat_iter n f x = N.iter (N.of_nat n) f x. -Proof. now rewrite N2Nat.inj_iter, !bij. Qed. +Proof. now rewrite N2Nat.inj_iter, !id. Qed. End Nat2N. -Hint Rewrite Nat2N.bij : Nnat. +Hint Rewrite Nat2N.id : Nnat. (** Compatibility notations *) Notation nat_of_N_inj := N2Nat.inj (only parsing). -Notation N_of_nat_of_N := N2Nat.bij (only parsing). +Notation N_of_nat_of_N := N2Nat.id (only parsing). Notation nat_of_Ndouble := N2Nat.inj_double (only parsing). Notation nat_of_Ndouble_plus_one := N2Nat.inj_succ_double (only parsing). Notation nat_of_Nsucc := N2Nat.inj_succ (only parsing). @@ -207,7 +217,7 @@ Notation nat_of_Ncompare := N2Nat.inj_compare (only parsing). Notation nat_of_Nmax := N2Nat.inj_max (only parsing). Notation nat_of_Nmin := N2Nat.inj_min (only parsing). -Notation nat_of_N_of_nat := Nat2N.bij (only parsing). +Notation nat_of_N_of_nat := Nat2N.id (only parsing). Notation N_of_nat_inj := Nat2N.inj (only parsing). Notation N_of_double := Nat2N.inj_double (only parsing). Notation N_of_double_plus_one := Nat2N.inj_succ_double (only parsing). |