diff options
Diffstat (limited to 'theories7/Arith/Div2.v')
| -rw-r--r-- | theories7/Arith/Div2.v | 174 |
1 files changed, 0 insertions, 174 deletions
diff --git a/theories7/Arith/Div2.v b/theories7/Arith/Div2.v deleted file mode 100644 index 8bd0160f..00000000 --- a/theories7/Arith/Div2.v +++ /dev/null @@ -1,174 +0,0 @@ -(************************************************************************) -(* 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: Div2.v,v 1.1.2.1 2004/07/16 19:31:24 herbelin Exp $ i*) - -Require Lt. -Require Plus. -Require Compare_dec. -Require Even. - -V7only [Import nat_scope.]. -Open Local Scope nat_scope. - -Implicit Variables Type n:nat. - -(** Here we define [n/2] and prove some of its properties *) - -Fixpoint div2 [n:nat] : nat := - Cases n of - O => O - | (S O) => O - | (S (S n')) => (S (div2 n')) - end. - -(** Since [div2] is recursively defined on [0], [1] and [(S (S n))], it is - useful to prove the corresponding induction principle *) - -Lemma ind_0_1_SS : (P:nat->Prop) - (P O) -> (P (S O)) -> ((n:nat)(P n)->(P (S (S n)))) -> (n:nat)(P n). -Proof. -Intros. -Cut (n:nat)(P n)/\(P (S n)). -Intros. Elim (H2 n). Auto with arith. - -NewInduction n0. Auto with arith. -Intros. Elim IHn0; Auto with arith. -Qed. - -(** [0 <n => n/2 < n] *) - -Lemma lt_div2 : (n:nat) (lt O n) -> (lt (div2 n) n). -Proof. -Intro n. Pattern n. Apply ind_0_1_SS. -Intro. Inversion H. -Auto with arith. -Intros. Simpl. -Case (zerop n0). -Intro. Rewrite e. Auto with arith. -Auto with arith. -Qed. - -Hints Resolve lt_div2 : arith. - -(** Properties related to the parity *) - -Lemma even_odd_div2 : (n:nat) - ((even n)<->(div2 n)=(div2 (S n))) /\ ((odd n)<->(S (div2 n))=(div2 (S n))). -Proof. -Intro n. Pattern n. Apply ind_0_1_SS. -(* n = 0 *) -Split. Split; Auto with arith. -Split. Intro H. Inversion H. -Intro H. Absurd (S (div2 O))=(div2 (S O)); Auto with arith. -(* n = 1 *) -Split. Split. Intro. Inversion H. Inversion H1. -Intro H. Absurd (div2 (S O))=(div2 (S (S O))). -Simpl. Discriminate. Assumption. -Split; Auto with arith. -(* n = (S (S n')) *) -Intros. Decompose [and] H. Unfold iff in H0 H1. -Decompose [and] H0. Decompose [and] H1. Clear H H0 H1. -Split; Split; Auto with arith. -Intro H. Inversion H. Inversion H1. -Change (S (div2 n0))=(S (div2 (S n0))). Auto with arith. -Intro H. Inversion H. Inversion H1. -Change (S (S (div2 n0)))=(S (div2 (S n0))). Auto with arith. -Qed. - -(** Specializations *) - -Lemma even_div2 : (n:nat) (even n) -> (div2 n)=(div2 (S n)). -Proof [n:nat](proj1 ? ? (proj1 ? ? (even_odd_div2 n))). - -Lemma div2_even : (n:nat) (div2 n)=(div2 (S n)) -> (even n). -Proof [n:nat](proj2 ? ? (proj1 ? ? (even_odd_div2 n))). - -Lemma odd_div2 : (n:nat) (odd n) -> (S (div2 n))=(div2 (S n)). -Proof [n:nat](proj1 ? ? (proj2 ? ? (even_odd_div2 n))). - -Lemma div2_odd : (n:nat) (S (div2 n))=(div2 (S n)) -> (odd n). -Proof [n:nat](proj2 ? ? (proj2 ? ? (even_odd_div2 n))). - -Hints Resolve even_div2 div2_even odd_div2 div2_odd : arith. - -(** Properties related to the double ([2n]) *) - -Definition double := [n:nat](plus n n). - -Hints Unfold double : arith. - -Lemma double_S : (n:nat) (double (S n))=(S (S (double n))). -Proof. -Intro. Unfold double. Simpl. Auto with arith. -Qed. - -Lemma double_plus : (m,n:nat) (double (plus m n))=(plus (double m) (double n)). -Proof. -Intros m n. Unfold double. -Do 2 Rewrite -> plus_assoc_r. Rewrite -> (plus_permute n). -Reflexivity. -Qed. - -Hints Resolve double_S : arith. - -Lemma even_odd_double : (n:nat) - ((even n)<->n=(double (div2 n))) /\ ((odd n)<->n=(S (double (div2 n)))). -Proof. -Intro n. Pattern n. Apply ind_0_1_SS. -(* n = 0 *) -Split; Split; Auto with arith. -Intro H. Inversion H. -(* n = 1 *) -Split; Split; Auto with arith. -Intro H. Inversion H. Inversion H1. -(* n = (S (S n')) *) -Intros. Decompose [and] H. Unfold iff in H0 H1. -Decompose [and] H0. Decompose [and] H1. Clear H H0 H1. -Split; Split. -Intro H. Inversion H. Inversion H1. -Simpl. Rewrite (double_S (div2 n0)). Auto with arith. -Simpl. Rewrite (double_S (div2 n0)). Intro H. Injection H. Auto with arith. -Intro H. Inversion H. Inversion H1. -Simpl. Rewrite (double_S (div2 n0)). Auto with arith. -Simpl. Rewrite (double_S (div2 n0)). Intro H. Injection H. Auto with arith. -Qed. - - -(** Specializations *) - -Lemma even_double : (n:nat) (even n) -> n=(double (div2 n)). -Proof [n:nat](proj1 ? ? (proj1 ? ? (even_odd_double n))). - -Lemma double_even : (n:nat) n=(double (div2 n)) -> (even n). -Proof [n:nat](proj2 ? ? (proj1 ? ? (even_odd_double n))). - -Lemma odd_double : (n:nat) (odd n) -> n=(S (double (div2 n))). -Proof [n:nat](proj1 ? ? (proj2 ? ? (even_odd_double n))). - -Lemma double_odd : (n:nat) n=(S (double (div2 n))) -> (odd n). -Proof [n:nat](proj2 ? ? (proj2 ? ? (even_odd_double n))). - -Hints Resolve even_double double_even odd_double double_odd : arith. - -(** Application: - - if [n] is even then there is a [p] such that [n = 2p] - - if [n] is odd then there is a [p] such that [n = 2p+1] - - (Immediate: it is [n/2]) *) - -Lemma even_2n : (n:nat) (even n) -> { p:nat | n=(double p) }. -Proof. -Intros n H. Exists (div2 n). Auto with arith. -Qed. - -Lemma odd_S2n : (n:nat) (odd n) -> { p:nat | n=(S (double p)) }. -Proof. -Intros n H. Exists (div2 n). Auto with arith. -Qed. - |