diff options
Diffstat (limited to 'theories/NArith/Nnat.v')
| -rw-r--r-- | theories/NArith/Nnat.v | 450 |
1 files changed, 156 insertions, 294 deletions
diff --git a/theories/NArith/Nnat.v b/theories/NArith/Nnat.v index f57fab0f..1b7e2f24 100644 --- a/theories/NArith/Nnat.v +++ b/theories/NArith/Nnat.v @@ -1,370 +1,232 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Nnat.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - -Require Import Arith_base. -Require Import Compare_dec. -Require Import Sumbool. -Require Import Div2. -Require Import Min. -Require Import Max. -Require Import BinPos. -Require Import BinNat. -Require Import BinInt. -Require Import Pnat. -Require Import Zmax. -Require Import Zmin. -Require Import Znat. - -(** Translation from [N] to [nat] and back. *) - -Definition nat_of_N (a:N) := - match a with - | N0 => 0%nat - | Npos p => nat_of_P p - end. - -Definition N_of_nat (n:nat) := - match n with - | O => N0 - | S n' => Npos (P_of_succ_nat n') - end. - -Lemma N_of_nat_of_N : forall a:N, N_of_nat (nat_of_N a) = a. -Proof. - destruct a as [| p]. reflexivity. - simpl in |- *. elim (ZL4 p). intros n H. rewrite H. simpl in |- *. - rewrite <- nat_of_P_o_P_of_succ_nat_eq_succ in H. - rewrite nat_of_P_inj with (1 := H). reflexivity. -Qed. - -Lemma nat_of_N_of_nat : forall n:nat, nat_of_N (N_of_nat n) = n. -Proof. - induction n. trivial. - intros. simpl in |- *. apply nat_of_P_o_P_of_succ_nat_eq_succ. -Qed. - -(** Interaction of this translation and usual operations. *) - -Lemma nat_of_Ndouble : forall a, nat_of_N (Ndouble a) = 2*(nat_of_N a). -Proof. - destruct a; simpl nat_of_N; auto. - apply nat_of_P_xO. -Qed. - -Lemma N_of_double : forall n, N_of_nat (2*n) = Ndouble (N_of_nat n). -Proof. - intros. - pattern n at 1; rewrite <- (nat_of_N_of_nat n). - rewrite <- nat_of_Ndouble. - apply N_of_nat_of_N. -Qed. - -Lemma nat_of_Ndouble_plus_one : - forall a, nat_of_N (Ndouble_plus_one a) = S (2*(nat_of_N a)). -Proof. - destruct a; simpl nat_of_N; auto. - apply nat_of_P_xI. -Qed. - -Lemma N_of_double_plus_one : - forall n, N_of_nat (S (2*n)) = Ndouble_plus_one (N_of_nat n). -Proof. - intros. - pattern n at 1; rewrite <- (nat_of_N_of_nat n). - rewrite <- nat_of_Ndouble_plus_one. - apply N_of_nat_of_N. -Qed. - -Lemma nat_of_Nsucc : forall a, nat_of_N (Nsucc a) = S (nat_of_N a). -Proof. - destruct a; simpl. - apply nat_of_P_xH. - apply nat_of_P_succ_morphism. -Qed. - -Lemma N_of_S : forall n, N_of_nat (S n) = Nsucc (N_of_nat n). -Proof. - intros. - pattern n at 1; rewrite <- (nat_of_N_of_nat n). - rewrite <- nat_of_Nsucc. - apply N_of_nat_of_N. -Qed. - -Lemma nat_of_Nplus : - forall a a', nat_of_N (Nplus a a') = (nat_of_N a)+(nat_of_N a'). -Proof. - destruct a; destruct a'; simpl; auto. - apply nat_of_P_plus_morphism. -Qed. - -Lemma N_of_plus : - forall n n', N_of_nat (n+n') = Nplus (N_of_nat n) (N_of_nat n'). -Proof. - intros. - pattern n at 1; rewrite <- (nat_of_N_of_nat n). - pattern n' at 1; rewrite <- (nat_of_N_of_nat n'). - rewrite <- nat_of_Nplus. - apply N_of_nat_of_N. -Qed. - -Lemma nat_of_Nminus : - forall a a', nat_of_N (Nminus a a') = ((nat_of_N a)-(nat_of_N a'))%nat. -Proof. - destruct a; destruct a'; simpl; auto with arith. - case_eq (Pcompare p p0 Eq); simpl; intros. - rewrite (Pcompare_Eq_eq _ _ H); auto with arith. - rewrite Pminus_mask_diag. simpl. apply minus_n_n. - rewrite Pminus_mask_Lt. pose proof (nat_of_P_lt_Lt_compare_morphism _ _ H). simpl. - symmetry; apply not_le_minus_0. auto with arith. assumption. - pose proof (Pminus_mask_Gt p p0 H) as H1. destruct H1 as [q [H1 _]]. rewrite H1; simpl. - replace q with (Pminus p p0) by (unfold Pminus; now rewrite H1). - apply nat_of_P_minus_morphism; auto. -Qed. - -Lemma N_of_minus : - forall n n', N_of_nat (n-n') = Nminus (N_of_nat n) (N_of_nat n'). -Proof. - intros. - pattern n at 1; rewrite <- (nat_of_N_of_nat n). - pattern n' at 1; rewrite <- (nat_of_N_of_nat n'). - rewrite <- nat_of_Nminus. - apply N_of_nat_of_N. -Qed. - -Lemma nat_of_Nmult : - forall a a', nat_of_N (Nmult a a') = (nat_of_N a)*(nat_of_N a'). -Proof. - destruct a; destruct a'; simpl; auto. - apply nat_of_P_mult_morphism. -Qed. +Require Import Arith_base Compare_dec Sumbool Div2 Min Max. +Require Import BinPos BinNat Pnat. -Lemma N_of_mult : - forall n n', N_of_nat (n*n') = Nmult (N_of_nat n) (N_of_nat n'). -Proof. - intros. - pattern n at 1; rewrite <- (nat_of_N_of_nat n). - pattern n' at 1; rewrite <- (nat_of_N_of_nat n'). - rewrite <- nat_of_Nmult. - apply N_of_nat_of_N. -Qed. - -Lemma nat_of_Ndiv2 : - forall a, nat_of_N (Ndiv2 a) = div2 (nat_of_N 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. -Qed. - -Lemma N_of_div2 : - forall n, N_of_nat (div2 n) = Ndiv2 (N_of_nat n). -Proof. - intros. - pattern n at 1; rewrite <- (nat_of_N_of_nat n). - rewrite <- nat_of_Ndiv2. - apply N_of_nat_of_N. -Qed. - -Lemma nat_of_Ncompare : - forall a a', Ncompare a a' = nat_compare (nat_of_N a) (nat_of_N a'). -Proof. - destruct a; destruct a'; simpl. - reflexivity. - assert (NZ : 0 < nat_of_P p) by auto using lt_O_nat_of_P. - destruct nat_of_P; [inversion NZ|auto]. - assert (NZ : 0 < nat_of_P p) by auto using lt_O_nat_of_P. - destruct nat_of_P; [inversion NZ|auto]. - apply nat_of_P_compare_morphism. -Qed. +(** * Conversions from [N] to [nat] *) -Lemma N_of_nat_compare : - forall n n', nat_compare n n' = Ncompare (N_of_nat n) (N_of_nat n'). -Proof. - intros. - pattern n at 1; rewrite <- (nat_of_N_of_nat n). - pattern n' at 1; rewrite <- (nat_of_N_of_nat n'). - symmetry; apply nat_of_Ncompare. -Qed. +Module N2Nat. -Lemma nat_of_Nmin : - forall a a', nat_of_N (Nmin a a') = min (nat_of_N a) (nat_of_N a'). -Proof. - intros; unfold Nmin; rewrite nat_of_Ncompare. - rewrite nat_compare_equiv; unfold nat_compare_alt. - destruct (lt_eq_lt_dec (nat_of_N a) (nat_of_N a')) as [[|]|]; - simpl; intros; symmetry; auto with arith. - apply min_l; rewrite e; auto with arith. -Qed. +(** [N.to_nat] is a bijection between [N] and [nat], + with [Pos.of_nat] as reciprocal. + See [Nat2N.id] below for the dual equation. *) -Lemma N_of_min : - forall n n', N_of_nat (min n n') = Nmin (N_of_nat n) (N_of_nat n'). +Lemma id a : N.of_nat (N.to_nat a) = a. Proof. - intros. - pattern n at 1; rewrite <- (nat_of_N_of_nat n). - pattern n' at 1; rewrite <- (nat_of_N_of_nat n'). - rewrite <- nat_of_Nmin. - apply N_of_nat_of_N. + 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.id_succ. Qed. -Lemma nat_of_Nmax : - forall a a', nat_of_N (Nmax a a') = max (nat_of_N a) (nat_of_N a'). -Proof. - intros; unfold Nmax; rewrite nat_of_Ncompare. - rewrite nat_compare_equiv; unfold nat_compare_alt. - destruct (lt_eq_lt_dec (nat_of_N a) (nat_of_N a')) as [[|]|]; - simpl; intros; symmetry; auto with arith. - apply max_r; rewrite e; auto with arith. -Qed. +(** [N.to_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 a a' : N.to_nat a = N.to_nat a' -> a = a'. Proof. - intros. - pattern n at 1; rewrite <- (nat_of_N_of_nat n). - pattern n' at 1; rewrite <- (nat_of_N_of_nat n'). - rewrite <- nat_of_Nmax. - apply N_of_nat_of_N. + intro H. rewrite <- (id a), <- (id a'). now f_equal. Qed. -(** Properties concerning [Z_of_N] *) - -Lemma Z_of_nat_of_N : forall n:N, Z_of_nat (nat_of_N n) = Z_of_N n. +Lemma inj_iff a a' : N.to_nat a = N.to_nat a' <-> a = a'. Proof. - destruct n; simpl; auto; symmetry; apply Zpos_eq_Z_of_nat_o_nat_of_P. + split. apply inj. intros; now subst. Qed. -Lemma Z_of_N_eq : forall n m, n = m -> Z_of_N n = Z_of_N m. -Proof. - intros; f_equal; assumption. -Qed. +(** Interaction of this translation and usual operations. *) -Lemma Z_of_N_eq_rev : forall n m, Z_of_N n = Z_of_N m -> n = m. +Lemma inj_double a : N.to_nat (N.double a) = 2*(N.to_nat a). Proof. - intros [|n] [|m]; simpl; intros; try discriminate; congruence. + destruct a; simpl N.to_nat; trivial. apply Pos2Nat.inj_xO. Qed. -Lemma Z_of_N_eq_iff : forall n m, n = m <-> Z_of_N n = Z_of_N m. +Lemma inj_succ_double a : N.to_nat (N.succ_double a) = S (2*(N.to_nat a)). Proof. - split; [apply Z_of_N_eq | apply Z_of_N_eq_rev]. + destruct a; simpl N.to_nat; trivial. apply Pos2Nat.inj_xI. Qed. -Lemma Z_of_N_le : forall n m, (n<=m)%N -> (Z_of_N n <= Z_of_N m)%Z. +Lemma inj_succ a : N.to_nat (N.succ a) = S (N.to_nat a). Proof. - intros [|n] [|m]; simpl; auto. + destruct a; simpl; trivial. apply Pos2Nat.inj_succ. Qed. -Lemma Z_of_N_le_rev : forall n m, (Z_of_N n <= Z_of_N m)%Z -> (n<=m)%N. +Lemma inj_add a a' : + N.to_nat (a + a') = N.to_nat a + N.to_nat a'. Proof. - intros [|n] [|m]; simpl; auto. + destruct a, a'; simpl; trivial. apply Pos2Nat.inj_add. Qed. -Lemma Z_of_N_le_iff : forall n m, (n<=m)%N <-> (Z_of_N n <= Z_of_N m)%Z. +Lemma inj_mul a a' : + N.to_nat (a * a') = N.to_nat a * N.to_nat a'. Proof. - split; [apply Z_of_N_le | apply Z_of_N_le_rev]. + destruct a, a'; simpl; trivial. apply Pos2Nat.inj_mul. Qed. -Lemma Z_of_N_lt : forall n m, (n<m)%N -> (Z_of_N n < Z_of_N m)%Z. +Lemma inj_sub a a' : + N.to_nat (a - a') = N.to_nat a - N.to_nat a'. Proof. - intros [|n] [|m]; simpl; auto. + 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 Z_of_N_lt_rev : forall n m, (Z_of_N n < Z_of_N m)%Z -> (n<m)%N. +Lemma inj_pred a : N.to_nat (N.pred a) = pred (N.to_nat a). Proof. - intros [|n] [|m]; simpl; auto. + intros. rewrite pred_of_minus, N.pred_sub. apply inj_sub. Qed. -Lemma Z_of_N_lt_iff : forall n m, (n<m)%N <-> (Z_of_N n < Z_of_N m)%Z. +Lemma inj_div2 a : N.to_nat (N.div2 a) = div2 (N.to_nat a). Proof. - split; [apply Z_of_N_lt | apply Z_of_N_lt_rev]. + 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 Z_of_N_ge : forall n m, (n>=m)%N -> (Z_of_N n >= Z_of_N m)%Z. +Lemma inj_compare a a' : + (a ?= a')%N = nat_compare (N.to_nat a) (N.to_nat a'). Proof. - intros [|n] [|m]; simpl; auto. + 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 Z_of_N_ge_rev : forall n m, (Z_of_N n >= Z_of_N m)%Z -> (n>=m)%N. +Lemma inj_max a a' : + N.to_nat (N.max a a') = max (N.to_nat a) (N.to_nat a'). Proof. - intros [|n] [|m]; simpl; auto. + unfold N.max. rewrite inj_compare; symmetry. + case nat_compare_spec; intros H; try rewrite H; auto with arith. Qed. -Lemma Z_of_N_ge_iff : forall n m, (n>=m)%N <-> (Z_of_N n >= Z_of_N m)%Z. +Lemma inj_min a a' : + N.to_nat (N.min a a') = min (N.to_nat a) (N.to_nat a'). Proof. - split; [apply Z_of_N_ge | apply Z_of_N_ge_rev]. + unfold N.min; rewrite inj_compare. symmetry. + case nat_compare_spec; intros H; try rewrite H; auto with arith. Qed. -Lemma Z_of_N_gt : forall n m, (n>m)%N -> (Z_of_N n > Z_of_N m)%Z. +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 [|n] [|m]; simpl; auto. + destruct a as [|a]. trivial. apply Pos2Nat.inj_iter. Qed. -Lemma Z_of_N_gt_rev : forall n m, (Z_of_N n > Z_of_N m)%Z -> (n>m)%N. -Proof. - intros [|n] [|m]; simpl; auto. -Qed. +End N2Nat. -Lemma Z_of_N_gt_iff : forall n m, (n>m)%N <-> (Z_of_N n > Z_of_N m)%Z. -Proof. - split; [apply Z_of_N_gt | apply Z_of_N_gt_rev]. -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.id + : Nnat. -Lemma Z_of_N_of_nat : forall n:nat, Z_of_N (N_of_nat n) = Z_of_nat n. -Proof. - destruct n; simpl; auto. -Qed. -Lemma Z_of_N_pos : forall p:positive, Z_of_N (Npos p) = Zpos p. -Proof. - destruct p; simpl; auto. -Qed. +(** * Conversions from [nat] to [N] *) -Lemma Z_of_N_abs : forall z:Z, Z_of_N (Zabs_N z) = Zabs z. -Proof. - destruct z; simpl; auto. -Qed. +Module Nat2N. -Lemma Z_of_N_le_0 : forall n, (0 <= Z_of_N n)%Z. -Proof. - destruct n; intro; discriminate. -Qed. +(** [N.of_nat] is an bijection between [nat] and [N], + with [Pos.to_nat] as reciprocal. + See [N2Nat.id] above for the dual equation. *) -Lemma Z_of_N_plus : forall n m:N, Z_of_N (n+m) = (Z_of_N n + Z_of_N m)%Z. +Lemma id n : N.to_nat (N.of_nat n) = n. Proof. - destruct n; destruct m; auto. + induction n; simpl; trivial. apply SuccNat2Pos.id_succ. Qed. -Lemma Z_of_N_mult : forall n m:N, Z_of_N (n*m) = (Z_of_N n * Z_of_N m)%Z. -Proof. - destruct n; destruct m; auto. -Qed. +Hint Rewrite id : Nnat. +Ltac nat2N := apply N2Nat.inj; now autorewrite with Nnat. -Lemma Z_of_N_minus : forall n m:N, Z_of_N (n-m) = Zmax 0 (Z_of_N n - Z_of_N m). -Proof. - intros; do 3 rewrite <- Z_of_nat_of_N; rewrite nat_of_Nminus; apply inj_minus. -Qed. +(** [N.of_nat] is hence injective *) -Lemma Z_of_N_succ : forall n:N, Z_of_N (Nsucc n) = Zsucc (Z_of_N n). +Lemma inj n n' : N.of_nat n = N.of_nat n' -> n = n'. Proof. - intros; do 2 rewrite <- Z_of_nat_of_N; rewrite nat_of_Nsucc; apply inj_S. + intros H. rewrite <- (id n), <- (id n'). now f_equal. Qed. -Lemma Z_of_N_min : forall n m:N, Z_of_N (Nmin n m) = Zmin (Z_of_N n) (Z_of_N m). +Lemma inj_iff n n' : N.of_nat n = N.of_nat n' <-> n = n'. Proof. - intros; do 3 rewrite <- Z_of_nat_of_N; rewrite nat_of_Nmin; apply inj_min. + split. apply inj. intros; now subst. Qed. -Lemma Z_of_N_max : forall n m:N, Z_of_N (Nmax n m) = Zmax (Z_of_N n) (Z_of_N m). -Proof. - intros; do 3 rewrite <- Z_of_nat_of_N; rewrite nat_of_Nmax; apply inj_max. -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.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'). +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, !id. Qed. + +End Nat2N. + +Hint Rewrite Nat2N.id : Nnat. + +(** Compatibility notations *) + +Notation nat_of_N_inj := N2Nat.inj (compat "8.3"). +Notation N_of_nat_of_N := N2Nat.id (compat "8.3"). +Notation nat_of_Ndouble := N2Nat.inj_double (compat "8.3"). +Notation nat_of_Ndouble_plus_one := N2Nat.inj_succ_double (compat "8.3"). +Notation nat_of_Nsucc := N2Nat.inj_succ (compat "8.3"). +Notation nat_of_Nplus := N2Nat.inj_add (compat "8.3"). +Notation nat_of_Nmult := N2Nat.inj_mul (compat "8.3"). +Notation nat_of_Nminus := N2Nat.inj_sub (compat "8.3"). +Notation nat_of_Npred := N2Nat.inj_pred (compat "8.3"). +Notation nat_of_Ndiv2 := N2Nat.inj_div2 (compat "8.3"). +Notation nat_of_Ncompare := N2Nat.inj_compare (compat "8.3"). +Notation nat_of_Nmax := N2Nat.inj_max (compat "8.3"). +Notation nat_of_Nmin := N2Nat.inj_min (compat "8.3"). + +Notation nat_of_N_of_nat := Nat2N.id (compat "8.3"). +Notation N_of_nat_inj := Nat2N.inj (compat "8.3"). +Notation N_of_double := Nat2N.inj_double (compat "8.3"). +Notation N_of_double_plus_one := Nat2N.inj_succ_double (compat "8.3"). +Notation N_of_S := Nat2N.inj_succ (compat "8.3"). +Notation N_of_pred := Nat2N.inj_pred (compat "8.3"). +Notation N_of_plus := Nat2N.inj_add (compat "8.3"). +Notation N_of_minus := Nat2N.inj_sub (compat "8.3"). +Notation N_of_mult := Nat2N.inj_mul (compat "8.3"). +Notation N_of_div2 := Nat2N.inj_div2 (compat "8.3"). +Notation N_of_nat_compare := Nat2N.inj_compare (compat "8.3"). +Notation N_of_min := Nat2N.inj_min (compat "8.3"). +Notation N_of_max := Nat2N.inj_max (compat "8.3"). |