diff options
Diffstat (limited to 'theories7/NArith')
| -rw-r--r-- | theories7/NArith/BinNat.v | 205 | ||||
| -rw-r--r-- | theories7/NArith/BinPos.v | 894 | ||||
| -rw-r--r-- | theories7/NArith/NArith.v | 14 | ||||
| -rw-r--r-- | theories7/NArith/Pnat.v | 472 |
4 files changed, 1585 insertions, 0 deletions
diff --git a/theories7/NArith/BinNat.v b/theories7/NArith/BinNat.v new file mode 100644 index 00000000..5e04e22e --- /dev/null +++ b/theories7/NArith/BinNat.v @@ -0,0 +1,205 @@ +(************************************************************************) +(* 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: BinNat.v,v 1.1.2.1 2004/07/16 19:31:30 herbelin Exp $ i*) + +Require BinPos. + +(**********************************************************************) +(** Binary natural numbers *) + +Inductive entier: Set := Nul : entier | Pos : positive -> entier. + +(** Declare binding key for scope positive_scope *) + +Delimits Scope N_scope with N. + +(** Automatically open scope N_scope for the constructors of N *) + +Bind Scope N_scope with entier. +Arguments Scope Pos [ N_scope ]. + +Open Local Scope N_scope. + +(** Operation x -> 2*x+1 *) + +Definition Un_suivi_de := [x] + Cases x of Nul => (Pos xH) | (Pos p) => (Pos (xI p)) end. + +(** Operation x -> 2*x *) + +Definition Zero_suivi_de := + [n] Cases n of Nul => Nul | (Pos p) => (Pos (xO p)) end. + +(** Successor *) + +Definition Nsucc := + [n] Cases n of Nul => (Pos xH) | (Pos p) => (Pos (add_un p)) end. + +(** Addition *) + +Definition Nplus := [n,m] + Cases n m of + | Nul _ => m + | _ Nul => n + | (Pos p) (Pos q) => (Pos (add p q)) + end. + +V8Infix "+" Nplus : N_scope. + +(** Multiplication *) + +Definition Nmult := [n,m] + Cases n m of + | Nul _ => Nul + | _ Nul => Nul + | (Pos p) (Pos q) => (Pos (times p q)) + end. + +V8Infix "*" Nmult : N_scope. + +(** Order *) + +Definition Ncompare := [n,m] + Cases n m of + | Nul Nul => EGAL + | Nul (Pos m') => INFERIEUR + | (Pos n') Nul => SUPERIEUR + | (Pos n') (Pos m') => (compare n' m' EGAL) + end. + +V8Infix "?=" Ncompare (at level 70, no associativity) : N_scope. + +(** Peano induction on binary natural numbers *) + +Theorem Nind : (P:(entier ->Prop)) + (P Nul) ->((n:entier)(P n) ->(P (Nsucc n))) ->(n:entier)(P n). +Proof. +NewDestruct n. + Assumption. + Apply Pind with P := [p](P (Pos p)). +Exact (H0 Nul H). +Intro p'; Exact (H0 (Pos p')). +Qed. + +(** Properties of addition *) + +Theorem Nplus_0_l : (n:entier)(Nplus Nul n)=n. +Proof. +Reflexivity. +Qed. + +Theorem Nplus_0_r : (n:entier)(Nplus n Nul)=n. +Proof. +NewDestruct n; Reflexivity. +Qed. + +Theorem Nplus_comm : (n,m:entier)(Nplus n m)=(Nplus m n). +Proof. +Intros. +NewDestruct n; NewDestruct m; Simpl; Try Reflexivity. +Rewrite add_sym; Reflexivity. +Qed. + +Theorem Nplus_assoc : + (n,m,p:entier)(Nplus n (Nplus m p))=(Nplus (Nplus n m) p). +Proof. +Intros. +NewDestruct n; Try Reflexivity. +NewDestruct m; Try Reflexivity. +NewDestruct p; Try Reflexivity. +Simpl; Rewrite add_assoc; Reflexivity. +Qed. + +Theorem Nplus_succ : (n,m:entier)(Nplus (Nsucc n) m)=(Nsucc (Nplus n m)). +Proof. +NewDestruct n; NewDestruct m. + Simpl; Reflexivity. + Unfold Nsucc Nplus; Rewrite <- ZL12bis; Reflexivity. + Simpl; Reflexivity. + Simpl; Rewrite ZL14bis; Reflexivity. +Qed. + +Theorem Nsucc_inj : (n,m:entier)(Nsucc n)=(Nsucc m)->n=m. +Proof. +NewDestruct n; NewDestruct m; Simpl; Intro H; + Reflexivity Orelse Injection H; Clear H; Intro H. + Symmetry in H; Contradiction add_un_not_un with p. + Contradiction add_un_not_un with p. + Rewrite add_un_inj with 1:=H; Reflexivity. +Qed. + +Theorem Nplus_reg_l : (n,m,p:entier)(Nplus n m)=(Nplus n p)->m=p. +Proof. +Intro n; Pattern n; Apply Nind; Clear n; Simpl. + Trivial. + Intros n IHn m p H0; Do 2 Rewrite Nplus_succ in H0. + Apply IHn; Apply Nsucc_inj; Assumption. +Qed. + +(** Properties of multiplication *) + +Theorem Nmult_1_l : (n:entier)(Nmult (Pos xH) n)=n. +Proof. +NewDestruct n; Reflexivity. +Qed. + +Theorem Nmult_1_r : (n:entier)(Nmult n (Pos xH))=n. +Proof. +NewDestruct n; Simpl; Try Reflexivity. +Rewrite times_x_1; Reflexivity. +Qed. + +Theorem Nmult_comm : (n,m:entier)(Nmult n m)=(Nmult m n). +Proof. +Intros. +NewDestruct n; NewDestruct m; Simpl; Try Reflexivity. +Rewrite times_sym; Reflexivity. +Qed. + +Theorem Nmult_assoc : + (n,m,p:entier)(Nmult n (Nmult m p))=(Nmult (Nmult n m) p). +Proof. +Intros. +NewDestruct n; Try Reflexivity. +NewDestruct m; Try Reflexivity. +NewDestruct p; Try Reflexivity. +Simpl; Rewrite times_assoc; Reflexivity. +Qed. + +Theorem Nmult_plus_distr_r : + (n,m,p:entier)(Nmult (Nplus n m) p)=(Nplus (Nmult n p) (Nmult m p)). +Proof. +Intros. +NewDestruct n; Try Reflexivity. +NewDestruct m; NewDestruct p; Try Reflexivity. +Simpl; Rewrite times_add_distr_l; Reflexivity. +Qed. + +Theorem Nmult_reg_r : (n,m,p:entier) ~p=Nul->(Nmult n p)=(Nmult m p) -> n=m. +Proof. +NewDestruct p; Intros Hp H. +Contradiction Hp; Reflexivity. +NewDestruct n; NewDestruct m; Reflexivity Orelse Try Discriminate H. +Injection H; Clear H; Intro H; Rewrite simpl_times_r with 1:=H; Reflexivity. +Qed. + +Theorem Nmult_0_l : (n:entier) (Nmult Nul n) = Nul. +Proof. +Reflexivity. +Qed. + +(** Properties of comparison *) + +Theorem Ncompare_Eq_eq : (n,m:entier) (Ncompare n m) = EGAL -> n = m. +Proof. +NewDestruct n as [|n]; NewDestruct m as [|m]; Simpl; Intro H; + Reflexivity Orelse Try Discriminate H. + Rewrite (compare_convert_EGAL n m H); Reflexivity. +Qed. + diff --git a/theories7/NArith/BinPos.v b/theories7/NArith/BinPos.v new file mode 100644 index 00000000..ae61587d --- /dev/null +++ b/theories7/NArith/BinPos.v @@ -0,0 +1,894 @@ +(************************************************************************) +(* 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: BinPos.v,v 1.1.2.1 2004/07/16 19:31:31 herbelin Exp $ i*) + +(**********************************************************************) +(** Binary positive numbers *) + +(** Original development by Pierre Crégut, CNET, Lannion, France *) + +Inductive positive : Set := + xI : positive -> positive +| xO : positive -> positive +| xH : positive. + +(** Declare binding key for scope positive_scope *) + +Delimits Scope positive_scope with positive. + +(** Automatically open scope positive_scope for type positive, xO and xI *) + +Bind Scope positive_scope with positive. +Arguments Scope xO [ positive_scope ]. +Arguments Scope xI [ positive_scope ]. + +(** Successor *) + +Fixpoint add_un [x:positive]:positive := + Cases x of + (xI x') => (xO (add_un x')) + | (xO x') => (xI x') + | xH => (xO xH) + end. + +(** Addition *) + +Fixpoint add [x:positive]:positive -> positive := [y:positive] + Cases x y of + | (xI x') (xI y') => (xO (add_carry x' y')) + | (xI x') (xO y') => (xI (add x' y')) + | (xI x') xH => (xO (add_un x')) + | (xO x') (xI y') => (xI (add x' y')) + | (xO x') (xO y') => (xO (add x' y')) + | (xO x') xH => (xI x') + | xH (xI y') => (xO (add_un y')) + | xH (xO y') => (xI y') + | xH xH => (xO xH) + end +with add_carry [x:positive]:positive -> positive := [y:positive] + Cases x y of + | (xI x') (xI y') => (xI (add_carry x' y')) + | (xI x') (xO y') => (xO (add_carry x' y')) + | (xI x') xH => (xI (add_un x')) + | (xO x') (xI y') => (xO (add_carry x' y')) + | (xO x') (xO y') => (xI (add x' y')) + | (xO x') xH => (xO (add_un x')) + | xH (xI y') => (xI (add_un y')) + | xH (xO y') => (xO (add_un y')) + | xH xH => (xI xH) + end. + +V7only [Notation "x + y" := (add x y) : positive_scope.]. +V8Infix "+" add : positive_scope. + +Open Local Scope positive_scope. + +(** From binary positive numbers to Peano natural numbers *) + +Fixpoint positive_to_nat [x:positive]:nat -> nat := + [pow2:nat] + Cases x of + (xI x') => (plus pow2 (positive_to_nat x' (plus pow2 pow2))) + | (xO x') => (positive_to_nat x' (plus pow2 pow2)) + | xH => pow2 + end. + +Definition convert := [x:positive] (positive_to_nat x (S O)). + +(** From Peano natural numbers to binary positive numbers *) + +Fixpoint anti_convert [n:nat]: positive := + Cases n of + O => xH + | (S x') => (add_un (anti_convert x')) + end. + +(** Operation x -> 2*x-1 *) + +Fixpoint double_moins_un [x:positive]:positive := + Cases x of + (xI x') => (xI (xO x')) + | (xO x') => (xI (double_moins_un x')) + | xH => xH + end. + +(** Predecessor *) + +Definition sub_un := [x:positive] + Cases x of + (xI x') => (xO x') + | (xO x') => (double_moins_un x') + | xH => xH + end. + +(** An auxiliary type for subtraction *) + +Inductive positive_mask: Set := + IsNul : positive_mask + | IsPos : positive -> positive_mask + | IsNeg : positive_mask. + +(** Operation x -> 2*x+1 *) + +Definition Un_suivi_de_mask := [x:positive_mask] + Cases x of IsNul => (IsPos xH) | IsNeg => IsNeg | (IsPos p) => (IsPos (xI p)) end. + +(** Operation x -> 2*x *) + +Definition Zero_suivi_de_mask := [x:positive_mask] + Cases x of IsNul => IsNul | IsNeg => IsNeg | (IsPos p) => (IsPos (xO p)) end. + +(** Operation x -> 2*x-2 *) + +Definition double_moins_deux := + [x:positive] Cases x of + (xI x') => (IsPos (xO (xO x'))) + | (xO x') => (IsPos (xO (double_moins_un x'))) + | xH => IsNul + end. + +(** Subtraction of binary positive numbers into a positive numbers mask *) + +Fixpoint sub_pos[x,y:positive]:positive_mask := + Cases x y of + | (xI x') (xI y') => (Zero_suivi_de_mask (sub_pos x' y')) + | (xI x') (xO y') => (Un_suivi_de_mask (sub_pos x' y')) + | (xI x') xH => (IsPos (xO x')) + | (xO x') (xI y') => (Un_suivi_de_mask (sub_neg x' y')) + | (xO x') (xO y') => (Zero_suivi_de_mask (sub_pos x' y')) + | (xO x') xH => (IsPos (double_moins_un x')) + | xH xH => IsNul + | xH _ => IsNeg + end +with sub_neg [x,y:positive]:positive_mask := + Cases x y of + (xI x') (xI y') => (Un_suivi_de_mask (sub_neg x' y')) + | (xI x') (xO y') => (Zero_suivi_de_mask (sub_pos x' y')) + | (xI x') xH => (IsPos (double_moins_un x')) + | (xO x') (xI y') => (Zero_suivi_de_mask (sub_neg x' y')) + | (xO x') (xO y') => (Un_suivi_de_mask (sub_neg x' y')) + | (xO x') xH => (double_moins_deux x') + | xH _ => IsNeg + end. + +(** Subtraction of binary positive numbers x and y, returns 1 if x<=y *) + +Definition true_sub := [x,y:positive] + Cases (sub_pos x y) of (IsPos z) => z | _ => xH end. + +V8Infix "-" true_sub : positive_scope. + +(** Multiplication on binary positive numbers *) + +Fixpoint times [x:positive] : positive -> positive:= + [y:positive] + Cases x of + (xI x') => (add y (xO (times x' y))) + | (xO x') => (xO (times x' y)) + | xH => y + end. + +V8Infix "*" times : positive_scope. + +(** Division by 2 rounded below but for 1 *) + +Definition Zdiv2_pos := + [z:positive]Cases z of xH => xH + | (xO p) => p + | (xI p) => p + end. + +V8Infix "/" Zdiv2_pos : positive_scope. + +(** Comparison on binary positive numbers *) + +Fixpoint compare [x,y:positive]: relation -> relation := + [r:relation] + Cases x y of + | (xI x') (xI y') => (compare x' y' r) + | (xI x') (xO y') => (compare x' y' SUPERIEUR) + | (xI x') xH => SUPERIEUR + | (xO x') (xI y') => (compare x' y' INFERIEUR) + | (xO x') (xO y') => (compare x' y' r) + | (xO x') xH => SUPERIEUR + | xH (xI y') => INFERIEUR + | xH (xO y') => INFERIEUR + | xH xH => r + end. + +V8Infix "?=" compare (at level 70, no associativity) : positive_scope. + +(**********************************************************************) +(** Miscellaneous properties of binary positive numbers *) + +Lemma ZL11: (x:positive) (x=xH) \/ ~(x=xH). +Proof. +Intros x;Case x;Intros; (Left;Reflexivity) Orelse (Right;Discriminate). +Qed. + +(**********************************************************************) +(** Properties of successor on binary positive numbers *) + +(** Specification of [xI] in term of [Psucc] and [xO] *) + +Lemma xI_add_un_xO : (x:positive)(xI x) = (add_un (xO x)). +Proof. +Reflexivity. +Qed. + +Lemma add_un_discr : (x:positive)x<>(add_un x). +Proof. +Intro x; NewDestruct x; Discriminate. +Qed. + +(** Successor and double *) + +Lemma is_double_moins_un : (x:positive) (add_un (double_moins_un x)) = (xO x). +Proof. +Intro x; NewInduction x as [x IHx|x|]; Simpl; Try Rewrite IHx; Reflexivity. +Qed. + +Lemma double_moins_un_add_un_xI : + (x:positive)(double_moins_un (add_un x))=(xI x). +Proof. +Intro x;NewInduction x as [x IHx|x|]; Simpl; Try Rewrite IHx; Reflexivity. +Qed. + +Lemma ZL1: (y:positive)(xO (add_un y)) = (add_un (add_un (xO y))). +Proof. +Intro y; Induction y; Simpl; Auto. +Qed. + +Lemma double_moins_un_xO_discr : (x:positive)(double_moins_un x)<>(xO x). +Proof. +Intro x; NewDestruct x; Discriminate. +Qed. + +(** Successor and predecessor *) + +Lemma add_un_not_un : (x:positive) (add_un x) <> xH. +Proof. +Intro x; NewDestruct x as [x|x|]; Discriminate. +Qed. + +Lemma sub_add_one : (x:positive) (sub_un (add_un x)) = x. +Proof. +(Intro x; NewDestruct x as [p|p|]; [Idtac | Idtac | Simpl;Auto]); +(NewInduction p as [p IHp||]; [Idtac | Reflexivity | Reflexivity ]); +Simpl; Simpl in IHp; Try Rewrite <- IHp; Reflexivity. +Qed. + +Lemma add_sub_one : (x:positive) (x=xH) \/ (add_un (sub_un x)) = x. +Proof. +Intro x; Induction x; [ + Simpl; Auto +| Simpl; Intros;Right;Apply is_double_moins_un +| Auto ]. +Qed. + +(** Injectivity of successor *) + +Lemma add_un_inj : (x,y:positive) (add_un x)=(add_un y) -> x=y. +Proof. +Intro x;NewInduction x; Intro y; NewDestruct y as [y|y|]; Simpl; + Intro H; Discriminate H Orelse Try (Injection H; Clear H; Intro H). +Rewrite (IHx y H); Reflexivity. +Absurd (add_un x)=xH; [ Apply add_un_not_un | Assumption ]. +Apply f_equal with 1:=H; Assumption. +Absurd (add_un y)=xH; [ Apply add_un_not_un | Symmetry; Assumption ]. +Reflexivity. +Qed. + +(**********************************************************************) +(** Properties of addition on binary positive numbers *) + +(** Specification of [Psucc] in term of [Pplus] *) + +Lemma ZL12: (q:positive) (add_un q) = (add q xH). +Proof. +Intro q; NewDestruct q; Reflexivity. +Qed. + +Lemma ZL12bis: (q:positive) (add_un q) = (add xH q). +Proof. +Intro q; NewDestruct q; Reflexivity. +Qed. + +(** Specification of [Pplus_carry] *) + +Theorem ZL13: (x,y:positive)(add_carry x y) = (add_un (add x y)). +Proof. +(Intro x; NewInduction x as [p IHp|p IHp|];Intro y; NewDestruct y;Simpl;Auto); + Rewrite IHp; Auto. +Qed. + +(** Commutativity *) + +Theorem add_sym : (x,y:positive) (add x y) = (add y x). +Proof. +Intro x; NewInduction x as [p IHp|p IHp|];Intro y; NewDestruct y;Simpl;Auto; + Try Do 2 Rewrite ZL13; Rewrite IHp;Auto. +Qed. + +(** Permutation of [Pplus] and [Psucc] *) + +Theorem ZL14: (x,y:positive)(add x (add_un y)) = (add_un (add x y)). +Proof. +Intro x; NewInduction x as [p IHp|p IHp|];Intro y; NewDestruct y;Simpl;Auto; [ + Rewrite ZL13; Rewrite IHp; Auto +| Rewrite ZL13; Auto +| NewDestruct p;Simpl;Auto +| Rewrite IHp;Auto +| NewDestruct p;Simpl;Auto ]. +Qed. + +Theorem ZL14bis: (x,y:positive)(add (add_un x) y) = (add_un (add x y)). +Proof. +Intros x y; Rewrite add_sym; Rewrite add_sym with x:=x; Apply ZL14. +Qed. + +Theorem ZL15: (q,z:positive) ~z=xH -> (add_carry q (sub_un z)) = (add q z). +Proof. +Intros q z H; Elim (add_sub_one z); [ + Intro;Absurd z=xH;Auto +| Intros E;Pattern 2 z ;Rewrite <- E; Rewrite ZL14; Rewrite ZL13; Trivial ]. +Qed. + +(** No neutral for addition on strictly positive numbers *) + +Lemma add_no_neutral : (x,y:positive) ~(add y x)=x. +Proof. +Intro x;NewInduction x; Intro y; NewDestruct y as [y|y|]; Simpl; Intro H; + Discriminate H Orelse Injection H; Clear H; Intro H; Apply (IHx y H). +Qed. + +Lemma add_carry_not_add_un : (x,y:positive) ~(add_carry y x)=(add_un x). +Proof. +Intros x y H; Absurd (add y x)=x; + [ Apply add_no_neutral + | Apply add_un_inj; Rewrite <- ZL13; Assumption ]. +Qed. + +(** Simplification *) + +Lemma add_carry_add : + (x,y,z,t:positive) (add_carry x z)=(add_carry y t) -> (add x z)=(add y t). +Proof. +Intros x y z t H; Apply add_un_inj; Do 2 Rewrite <- ZL13; Assumption. +Qed. + +Lemma simpl_add_r : (x,y,z:positive) (add x z)=(add y z) -> x=y. +Proof. +Intros x y z; Generalize x y; Clear x y. +NewInduction z as [z|z|]. + NewDestruct x as [x|x|]; Intro y; NewDestruct y as [y|y|]; Simpl; Intro H; + Discriminate H Orelse Try (Injection H; Clear H; Intro H). + Rewrite IHz with 1:=(add_carry_add ? ? ? ? H); Reflexivity. + Absurd (add_carry x z)=(add_un z); + [ Apply add_carry_not_add_un | Assumption ]. + Rewrite IHz with 1:=H; Reflexivity. + Symmetry in H; Absurd (add_carry y z)=(add_un z); + [ Apply add_carry_not_add_un | Assumption ]. + Reflexivity. + NewDestruct x as [x|x|]; Intro y; NewDestruct y as [y|y|]; Simpl; Intro H; + Discriminate H Orelse Try (Injection H; Clear H; Intro H). + Rewrite IHz with 1:=H; Reflexivity. + Absurd (add x z)=z; [ Apply add_no_neutral | Assumption ]. + Rewrite IHz with 1:=H; Reflexivity. + Symmetry in H; Absurd y+z=z; [ Apply add_no_neutral | Assumption ]. + Reflexivity. + Intros H x y; Apply add_un_inj; Do 2 Rewrite ZL12; Assumption. +Qed. + +Lemma simpl_add_l : (x,y,z:positive) (add x y)=(add x z) -> y=z. +Proof. +Intros x y z H;Apply simpl_add_r with z:=x; + Rewrite add_sym with x:=z; Rewrite add_sym with x:=y; Assumption. +Qed. + +Lemma simpl_add_carry_r : + (x,y,z:positive) (add_carry x z)=(add_carry y z) -> x=y. +Proof. +Intros x y z H; Apply simpl_add_r with z:=z; Apply add_carry_add; Assumption. +Qed. + +Lemma simpl_add_carry_l : + (x,y,z:positive) (add_carry x y)=(add_carry x z) -> y=z. +Proof. +Intros x y z H;Apply simpl_add_r with z:=x; +Rewrite add_sym with x:=z; Rewrite add_sym with x:=y; Apply add_carry_add; +Assumption. +Qed. + +(** Addition on positive is associative *) + +Theorem add_assoc: (x,y,z:positive)(add x (add y z)) = (add (add x y) z). +Proof. +Intros x y; Generalize x; Clear x. +NewInduction y as [y|y|]; Intro x. + NewDestruct x as [x|x|]; + Intro z; NewDestruct z as [z|z|]; Simpl; Repeat Rewrite ZL13; + Repeat Rewrite ZL14; Repeat Rewrite ZL14bis; Reflexivity Orelse + Repeat Apply f_equal with A:=positive; Apply IHy. + NewDestruct x as [x|x|]; + Intro z; NewDestruct z as [z|z|]; Simpl; Repeat Rewrite ZL13; + Repeat Rewrite ZL14; Repeat Rewrite ZL14bis; Reflexivity Orelse + Repeat Apply f_equal with A:=positive; Apply IHy. + Intro z; Rewrite add_sym with x:=xH; Do 2 Rewrite <- ZL12; Rewrite ZL14bis; Rewrite ZL14; Reflexivity. +Qed. + +(** Commutation of addition with the double of a positive number *) + +Lemma add_xI_double_moins_un : + (p,q:positive)(xO (add p q)) = (add (xI p) (double_moins_un q)). +Proof. +Intros; Change (xI p) with (add (xO p) xH). +Rewrite <- add_assoc; Rewrite <- ZL12bis; Rewrite is_double_moins_un. +Reflexivity. +Qed. + +Lemma add_xO_double_moins_un : + (p,q:positive) (double_moins_un (add p q)) = (add (xO p) (double_moins_un q)). +Proof. +NewInduction p as [p IHp|p IHp|]; NewDestruct q as [q|q|]; + Simpl; Try Rewrite ZL13; Try Rewrite double_moins_un_add_un_xI; + Try Rewrite IHp; Try Rewrite add_xI_double_moins_un; Try Reflexivity. + Rewrite <- is_double_moins_un; Rewrite ZL12bis; Reflexivity. +Qed. + +(** Misc *) + +Lemma add_x_x : (x:positive) (add x x) = (xO x). +Proof. +Intro x;NewInduction x; Simpl; Try Rewrite ZL13; Try Rewrite IHx; Reflexivity. +Qed. + +(**********************************************************************) +(** Peano induction on binary positive positive numbers *) + +Fixpoint plus_iter [x:positive] : positive -> positive := + [y]Cases x of + | xH => (add_un y) + | (xO x) => (plus_iter x (plus_iter x y)) + | (xI x) => (plus_iter x (plus_iter x (add_un y))) + end. + +Lemma plus_iter_add : (x,y:positive)(plus_iter x y)=(add x y). +Proof. +Intro x;NewInduction x as [p IHp|p IHp|]; Intro y; NewDestruct y; Simpl; + Reflexivity Orelse Do 2 Rewrite IHp; Rewrite add_assoc; Rewrite add_x_x; + Try Reflexivity. +Rewrite ZL13; Rewrite <- ZL14; Reflexivity. +Rewrite ZL12; Reflexivity. +Qed. + +Lemma plus_iter_xO : (x:positive)(plus_iter x x)=(xO x). +Proof. +Intro; Rewrite <- add_x_x; Apply plus_iter_add. +Qed. + +Lemma plus_iter_xI : (x:positive)(add_un (plus_iter x x))=(xI x). +Proof. +Intro; Rewrite xI_add_un_xO; Rewrite <- add_x_x; + Apply (f_equal positive); Apply plus_iter_add. +Qed. + +Lemma iterate_add : (P:(positive->Type)) + ((n:positive)(P n) ->(P (add_un n)))->(p,n:positive)(P n) -> + (P (plus_iter p n)). +Proof. +Intros P H; NewInduction p; Simpl; Intros. +Apply IHp; Apply IHp; Apply H; Assumption. +Apply IHp; Apply IHp; Assumption. +Apply H; Assumption. +Defined. + +(** Peano induction *) + +Theorem Pind : (P:(positive->Prop)) + (P xH) ->((n:positive)(P n) ->(P (add_un n))) ->(n:positive)(P n). +Proof. +Intros P H1 Hsucc n; NewInduction n. +Rewrite <- plus_iter_xI; Apply Hsucc; Apply iterate_add; Assumption. +Rewrite <- plus_iter_xO; Apply iterate_add; Assumption. +Assumption. +Qed. + +(** Peano recursion *) + +Definition Prec : (A:Set)A->(positive->A->A)->positive->A := + [A;a;f]Fix Prec { Prec [p:positive] : A := + Cases p of + | xH => a + | (xO p) => (iterate_add [_]A f p p (Prec p)) + | (xI p) => (f (plus_iter p p) (iterate_add [_]A f p p (Prec p))) + end}. + +(** Peano case analysis *) + +Theorem Pcase : (P:(positive->Prop)) + (P xH) ->((n:positive)(P (add_un n))) ->(n:positive)(P n). +Proof. +Intros; Apply Pind; Auto. +Qed. + +Check + let fact = (Prec positive xH [p;r](times (add_un p) r)) in + let seven = (xI (xI xH)) in + let five_thousand_forty= (xO(xO(xO(xO(xI(xI(xO(xI(xI(xI(xO(xO xH)))))))))))) + in ((refl_equal ? ?) :: (fact seven) = five_thousand_forty). + +(**********************************************************************) +(** Properties of multiplication on binary positive numbers *) + +(** One is right neutral for multiplication *) + +Lemma times_x_1 : (x:positive) (times x xH) = x. +Proof. +Intro x;NewInduction x; Simpl. + Rewrite IHx; Reflexivity. + Rewrite IHx; Reflexivity. + Reflexivity. +Qed. + +(** Right reduction properties for multiplication *) + +Lemma times_x_double : (x,y:positive) (times x (xO y)) = (xO (times x y)). +Proof. +Intros x y; NewInduction x; Simpl. + Rewrite IHx; Reflexivity. + Rewrite IHx; Reflexivity. + Reflexivity. +Qed. + +Lemma times_x_double_plus_one : + (x,y:positive) (times x (xI y)) = (add x (xO (times x y))). +Proof. +Intros x y; NewInduction x; Simpl. + Rewrite IHx; Do 2 Rewrite add_assoc; Rewrite add_sym with x:=y; Reflexivity. + Rewrite IHx; Reflexivity. + Reflexivity. +Qed. + +(** Commutativity of multiplication *) + +Theorem times_sym : (x,y:positive) (times x y) = (times y x). +Proof. +Intros x y; NewInduction y; Simpl. + Rewrite <- IHy; Apply times_x_double_plus_one. + Rewrite <- IHy; Apply times_x_double. + Apply times_x_1. +Qed. + +(** Distributivity of multiplication over addition *) + +Theorem times_add_distr: + (x,y,z:positive) (times x (add y z)) = (add (times x y) (times x z)). +Proof. +Intros x y z; NewInduction x; Simpl. + Rewrite IHx; Rewrite <- add_assoc with y := (xO (times x y)); + Rewrite -> add_assoc with x := (xO (times x y)); + Rewrite -> add_sym with x := (xO (times x y)); + Rewrite <- add_assoc with y := (xO (times x y)); + Rewrite -> add_assoc with y := z; Reflexivity. + Rewrite IHx; Reflexivity. + Reflexivity. +Qed. + +Theorem times_add_distr_l: + (x,y,z:positive) (times (add x y) z) = (add (times x z) (times y z)). +Proof. +Intros x y z; Do 3 Rewrite times_sym with y:=z; Apply times_add_distr. +Qed. + +(** Associativity of multiplication *) + +Theorem times_assoc : + ((x,y,z:positive) (times x (times y z))= (times (times x y) z)). +Proof. +Intro x;NewInduction x as [x|x|]; Simpl; Intros y z. + Rewrite IHx; Rewrite times_add_distr_l; Reflexivity. + Rewrite IHx; Reflexivity. + Reflexivity. +Qed. + +(** Parity properties of multiplication *) + +Lemma times_discr_xO_xI : + (x,y,z:positive)(times (xI x) z)<>(times (xO y) z). +Proof. +Intros x y z; NewInduction z as [|z IHz|]; Try Discriminate. +Intro H; Apply IHz; Clear IHz. +Do 2 Rewrite times_x_double in H. +Injection H; Clear H; Intro H; Exact H. +Qed. + +Lemma times_discr_xO : (x,y:positive)(times (xO x) y)<>y. +Proof. +Intros x y; NewInduction y; Try Discriminate. +Rewrite times_x_double; Injection; Assumption. +Qed. + +(** Simplification properties of multiplication *) + +Theorem simpl_times_r : (x,y,z:positive) (times x z)=(times y z) -> x=y. +Proof. +Intro x;NewInduction x as [p IHp|p IHp|]; Intro y; NewDestruct y as [q|q|]; Intros z H; + Reflexivity Orelse Apply (f_equal positive) Orelse Apply False_ind. + Simpl in H; Apply IHp with (xO z); Simpl; Do 2 Rewrite times_x_double; + Apply simpl_add_l with 1 := H. + Apply times_discr_xO_xI with 1 := H. + Simpl in H; Rewrite add_sym in H; Apply add_no_neutral with 1 := H. + Symmetry in H; Apply times_discr_xO_xI with 1 := H. + Apply IHp with (xO z); Simpl; Do 2 Rewrite times_x_double; Assumption. + Apply times_discr_xO with 1:=H. + Simpl in H; Symmetry in H; Rewrite add_sym in H; + Apply add_no_neutral with 1 := H. + Symmetry in H; Apply times_discr_xO with 1:=H. +Qed. + +Theorem simpl_times_l : (x,y,z:positive) (times z x)=(times z y) -> x=y. +Proof. +Intros x y z H; Apply simpl_times_r with z:=z. +Rewrite times_sym with x:=x; Rewrite times_sym with x:=y; Assumption. +Qed. + +(** Inversion of multiplication *) + +Lemma times_one_inversion_l : (x,y:positive) (times x y)=xH -> x=xH. +Proof. +Intros x y; NewDestruct x; Simpl. + NewDestruct y; Intro; Discriminate. + Intro; Discriminate. + Reflexivity. +Qed. + +(**********************************************************************) +(** Properties of comparison on binary positive numbers *) + +Theorem compare_convert1 : + (x,y:positive) + ~(compare x y SUPERIEUR) = EGAL /\ ~(compare x y INFERIEUR) = EGAL. +Proof. +Intro x; NewInduction x as [p IHp|p IHp|]; Intro y; NewDestruct y as [q|q|]; + Split;Simpl;Auto; + Discriminate Orelse (Elim (IHp q); Auto). +Qed. + +Theorem compare_convert_EGAL : (x,y:positive) (compare x y EGAL) = EGAL -> x=y. +Proof. +Intro x; NewInduction x as [p IHp|p IHp|]; + Intro y; NewDestruct y as [q|q|];Simpl;Auto; Intro H; [ + Rewrite (IHp q); Trivial +| Absurd (compare p q SUPERIEUR)=EGAL ; + [ Elim (compare_convert1 p q);Auto | Assumption ] +| Discriminate H +| Absurd (compare p q INFERIEUR) = EGAL; + [ Elim (compare_convert1 p q);Auto | Assumption ] +| Rewrite (IHp q);Auto +| Discriminate H +| Discriminate H +| Discriminate H ]. +Qed. + +Lemma ZLSI: + (x,y:positive) (compare x y SUPERIEUR) = INFERIEUR -> + (compare x y EGAL) = INFERIEUR. +Proof. +Intro x; Induction x;Intro y; Induction y;Simpl;Auto; + Discriminate Orelse Intros H;Discriminate H. +Qed. + +Lemma ZLIS: + (x,y:positive) (compare x y INFERIEUR) = SUPERIEUR -> + (compare x y EGAL) = SUPERIEUR. +Proof. +Intro x; Induction x;Intro y; Induction y;Simpl;Auto; + Discriminate Orelse Intros H;Discriminate H. +Qed. + +Lemma ZLII: + (x,y:positive) (compare x y INFERIEUR) = INFERIEUR -> + (compare x y EGAL) = INFERIEUR \/ x = y. +Proof. +(Intro x; NewInduction x as [p IHp|p IHp|]; + Intro y; NewDestruct y as [q|q|];Simpl;Auto;Try Discriminate); + Intro H2; Elim (IHp q H2);Auto; Intros E;Rewrite E; + Auto. +Qed. + +Lemma ZLSS: + (x,y:positive) (compare x y SUPERIEUR) = SUPERIEUR -> + (compare x y EGAL) = SUPERIEUR \/ x = y. +Proof. +(Intro x; NewInduction x as [p IHp|p IHp|]; + Intro y; NewDestruct y as [q|q|];Simpl;Auto;Try Discriminate); + Intro H2; Elim (IHp q H2);Auto; Intros E;Rewrite E; + Auto. +Qed. + +Lemma Dcompare : (r:relation) r=EGAL \/ r = INFERIEUR \/ r = SUPERIEUR. +Proof. +Induction r; Auto. +Qed. + +Tactic Definition ElimPcompare c1 c2:= + Elim (Dcompare (compare c1 c2 EGAL)); [ Idtac | + Let x = FreshId "H" In Intro x; Case x; Clear x ]. + +Theorem convert_compare_EGAL: (x:positive)(compare x x EGAL)=EGAL. +Intro x; Induction x; Auto. +Qed. + +Lemma Pcompare_antisym : + (x,y:positive)(r:relation) (Op (compare x y r)) = (compare y x (Op r)). +Proof. +Intro x; NewInduction x as [p IHp|p IHp|]; Intro y; NewDestruct y; +Intro r; Reflexivity Orelse (Symmetry; Assumption) Orelse Discriminate H +Orelse Simpl; Apply IHp Orelse Try Rewrite IHp; Try Reflexivity. +Qed. + +Lemma ZC1: + (x,y:positive)(compare x y EGAL)=SUPERIEUR -> (compare y x EGAL)=INFERIEUR. +Proof. +Intros; Change EGAL with (Op EGAL). +Rewrite <- Pcompare_antisym; Rewrite H; Reflexivity. +Qed. + +Lemma ZC2: + (x,y:positive)(compare x y EGAL)=INFERIEUR -> (compare y x EGAL)=SUPERIEUR. +Proof. +Intros; Change EGAL with (Op EGAL). +Rewrite <- Pcompare_antisym; Rewrite H; Reflexivity. +Qed. + +Lemma ZC3: (x,y:positive)(compare x y EGAL)=EGAL -> (compare y x EGAL)=EGAL. +Proof. +Intros; Change EGAL with (Op EGAL). +Rewrite <- Pcompare_antisym; Rewrite H; Reflexivity. +Qed. + +Lemma ZC4: (x,y:positive) (compare x y EGAL) = (Op (compare y x EGAL)). +Proof. +Intros; Change 1 EGAL with (Op EGAL). +Symmetry; Apply Pcompare_antisym. +Qed. + +(**********************************************************************) +(** Properties of subtraction on binary positive numbers *) + +Lemma ZS: (p:positive_mask) (Zero_suivi_de_mask p) = IsNul -> p = IsNul. +Proof. +NewDestruct p; Simpl; [ Trivial | Discriminate 1 | Discriminate 1 ]. +Qed. + +Lemma US: (p:positive_mask) ~(Un_suivi_de_mask p)=IsNul. +Proof. +Induction p; Intros; Discriminate. +Qed. + +Lemma USH: (p:positive_mask) (Un_suivi_de_mask p) = (IsPos xH) -> p = IsNul. +Proof. +NewDestruct p; Simpl; [ Trivial | Discriminate 1 | Discriminate 1 ]. +Qed. + +Lemma ZSH: (p:positive_mask) ~(Zero_suivi_de_mask p)= (IsPos xH). +Proof. +Induction p; Intros; Discriminate. +Qed. + +Theorem sub_pos_x_x : (x:positive) (sub_pos x x) = IsNul. +Proof. +Intro x; NewInduction x as [p IHp|p IHp|]; [ + Simpl; Rewrite IHp;Simpl; Trivial +| Simpl; Rewrite IHp;Auto +| Auto ]. +Qed. + +Lemma ZL10: (x,y:positive) + (sub_pos x y) = (IsPos xH) -> (sub_neg x y) = IsNul. +Proof. +Intro x; NewInduction x as [p|p|]; Intro y; NewDestruct y as [q|q|]; Simpl; + Intro H; Try Discriminate H; [ + Absurd (Zero_suivi_de_mask (sub_pos p q))=(IsPos xH); + [ Apply ZSH | Assumption ] +| Assert Heq : (sub_pos p q)=IsNul; + [ Apply USH;Assumption | Rewrite Heq; Reflexivity ] +| Assert Heq : (sub_neg p q)=IsNul; + [ Apply USH;Assumption | Rewrite Heq; Reflexivity ] +| Absurd (Zero_suivi_de_mask (sub_pos p q))=(IsPos xH); + [ Apply ZSH | Assumption ] +| NewDestruct p; Simpl; [ Discriminate H | Discriminate H | Reflexivity ] ]. +Qed. + +(** Properties of subtraction valid only for x>y *) + +Lemma sub_pos_SUPERIEUR: + (x,y:positive)(compare x y EGAL)=SUPERIEUR -> + (EX h:positive | (sub_pos x y) = (IsPos h) /\ (add y h) = x /\ + (h = xH \/ (sub_neg x y) = (IsPos (sub_un h)))). +Proof. +Intro x;NewInduction x as [p|p|];Intro y; NewDestruct y as [q|q|]; Simpl; Intro H; + Try Discriminate H. + NewDestruct (IHp q H) as [z [H4 [H6 H7]]]; Exists (xO z); Split. + Rewrite H4; Reflexivity. + Split. + Simpl; Rewrite H6; Reflexivity. + Right; Clear H6; NewDestruct (ZL11 z) as [H8|H8]; [ + Rewrite H8; Rewrite H8 in H4; + Rewrite ZL10; [ Reflexivity | Assumption ] + | Clear H4; NewDestruct H7 as [H9|H9]; [ + Absurd z=xH; Assumption + | Rewrite H9; Clear H9; NewDestruct z; + [ Reflexivity | Reflexivity | Absurd xH=xH; Trivial ]]]. + Case ZLSS with 1:=H; [ + Intros H3;Elim (IHp q H3); Intros z H4; Exists (xI z); + Elim H4;Intros H5 H6;Elim H6;Intros H7 H8; Split; [ + Simpl;Rewrite H5;Auto + | Split; [ + Simpl; Rewrite H7; Trivial + | Right; + Change (Zero_suivi_de_mask (sub_pos p q))=(IsPos (sub_un (xI z))); + Rewrite H5; Auto ]] + | Intros H3; Exists xH; Rewrite H3; Split; [ + Simpl; Rewrite sub_pos_x_x; Auto + | Split; Auto ]]. + Exists (xO p); Auto. + NewDestruct (IHp q) as [z [H4 [H6 H7]]]. + Apply ZLIS; Assumption. + NewDestruct (ZL11 z) as [vZ|]; [ + Exists xH; Split; [ + Rewrite ZL10; [ Reflexivity | Rewrite vZ in H4;Assumption ] + | Split; [ + Simpl; Rewrite ZL12; Rewrite <- vZ; Rewrite H6; Trivial + | Auto ]] + | Exists (xI (sub_un z)); NewDestruct H7 as [|H8];[ + Absurd z=xH;Assumption + | Split; [ + Rewrite H8; Trivial + | Split; [ Simpl; Rewrite ZL15; [ + Rewrite H6;Trivial + | Assumption ] + | Right; Rewrite H8; Reflexivity]]]]. + NewDestruct (IHp q H) as [z [H4 [H6 H7]]]. + Exists (xO z); Split; [ + Rewrite H4;Auto + | Split; [ + Simpl;Rewrite H6;Reflexivity + | Right; + Change (Un_suivi_de_mask (sub_neg p q))=(IsPos (double_moins_un z)); + NewDestruct (ZL11 z) as [H8|H8]; [ + Rewrite H8; Simpl; + Assert H9:(sub_neg p q)=IsNul;[ + Apply ZL10;Rewrite <- H8;Assumption + | Rewrite H9;Reflexivity ] + | NewDestruct H7 as [H9|H9]; [ + Absurd z=xH;Auto + | Rewrite H9; NewDestruct z; Simpl; + [ Reflexivity + | Reflexivity + | Absurd xH=xH; [Assumption | Reflexivity]]]]]]. + Exists (double_moins_un p); Split; [ + Reflexivity + | Clear IHp; Split; [ + NewDestruct p; Simpl; [ + Reflexivity + | Rewrite is_double_moins_un; Reflexivity + | Reflexivity ] + | NewDestruct p; [Right|Right|Left]; Reflexivity ]]. +Qed. + +Theorem sub_add: +(x,y:positive) (compare x y EGAL) = SUPERIEUR -> (add y (true_sub x y)) = x. +Proof. +Intros x y H;Elim sub_pos_SUPERIEUR with 1:=H; +Intros z H1;Elim H1;Intros H2 H3; Elim H3;Intros H4 H5; +Unfold true_sub ;Rewrite H2; Exact H4. +Qed. + diff --git a/theories7/NArith/NArith.v b/theories7/NArith/NArith.v new file mode 100644 index 00000000..d924ae2e --- /dev/null +++ b/theories7/NArith/NArith.v @@ -0,0 +1,14 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + +(* $Id: NArith.v,v 1.1.2.1 2004/07/16 19:31:31 herbelin Exp $ *) + +(** Library for binary natural numbers *) + +Require Export BinPos. +Require Export BinNat. 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. + |