diff options
Diffstat (limited to 'theories/ZArith/Zcomplements.v')
| -rw-r--r-- | theories/ZArith/Zcomplements.v | 212 |
1 files changed, 212 insertions, 0 deletions
diff --git a/theories/ZArith/Zcomplements.v b/theories/ZArith/Zcomplements.v new file mode 100644 index 00000000..b60cd37c --- /dev/null +++ b/theories/ZArith/Zcomplements.v @@ -0,0 +1,212 @@ +(************************************************************************) +(* 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: Zcomplements.v,v 1.26.2.1 2004/07/16 19:31:21 herbelin Exp $ i*) + +Require Import ZArithRing. +Require Import ZArith_base. +Require Import Omega. +Require Import Wf_nat. +Open Local Scope Z_scope. + + +(**********************************************************************) +(** About parity *) + +Lemma two_or_two_plus_one : + forall n:Z, {y : Z | n = 2 * y} + {y : Z | n = 2 * y + 1}. +Proof. +intro x; destruct x. +left; split with 0; reflexivity. + +destruct p. +right; split with (Zpos p); reflexivity. + +left; split with (Zpos p); reflexivity. + +right; split with 0; reflexivity. + +destruct p. +right; split with (Zneg (1 + p)). +rewrite BinInt.Zneg_xI. +rewrite BinInt.Zneg_plus_distr. +omega. + +left; split with (Zneg p); reflexivity. + +right; split with (-1); reflexivity. +Qed. + +(**********************************************************************) +(** The biggest power of 2 that is stricly less than [a] + + Easy to compute: replace all "1" of the binary representation by + "0", except the first "1" (or the first one :-) *) + +Fixpoint floor_pos (a:positive) : positive := + match a with + | xH => 1%positive + | xO a' => xO (floor_pos a') + | xI b' => xO (floor_pos b') + end. + +Definition floor (a:positive) := Zpos (floor_pos a). + +Lemma floor_gt0 : forall p:positive, floor p > 0. +Proof. +intro. +compute in |- *. +trivial. +Qed. + +Lemma floor_ok : forall p:positive, floor p <= Zpos p < 2 * floor p. +Proof. +unfold floor in |- *. +intro a; induction a as [p| p| ]. + +simpl in |- *. +repeat rewrite BinInt.Zpos_xI. +rewrite (BinInt.Zpos_xO (xO (floor_pos p))). +rewrite (BinInt.Zpos_xO (floor_pos p)). +omega. + +simpl in |- *. +repeat rewrite BinInt.Zpos_xI. +rewrite (BinInt.Zpos_xO (xO (floor_pos p))). +rewrite (BinInt.Zpos_xO (floor_pos p)). +rewrite (BinInt.Zpos_xO p). +omega. + +simpl in |- *; omega. +Qed. + +(**********************************************************************) +(** Two more induction principles over [Z]. *) + +Theorem Z_lt_abs_rec : + forall P:Z -> Set, + (forall n:Z, (forall m:Z, Zabs m < Zabs n -> P m) -> P n) -> + forall n:Z, P n. +Proof. +intros P HP p. +set (Q := fun z => 0 <= z -> P z * P (- z)) in *. +cut (Q (Zabs p)); [ intros | apply (Z_lt_rec Q); auto with zarith ]. +elim (Zabs_dec p); intro eq; rewrite eq; elim H; auto with zarith. +unfold Q in |- *; clear Q; intros. +apply pair; apply HP. +rewrite Zabs_eq; auto; intros. +elim (H (Zabs m)); intros; auto with zarith. +elim (Zabs_dec m); intro eq; rewrite eq; trivial. +rewrite Zabs_non_eq; auto with zarith. +rewrite Zopp_involutive; intros. +elim (H (Zabs m)); intros; auto with zarith. +elim (Zabs_dec m); intro eq; rewrite eq; trivial. +Qed. + +Theorem Z_lt_abs_induction : + forall P:Z -> Prop, + (forall n:Z, (forall m:Z, Zabs m < Zabs n -> P m) -> P n) -> + forall n:Z, P n. +Proof. +intros P HP p. +set (Q := fun z => 0 <= z -> P z /\ P (- z)) in *. +cut (Q (Zabs p)); [ intros | apply (Z_lt_induction Q); auto with zarith ]. +elim (Zabs_dec p); intro eq; rewrite eq; elim H; auto with zarith. +unfold Q in |- *; clear Q; intros. +split; apply HP. +rewrite Zabs_eq; auto; intros. +elim (H (Zabs m)); intros; auto with zarith. +elim (Zabs_dec m); intro eq; rewrite eq; trivial. +rewrite Zabs_non_eq; auto with zarith. +rewrite Zopp_involutive; intros. +elim (H (Zabs m)); intros; auto with zarith. +elim (Zabs_dec m); intro eq; rewrite eq; trivial. +Qed. + +(** To do case analysis over the sign of [z] *) + +Lemma Zcase_sign : + forall (n:Z) (P:Prop), (n = 0 -> P) -> (n > 0 -> P) -> (n < 0 -> P) -> P. +Proof. +intros x P Hzero Hpos Hneg. +induction x as [| p| p]. +apply Hzero; trivial. +apply Hpos; apply Zorder.Zgt_pos_0. +apply Hneg; apply Zorder.Zlt_neg_0. +Qed. + +Lemma sqr_pos : forall n:Z, n * n >= 0. +Proof. +intro x. +apply (Zcase_sign x (x * x >= 0)). +intros H; rewrite H; omega. +intros H; replace 0 with (0 * 0). +apply Zmult_ge_compat; omega. +omega. +intros H; replace 0 with (0 * 0). +replace (x * x) with (- x * - x). +apply Zmult_ge_compat; omega. +ring. +omega. +Qed. + +(**********************************************************************) +(** A list length in Z, tail recursive. *) + +Require Import List. + +Fixpoint Zlength_aux (acc:Z) (A:Set) (l:list A) {struct l} : Z := + match l with + | nil => acc + | _ :: l => Zlength_aux (Zsucc acc) A l + end. + +Definition Zlength := Zlength_aux 0. +Implicit Arguments Zlength [A]. + +Section Zlength_properties. + +Variable A : Set. + +Implicit Type l : list A. + +Lemma Zlength_correct : forall l, Zlength l = Z_of_nat (length l). +Proof. +assert (forall l (acc:Z), Zlength_aux acc A l = acc + Z_of_nat (length l)). +simple induction l. +simpl in |- *; auto with zarith. +intros; simpl (length (a :: l0)) in |- *; rewrite Znat.inj_S. +simpl in |- *; rewrite H; auto with zarith. +unfold Zlength in |- *; intros; rewrite H; auto. +Qed. + +Lemma Zlength_nil : Zlength (A:=A) nil = 0. +Proof. +auto. +Qed. + +Lemma Zlength_cons : forall (x:A) l, Zlength (x :: l) = Zsucc (Zlength l). +Proof. +intros; do 2 rewrite Zlength_correct. +simpl (length (x :: l)) in |- *; rewrite Znat.inj_S; auto. +Qed. + +Lemma Zlength_nil_inv : forall l, Zlength l = 0 -> l = nil. +Proof. +intro l; rewrite Zlength_correct. +case l; auto. +intros x l'; simpl (length (x :: l')) in |- *. +rewrite Znat.inj_S. +intros; elimtype False; generalize (Zle_0_nat (length l')); omega. +Qed. + +End Zlength_properties. + +Implicit Arguments Zlength_correct [A]. +Implicit Arguments Zlength_cons [A]. +Implicit Arguments Zlength_nil_inv [A].
\ No newline at end of file |