diff options
Diffstat (limited to 'theories7/Arith/Div2.v')
| -rw-r--r-- | theories7/Arith/Div2.v | 174 |
1 files changed, 174 insertions, 0 deletions
diff --git a/theories7/Arith/Div2.v b/theories7/Arith/Div2.v new file mode 100644 index 00000000..8bd0160f --- /dev/null +++ b/theories7/Arith/Div2.v @@ -0,0 +1,174 @@ +(************************************************************************) +(* 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. + |