From f1c9bb9d37e3bcefb5838c57e7ae45923d99c4ff Mon Sep 17 00:00:00 2001 From: letouzey Date: Thu, 5 May 2011 15:12:53 +0000 Subject: Modularization of Nnat For instance, nat_of_Nplus is now N2Nat.inj_add Note that we add an iter function in BinNat.N git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14105 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/NArith/BinNatDef.v | 16 ++- theories/NArith/Nnat.v | 270 +++++++++++++++++++++++++------------------- 2 files changed, 163 insertions(+), 123 deletions(-) (limited to 'theories/NArith') diff --git a/theories/NArith/BinNatDef.v b/theories/NArith/BinNatDef.v index 535f88c86..ec91dc5db 100644 --- a/theories/NArith/BinNatDef.v +++ b/theories/NArith/BinNatDef.v @@ -351,14 +351,22 @@ Definition testbit a n := Definition to_nat (a:N) := match a with - | 0 => O - | Npos p => Pos.to_nat p + | 0 => O + | Npos p => Pos.to_nat p end. Definition of_nat (n:nat) := match n with - | O => 0 - | S n' => Npos (Pos.of_succ_nat n') + | O => 0 + | S n' => Npos (Pos.of_succ_nat n') + end. + +(** Iteration of a function *) + +Definition iter (n:N) {A} (f:A->A) (x:A) : A := + match n with + | 0 => x + | Npos p => Pos.iter p f x end. End N. \ No newline at end of file diff --git a/theories/NArith/Nnat.v b/theories/NArith/Nnat.v index 05ca4a550..ccf1e9dc6 100644 --- a/theories/NArith/Nnat.v +++ b/theories/NArith/Nnat.v @@ -9,182 +9,214 @@ Require Import Arith_base Compare_dec Sumbool Div2 Min Max. Require Import BinPos BinNat Pnat. -Lemma N_of_nat_of_N : forall a:N, N_of_nat (nat_of_N a) = a. -Proof. - destruct a as [| p]. reflexivity. - simpl. elim (nat_of_P_is_S p). intros n H. rewrite H. simpl. - rewrite <- nat_of_P_of_succ_nat in H. - rewrite nat_of_P_inj with (1 := H). reflexivity. -Qed. +(** * Conversions from [N] to [nat] *) -Lemma nat_of_N_of_nat : forall n:nat, nat_of_N (N_of_nat n) = n. -Proof. - induction n. trivial. - intros. simpl. apply nat_of_P_of_succ_nat. -Qed. +Module N2Nat. -Lemma nat_of_N_inj : forall n n', nat_of_N n = nat_of_N n' -> n = n'. +(** [N.to_nat] is a bijection between [N] and [nat], + with [Pos.of_nat] as reciprocal. + See [Nat2N.bij] below for the dual equation. *) + +Lemma bij a : N.of_nat (N.to_nat a) = a. Proof. - intros n n' H. - rewrite <- (N_of_nat_of_N n), <- (N_of_nat_of_N n'). now f_equal. + 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. Qed. -Lemma N_of_nat_inj : forall n n', N_of_nat n = N_of_nat n' -> n = n'. +(** [N.to_nat] is hence injective *) + +Lemma inj a a' : N.to_nat a = N.to_nat a' -> a = a'. Proof. - intros n n' H. - rewrite <- (nat_of_N_of_nat n), <- (nat_of_N_of_nat n'). now f_equal. + intro H. rewrite <- (bij a), <- (bij a'). now f_equal. Qed. -Hint Rewrite nat_of_N_of_nat N_of_nat_of_N : Nnat. - (** Interaction of this translation and usual operations. *) -Lemma nat_of_Ndouble : forall a, nat_of_N (Ndouble a) = 2*(nat_of_N a). +Lemma inj_double a : N.to_nat (N.double a) = 2*(N.to_nat a). Proof. - destruct a; simpl nat_of_N; trivial. apply nat_of_P_xO. + destruct a; simpl N.to_nat; trivial. apply Pos2Nat.inj_xO. Qed. -Lemma nat_of_Ndouble_plus_one : - forall a, nat_of_N (Ndouble_plus_one a) = S (2*(nat_of_N a)). +Lemma inj_succ_double a : N.to_nat (N.succ_double a) = S (2*(N.to_nat a)). Proof. - destruct a; simpl nat_of_N; trivial. apply nat_of_P_xI. + destruct a; simpl N.to_nat; trivial. apply Pos2Nat.inj_xI. Qed. -Lemma nat_of_Nsucc : forall a, nat_of_N (Nsucc a) = S (nat_of_N a). +Lemma inj_succ a : N.to_nat (N.succ a) = S (N.to_nat a). Proof. - destruct a; simpl. - apply nat_of_P_xH. - apply Psucc_S. + destruct a; simpl; trivial. apply Pos2Nat.inj_succ. Qed. -Lemma nat_of_Nplus : - forall a a', nat_of_N (Nplus a a') = (nat_of_N a)+(nat_of_N a'). +Lemma inj_add a a' : + N.to_nat (a + a') = N.to_nat a + N.to_nat a'. Proof. - destruct a; destruct a'; simpl; auto. - apply Pplus_plus. + destruct a, a'; simpl; trivial. apply Pos2Nat.inj_add. Qed. -Lemma nat_of_Nmult : - forall a a', nat_of_N (Nmult a a') = (nat_of_N a)*(nat_of_N a'). +Lemma inj_mul a a' : + N.to_nat (a * a') = N.to_nat a * N.to_nat a'. Proof. - destruct a; destruct a'; simpl; auto. - apply Pmult_mult. + destruct a, a'; simpl; trivial. apply Pos2Nat.inj_mul. Qed. -Lemma nat_of_Nminus : - forall a a', nat_of_N (Nminus a a') = ((nat_of_N a)-(nat_of_N a'))%nat. +Lemma inj_sub a a' : + N.to_nat (a - a') = N.to_nat a - N.to_nat a'. Proof. - intros [|a] [|a']; simpl; auto with arith. - destruct (Pcompare_spec a a'). - subst. now rewrite Pminus_mask_diag, <- minus_n_n. - rewrite Pminus_mask_Lt by trivial. apply Plt_lt in H. - simpl; symmetry; apply not_le_minus_0; auto with arith. - destruct (Pminus_mask_Gt a a' (ZC2 _ _ H)) as (q & -> & Hq & _). - simpl. apply plus_minus. now rewrite <- Hq, Pplus_plus. + destruct a as [|a], a' as [|a']; simpl; auto with arith. + destruct (Pos.compare_spec a a'). + subst. now rewrite Pos.sub_mask_diag, <- minus_n_n. + rewrite Pos.sub_mask_neg; trivial. apply Pos2Nat.inj_lt in H. + simpl; symmetry; apply not_le_minus_0; auto with arith. + destruct (Pos.sub_mask_pos' _ _ H) as (q & -> & Hq). + simpl. apply plus_minus. now rewrite <- Hq, Pos2Nat.inj_add. Qed. -Lemma nat_of_Npred : forall a, nat_of_N (Npred a) = pred (nat_of_N a). +Lemma inj_pred a : N.to_nat (N.pred a) = pred (N.to_nat a). Proof. - intros. rewrite pred_of_minus, Npred_minus. apply nat_of_Nminus. + intros. rewrite pred_of_minus, N.pred_sub. apply inj_sub. Qed. -Lemma nat_of_Ndiv2 : - forall a, nat_of_N (Ndiv2 a) = div2 (nat_of_N a). +Lemma inj_div2 a : N.to_nat (N.div2 a) = div2 (N.to_nat a). Proof. - destruct a; simpl in *; auto. - destruct p; auto. - rewrite nat_of_P_xI. - rewrite div2_double_plus_one; auto. - rewrite nat_of_P_xO. - rewrite div2_double; auto. + destruct a as [|[p|p| ]]; trivial. + simpl N.to_nat. now rewrite Pos2Nat.inj_xI, div2_double_plus_one. + simpl N.to_nat. now rewrite Pos2Nat.inj_xO, div2_double. Qed. -Lemma nat_of_Ncompare : - forall a a', Ncompare a a' = nat_compare (nat_of_N a) (nat_of_N a'). +Lemma inj_compare a a' : + N.compare a a' = nat_compare (N.to_nat a) (N.to_nat a'). Proof. - destruct a; destruct a'; simpl; trivial. - now destruct (nat_of_P_is_S p) as (n,->). - now destruct (nat_of_P_is_S p) as (n,->). - apply Pcompare_nat_compare. + destruct a, a'; simpl; trivial. + now destruct (Pos2Nat.is_succ p) as (n,->). + now destruct (Pos2Nat.is_succ p) as (n,->). + apply Pos2Nat.inj_compare. Qed. -Lemma nat_of_Nmax : - forall a a', nat_of_N (Nmax a a') = max (nat_of_N a) (nat_of_N a'). +Lemma inj_max a a' : + N.to_nat (N.max a a') = max (N.to_nat a) (N.to_nat a'). Proof. - intros; unfold Nmax; rewrite nat_of_Ncompare. symmetry. - case nat_compare_spec; intros H; try rewrite H; auto with arith. + unfold N.max. rewrite inj_compare; symmetry. + case nat_compare_spec; intros H; try rewrite H; auto with arith. Qed. -Lemma nat_of_Nmin : - forall a a', nat_of_N (Nmin a a') = min (nat_of_N a) (nat_of_N a'). +Lemma inj_min a a' : + N.to_nat (N.min a a') = min (N.to_nat a) (N.to_nat a'). Proof. - intros; unfold Nmin; rewrite nat_of_Ncompare. symmetry. + unfold N.min; rewrite inj_compare. symmetry. case nat_compare_spec; intros H; try rewrite H; auto with arith. Qed. -Hint Rewrite nat_of_Ndouble nat_of_Ndouble_plus_one - nat_of_Nsucc nat_of_Nplus nat_of_Nmult nat_of_Nminus - nat_of_Npred nat_of_Ndiv2 nat_of_Nmax nat_of_Nmin : Nnat. - -Lemma N_of_double : forall n, N_of_nat (2*n) = Ndouble (N_of_nat n). +Lemma inj_iter a {A} (f:A->A) (x:A) : + N.iter a f x = nat_iter (N.to_nat a) f x. Proof. - intros. apply nat_of_N_inj. now autorewrite with Nnat. + destruct a as [|a]. trivial. apply Pos2Nat.inj_iter. Qed. -Lemma N_of_double_plus_one : - forall n, N_of_nat (S (2*n)) = Ndouble_plus_one (N_of_nat n). -Proof. - intros. apply nat_of_N_inj. now autorewrite with Nnat. -Qed. +End N2Nat. -Lemma N_of_S : forall n, N_of_nat (S n) = Nsucc (N_of_nat n). -Proof. - intros. apply nat_of_N_inj. now autorewrite with Nnat. -Qed. +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 + : Nnat. -Lemma N_of_pred : forall n, N_of_nat (pred n) = Npred (N_of_nat n). -Proof. - intros. apply nat_of_N_inj. now autorewrite with Nnat. -Qed. -Lemma N_of_plus : - forall n n', N_of_nat (n+n') = Nplus (N_of_nat n) (N_of_nat n'). -Proof. - intros. apply nat_of_N_inj. now autorewrite with Nnat. -Qed. +(** * Conversions from [nat] to [N] *) -Lemma N_of_minus : - forall n n', N_of_nat (n-n') = Nminus (N_of_nat n) (N_of_nat n'). -Proof. - intros. apply nat_of_N_inj. now autorewrite with Nnat. -Qed. +Module Nat2N. -Lemma N_of_mult : - forall n n', N_of_nat (n*n') = Nmult (N_of_nat n) (N_of_nat n'). -Proof. - intros. apply nat_of_N_inj. now autorewrite with Nnat. -Qed. +(** [N.of_nat] is a bijection between [nat] and [N], + with [Pos.to_nat] as reciprocal. + See [N2Nat.bij] above for the dual equation. *) -Lemma N_of_div2 : - forall n, N_of_nat (div2 n) = Ndiv2 (N_of_nat n). +Lemma bij n : N.to_nat (N.of_nat n) = n. Proof. - intros. apply nat_of_N_inj. now autorewrite with Nnat. + induction n; simpl; trivial. apply SuccNat2Pos.bij. Qed. -Lemma N_of_nat_compare : - forall n n', nat_compare n n' = Ncompare (N_of_nat n) (N_of_nat n'). -Proof. - intros. rewrite nat_of_Ncompare. now autorewrite with Nnat. -Qed. +Hint Rewrite bij : Nnat. +Ltac nat2N := apply N2Nat.inj; now autorewrite with Nnat. -Lemma N_of_min : - forall n n', N_of_nat (min n n') = Nmin (N_of_nat n) (N_of_nat n'). -Proof. - intros. apply nat_of_N_inj. now autorewrite with Nnat. -Qed. +(** [N.of_nat] is hence injective *) -Lemma N_of_max : - forall n n', N_of_nat (max n n') = Nmax (N_of_nat n) (N_of_nat n'). +Lemma inj n n' : N.of_nat n = N.of_nat n' -> n = n'. Proof. - intros. apply nat_of_N_inj. now autorewrite with Nnat. + intros H. rewrite <- (bij n), <- (bij n'). now f_equal. Qed. + +(** Interaction of this translation and usual operations. *) + +Lemma inj_double n : N.of_nat (2*n) = N.double (N.of_nat n). +Proof. nat2N. Qed. + +Lemma inj_succ_double n : N.of_nat (S (2*n)) = N.succ_double (N.of_nat n). +Proof. nat2N. Qed. + +Lemma inj_succ n : N.of_nat (S n) = N.succ (N.of_nat n). +Proof. nat2N. Qed. + +Lemma inj_pred n : N.of_nat (pred n) = N.pred (N.of_nat n). +Proof. nat2N. Qed. + +Lemma inj_add n n' : N.of_nat (n+n') = (N.of_nat n + N.of_nat n')%N. +Proof. nat2N. Qed. + +Lemma inj_sub n n' : N.of_nat (n-n') = (N.of_nat n - N.of_nat n')%N. +Proof. nat2N. Qed. + +Lemma inj_mul n n' : N.of_nat (n*n') = (N.of_nat n * N.of_nat n')%N. +Proof. nat2N. Qed. + +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. + +Lemma inj_min n n' : + N.of_nat (min n n') = N.min (N.of_nat n) (N.of_nat n'). +Proof. nat2N. Qed. + +Lemma inj_max n n' : + N.of_nat (max n n') = N.max (N.of_nat n) (N.of_nat n'). +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. + +End Nat2N. + +Hint Rewrite Nat2N.bij : Nnat. + +(** Compatibility notations *) + +Notation nat_of_N_inj := N2Nat.inj (only parsing). +Notation N_of_nat_of_N := N2Nat.bij (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). +Notation nat_of_Nplus := N2Nat.inj_add (only parsing). +Notation nat_of_Nmult := N2Nat.inj_mul (only parsing). +Notation nat_of_Nminus := N2Nat.inj_sub (only parsing). +Notation nat_of_Npred := N2Nat.inj_pred (only parsing). +Notation nat_of_Ndiv2 := N2Nat.inj_div2 (only parsing). +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 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). +Notation N_of_S := Nat2N.inj_succ (only parsing). +Notation N_of_pred := Nat2N.inj_pred (only parsing). +Notation N_of_plus := Nat2N.inj_add (only parsing). +Notation N_of_minus := Nat2N.inj_sub (only parsing). +Notation N_of_mult := Nat2N.inj_mul (only parsing). +Notation N_of_div2 := Nat2N.inj_div2 (only parsing). +Notation N_of_nat_compare := Nat2N.inj_compare (only parsing). +Notation N_of_min := Nat2N.inj_min (only parsing). +Notation N_of_max := Nat2N.inj_max (only parsing). -- cgit v1.2.3