diff options
Diffstat (limited to 'theories/ZArith/Znat.v')
| -rw-r--r-- | theories/ZArith/Znat.v | 207 |
1 files changed, 177 insertions, 30 deletions
diff --git a/theories/ZArith/Znat.v b/theories/ZArith/Znat.v index f0a3d47b..c5b5edc1 100644 --- a/theories/ZArith/Znat.v +++ b/theories/ZArith/Znat.v @@ -6,9 +6,9 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Znat.v 9302 2006-10-27 21:21:17Z barras $ i*) +(*i $Id: Znat.v 10726 2008-03-28 18:15:23Z notin $ i*) -(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *) +(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *) Require Export Arith_base. Require Import BinPos. @@ -17,6 +17,7 @@ Require Import Zcompare. Require Import Zorder. Require Import Decidable. Require Import Peano_dec. +Require Import Min Max Zmin Zmax. Require Export Compare_dec. Open Local Scope Z_scope. @@ -26,6 +27,13 @@ Definition neq (x y:nat) := x <> y. (************************************************) (** Properties of the injection from nat into Z *) +(** Injection and successor *) + +Theorem inj_0 : Z_of_nat 0 = 0%Z. +Proof. + reflexivity. +Qed. + Theorem inj_S : forall n:nat, Z_of_nat (S n) = Zsucc (Z_of_nat n). Proof. intro y; induction y as [| n H]; @@ -33,25 +41,12 @@ Proof. | change (Zpos (Psucc (P_of_succ_nat n)) = Zsucc (Z_of_nat (S n))) in |- *; rewrite Zpos_succ_morphism; trivial with arith ]. Qed. - -Theorem inj_plus : forall n m:nat, Z_of_nat (n + m) = Z_of_nat n + Z_of_nat m. -Proof. - intro x; induction x as [| n H]; intro y; destruct y as [| m]; - [ simpl in |- *; trivial with arith - | simpl in |- *; trivial with arith - | simpl in |- *; rewrite <- plus_n_O; trivial with arith - | change (Z_of_nat (S (n + S m)) = Z_of_nat (S n) + Z_of_nat (S m)) in |- *; - rewrite inj_S; rewrite H; do 2 rewrite inj_S; rewrite Zplus_succ_l; - trivial with arith ]. -Qed. -Theorem inj_mult : forall n m:nat, Z_of_nat (n * m) = Z_of_nat n * Z_of_nat m. +(** Injection and equality. *) + +Theorem inj_eq : forall n m:nat, n = m -> Z_of_nat n = Z_of_nat m. Proof. - intro x; induction x as [| n H]; - [ simpl in |- *; trivial with arith - | intro y; rewrite inj_S; rewrite <- Zmult_succ_l_reverse; rewrite <- H; - rewrite <- inj_plus; simpl in |- *; rewrite plus_comm; - trivial with arith ]. + intros x y H; rewrite H; trivial with arith. Qed. Theorem inj_neq : forall n m:nat, neq n m -> Zne (Z_of_nat n) (Z_of_nat m). @@ -66,6 +61,24 @@ Proof. intros E; rewrite E; auto with arith ]. Qed. +Theorem inj_eq_rev : forall n m:nat, Z_of_nat n = Z_of_nat m -> n = m. +Proof. + intros x y H. + destruct (eq_nat_dec x y) as [H'|H']; auto. + elimtype False. + exact (inj_neq _ _ H' H). +Qed. + +Theorem inj_eq_iff : forall n m:nat, n=m <-> Z_of_nat n = Z_of_nat m. +Proof. + split; [apply inj_eq | apply inj_eq_rev]. +Qed. + + +(** Injection and order relations: *) + +(** One way ... *) + Theorem inj_le : forall n m:nat, (n <= m)%nat -> Z_of_nat n <= Z_of_nat m. Proof. intros x y; intros H; elim H; @@ -81,29 +94,100 @@ Proof. exact H. Qed. +Theorem inj_ge : forall n m:nat, (n >= m)%nat -> Z_of_nat n >= Z_of_nat m. +Proof. + intros x y H; apply Zle_ge; apply inj_le; apply H. +Qed. + Theorem inj_gt : forall n m:nat, (n > m)%nat -> Z_of_nat n > Z_of_nat m. Proof. intros x y H; apply Zlt_gt; apply inj_lt; exact H. Qed. -Theorem inj_ge : forall n m:nat, (n >= m)%nat -> Z_of_nat n >= Z_of_nat m. +(** The other way ... *) + +Theorem inj_le_rev : forall n m:nat, Z_of_nat n <= Z_of_nat m -> (n <= m)%nat. Proof. - intros x y H; apply Zle_ge; apply inj_le; apply H. + intros x y H. + destruct (le_lt_dec x y) as [H0|H0]; auto. + elimtype False. + assert (H1:=inj_lt _ _ H0). + red in H; red in H1. + rewrite <- Zcompare_antisym in H; rewrite H1 in H; auto. Qed. -Theorem inj_eq : forall n m:nat, n = m -> Z_of_nat n = Z_of_nat m. +Theorem inj_lt_rev : forall n m:nat, Z_of_nat n < Z_of_nat m -> (n < m)%nat. Proof. - intros x y H; rewrite H; trivial with arith. + intros x y H. + destruct (le_lt_dec y x) as [H0|H0]; auto. + elimtype False. + assert (H1:=inj_le _ _ H0). + red in H; red in H1. + rewrite <- Zcompare_antisym in H1; rewrite H in H1; auto. Qed. -Theorem intro_Z : - forall n:nat, exists y : Z, Z_of_nat n = y /\ 0 <= y * 1 + 0. +Theorem inj_ge_rev : forall n m:nat, Z_of_nat n >= Z_of_nat m -> (n >= m)%nat. Proof. - intros x; exists (Z_of_nat x); split; - [ trivial with arith - | rewrite Zmult_comm; rewrite Zmult_1_l; rewrite Zplus_0_r; - unfold Zle in |- *; elim x; intros; simpl in |- *; - discriminate ]. + intros x y H. + destruct (le_lt_dec y x) as [H0|H0]; auto. + elimtype False. + assert (H1:=inj_gt _ _ H0). + red in H; red in H1. + rewrite <- Zcompare_antisym in H; rewrite H1 in H; auto. +Qed. + +Theorem inj_gt_rev : forall n m:nat, Z_of_nat n > Z_of_nat m -> (n > m)%nat. +Proof. + intros x y H. + destruct (le_lt_dec x y) as [H0|H0]; auto. + elimtype False. + assert (H1:=inj_ge _ _ H0). + red in H; red in H1. + rewrite <- Zcompare_antisym in H1; rewrite H in H1; auto. +Qed. + +(* Both ways ... *) + +Theorem inj_le_iff : forall n m:nat, (n<=m)%nat <-> Z_of_nat n <= Z_of_nat m. +Proof. + split; [apply inj_le | apply inj_le_rev]. +Qed. + +Theorem inj_lt_iff : forall n m:nat, (n<m)%nat <-> Z_of_nat n < Z_of_nat m. +Proof. + split; [apply inj_lt | apply inj_lt_rev]. +Qed. + +Theorem inj_ge_iff : forall n m:nat, (n>=m)%nat <-> Z_of_nat n >= Z_of_nat m. +Proof. + split; [apply inj_ge | apply inj_ge_rev]. +Qed. + +Theorem inj_gt_iff : forall n m:nat, (n>m)%nat <-> Z_of_nat n > Z_of_nat m. +Proof. + split; [apply inj_gt | apply inj_gt_rev]. +Qed. + +(** Injection and usual operations *) + +Theorem inj_plus : forall n m:nat, Z_of_nat (n + m) = Z_of_nat n + Z_of_nat m. +Proof. + intro x; induction x as [| n H]; intro y; destruct y as [| m]; + [ simpl in |- *; trivial with arith + | simpl in |- *; trivial with arith + | simpl in |- *; rewrite <- plus_n_O; trivial with arith + | change (Z_of_nat (S (n + S m)) = Z_of_nat (S n) + Z_of_nat (S m)) in |- *; + rewrite inj_S; rewrite H; do 2 rewrite inj_S; rewrite Zplus_succ_l; + trivial with arith ]. +Qed. + +Theorem inj_mult : forall n m:nat, Z_of_nat (n * m) = Z_of_nat n * Z_of_nat m. +Proof. + intro x; induction x as [| n H]; + [ simpl in |- *; trivial with arith + | intro y; rewrite inj_S; rewrite <- Zmult_succ_l_reverse; rewrite <- H; + rewrite <- inj_plus; simpl in |- *; rewrite plus_comm; + trivial with arith ]. Qed. Theorem inj_minus1 : @@ -121,6 +205,46 @@ Proof. [ trivial with arith | apply gt_not_le; assumption ]. Qed. +Theorem inj_minus : forall n m:nat, + Z_of_nat (minus n m) = Zmax 0 (Z_of_nat n - Z_of_nat m). +Proof. + intros. + rewrite Zmax_comm. + unfold Zmax. + destruct (le_lt_dec m n) as [H|H]. + + rewrite (inj_minus1 _ _ H). + assert (H':=Zle_minus_le_0 _ _ (inj_le _ _ H)). + unfold Zle in H'. + rewrite <- Zcompare_antisym in H'. + destruct Zcompare; simpl in *; intuition. + + rewrite (inj_minus2 _ _ H). + assert (H':=Zplus_lt_compat_r _ _ (- Z_of_nat m) (inj_lt _ _ H)). + rewrite Zplus_opp_r in H'. + unfold Zminus; rewrite H'; auto. +Qed. + +Theorem inj_min : forall n m:nat, + Z_of_nat (min n m) = Zmin (Z_of_nat n) (Z_of_nat m). +Proof. + induction n; destruct m; try (compute; auto; fail). + simpl min. + do 3 rewrite inj_S. + rewrite <- Zsucc_min_distr; f_equal; auto. +Qed. + +Theorem inj_max : forall n m:nat, + Z_of_nat (max n m) = Zmax (Z_of_nat n) (Z_of_nat m). +Proof. + induction n; destruct m; try (compute; auto; fail). + simpl max. + do 3 rewrite inj_S. + rewrite <- Zsucc_max_distr; f_equal; auto. +Qed. + +(** Composition of injections **) + Theorem Zpos_eq_Z_of_nat_o_nat_of_P : forall p:positive, Zpos p = Z_of_nat (nat_of_P p). Proof. @@ -136,3 +260,26 @@ Proof. rewrite inj_plus; repeat rewrite <- H. rewrite Zpos_xO; simpl in |- *; rewrite Pplus_diag; reflexivity. Qed. + +(** Misc *) + +Theorem intro_Z : + forall n:nat, exists y : Z, Z_of_nat n = y /\ 0 <= y * 1 + 0. +Proof. + intros x; exists (Z_of_nat x); split; + [ trivial with arith + | rewrite Zmult_comm; rewrite Zmult_1_l; rewrite Zplus_0_r; + unfold Zle in |- *; elim x; intros; simpl in |- *; + discriminate ]. +Qed. + +Lemma Zpos_P_of_succ_nat : forall n:nat, + Zpos (P_of_succ_nat n) = Zsucc (Z_of_nat n). +Proof. + intros. + unfold Z_of_nat. + destruct n. + simpl; auto. + simpl (P_of_succ_nat (S n)). + apply Zpos_succ_morphism. +Qed. |