diff options
author | Jason Gross <jgross@mit.edu> | 2016-02-05 15:24:42 -0500 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2016-02-05 15:24:42 -0500 |
commit | a47b49b11d17add5ca1ea5e650d2f344219b4f7e (patch) | |
tree | 699bff16674a68d1a5dc059bfdbd2f9ca85e95a7 /coqprime/N/NatAux.v | |
parent | 1f83ff39458ca80acf3192c938490cf4988b7489 (diff) |
Update build process to use COQPATH & _CoqProject
Removed all of the files not built by default; they can be resurrected from git
history. _CoqProject is the standard way to list the files in a project and to
give information to coq_makefile. COQPATH is the standard way to make use of
not-yet-installed libraries that are not part of your project (i.e., you don't
want to remove them when you `make clean`, etc.).
Diffstat (limited to 'coqprime/N/NatAux.v')
-rw-r--r-- | coqprime/N/NatAux.v | 72 |
1 files changed, 0 insertions, 72 deletions
diff --git a/coqprime/N/NatAux.v b/coqprime/N/NatAux.v deleted file mode 100644 index eab09150c..000000000 --- a/coqprime/N/NatAux.v +++ /dev/null @@ -1,72 +0,0 @@ - -(*************************************************************) -(* This file is distributed under the terms of the *) -(* GNU Lesser General Public License Version 2.1 *) -(*************************************************************) -(* Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr *) -(*************************************************************) - -(********************************************************************** - Aux.v - - Auxillary functions & Theorems - **********************************************************************) -Require Export Arith. - -(************************************** - Some properties of minus -**************************************) - -Theorem minus_O : forall a b : nat, a <= b -> a - b = 0. -intros a; elim a; simpl in |- *; auto with arith. -intros a1 Rec b; case b; elim b; auto with arith. -Qed. - - -(************************************** - Definitions and properties of the power for nat -**************************************) - -Fixpoint pow (n m: nat) {struct m} : nat := match m with O => 1%nat | (S m1) => (n * pow n m1)%nat end. - -Theorem pow_add: forall n m p, pow n (m + p) = (pow n m * pow n p)%nat. -intros n m; elim m; simpl. -intros p; rewrite plus_0_r; auto. -intros m1 Rec p; rewrite Rec; auto with arith. -Qed. - - -Theorem pow_pos: forall p n, (0 < p)%nat -> (0 < pow p n)%nat. -intros p1 n H; elim n; simpl; auto with arith. -intros n1 H1; replace 0%nat with (p1 * 0)%nat; auto with arith. -repeat rewrite (mult_comm p1); apply mult_lt_compat_r; auto with arith. -Qed. - - -Theorem pow_monotone: forall n p q, (1 < n)%nat -> (p < q)%nat -> (pow n p < pow n q)%nat. -intros n p1 q1 H H1; elim H1; simpl. -pattern (pow n p1) at 1; rewrite <- (mult_1_l (pow n p1)). -apply mult_lt_compat_r; auto. -apply pow_pos; auto with arith. -intros n1 H2 H3. -apply lt_trans with (1 := H3). -pattern (pow n n1) at 1; rewrite <- (mult_1_l (pow n n1)). -apply mult_lt_compat_r; auto. -apply pow_pos; auto with arith. -Qed. - -(************************************ - Definition of the divisibility for nat -**************************************) - -Definition divide a b := exists c, b = a * c. - - -Theorem divide_le: forall p q, (1 < q)%nat -> divide p q -> (p <= q)%nat. -intros p1 q1 H (x, H1); subst. -apply le_trans with (p1 * 1)%nat; auto with arith. -rewrite mult_1_r; auto with arith. -apply mult_le_compat_l. -case (le_lt_or_eq 0 x); auto with arith. -intros H2; subst; contradict H; rewrite mult_0_r; auto with arith. -Qed. |