diff options
author | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
commit | 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch) | |
tree | 631ad791a7685edafeb1fb2e8faeedc8379318ae /theories/Numbers/Integer/SpecViaZ | |
parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) |
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'theories/Numbers/Integer/SpecViaZ')
-rw-r--r-- | theories/Numbers/Integer/SpecViaZ/ZSig.v | 116 | ||||
-rw-r--r-- | theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v | 267 |
2 files changed, 160 insertions, 223 deletions
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSig.v b/theories/Numbers/Integer/SpecViaZ/ZSig.v index 0af98c74..ffa91706 100644 --- a/theories/Numbers/Integer/SpecViaZ/ZSig.v +++ b/theories/Numbers/Integer/SpecViaZ/ZSig.v @@ -8,7 +8,7 @@ (* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) (************************************************************************) -(*i $Id: ZSig.v 11027 2008-06-01 13:28:59Z letouzey $ i*) +(*i $Id$ i*) Require Import ZArith Znumtheory. @@ -25,93 +25,77 @@ Module Type ZType. Parameter t : Type. Parameter to_Z : t -> Z. - Notation "[ x ]" := (to_Z x). + Local Notation "[ x ]" := (to_Z x). - Definition eq x y := ([x] = [y]). + Definition eq x y := [x] = [y]. + Definition lt x y := [x] < [y]. + Definition le x y := [x] <= [y]. Parameter of_Z : Z -> t. Parameter spec_of_Z: forall x, to_Z (of_Z x) = x. + Parameter compare : t -> t -> comparison. + Parameter eq_bool : t -> t -> bool. + Parameter min : t -> t -> t. + Parameter max : t -> t -> t. Parameter zero : t. Parameter one : t. Parameter minus_one : t. - - Parameter spec_0: [zero] = 0. - Parameter spec_1: [one] = 1. - Parameter spec_m1: [minus_one] = -1. - - Parameter compare : t -> t -> comparison. - - Parameter spec_compare: forall x y, - match compare x y with - | Eq => [x] = [y] - | Lt => [x] < [y] - | Gt => [x] > [y] - end. - - Definition lt n m := compare n m = Lt. - Definition le n m := compare n m <> Gt. - Definition min n m := match compare n m with Gt => m | _ => n end. - Definition max n m := match compare n m with Lt => m | _ => n end. - - Parameter eq_bool : t -> t -> bool. - - Parameter spec_eq_bool: forall x y, - if eq_bool x y then [x] = [y] else [x] <> [y]. - Parameter succ : t -> t. - - Parameter spec_succ: forall n, [succ n] = [n] + 1. - Parameter add : t -> t -> t. - - Parameter spec_add: forall x y, [add x y] = [x] + [y]. - Parameter pred : t -> t. - - Parameter spec_pred: forall x, [pred x] = [x] - 1. - Parameter sub : t -> t -> t. - - Parameter spec_sub: forall x y, [sub x y] = [x] - [y]. - Parameter opp : t -> t. - - Parameter spec_opp: forall x, [opp x] = - [x]. - Parameter mul : t -> t -> t. - - Parameter spec_mul: forall x y, [mul x y] = [x] * [y]. - Parameter square : t -> t. - - Parameter spec_square: forall x, [square x] = [x] * [x]. - Parameter power_pos : t -> positive -> t. - - Parameter spec_power_pos: forall x n, [power_pos x n] = [x] ^ Zpos n. - + Parameter power : t -> N -> t. Parameter sqrt : t -> t. - - Parameter spec_sqrt: forall x, 0 <= [x] -> - [sqrt x] ^ 2 <= [x] < ([sqrt x] + 1) ^ 2. - Parameter div_eucl : t -> t -> t * t. - - Parameter spec_div_eucl: forall x y, [y] <> 0 -> - let (q,r) := div_eucl x y in ([q], [r]) = Zdiv_eucl [x] [y]. - Parameter div : t -> t -> t. - - Parameter spec_div: forall x y, [y] <> 0 -> [div x y] = [x] / [y]. - Parameter modulo : t -> t -> t. - - Parameter spec_modulo: forall x y, [y] <> 0 -> - [modulo x y] = [x] mod [y]. - Parameter gcd : t -> t -> t. + Parameter sgn : t -> t. + Parameter abs : t -> t. + Parameter spec_compare: forall x y, compare x y = Zcompare [x] [y]. + Parameter spec_eq_bool: forall x y, eq_bool x y = Zeq_bool [x] [y]. + Parameter spec_min : forall x y, [min x y] = Zmin [x] [y]. + Parameter spec_max : forall x y, [max x y] = Zmax [x] [y]. + Parameter spec_0: [zero] = 0. + Parameter spec_1: [one] = 1. + Parameter spec_m1: [minus_one] = -1. + Parameter spec_succ: forall n, [succ n] = [n] + 1. + Parameter spec_add: forall x y, [add x y] = [x] + [y]. + Parameter spec_pred: forall x, [pred x] = [x] - 1. + Parameter spec_sub: forall x y, [sub x y] = [x] - [y]. + Parameter spec_opp: forall x, [opp x] = - [x]. + Parameter spec_mul: forall x y, [mul x y] = [x] * [y]. + Parameter spec_square: forall x, [square x] = [x] * [x]. + Parameter spec_power_pos: forall x n, [power_pos x n] = [x] ^ Zpos n. + Parameter spec_power: forall x n, [power x n] = [x] ^ Z_of_N n. + Parameter spec_sqrt: forall x, 0 <= [x] -> + [sqrt x] ^ 2 <= [x] < ([sqrt x] + 1) ^ 2. + Parameter spec_div_eucl: forall x y, + let (q,r) := div_eucl x y in ([q], [r]) = Zdiv_eucl [x] [y]. + Parameter spec_div: forall x y, [div x y] = [x] / [y]. + Parameter spec_modulo: forall x y, [modulo x y] = [x] mod [y]. Parameter spec_gcd: forall a b, [gcd a b] = Zgcd (to_Z a) (to_Z b). + Parameter spec_sgn : forall x, [sgn x] = Zsgn [x]. + Parameter spec_abs : forall x, [abs x] = Zabs [x]. End ZType. + +Module Type ZType_Notation (Import Z:ZType). + Notation "[ x ]" := (to_Z x). + Infix "==" := eq (at level 70). + Notation "0" := zero. + Infix "+" := add. + Infix "-" := sub. + Infix "*" := mul. + Notation "- x" := (opp x). + Infix "<=" := le. + Infix "<" := lt. +End ZType_Notation. + +Module Type ZType' := ZType <+ ZType_Notation.
\ No newline at end of file diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v index aceb8984..bcecb6a8 100644 --- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v +++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v @@ -6,119 +6,74 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ZSigZAxioms.v 11282 2008-07-28 11:51:53Z msozeau $ i*) +(*i $Id$ i*) -Require Import ZArith. -Require Import ZAxioms. -Require Import ZSig. +Require Import ZArith ZAxioms ZDivFloor ZSig. -(** * The interface [ZSig.ZType] implies the interface [ZAxiomsSig] *) +(** * The interface [ZSig.ZType] implies the interface [ZAxiomsSig] -Module ZSig_ZAxioms (Z:ZType) <: ZAxiomsSig. + It also provides [sgn], [abs], [div], [mod] +*) -Delimit Scope IntScope with Int. -Bind Scope IntScope with Z.t. -Open Local Scope IntScope. -Notation "[ x ]" := (Z.to_Z x) : IntScope. -Infix "==" := Z.eq (at level 70) : IntScope. -Notation "0" := Z.zero : IntScope. -Infix "+" := Z.add : IntScope. -Infix "-" := Z.sub : IntScope. -Infix "*" := Z.mul : IntScope. -Notation "- x" := (Z.opp x) : IntScope. -Hint Rewrite - Z.spec_0 Z.spec_1 Z.spec_add Z.spec_sub Z.spec_pred Z.spec_succ - Z.spec_mul Z.spec_opp Z.spec_of_Z : Zspec. +Module ZTypeIsZAxioms (Import Z : ZType'). -Ltac zsimpl := unfold Z.eq in *; autorewrite with Zspec. +Hint Rewrite + spec_0 spec_1 spec_add spec_sub spec_pred spec_succ + spec_mul spec_opp spec_of_Z spec_div spec_modulo + spec_compare spec_eq_bool spec_max spec_min spec_abs spec_sgn + : zsimpl. -Module Export NZOrdAxiomsMod <: NZOrdAxiomsSig. -Module Export NZAxiomsMod <: NZAxiomsSig. +Ltac zsimpl := autorewrite with zsimpl. +Ltac zcongruence := repeat red; intros; zsimpl; congruence. +Ltac zify := unfold eq, lt, le in *; zsimpl. -Definition NZ := Z.t. -Definition NZeq := Z.eq. -Definition NZ0 := Z.zero. -Definition NZsucc := Z.succ. -Definition NZpred := Z.pred. -Definition NZadd := Z.add. -Definition NZsub := Z.sub. -Definition NZmul := Z.mul. +Instance eq_equiv : Equivalence eq. +Proof. unfold eq. firstorder. Qed. -Theorem NZeq_equiv : equiv Z.t Z.eq. -Proof. -repeat split; repeat red; intros; auto; congruence. -Qed. - -Add Relation Z.t Z.eq - reflexivity proved by (proj1 NZeq_equiv) - symmetry proved by (proj2 (proj2 NZeq_equiv)) - transitivity proved by (proj1 (proj2 NZeq_equiv)) - as NZeq_rel. - -Add Morphism NZsucc with signature Z.eq ==> Z.eq as NZsucc_wd. -Proof. -intros; zsimpl; f_equal; assumption. -Qed. - -Add Morphism NZpred with signature Z.eq ==> Z.eq as NZpred_wd. -Proof. -intros; zsimpl; f_equal; assumption. -Qed. +Local Obligation Tactic := zcongruence. -Add Morphism NZadd with signature Z.eq ==> Z.eq ==> Z.eq as NZadd_wd. -Proof. -intros; zsimpl; f_equal; assumption. -Qed. - -Add Morphism NZsub with signature Z.eq ==> Z.eq ==> Z.eq as NZsub_wd. -Proof. -intros; zsimpl; f_equal; assumption. -Qed. +Program Instance succ_wd : Proper (eq ==> eq) succ. +Program Instance pred_wd : Proper (eq ==> eq) pred. +Program Instance add_wd : Proper (eq ==> eq ==> eq) add. +Program Instance sub_wd : Proper (eq ==> eq ==> eq) sub. +Program Instance mul_wd : Proper (eq ==> eq ==> eq) mul. -Add Morphism NZmul with signature Z.eq ==> Z.eq ==> Z.eq as NZmul_wd. +Theorem pred_succ : forall n, pred (succ n) == n. Proof. -intros; zsimpl; f_equal; assumption. -Qed. - -Theorem NZpred_succ : forall n, Z.pred (Z.succ n) == n. -Proof. -intros; zsimpl; auto with zarith. +intros. zify. auto with zarith. Qed. Section Induction. Variable A : Z.t -> Prop. -Hypothesis A_wd : predicate_wd Z.eq A. +Hypothesis A_wd : Proper (eq==>iff) A. Hypothesis A0 : A 0. -Hypothesis AS : forall n, A n <-> A (Z.succ n). - -Add Morphism A with signature Z.eq ==> iff as A_morph. -Proof. apply A_wd. Qed. +Hypothesis AS : forall n, A n <-> A (succ n). -Let B (z : Z) := A (Z.of_Z z). +Let B (z : Z) := A (of_Z z). Lemma B0 : B 0. Proof. unfold B; simpl. rewrite <- (A_wd 0); auto. -zsimpl; auto. +zify. auto. Qed. Lemma BS : forall z : Z, B z -> B (z + 1). Proof. intros z H. unfold B in *. apply -> AS in H. -setoid_replace (Z.of_Z (z + 1)) with (Z.succ (Z.of_Z z)); auto. -zsimpl; auto. +setoid_replace (of_Z (z + 1)) with (succ (of_Z z)); auto. +zify. auto. Qed. Lemma BP : forall z : Z, B z -> B (z - 1). Proof. intros z H. unfold B in *. rewrite AS. -setoid_replace (Z.succ (Z.of_Z (z - 1))) with (Z.of_Z z); auto. -zsimpl; auto with zarith. +setoid_replace (succ (of_Z (z - 1))) with (of_Z z); auto. +zify. auto with zarith. Qed. Lemma B_holds : forall z : Z, B z. @@ -135,172 +90,170 @@ intros; rewrite Zopp_succ; unfold Zpred; apply BP; auto. subst z'; auto with zarith. Qed. -Theorem NZinduction : forall n, A n. +Theorem bi_induction : forall n, A n. Proof. -intro n. setoid_replace n with (Z.of_Z (Z.to_Z n)). +intro n. setoid_replace n with (of_Z (to_Z n)). apply B_holds. -zsimpl; auto. +zify. auto. Qed. End Induction. -Theorem NZadd_0_l : forall n, 0 + n == n. +Theorem add_0_l : forall n, 0 + n == n. Proof. -intros; zsimpl; auto with zarith. +intros. zify. auto with zarith. Qed. -Theorem NZadd_succ_l : forall n m, (Z.succ n) + m == Z.succ (n + m). +Theorem add_succ_l : forall n m, (succ n) + m == succ (n + m). Proof. -intros; zsimpl; auto with zarith. +intros. zify. auto with zarith. Qed. -Theorem NZsub_0_r : forall n, n - 0 == n. +Theorem sub_0_r : forall n, n - 0 == n. Proof. -intros; zsimpl; auto with zarith. +intros. zify. auto with zarith. Qed. -Theorem NZsub_succ_r : forall n m, n - (Z.succ m) == Z.pred (n - m). +Theorem sub_succ_r : forall n m, n - (succ m) == pred (n - m). Proof. -intros; zsimpl; auto with zarith. +intros. zify. auto with zarith. Qed. -Theorem NZmul_0_l : forall n, 0 * n == 0. +Theorem mul_0_l : forall n, 0 * n == 0. Proof. -intros; zsimpl; auto with zarith. +intros. zify. auto with zarith. Qed. -Theorem NZmul_succ_l : forall n m, (Z.succ n) * m == n * m + m. +Theorem mul_succ_l : forall n m, (succ n) * m == n * m + m. Proof. -intros; zsimpl; ring. +intros. zify. ring. Qed. -End NZAxiomsMod. +(** Order *) -Definition NZlt := Z.lt. -Definition NZle := Z.le. -Definition NZmin := Z.min. -Definition NZmax := Z.max. +Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y). +Proof. + intros. zify. destruct (Zcompare_spec [x] [y]); auto. +Qed. -Infix "<=" := Z.le : IntScope. -Infix "<" := Z.lt : IntScope. +Definition eqb := eq_bool. -Lemma spec_compare_alt : forall x y, Z.compare x y = ([x] ?= [y])%Z. +Lemma eqb_eq : forall x y, eq_bool x y = true <-> x == y. Proof. - intros; generalize (Z.spec_compare x y). - destruct (Z.compare x y); auto. - intros H; rewrite H; symmetry; apply Zcompare_refl. + intros. zify. symmetry. apply Zeq_is_eq_bool. Qed. -Lemma spec_lt : forall x y, (x<y) <-> ([x]<[y])%Z. +Instance compare_wd : Proper (eq ==> eq ==> Logic.eq) compare. Proof. - intros; unfold Z.lt, Zlt; rewrite spec_compare_alt; intuition. +intros x x' Hx y y' Hy. rewrite 2 spec_compare, Hx, Hy; intuition. Qed. -Lemma spec_le : forall x y, (x<=y) <-> ([x]<=[y])%Z. +Instance lt_wd : Proper (eq ==> eq ==> iff) lt. Proof. - intros; unfold Z.le, Zle; rewrite spec_compare_alt; intuition. +intros x x' Hx y y' Hy; unfold lt; rewrite Hx, Hy; intuition. Qed. -Lemma spec_min : forall x y, [Z.min x y] = Zmin [x] [y]. +Theorem lt_eq_cases : forall n m, n <= m <-> n < m \/ n == m. Proof. - intros; unfold Z.min, Zmin. - rewrite spec_compare_alt; destruct Zcompare; auto. +intros. zify. omega. Qed. -Lemma spec_max : forall x y, [Z.max x y] = Zmax [x] [y]. +Theorem lt_irrefl : forall n, ~ n < n. Proof. - intros; unfold Z.max, Zmax. - rewrite spec_compare_alt; destruct Zcompare; auto. +intros. zify. omega. Qed. -Add Morphism Z.compare with signature Z.eq ==> Z.eq ==> (@eq comparison) as compare_wd. -Proof. -intros x x' Hx y y' Hy. -rewrite 2 spec_compare_alt; unfold Z.eq in *; rewrite Hx, Hy; intuition. +Theorem lt_succ_r : forall n m, n < (succ m) <-> n <= m. +Proof. +intros. zify. omega. Qed. -Add Morphism Z.lt with signature Z.eq ==> Z.eq ==> iff as NZlt_wd. +Theorem min_l : forall n m, n <= m -> min n m == n. Proof. -intros x x' Hx y y' Hy; unfold Z.lt; rewrite Hx, Hy; intuition. +intros n m. zify. omega with *. Qed. -Add Morphism Z.le with signature Z.eq ==> Z.eq ==> iff as NZle_wd. +Theorem min_r : forall n m, m <= n -> min n m == m. Proof. -intros x x' Hx y y' Hy; unfold Z.le; rewrite Hx, Hy; intuition. +intros n m. zify. omega with *. Qed. -Add Morphism Z.min with signature Z.eq ==> Z.eq ==> Z.eq as NZmin_wd. +Theorem max_l : forall n m, m <= n -> max n m == n. Proof. -intros; red; rewrite 2 spec_min; congruence. +intros n m. zify. omega with *. Qed. -Add Morphism Z.max with signature Z.eq ==> Z.eq ==> Z.eq as NZmax_wd. +Theorem max_r : forall n m, n <= m -> max n m == m. Proof. -intros; red; rewrite 2 spec_max; congruence. +intros n m. zify. omega with *. Qed. -Theorem NZlt_eq_cases : forall n m, n <= m <-> n < m \/ n == m. +(** Part specific to integers, not natural numbers *) + +Program Instance opp_wd : Proper (eq ==> eq) opp. + +Theorem succ_pred : forall n, succ (pred n) == n. Proof. -intros. -unfold Z.eq; rewrite spec_lt, spec_le; omega. +intros. zify. auto with zarith. Qed. -Theorem NZlt_irrefl : forall n, ~ n < n. +Theorem opp_0 : - 0 == 0. Proof. -intros; rewrite spec_lt; auto with zarith. +intros. zify. auto with zarith. Qed. -Theorem NZlt_succ_r : forall n m, n < (Z.succ m) <-> n <= m. +Theorem opp_succ : forall n, - (succ n) == pred (- n). Proof. -intros; rewrite spec_lt, spec_le, Z.spec_succ; omega. +intros. zify. auto with zarith. Qed. -Theorem NZmin_l : forall n m, n <= m -> Z.min n m == n. +Theorem abs_eq : forall n, 0 <= n -> abs n == n. Proof. -intros n m; unfold Z.eq; rewrite spec_le, spec_min. -generalize (Zmin_spec [n] [m]); omega. +intros n. zify. omega with *. Qed. -Theorem NZmin_r : forall n m, m <= n -> Z.min n m == m. +Theorem abs_neq : forall n, n <= 0 -> abs n == -n. Proof. -intros n m; unfold Z.eq; rewrite spec_le, spec_min. -generalize (Zmin_spec [n] [m]); omega. +intros n. zify. omega with *. Qed. -Theorem NZmax_l : forall n m, m <= n -> Z.max n m == n. +Theorem sgn_null : forall n, n==0 -> sgn n == 0. Proof. -intros n m; unfold Z.eq; rewrite spec_le, spec_max. -generalize (Zmax_spec [n] [m]); omega. +intros n. zify. omega with *. Qed. -Theorem NZmax_r : forall n m, n <= m -> Z.max n m == m. +Theorem sgn_pos : forall n, 0<n -> sgn n == succ 0. Proof. -intros n m; unfold Z.eq; rewrite spec_le, spec_max. -generalize (Zmax_spec [n] [m]); omega. +intros n. zify. omega with *. Qed. -End NZOrdAxiomsMod. - -Definition Zopp := Z.opp. - -Add Morphism Z.opp with signature Z.eq ==> Z.eq as Zopp_wd. +Theorem sgn_neg : forall n, n<0 -> sgn n == opp (succ 0). Proof. -intros; zsimpl; auto with zarith. +intros n. zify. omega with *. Qed. -Theorem Zsucc_pred : forall n, Z.succ (Z.pred n) == n. +Program Instance div_wd : Proper (eq==>eq==>eq) div. +Program Instance mod_wd : Proper (eq==>eq==>eq) modulo. + +Theorem div_mod : forall a b, ~b==0 -> a == b*(div a b) + (modulo a b). Proof. -red; intros; zsimpl; auto with zarith. +intros a b. zify. intros. apply Z_div_mod_eq_full; auto. Qed. -Theorem Zopp_0 : - 0 == 0. +Theorem mod_pos_bound : + forall a b, 0 < b -> 0 <= modulo a b /\ modulo a b < b. Proof. -red; intros; zsimpl; auto with zarith. +intros a b. zify. intros. apply Z_mod_lt; auto with zarith. Qed. -Theorem Zopp_succ : forall n, - (Z.succ n) == Z.pred (- n). +Theorem mod_neg_bound : + forall a b, b < 0 -> b < modulo a b /\ modulo a b <= 0. Proof. -intros; zsimpl; auto with zarith. +intros a b. zify. intros. apply Z_mod_neg; auto with zarith. Qed. -End ZSig_ZAxioms. +End ZTypeIsZAxioms. + +Module ZType_ZAxioms (Z : ZType) + <: ZAxiomsSig <: ZDivSig <: HasCompare Z <: HasEqBool Z <: HasMinMax Z + := Z <+ ZTypeIsZAxioms. |