diff options
Diffstat (limited to 'theories7/NArith/BinNat.v')
| -rw-r--r-- | theories7/NArith/BinNat.v | 205 |
1 files changed, 205 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. + |