diff options
Diffstat (limited to 'theories7/ZArith/Zcomplements.v')
| -rw-r--r-- | theories7/ZArith/Zcomplements.v | 212 |
1 files changed, 212 insertions, 0 deletions
diff --git a/theories7/ZArith/Zcomplements.v b/theories7/ZArith/Zcomplements.v new file mode 100644 index 00000000..72d837b6 --- /dev/null +++ b/theories7/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.1.2.1 2004/07/16 19:31:43 herbelin Exp $ i*) + +Require ZArithRing. +Require ZArith_base. +Require Omega. +Require Wf_nat. +V7only [Import Z_scope.]. +Open Local Scope Z_scope. + +V7only [Set Implicit Arguments.]. + +(**********************************************************************) +(** About parity *) + +Lemma two_or_two_plus_one : (x:Z) { y:Z | `x = 2*y`}+{ y:Z | `x = 2*y+1`}. +Proof. +Intro x; NewDestruct x. +Left ; Split with ZERO; Reflexivity. + +NewDestruct p. +Right ; Split with (POS p); Reflexivity. + +Left ; Split with (POS p); Reflexivity. + +Right ; Split with ZERO; Reflexivity. + +NewDestruct p. +Right ; Split with (NEG (add xH p)). +Rewrite NEG_xI. +Rewrite NEG_add. +Omega. + +Left ; Split with (NEG 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 := + Cases a of + | xH => xH + | (xO a') => (xO (floor_pos a')) + | (xI b') => (xO (floor_pos b')) + end. + +Definition floor := [a:positive](POS (floor_pos a)). + +Lemma floor_gt0 : (x:positive) `(floor x) > 0`. +Proof. +Intro. +Compute. +Trivial. +Qed. + +Lemma floor_ok : (a:positive) + `(floor a) <= (POS a) < 2*(floor a)`. +Proof. +Unfold floor. +Intro a; NewInduction a as [p|p|]. + +Simpl. +Repeat Rewrite POS_xI. +Rewrite (POS_xO (xO (floor_pos p))). +Rewrite (POS_xO (floor_pos p)). +Omega. + +Simpl. +Repeat Rewrite POS_xI. +Rewrite (POS_xO (xO (floor_pos p))). +Rewrite (POS_xO (floor_pos p)). +Rewrite (POS_xO p). +Omega. + +Simpl; Omega. +Qed. + +(**********************************************************************) +(** Two more induction principles over [Z]. *) + +Theorem Z_lt_abs_rec : (P: Z -> Set) + ((n: Z) ((m: Z) `|m|<|n|` -> (P m)) -> (P n)) -> (p: Z) (P p). +Proof. +Intros P HP p. +LetTac Q:=[z]`0<=z`->(P z)*(P `-z`). +Cut (Q `|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;Clear Q;Intros. +Apply pair;Apply HP. +Rewrite Zabs_eq;Auto;Intros. +Elim (H `|m|`);Intros;Auto with zarith. +Elim (Zabs_dec m);Intro eq;Rewrite eq;Trivial. +Rewrite Zabs_non_eq;Auto with zarith. +Rewrite Zopp_Zopp;Intros. +Elim (H `|m|`);Intros;Auto with zarith. +Elim (Zabs_dec m);Intro eq;Rewrite eq;Trivial. +Qed. + +Theorem Z_lt_abs_induction : (P: Z -> Prop) + ((n: Z) ((m: Z) `|m|<|n|` -> (P m)) -> (P n)) -> (p: Z) (P p). +Proof. +Intros P HP p. +LetTac Q:=[z]`0<=z`->(P z) /\ (P `-z`). +Cut (Q `|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;Clear Q;Intros. +Split;Apply HP. +Rewrite Zabs_eq;Auto;Intros. +Elim (H `|m|`);Intros;Auto with zarith. +Elim (Zabs_dec m);Intro eq;Rewrite eq;Trivial. +Rewrite Zabs_non_eq;Auto with zarith. +Rewrite Zopp_Zopp;Intros. +Elim (H `|m|`);Intros;Auto with zarith. +Elim (Zabs_dec m);Intro eq;Rewrite eq;Trivial. +Qed. +V7only [Unset Implicit Arguments.]. + +(** To do case analysis over the sign of [z] *) + +Lemma Zcase_sign : (x:Z)(P:Prop) + (`x=0` -> P) -> + (`x>0` -> P) -> + (`x<0` -> P) -> P. +Proof. +Intros x P Hzero Hpos Hneg. +Induction x. +Apply Hzero; Trivial. +Apply Hpos; Apply POS_gt_ZERO. +Apply Hneg; Apply NEG_lt_ZERO. +Save. + +Lemma sqr_pos : (x:Z)`x*x >= 0`. +Proof. +Intro x. +Apply (Zcase_sign x `x*x >= 0`). +Intros H; Rewrite H; Omega. +Intros H; Replace `0` with `0*0`. +Apply Zge_Zmult_pos_compat; Omega. +Omega. +Intros H; Replace `0` with `0*0`. +Replace `x*x` with `(-x)*(-x)`. +Apply Zge_Zmult_pos_compat; Omega. +Ring. +Omega. +Save. + +(**********************************************************************) +(** A list length in Z, tail recursive. *) + +Require PolyList. + +Fixpoint Zlength_aux [acc: Z; A:Set; l:(list A)] : Z := Cases l of + nil => acc + | (cons _ l) => (Zlength_aux (Zs acc) A l) +end. + +Definition Zlength := (Zlength_aux 0). +Implicits Zlength [1]. + +Section Zlength_properties. + +Variable A:Set. + +Implicit Variable Type l:(list A). + +Lemma Zlength_correct : (l:(list A))(Zlength l)=(inject_nat (length l)). +Proof. +Assert (l:(list A))(acc:Z)(Zlength_aux acc A l)=acc+(inject_nat (length l)). +Induction l. +Simpl; Auto with zarith. +Intros; Simpl (length (cons a l0)); Rewrite inj_S. +Simpl; Rewrite H; Auto with zarith. +Unfold Zlength; Intros; Rewrite H; Auto. +Qed. + +Lemma Zlength_nil : (Zlength 1!A (nil A))=0. +Proof. +Auto. +Qed. + +Lemma Zlength_cons : (x:A)(l:(list A))(Zlength (cons x l))=(Zs (Zlength l)). +Proof. +Intros; Do 2 Rewrite Zlength_correct. +Simpl (length (cons x l)); Rewrite inj_S; Auto. +Qed. + +Lemma Zlength_nil_inv : (l:(list A))(Zlength l)=0 -> l=(nil ?). +Proof. +Intro l; Rewrite Zlength_correct. +Case l; Auto. +Intros x l'; Simpl (length (cons x l')). +Rewrite inj_S. +Intros; ElimType False; Generalize (ZERO_le_inj (length l')); Omega. +Qed. + +End Zlength_properties. + +Implicits Zlength_correct [1]. +Implicits Zlength_cons [1]. +Implicits Zlength_nil_inv [1]. |