diff options
Diffstat (limited to 'theories7/ZArith/Zcomplements.v')
| -rw-r--r-- | theories7/ZArith/Zcomplements.v | 212 |
1 files changed, 0 insertions, 212 deletions
diff --git a/theories7/ZArith/Zcomplements.v b/theories7/ZArith/Zcomplements.v deleted file mode 100644 index 72d837b6..00000000 --- a/theories7/ZArith/Zcomplements.v +++ /dev/null @@ -1,212 +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: 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]. |