diff options
Diffstat (limited to 'theories7/NArith/Pnat.v')
| -rw-r--r-- | theories7/NArith/Pnat.v | 472 |
1 files changed, 472 insertions, 0 deletions
diff --git a/theories7/NArith/Pnat.v b/theories7/NArith/Pnat.v new file mode 100644 index 00000000..d62661ed --- /dev/null +++ b/theories7/NArith/Pnat.v @@ -0,0 +1,472 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: Pnat.v,v 1.1.2.1 2004/07/16 19:31:31 herbelin Exp $ i*) + +Require BinPos. + +(**********************************************************************) +(** Properties of the injection from binary positive numbers to Peano + natural numbers *) + +(** Original development by Pierre Crégut, CNET, Lannion, France *) + +Require Le. +Require Lt. +Require Gt. +Require Plus. +Require Mult. +Require Minus. + +(** [nat_of_P] is a morphism for addition *) + +Lemma convert_add_un : + (x:positive)(m:nat) + (positive_to_nat (add_un x) m) = (plus m (positive_to_nat x m)). +Proof. +Intro x; NewInduction x as [p IHp|p IHp|]; Simpl; Auto; Intro m; Rewrite IHp; +Rewrite plus_assoc_l; Trivial. +Qed. + +Lemma cvt_add_un : + (p:positive) (convert (add_un p)) = (S (convert p)). +Proof. + Intro; Change (S (convert p)) with (plus (S O) (convert p)); + Unfold convert; Apply convert_add_un. +Qed. + +Theorem convert_add_carry : + (x,y:positive)(m:nat) + (positive_to_nat (add_carry x y) m) = + (plus m (positive_to_nat (add x y) m)). +Proof. +Intro x; NewInduction x as [p IHp|p IHp|]; + Intro y; NewDestruct y; Simpl; Auto with arith; Intro m; [ + Rewrite IHp; Rewrite plus_assoc_l; Trivial with arith +| Rewrite IHp; Rewrite plus_assoc_l; Trivial with arith +| Rewrite convert_add_un; Rewrite plus_assoc_l; Trivial with arith +| Rewrite convert_add_un; Apply plus_assoc_r ]. +Qed. + +Theorem cvt_carry : + (x,y:positive)(convert (add_carry x y)) = (S (convert (add x y))). +Proof. +Intros;Unfold convert; Rewrite convert_add_carry; Simpl; Trivial with arith. +Qed. + +Theorem add_verif : + (x,y:positive)(m:nat) + (positive_to_nat (add x y) m) = + (plus (positive_to_nat x m) (positive_to_nat y m)). +Proof. +Intro x; NewInduction x as [p IHp|p IHp|]; + Intro y; NewDestruct y;Simpl;Auto with arith; [ + Intros m;Rewrite convert_add_carry; Rewrite IHp; + Rewrite plus_assoc_r; Rewrite plus_assoc_r; + Rewrite (plus_permute m (positive_to_nat p (plus m m))); Trivial with arith +| Intros m; Rewrite IHp; Apply plus_assoc_l +| Intros m; Rewrite convert_add_un; + Rewrite (plus_sym (plus m (positive_to_nat p (plus m m)))); + Apply plus_assoc_r +| Intros m; Rewrite IHp; Apply plus_permute +| Intros m; Rewrite convert_add_un; Apply plus_assoc_r ]. +Qed. + +Theorem convert_add: + (x,y:positive) (convert (add x y)) = (plus (convert x) (convert y)). +Proof. +Intros x y; Exact (add_verif x y (S O)). +Qed. + +(** [Pmult_nat] is a morphism for addition *) + +Lemma ZL2: + (y:positive)(m:nat) + (positive_to_nat y (plus m m)) = + (plus (positive_to_nat y m) (positive_to_nat y m)). +Proof. +Intro y; NewInduction y as [p H|p H|]; Intro m; [ + Simpl; Rewrite H; Rewrite plus_assoc_r; + Rewrite (plus_permute m (positive_to_nat p (plus m m))); + Rewrite plus_assoc_r; Auto with arith +| Simpl; Rewrite H; Auto with arith +| Simpl; Trivial with arith ]. +Qed. + +Lemma ZL6: + (p:positive) (positive_to_nat p (S (S O))) = (plus (convert p) (convert p)). +Proof. +Intro p;Change (2) with (plus (S O) (S O)); Rewrite ZL2; Trivial. +Qed. + +(** [nat_of_P] is a morphism for multiplication *) + +Theorem times_convert : + (x,y:positive) (convert (times x y)) = (mult (convert x) (convert y)). +Proof. +Intros x y; NewInduction x as [ x' H | x' H | ]; [ + Change (times (xI x') y) with (add y (xO (times x' y))); Rewrite convert_add; + Unfold 2 3 convert; Simpl; Do 2 Rewrite ZL6; Rewrite H; + Rewrite -> mult_plus_distr; Reflexivity +| Unfold 1 2 convert; Simpl; Do 2 Rewrite ZL6; + Rewrite H; Rewrite mult_plus_distr; Reflexivity +| Simpl; Rewrite <- plus_n_O; Reflexivity ]. +Qed. +V7only [ + Comments "Compatibility with the old version of times and times_convert". + Syntactic Definition times1 := + [x:positive;_:positive->positive;y:positive](times x y). + Syntactic Definition times1_convert := + [x,y:positive;_:positive->positive](times_convert x y). +]. + +(** [nat_of_P] maps to the strictly positive subset of [nat] *) + +Lemma ZL4: (y:positive) (EX h:nat |(convert y)=(S h)). +Proof. +Intro y; NewInduction y as [p H|p H|]; [ + NewDestruct H as [x H1]; Exists (plus (S x) (S x)); + Unfold convert ;Simpl; Change (2) with (plus (1) (1)); Rewrite ZL2; Unfold convert in H1; + Rewrite H1; Auto with arith +| NewDestruct H as [x H2]; Exists (plus x (S x)); Unfold convert; + Simpl; Change (2) with (plus (1) (1)); Rewrite ZL2;Unfold convert in H2; Rewrite H2; Auto with arith +| Exists O ;Auto with arith ]. +Qed. + +(** Extra lemmas on [lt] on Peano natural numbers *) + +Lemma ZL7: + (m,n:nat) (lt m n) -> (lt (plus m m) (plus n n)). +Proof. +Intros m n H; Apply lt_trans with m:=(plus m n); [ + Apply lt_reg_l with 1:=H +| Rewrite (plus_sym m n); Apply lt_reg_l with 1:=H ]. +Qed. + +Lemma ZL8: + (m,n:nat) (lt m n) -> (lt (S (plus m m)) (plus n n)). +Proof. +Intros m n H; Apply le_lt_trans with m:=(plus m n); [ + Change (lt (plus m m) (plus m n)) ; Apply lt_reg_l with 1:=H +| Rewrite (plus_sym m n); Apply lt_reg_l with 1:=H ]. +Qed. + +(** [nat_of_P] is a morphism from [positive] to [nat] for [lt] (expressed + from [compare] on [positive]) + + Part 1: [lt] on [positive] is finer than [lt] on [nat] +*) + +Lemma compare_convert_INFERIEUR : + (x,y:positive) (compare x y EGAL) = INFERIEUR -> + (lt (convert x) (convert y)). +Proof. +Intro x; NewInduction x as [p H|p H|];Intro y; NewDestruct y as [q|q|]; + Intro H2; [ + Unfold convert ;Simpl; Apply lt_n_S; + Do 2 Rewrite ZL6; Apply ZL7; Apply H; Simpl in H2; Assumption +| Unfold convert ;Simpl; Do 2 Rewrite ZL6; + Apply ZL8; Apply H;Simpl in H2; Apply ZLSI;Assumption +| Simpl; Discriminate H2 +| Simpl; Unfold convert ;Simpl;Do 2 Rewrite ZL6; + Elim (ZLII p q H2); [ + Intros H3;Apply lt_S;Apply ZL7; Apply H;Apply H3 + | Intros E;Rewrite E;Apply lt_n_Sn] +| Simpl; Unfold convert ;Simpl;Do 2 Rewrite ZL6; + Apply ZL7;Apply H;Assumption +| Simpl; Discriminate H2 +| Unfold convert ;Simpl; Apply lt_n_S; Rewrite ZL6; + Elim (ZL4 q);Intros h H3; Rewrite H3;Simpl; Apply lt_O_Sn +| Unfold convert ;Simpl; Rewrite ZL6; Elim (ZL4 q);Intros h H3; + Rewrite H3; Simpl; Rewrite <- plus_n_Sm; Apply lt_n_S; Apply lt_O_Sn +| Simpl; Discriminate H2 ]. +Qed. + +(** [nat_of_P] is a morphism from [positive] to [nat] for [gt] (expressed + from [compare] on [positive]) + + Part 1: [gt] on [positive] is finer than [gt] on [nat] +*) + +Lemma compare_convert_SUPERIEUR : + (x,y:positive) (compare x y EGAL)=SUPERIEUR -> (gt (convert x) (convert y)). +Proof. +Unfold gt; Intro x; NewInduction x as [p H|p H|]; + Intro y; NewDestruct y as [q|q|]; Intro H2; [ + Simpl; Unfold convert ;Simpl;Do 2 Rewrite ZL6; + Apply lt_n_S; Apply ZL7; Apply H;Assumption +| Simpl; Unfold convert ;Simpl; Do 2 Rewrite ZL6; + Elim (ZLSS p q H2); [ + Intros H3;Apply lt_S;Apply ZL7;Apply H;Assumption + | Intros E;Rewrite E;Apply lt_n_Sn] +| Unfold convert ;Simpl; Rewrite ZL6;Elim (ZL4 p); + Intros h H3;Rewrite H3;Simpl; Apply lt_n_S; Apply lt_O_Sn +| Simpl;Unfold convert ;Simpl;Do 2 Rewrite ZL6; + Apply ZL8; Apply H; Apply ZLIS; Assumption +| Simpl; Unfold convert ;Simpl;Do 2 Rewrite ZL6; + Apply ZL7;Apply H;Assumption +| Unfold convert ;Simpl; Rewrite ZL6; Elim (ZL4 p); + Intros h H3;Rewrite H3;Simpl; Rewrite <- plus_n_Sm;Apply lt_n_S; + Apply lt_O_Sn +| Simpl; Discriminate H2 +| Simpl; Discriminate H2 +| Simpl; Discriminate H2 ]. +Qed. + +(** [nat_of_P] is a morphism from [positive] to [nat] for [lt] (expressed + from [compare] on [positive]) + + Part 2: [lt] on [nat] is finer than [lt] on [positive] +*) + +Lemma convert_compare_INFERIEUR : + (x,y:positive)(lt (convert x) (convert y)) -> (compare x y EGAL) = INFERIEUR. +Proof. +Intros x y; Unfold gt; Elim (Dcompare (compare x y EGAL)); [ + Intros E; Rewrite (compare_convert_EGAL x y E); + Intros H;Absurd (lt (convert y) (convert y)); [ Apply lt_n_n | Assumption ] +| Intros H;Elim H; [ + Auto + | Intros H1 H2; Absurd (lt (convert x) (convert y)); [ + Apply lt_not_sym; Change (gt (convert x) (convert y)); + Apply compare_convert_SUPERIEUR; Assumption + | Assumption ]]]. +Qed. + +(** [nat_of_P] is a morphism from [positive] to [nat] for [gt] (expressed + from [compare] on [positive]) + + Part 2: [gt] on [nat] is finer than [gt] on [positive] +*) + +Lemma convert_compare_SUPERIEUR : + (x,y:positive)(gt (convert x) (convert y)) -> (compare x y EGAL) = SUPERIEUR. +Proof. +Intros x y; Unfold gt; Elim (Dcompare (compare x y EGAL)); [ + Intros E; Rewrite (compare_convert_EGAL x y E); + Intros H;Absurd (lt (convert y) (convert y)); [ Apply lt_n_n | Assumption ] +| Intros H;Elim H; [ + Intros H1 H2; Absurd (lt (convert y) (convert x)); [ + Apply lt_not_sym; Apply compare_convert_INFERIEUR; Assumption + | Assumption ] + | Auto]]. +Qed. + +(** [nat_of_P] is strictly positive *) + +Lemma compare_positive_to_nat_O : + (p:positive)(m:nat)(le m (positive_to_nat p m)). +NewInduction p; Simpl; Auto with arith. +Intro m; Apply le_trans with (plus m m); Auto with arith. +Qed. + +Lemma compare_convert_O : (p:positive)(lt O (convert p)). +Intro; Unfold convert; Apply lt_le_trans with (S O); Auto with arith. +Apply compare_positive_to_nat_O. +Qed. + +(** Pmult_nat permutes with multiplication *) + +Lemma positive_to_nat_mult : (p:positive) (n,m:nat) + (positive_to_nat p (mult m n))=(mult m (positive_to_nat p n)). +Proof. + Induction p. Intros. Simpl. Rewrite mult_plus_distr_r. Rewrite <- (mult_plus_distr_r m n n). + Rewrite (H (plus n n) m). Reflexivity. + Intros. Simpl. Rewrite <- (mult_plus_distr_r m n n). Apply H. + Trivial. +Qed. + +Lemma positive_to_nat_2 : (p:positive) + (positive_to_nat p (2))=(mult (2) (positive_to_nat p (1))). +Proof. + Intros. Rewrite <- positive_to_nat_mult. Reflexivity. +Qed. + +Lemma positive_to_nat_4 : (p:positive) + (positive_to_nat p (4))=(mult (2) (positive_to_nat p (2))). +Proof. + Intros. Rewrite <- positive_to_nat_mult. Reflexivity. +Qed. + +(** Mapping of xH, xO and xI through [nat_of_P] *) + +Lemma convert_xH : (convert xH)=(1). +Proof. + Reflexivity. +Qed. + +Lemma convert_xO : (p:positive) (convert (xO p))=(mult (2) (convert p)). +Proof. + Induction p. Unfold convert. Simpl. Intros. Rewrite positive_to_nat_2. + Rewrite positive_to_nat_4. Rewrite H. Simpl. Rewrite <- plus_Snm_nSm. Reflexivity. + Unfold convert. Simpl. Intros. Rewrite positive_to_nat_2. Rewrite positive_to_nat_4. + Rewrite H. Reflexivity. + Reflexivity. +Qed. + +Lemma convert_xI : (p:positive) (convert (xI p))=(S (mult (2) (convert p))). +Proof. + Induction p. Unfold convert. Simpl. Intro p0. Intro. Rewrite positive_to_nat_2. + Rewrite positive_to_nat_4; Injection H; Intro H1; Rewrite H1; Rewrite <- plus_Snm_nSm; Reflexivity. + Unfold convert. Simpl. Intros. Rewrite positive_to_nat_2. Rewrite positive_to_nat_4. + Injection H; Intro H1; Rewrite H1; Reflexivity. + Reflexivity. +Qed. + +(**********************************************************************) +(** Properties of the shifted injection from Peano natural numbers to + binary positive numbers *) + +(** Composition of [P_of_succ_nat] and [nat_of_P] is successor on [nat] *) + +Theorem bij1 : (m:nat) (convert (anti_convert m)) = (S m). +Proof. +Intro m; NewInduction m as [|n H]; [ + Reflexivity +| Simpl; Rewrite cvt_add_un; Rewrite H; Auto ]. +Qed. + +(** Miscellaneous lemmas on [P_of_succ_nat] *) + +Lemma ZL3: (x:nat) (add_un (anti_convert (plus x x))) = (xO (anti_convert x)). +Proof. +Intro x; NewInduction x as [|n H]; [ + Simpl; Auto with arith +| Simpl; Rewrite plus_sym; Simpl; Rewrite H; Rewrite ZL1;Auto with arith]. +Qed. + +Lemma ZL5: (x:nat) (anti_convert (plus (S x) (S x))) = (xI (anti_convert x)). +Proof. +Intro x; NewInduction x as [|n H];Simpl; [ + Auto with arith +| Rewrite <- plus_n_Sm; Simpl; Simpl in H; Rewrite H; Auto with arith]. +Qed. + +(** Composition of [nat_of_P] and [P_of_succ_nat] is successor on [positive] *) + +Theorem bij2 : (x:positive) (anti_convert (convert x)) = (add_un x). +Proof. +Intro x; NewInduction x as [p H|p H|]; [ + Simpl; Rewrite <- H; Change (2) with (plus (1) (1)); + Rewrite ZL2; Elim (ZL4 p); + Unfold convert; Intros n H1;Rewrite H1; Rewrite ZL3; Auto with arith +| Unfold convert ;Simpl; Change (2) with (plus (1) (1)); + Rewrite ZL2; + Rewrite <- (sub_add_one + (anti_convert + (plus (positive_to_nat p (S O)) (positive_to_nat p (S O))))); + Rewrite <- (sub_add_one (xI p)); + Simpl;Rewrite <- H;Elim (ZL4 p); Unfold convert ;Intros n H1;Rewrite H1; + Rewrite ZL5; Simpl; Trivial with arith +| Unfold convert; Simpl; Auto with arith ]. +Qed. + +(** Composition of [nat_of_P], [P_of_succ_nat] and [Ppred] is identity + on [positive] *) + +Theorem bij3: (x:positive)(sub_un (anti_convert (convert x))) = x. +Proof. +Intros x; Rewrite bij2; Rewrite sub_add_one; Trivial with arith. +Qed. + +(**********************************************************************) +(** Extra properties of the injection from binary positive numbers to Peano + natural numbers *) + +(** [nat_of_P] is a morphism for subtraction on positive numbers *) + +Theorem true_sub_convert: + (x,y:positive) (compare x y EGAL) = SUPERIEUR -> + (convert (true_sub x y)) = (minus (convert x) (convert y)). +Proof. +Intros x y H; Apply plus_reg_l with (convert y); +Rewrite le_plus_minus_r; [ + Rewrite <- convert_add; Rewrite sub_add; Auto with arith +| Apply lt_le_weak; Exact (compare_convert_SUPERIEUR x y H)]. +Qed. + +(** [nat_of_P] is injective *) + +Lemma convert_intro : (x,y:positive)(convert x)=(convert y) -> x=y. +Proof. +Intros x y H;Rewrite <- (bij3 x);Rewrite <- (bij3 y); Rewrite H; Trivial with arith. +Qed. + +Lemma ZL16: (p,q:positive)(lt (minus (convert p) (convert q)) (convert p)). +Proof. +Intros p q; Elim (ZL4 p);Elim (ZL4 q); Intros h H1 i H2; +Rewrite H1;Rewrite H2; Simpl;Unfold lt; Apply le_n_S; Apply le_minus. +Qed. + +Lemma ZL17: (p,q:positive)(lt (convert p) (convert (add p q))). +Proof. +Intros p q; Rewrite convert_add;Unfold lt;Elim (ZL4 q); Intros k H;Rewrite H; +Rewrite plus_sym;Simpl; Apply le_n_S; Apply le_plus_r. +Qed. + +(** Comparison and subtraction *) + +Lemma compare_true_sub_right : + (p,q,z:positive) + (compare q p EGAL)=INFERIEUR-> + (compare z p EGAL)=SUPERIEUR-> + (compare z q EGAL)=SUPERIEUR-> + (compare (true_sub z p) (true_sub z q) EGAL)=INFERIEUR. +Proof. +Intros; Apply convert_compare_INFERIEUR; Rewrite true_sub_convert; [ + Rewrite true_sub_convert; [ + Apply simpl_lt_plus_l with p:=(convert q); Rewrite le_plus_minus_r; [ + Rewrite plus_sym; Apply simpl_lt_plus_l with p:=(convert p); + Rewrite plus_assoc_l; Rewrite le_plus_minus_r; [ + Rewrite (plus_sym (convert p)); Apply lt_reg_l; + Apply compare_convert_INFERIEUR; Assumption + | Apply lt_le_weak; Apply compare_convert_INFERIEUR; + Apply ZC1; Assumption ] + | Apply lt_le_weak;Apply compare_convert_INFERIEUR; + Apply ZC1; Assumption ] + | Assumption ] + | Assumption ]. +Qed. + +Lemma compare_true_sub_left : + (p,q,z:positive) + (compare q p EGAL)=INFERIEUR-> + (compare p z EGAL)=SUPERIEUR-> + (compare q z EGAL)=SUPERIEUR-> + (compare (true_sub q z) (true_sub p z) EGAL)=INFERIEUR. +Proof. +Intros p q z; Intros; + Apply convert_compare_INFERIEUR; Rewrite true_sub_convert; [ + Rewrite true_sub_convert; [ + Unfold gt; Apply simpl_lt_plus_l with p:=(convert z); + Rewrite le_plus_minus_r; [ + Rewrite le_plus_minus_r; [ + Apply compare_convert_INFERIEUR;Assumption + | Apply lt_le_weak; Apply compare_convert_INFERIEUR;Apply ZC1;Assumption] + | Apply lt_le_weak; Apply compare_convert_INFERIEUR;Apply ZC1; Assumption] + | Assumption] +| Assumption]. +Qed. + +(** Distributivity of multiplication over subtraction *) + +Theorem times_true_sub_distr: + (x,y,z:positive) (compare y z EGAL) = SUPERIEUR -> + (times x (true_sub y z)) = (true_sub (times x y) (times x z)). +Proof. +Intros x y z H; Apply convert_intro; +Rewrite times_convert; Rewrite true_sub_convert; [ + Rewrite true_sub_convert; [ + Do 2 Rewrite times_convert; + Do 3 Rewrite (mult_sym (convert x));Apply mult_minus_distr + | Apply convert_compare_SUPERIEUR; Do 2 Rewrite times_convert; + Unfold gt; Elim (ZL4 x);Intros h H1;Rewrite H1; Apply lt_mult_left; + Exact (compare_convert_SUPERIEUR y z H) ] +| Assumption ]. +Qed. + |