diff options
Diffstat (limited to 'theories/Arith/Div2.v')
| -rw-r--r-- | theories/Arith/Div2.v | 167 |
1 files changed, 69 insertions, 98 deletions
diff --git a/theories/Arith/Div2.v b/theories/Arith/Div2.v index 45fddd72..1c65a192 100644 --- a/theories/Arith/Div2.v +++ b/theories/Arith/Div2.v @@ -1,15 +1,16 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -Require Import Lt. -Require Import Plus. -Require Import Compare_dec. -Require Import Even. +(** Nota : this file is OBSOLETE, and left only for compatibility. + Please consider using [Nat.div2] directly, and results about it + (see file PeanoNat). *) + +Require Import PeanoNat Even. Local Open Scope nat_scope. @@ -17,12 +18,7 @@ Implicit Type n : nat. (** Here we define [n/2] and prove some of its properties *) -Fixpoint div2 n : nat := - match n with - | O => 0 - | S O => 0 - | S (S n') => S (div2 n') - end. +Notation div2 := Nat.div2 (compat "8.4"). (** Since [div2] is recursively defined on [0], [1] and [(S (S n))], it is useful to prove the corresponding induction principle *) @@ -31,53 +27,48 @@ Lemma ind_0_1_SS : forall P:nat -> Prop, P 0 -> P 1 -> (forall n, P n -> P (S (S n))) -> forall n, P n. Proof. - intros P H0 H1 Hn. - cut (forall n, P n /\ P (S n)). - intros H'n n. elim (H'n n). auto with arith. - - induction n. auto with arith. - intros. elim IHn; auto with arith. + intros P H0 H1 H2. + fix 1. + destruct n as [|[|n]]. + - exact H0. + - exact H1. + - apply H2, ind_0_1_SS. Qed. (** [0 <n => n/2 < n] *) -Lemma lt_div2 : forall n, 0 < n -> div2 n < n. -Proof. - intro n. pattern n. apply ind_0_1_SS. - (* n = 0 *) - inversion 1. - (* n=1 *) - simpl; trivial. - (* n=S S n' *) - intro n'; case (zerop n'). - intro n'_eq_0. rewrite n'_eq_0. auto with arith. - auto with arith. -Qed. +Lemma lt_div2 n : 0 < n -> div2 n < n. +Proof. apply Nat.lt_div2. Qed. Hint Resolve lt_div2: arith. (** Properties related to the parity *) -Lemma even_div2 : forall n, even n -> div2 n = div2 (S n) -with odd_div2 : forall n, odd n -> S (div2 n) = div2 (S n). +Lemma even_div2 n : even n -> div2 n = div2 (S n). Proof. - destruct n; intro H. - (* 0 *) trivial. - (* S n *) inversion_clear H. apply odd_div2 in H0 as <-. trivial. - destruct n; intro. - (* 0 *) inversion H. - (* S n *) inversion_clear H. apply even_div2 in H0 as <-. trivial. + rewrite Even.even_equiv. intros (p,->). + rewrite Nat.div2_succ_double. apply Nat.div2_double. Qed. -Lemma div2_even n : div2 n = div2 (S n) -> even n -with div2_odd n : S (div2 n) = div2 (S n) -> odd n. +Lemma odd_div2 n : odd n -> S (div2 n) = div2 (S n). Proof. -{ destruct n; intro H. - - constructor. - - constructor. apply div2_odd. rewrite H. trivial. } -{ destruct n; intro H. - - discriminate. - - constructor. apply div2_even. injection H as <-. trivial. } + rewrite Even.odd_equiv. intros (p,->). + rewrite Nat.add_1_r, Nat.div2_succ_double. + simpl. f_equal. symmetry. apply Nat.div2_double. +Qed. + +Lemma div2_even n : div2 n = div2 (S n) -> even n. +Proof. + destruct (even_or_odd n) as [Ev|Od]; trivial. + apply odd_div2 in Od. rewrite <- Od. intro Od'. + elim (n_Sn _ Od'). +Qed. + +Lemma div2_odd n : S (div2 n) = div2 (S n) -> odd n. +Proof. + destruct (even_or_odd n) as [Ev|Od]; trivial. + apply even_div2 in Ev. rewrite <- Ev. intro Ev'. + symmetry in Ev'. elim (n_Sn _ Ev'). Qed. Hint Resolve even_div2 div2_even odd_div2 div2_odd: arith. @@ -93,58 +84,52 @@ Qed. (** Properties related to the double ([2n]) *) -Definition double n := n + n. +Notation double := Nat.double (compat "8.4"). -Hint Unfold double: arith. +Hint Unfold double Nat.double: arith. -Lemma double_S : forall n, double (S n) = S (S (double n)). +Lemma double_S n : double (S n) = S (S (double n)). Proof. - intro. unfold double. simpl. auto with arith. + apply Nat.add_succ_r. Qed. -Lemma double_plus : forall n (m:nat), double (n + m) = double n + double m. +Lemma double_plus n m : double (n + m) = double n + double m. Proof. - intros m n. unfold double. - do 2 rewrite plus_assoc_reverse. rewrite (plus_permute n). - reflexivity. + apply Nat.add_shuffle1. Qed. Hint Resolve double_S: arith. -Lemma even_odd_double : - forall n, - (even n <-> n = double (div2 n)) /\ (odd n <-> n = S (double (div2 n))). +Lemma even_odd_double n : + (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. destruct H as ((IH1,IH2),(IH3,IH4)). - 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. + revert n. fix 1. destruct n as [|[|n]]. + - (* n = 0 *) + split; split; auto with arith. inversion 1. + - (* n = 1 *) + split; split; auto with arith. inversion_clear 1. inversion H0. + - (* n = (S (S n')) *) + destruct (even_odd_double n) as ((Ev,Ev'),(Od,Od')). + split; split; simpl div2; rewrite ?double_S. + + inversion_clear 1. inversion_clear H0. auto. + + injection 1. auto with arith. + + inversion_clear 1. inversion_clear H0. auto. + + injection 1. auto with arith. Qed. + (** Specializations *) -Lemma even_double : forall n, even n -> n = double (div2 n). -Proof fun n => proj1 (proj1 (even_odd_double n)). +Lemma even_double n : even n -> n = double (div2 n). +Proof proj1 (proj1 (even_odd_double n)). -Lemma double_even : forall n, n = double (div2 n) -> even n. -Proof fun n => proj2 (proj1 (even_odd_double n)). +Lemma double_even n : n = double (div2 n) -> even n. +Proof proj2 (proj1 (even_odd_double n)). -Lemma odd_double : forall n, odd n -> n = S (double (div2 n)). -Proof fun n => proj1 (proj2 (even_odd_double n)). +Lemma odd_double n : odd n -> n = S (double (div2 n)). +Proof proj1 (proj2 (even_odd_double n)). -Lemma double_odd : forall n, n = S (double (div2 n)) -> odd n. -Proof fun n => proj2 (proj2 (even_odd_double n)). +Lemma double_odd n : n = S (double (div2 n)) -> odd n. +Proof proj2 (proj2 (even_odd_double n)). Hint Resolve even_double double_even odd_double double_odd: arith. @@ -166,22 +151,8 @@ Defined. (** Doubling before dividing by two brings back to the initial number. *) -Lemma div2_double : forall n:nat, div2 (2*n) = n. -Proof. - induction n. - simpl; auto. - simpl. - replace (n+S(n+0)) with (S (2*n)). - f_equal; auto. - simpl; auto with arith. -Qed. +Lemma div2_double n : div2 (2*n) = n. +Proof. apply Nat.div2_double. Qed. -Lemma div2_double_plus_one : forall n:nat, div2 (S (2*n)) = n. -Proof. - induction n. - simpl; auto. - simpl. - replace (n+S(n+0)) with (S (2*n)). - f_equal; auto. - simpl; auto with arith. -Qed. +Lemma div2_double_plus_one n : div2 (S (2*n)) = n. +Proof. apply Nat.div2_succ_double. Qed. |