diff options
Diffstat (limited to 'theories/ZArith/Zcomplements.v')
| -rw-r--r-- | theories/ZArith/Zcomplements.v | 258 |
1 files changed, 129 insertions, 129 deletions
diff --git a/theories/ZArith/Zcomplements.v b/theories/ZArith/Zcomplements.v index 817fbc1b..78c8a976 100644 --- a/theories/ZArith/Zcomplements.v +++ b/theories/ZArith/Zcomplements.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Zcomplements.v 5920 2004-07-16 20:01:26Z herbelin $ i*) +(*i $Id: Zcomplements.v 9245 2006-10-17 12:53:34Z notin $ i*) Require Import ZArithRing. Require Import ZArith_base. @@ -19,27 +19,27 @@ 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}. + 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. + 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. (**********************************************************************) @@ -50,109 +50,109 @@ Qed. Fixpoint floor_pos (a:positive) : positive := match a with - | xH => 1%positive - | xO a' => xO (floor_pos a') - | xI b' => xO (floor_pos b') + | 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. + 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. + 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. + 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. + 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. + 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. + 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. + 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. + 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. + 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. (**********************************************************************) @@ -162,8 +162,8 @@ 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 + | nil => acc + | _ :: l => Zlength_aux (Zsucc acc) A l end. Definition Zlength := Zlength_aux 0. @@ -171,42 +171,42 @@ 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. + 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 +Implicit Arguments Zlength_nil_inv [A]. |