diff options
| -rw-r--r-- | Makefile.common | 13 | ||||
| -rw-r--r-- | theories/Numbers/Integer/BigZ/BigZ.v | 119 | ||||
| -rw-r--r-- | theories/Numbers/Integer/BigZ/ZMake.v | 95 | ||||
| -rw-r--r-- | theories/Numbers/Integer/SpecViaZ/ZSig.v | 117 | ||||
| -rw-r--r-- | theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v | 306 | ||||
| -rw-r--r-- | theories/Numbers/Natural/BigN/BigN.v | 73 | ||||
| -rw-r--r-- | theories/Numbers/Natural/BigN/NBigN.v | 364 | ||||
| -rw-r--r-- | theories/Numbers/Natural/BigN/NMake_gen.ml | 17 | ||||
| -rw-r--r-- | theories/Numbers/Natural/SpecViaZ/NSig.v | 115 | ||||
| -rw-r--r-- | theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v | 356 | ||||
| -rw-r--r-- | theories/Numbers/Rational/BigQ/Q0Make.v | 4 | ||||
| -rw-r--r-- | theories/Numbers/Rational/BigQ/QbiMake.v | 4 | ||||
| -rw-r--r-- | theories/Numbers/Rational/BigQ/QifMake.v | 4 | ||||
| -rw-r--r-- | theories/Numbers/Rational/BigQ/QpMake.v | 45 | ||||
| -rw-r--r-- | theories/Numbers/Rational/BigQ/QvMake.v | 4 |
15 files changed, 1111 insertions, 525 deletions
diff --git a/Makefile.common b/Makefile.common index c968b41b87..0053dafdcf 100644 --- a/Makefile.common +++ b/Makefile.common @@ -685,10 +685,14 @@ NATURALPEANOVO:=$(addprefix theories/Numbers/Natural/Peano/, \ NATURALBINARYVO:=$(addprefix theories/Numbers/Natural/Binary/, \ NBinDefs.vo NBinary.vo ) +NATURALSPECVIAZVO:=$(addprefix theories/Numbers/Natural/SpecViaZ/, \ + NSig.vo NSigNAxioms.vo ) + NATURALBIGNVO:=$(addprefix theories/Numbers/Natural/BigN/, \ - Nbasic.vo NMake.vo BigN.vo NBigN.vo ) + Nbasic.vo NMake.vo BigN.vo ) -NATURALVO:=$(NATURALABSTRACTVO) $(NATURALPEANOVO) $(NATURALBINARYVO) $(NATURALBIGNVO) +NATURALVO:=$(NATURALABSTRACTVO) $(NATURALPEANOVO) $(NATURALBINARYVO) \ + $(NATURALSPECVIAZVO) $(NATURALBIGNVO) INTEGERABSTRACTVO:=$(addprefix theories/Numbers/Integer/Abstract/, \ ZAxioms.vo ZBase.vo ZPlus.vo ZTimes.vo \ @@ -700,11 +704,14 @@ INTEGERBINARYVO:=$(addprefix theories/Numbers/Integer/Binary/, \ INTEGERNATPAIRSVO:=$(addprefix theories/Numbers/Integer/NatPairs/, \ ZNatPairs.vo ) +INTEGERSPECVIAZVO:=$(addprefix theories/Numbers/Integer/SpecViaZ/, \ + ZSig.vo ZSigZAxioms.vo ) + INTEGERBIGZVO:=$(addprefix theories/Numbers/Integer/BigZ/, \ ZMake.vo BigZ.vo ) INTEGERVO:=$(INTEGERABSTRACTVO) $(INTEGERBINARYVO) $(INTEGERNATPAIRSVO) \ - $(INTEGERBIGZVO) + $(INTEGERSPECVIAZVO) $(INTEGERBIGZVO) RATIONALBIGQVO:=$(addprefix theories/Numbers/Rational/BigQ/, \ QMake_base.vo QpMake.vo QvMake.vo Q0Make.vo \ diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v index 934fbc4280..d2f9b0a024 100644 --- a/theories/Numbers/Integer/BigZ/BigZ.v +++ b/theories/Numbers/Integer/BigZ/BigZ.v @@ -11,50 +11,99 @@ (*i $Id$ i*) Require Export BigN. +Require Import ZTimesOrder. +Require Import ZSig. +Require Import ZSigZAxioms. Require Import ZMake. +Module BigZ <: ZType := ZMake.Make BigN. -Module BigZ := Make BigN. +(** Module [BigZ] implements [ZAxiomsSig] *) +Module Export BigZAxiomsMod := ZSig_ZAxioms BigZ. +Module Export BigZTimesOrderPropMod := ZTimesOrderPropFunct BigZAxiomsMod. -Definition bigZ := BigZ.t. +(** Notations about [BigZ] *) + +Notation bigZ := BigZ.t. Delimit Scope bigZ_scope with bigZ. Bind Scope bigZ_scope with bigZ. Bind Scope bigZ_scope with BigZ.t. Bind Scope bigZ_scope with BigZ.t_. -Notation " i + j " := (BigZ.add i j) : bigZ_scope. -Notation " i - j " := (BigZ.sub i j) : bigZ_scope. -Notation " i * j " := (BigZ.mul i j) : bigZ_scope. -Notation " i / j " := (BigZ.div i j) : bigZ_scope. -Notation " i ?= j " := (BigZ.compare i j) : bigZ_scope. - - - Theorem spec_to_Z: - forall n, BigN.to_Z (BigZ.to_N n) = - (Zsgn (BigZ.to_Z n) * BigZ.to_Z n)%Z. - intros n; case n; simpl; intros p; - generalize (BigN.spec_pos p); case (BigN.to_Z p); auto. - intros p1 H1; case H1; auto. - intros p1 H1; case H1; auto. - Qed. - - Theorem spec_to_N n: - (BigZ.to_Z n = - Zsgn (BigZ.to_Z n) * (BigN.to_Z (BigZ.to_N n)))%Z. - intros n; case n; simpl; intros p; - generalize (BigN.spec_pos p); case (BigN.to_Z p); auto. - intros p1 H1; case H1; auto. - intros p1 H1; case H1; auto. - Qed. - - Theorem spec_to_Z_pos: - forall n, (0 <= BigZ.to_Z n -> - BigN.to_Z (BigZ.to_N n) = BigZ.to_Z n)%Z. - intros n; case n; simpl; intros p; - generalize (BigN.spec_pos p); case (BigN.to_Z p); auto. - intros p1 _ H1; case H1; auto. - intros p1 H1; case H1; auto. - Qed. +Notation Local "0" := BigZ.zero : bigZ_scope. +Infix "+" := BigZ.add : bigZ_scope. +Infix "-" := BigZ.sub : bigZ_scope. +Notation "- x" := (BigZ.opp x) : bigZ_scope. +Infix "*" := BigZ.mul : bigZ_scope. +Infix "/" := BigZ.div : bigZ_scope. +Infix "?=" := BigZ.compare : bigZ_scope. +Infix "==" := BigZ.eq (at level 70, no associativity) : bigZ_scope. +Infix "<" := BigZ.lt : bigZ_scope. +Infix "<=" := BigZ.le : bigZ_scope. +Notation "[ i ]" := (BigZ.to_Z i) : bigZ_scope. + +Open Scope bigZ_scope. + +(** Some additional results about [BigZ] *) + +Theorem spec_to_Z: forall n:bigZ, + BigN.to_Z (BigZ.to_N n) = ((Zsgn [n]) * [n])%Z. +Proof. +intros n; case n; simpl; intros p; + generalize (BigN.spec_pos p); case (BigN.to_Z p); auto. +intros p1 H1; case H1; auto. +intros p1 H1; case H1; auto. +Qed. + +Theorem spec_to_N n: + ([n] = Zsgn [n] * (BigN.to_Z (BigZ.to_N n)))%Z. +Proof. +intros n; case n; simpl; intros p; + generalize (BigN.spec_pos p); case (BigN.to_Z p); auto. +intros p1 H1; case H1; auto. +intros p1 H1; case H1; auto. +Qed. + +Theorem spec_to_Z_pos: forall n, (0 <= [n])%Z -> + BigN.to_Z (BigZ.to_N n) = [n]. +Proof. +intros n; case n; simpl; intros p; + generalize (BigN.spec_pos p); case (BigN.to_Z p); auto. +intros p1 _ H1; case H1; auto. +intros p1 H1; case H1; auto. +Qed. + +Lemma sub_opp : forall x y : bigZ, x - y == x + (- y). +Proof. +red; intros; zsimpl; auto. +Qed. + +Lemma plus_opp : forall x : bigZ, x + (- x) == 0. +Proof. +red; intros; zsimpl; auto with zarith. +Qed. + +(** [BigZ] is a ring *) + +Lemma BigZring : + ring_theory BigZ.zero BigZ.one BigZ.add BigZ.mul BigZ.sub BigZ.opp BigZ.eq. +Proof. +constructor. +exact Zplus_0_l. +exact Zplus_comm. +exact Zplus_assoc. +exact Ztimes_1_l. +exact Ztimes_comm. +exact Ztimes_assoc. +exact Ztimes_plus_distr_r. +exact sub_opp. +exact plus_opp. +Qed. + +Add Ring BigZr : BigZring. + +(** Todo: tactic translating from [BigZ] to [Z] + omega *) +(** Todo: micromega *) diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v index 83171388d9..cbf6f701f2 100644 --- a/theories/Numbers/Integer/BigZ/ZMake.v +++ b/theories/Numbers/Integer/BigZ/ZMake.v @@ -12,94 +12,18 @@ Require Import ZArith. Require Import BigNumPrelude. +Require Import NSig. +Require Import ZSig. Open Scope Z_scope. -Module Type NType. - - Parameter t : Type. - - Parameter zero : t. - Parameter one : t. - - Parameter of_N : N -> t. - Parameter to_Z : t -> Z. - Parameter spec_pos: forall x, 0 <= to_Z x. - Parameter spec_0: to_Z zero = 0. - Parameter spec_1: to_Z one = 1. - Parameter spec_of_N: forall x, to_Z (of_N x) = Z_of_N x. - - Parameter compare : t -> t -> comparison. - - Parameter spec_compare: forall x y, - match compare x y with - Eq => to_Z x = to_Z y - | Lt => to_Z x < to_Z y - | Gt => to_Z x > to_Z y - end. - - Parameter eq_bool : t -> t -> bool. - - Parameter spec_eq_bool: forall x y, - if eq_bool x y then to_Z x = to_Z y else to_Z x <> to_Z y. - - Parameter succ : t -> t. - - Parameter spec_succ: forall n, to_Z (succ n) = to_Z n + 1. - - Parameter add : t -> t -> t. - - Parameter spec_add: forall x y, to_Z (add x y) = to_Z x + to_Z y. - - Parameter pred : t -> t. - - Parameter spec_pred: forall x, 0 < to_Z x -> to_Z (pred x) = to_Z x - 1. - - Parameter sub : t -> t -> t. - - Parameter spec_sub: forall x y, to_Z y <= to_Z x -> - to_Z (sub x y) = to_Z x - to_Z y. - - Parameter mul : t -> t -> t. - - Parameter spec_mul: forall x y, to_Z (mul x y) = to_Z x * to_Z y. - - Parameter square : t -> t. - - Parameter spec_square: forall x, to_Z (square x) = to_Z x * to_Z x. - - Parameter power_pos : t -> positive -> t. - - Parameter spec_power_pos: forall x n, to_Z (power_pos x n) = to_Z x ^ Zpos n. - - Parameter sqrt : t -> t. - - Parameter spec_sqrt: forall x, to_Z (sqrt x) ^ 2 <= to_Z x < (to_Z (sqrt x) + 1) ^ 2. - - Parameter div_eucl : t -> t -> t * t. - - Parameter spec_div_eucl: forall x y, - 0 < to_Z y -> - let (q,r) := div_eucl x y in (to_Z q, to_Z r) = (Zdiv_eucl (to_Z x) (to_Z y)). +(** * ZMake - Parameter div : t -> t -> t. - - Parameter spec_div: forall x y, - 0 < to_Z y -> to_Z (div x y) = to_Z x / to_Z y. - - Parameter modulo : t -> t -> t. - - Parameter spec_modulo: - forall x y, 0 < to_Z y -> to_Z (modulo x y) = to_Z x mod to_Z y. - - Parameter gcd : t -> t -> t. - - Parameter spec_gcd: forall a b, to_Z (gcd a b) = Zgcd (to_Z a) (to_Z b). - - -End NType. + A generic transformation from a structure of natural numbers + [NSig.NType] to a structure of integers [ZSig.ZType]. +*) -Module Make (N:NType). +Module Make (N:NType) <: ZType. Inductive t_ := | Pos : N.t -> t_ @@ -131,6 +55,7 @@ Module Make (N:NType). intros; rewrite N.spec_of_N; auto. Qed. + Definition eq x y := (to_Z x = to_Z y). Theorem spec_0: to_Z zero = 0. exact N.spec_0. @@ -160,6 +85,10 @@ Module Make (N:NType). | Neg nx, Neg ny => N.compare ny nx 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. Theorem spec_compare: forall x y, match compare x y with diff --git a/theories/Numbers/Integer/SpecViaZ/ZSig.v b/theories/Numbers/Integer/SpecViaZ/ZSig.v new file mode 100644 index 0000000000..4e45939831 --- /dev/null +++ b/theories/Numbers/Integer/SpecViaZ/ZSig.v @@ -0,0 +1,117 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) +(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) +(************************************************************************) + +(*i $Id$ i*) + +Require Import ZArith Znumtheory. + +Open Scope Z_scope. + +(** * ZSig *) + +(** Interface of a rich structure about integers. + Specifications are written via translation to Z. +*) + +Module Type ZType. + + Parameter t : Type. + + Parameter to_Z : t -> Z. + Notation "[ x ]" := (to_Z x). + + Definition eq x y := ([x] = [y]). + + Parameter of_Z : Z -> t. + Parameter spec_of_Z: forall x, to_Z (of_Z x) = x. + + 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 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 spec_gcd: forall a b, [gcd a b] = Zgcd (to_Z a) (to_Z b). + +End ZType. diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v new file mode 100644 index 0000000000..3d9d3d1901 --- /dev/null +++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v @@ -0,0 +1,306 @@ +(************************************************************************) +(* 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$ i*) + +Require Import ZArith. +Require Import ZAxioms. +Require Import ZSig. + +(** * The interface [ZSig.ZType] implies the interface [ZAxiomsSig] *) + +Module ZSig_ZAxioms (Z:ZType) <: ZAxiomsSig. + +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. + +Ltac zsimpl := unfold Z.eq in *; autorewrite with Zspec. + +Module Export NZOrdAxiomsMod <: NZOrdAxiomsSig. +Module Export NZAxiomsMod <: NZAxiomsSig. + +Definition NZ := Z.t. +Definition NZeq := Z.eq. +Definition NZ0 := Z.zero. +Definition NZsucc := Z.succ. +Definition NZpred := Z.pred. +Definition NZplus := Z.add. +Definition NZminus := Z.sub. +Definition NZtimes := Z.mul. + +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. + +Add Morphism NZplus with signature Z.eq ==> Z.eq ==> Z.eq as NZplus_wd. +Proof. +intros; zsimpl; f_equal; assumption. +Qed. + +Add Morphism NZminus with signature Z.eq ==> Z.eq ==> Z.eq as NZminus_wd. +Proof. +intros; zsimpl; f_equal; assumption. +Qed. + +Add Morphism NZtimes with signature Z.eq ==> Z.eq ==> Z.eq as NZtimes_wd. +Proof. +intros; zsimpl; f_equal; assumption. +Qed. + +Theorem NZpred_succ : forall n, Z.pred (Z.succ n) == n. +Proof. +intros; zsimpl; auto with zarith. +Qed. + +Section Induction. + +Variable A : Z.t -> Prop. +Hypothesis A_wd : predicate_wd Z.eq 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. + +Let B (z : Z) := A (Z.of_Z z). + +Lemma B0 : B 0. +Proof. +unfold B; simpl. +rewrite <- (A_wd 0); auto. +zsimpl; 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. +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. +Qed. + +Lemma B_holds : forall z : Z, B z. +Proof. +intros; destruct (Z_lt_le_dec 0 z). +apply natlike_ind; auto with zarith. +apply B0. +intros; apply BS; auto. +replace z with (-(-z))%Z in * by (auto with zarith). +remember (-z)%Z as z'. +pattern z'; apply natlike_ind. +apply B0. +intros; rewrite Zopp_succ; unfold Zpred; apply BP; auto. +subst z'; auto with zarith. +Qed. + +Theorem NZinduction : forall n, A n. +Proof. +intro n. setoid_replace n with (Z.of_Z (Z.to_Z n)). +apply B_holds. +zsimpl; auto. +Qed. + +End Induction. + +Theorem NZplus_0_l : forall n, 0 + n == n. +Proof. +intros; zsimpl; auto with zarith. +Qed. + +Theorem NZplus_succ_l : forall n m, (Z.succ n) + m == Z.succ (n + m). +Proof. +intros; zsimpl; auto with zarith. +Qed. + +Theorem NZminus_0_r : forall n, n - 0 == n. +Proof. +intros; zsimpl; auto with zarith. +Qed. + +Theorem NZminus_succ_r : forall n m, n - (Z.succ m) == Z.pred (n - m). +Proof. +intros; zsimpl; auto with zarith. +Qed. + +Theorem NZtimes_0_l : forall n, 0 * n == 0. +Proof. +intros; zsimpl; auto with zarith. +Qed. + +Theorem NZtimes_succ_l : forall n m, (Z.succ n) * m == n * m + m. +Proof. +intros; zsimpl; ring. +Qed. + +End NZAxiomsMod. + +Definition NZlt := Z.lt. +Definition NZle := Z.le. +Definition NZmin := Z.min. +Definition NZmax := Z.max. + +Infix "<=" := Z.le : IntScope. +Infix "<" := Z.lt : IntScope. + +Lemma spec_compare_alt : forall x y, Z.compare x y = ([x] ?= [y])%Z. +Proof. + intros; generalize (Z.spec_compare x y). + destruct (Z.compare x y); auto. + intros H; rewrite H; symmetry; apply Zcompare_refl. +Qed. + +Lemma spec_lt : forall x y, (x<y) <-> ([x]<[y])%Z. +Proof. + intros; unfold Z.lt, Zlt; rewrite spec_compare_alt; intuition. +Qed. + +Lemma spec_le : forall x y, (x<=y) <-> ([x]<=[y])%Z. +Proof. + intros; unfold Z.le, Zle; rewrite spec_compare_alt; intuition. +Qed. + +Lemma spec_min : forall x y, [Z.min x y] = Zmin [x] [y]. +Proof. + intros; unfold Z.min, Zmin. + rewrite spec_compare_alt; destruct Zcompare; auto. +Qed. + +Lemma spec_max : forall x y, [Z.max x y] = Zmax [x] [y]. +Proof. + intros; unfold Z.max, Zmax. + rewrite spec_compare_alt; destruct Zcompare; auto. +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; rewrite Hx, Hy; intuition. +Qed. + +Add Morphism Z.lt with signature Z.eq ==> Z.eq ==> iff as NZlt_wd. +Proof. +intros x x' Hx y y' Hy; unfold Z.lt; rewrite Hx, Hy; intuition. +Qed. + +Add Morphism Z.le with signature Z.eq ==> Z.eq ==> iff as NZle_wd. +Proof. +intros x x' Hx y y' Hy; unfold Z.le; rewrite Hx, Hy; intuition. +Qed. + +Add Morphism Z.min with signature Z.eq ==> Z.eq ==> Z.eq as NZmin_wd. +Proof. +intros; red; rewrite 2 spec_min; congruence. +Qed. + +Add Morphism Z.max with signature Z.eq ==> Z.eq ==> Z.eq as NZmax_wd. +Proof. +intros; red; rewrite 2 spec_max; congruence. +Qed. + +Theorem NZlt_eq_cases : forall n m, n <= m <-> n < m \/ n == m. +Proof. +intros. +unfold Z.eq; rewrite spec_lt, spec_le; omega. +Qed. + +Theorem NZlt_irrefl : forall n, ~ n < n. +Proof. +intros; rewrite spec_lt; auto with zarith. +Qed. + +Theorem NZlt_succ_r : forall n m, n < (Z.succ m) <-> n <= m. +Proof. +intros; rewrite spec_lt, spec_le, Z.spec_succ; omega. +Qed. + +Theorem NZmin_l : forall n m, n <= m -> Z.min n m == n. +Proof. +intros n m; unfold Z.eq; rewrite spec_le, spec_min. +generalize (Zmin_spec [n] [m]); omega. +Qed. + +Theorem NZmin_r : forall n m, m <= n -> Z.min n m == m. +Proof. +intros n m; unfold Z.eq; rewrite spec_le, spec_min. +generalize (Zmin_spec [n] [m]); omega. +Qed. + +Theorem NZmax_l : forall n m, m <= n -> Z.max n m == n. +Proof. +intros n m; unfold Z.eq; rewrite spec_le, spec_max. +generalize (Zmax_spec [n] [m]); omega. +Qed. + +Theorem NZmax_r : forall n m, n <= m -> Z.max n m == m. +Proof. +intros n m; unfold Z.eq; rewrite spec_le, spec_max. +generalize (Zmax_spec [n] [m]); omega. +Qed. + +End NZOrdAxiomsMod. + +Definition Zopp := Z.opp. + +Add Morphism Z.opp with signature Z.eq ==> Z.eq as Zopp_wd. +Proof. +intros; zsimpl; auto with zarith. +Qed. + +Theorem Zsucc_pred : forall n, Z.succ (Z.pred n) == n. +Proof. +red; intros; zsimpl; auto with zarith. +Qed. + +Theorem Zopp_0 : - 0 == 0. +Proof. +red; intros; zsimpl; auto with zarith. +Qed. + +Theorem Zopp_succ : forall n, - (Z.succ n) == Z.pred (- n). +Proof. +intros; zsimpl; auto with zarith. +Qed. + +End ZSig_ZAxioms. diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v index 033364f72d..881b7984cf 100644 --- a/theories/Numbers/Natural/BigN/BigN.v +++ b/theories/Numbers/Natural/BigN/BigN.v @@ -17,32 +17,67 @@ Author: Arnaud Spiwack Require Export Int31. Require Import CyclicAxioms. Require Import Cyclic31. +Require Import NSig. +Require Import NSigNAxioms. Require Import NMake. +Require Import NMinus. -Open Scope int31_scope. +Module BigN <: NType := NMake.Make Int31Cyclic. -Module BigN := NMake.Make Int31Cyclic. +(** Module [BigN] implements [NAxiomsSig] *) -Definition bigN := BigN.t. +Module Export BigNAxiomsMod := NSig_NAxioms BigN. +Module Export BigNMinusPropMod := NMinusPropFunct BigNAxiomsMod. + +(** Notations about [BigN] *) + +Notation bigN := BigN.t. Delimit Scope bigN_scope with bigN. Bind Scope bigN_scope with bigN. Bind Scope bigN_scope with BigN.t. Bind Scope bigN_scope with BigN.t_. -Notation " i + j " := (BigN.add i j) : bigN_scope. -Notation " i - j " := (BigN.sub i j) : bigN_scope. -Notation " i * j " := (BigN.mul i j) : bigN_scope. -Notation " i / j " := (BigN.div i j) : bigN_scope. -Notation " i ?= j " := (BigN.compare i j) : bigN_scope. - - Theorem succ_pred: forall q, - (0 < BigN.to_Z q -> - BigN.to_Z (BigN.succ (BigN.pred q)) = BigN.to_Z q)%Z. - intros q Hq. - rewrite BigN.spec_succ. - rewrite BigN.spec_pred; auto. - generalize Hq; set (a := BigN.to_Z q). - ring_simplify (a - 1 + 1)%Z; auto. - Qed. - +Notation Local "0" := BigN.zero : bigN_scope. (* temporary notation *) +Infix "+" := BigN.add : bigN_scope. +Infix "-" := BigN.sub : bigN_scope. +Infix "*" := BigN.mul : bigN_scope. +Infix "/" := BigN.div : bigN_scope. +Infix "?=" := BigN.compare : bigN_scope. +Infix "==" := BigN.eq (at level 70, no associativity) : bigN_scope. +Infix "<" := BigN.lt : bigN_scope. +Infix "<=" := BigN.le : bigN_scope. +Notation "[ i ]" := (BigN.to_Z i) : bigN_scope. + +Open Scope bigN_scope. + +(** Example of reasoning about [BigN] *) + +Theorem succ_pred: forall q:bigN, + 0 < q -> BigN.succ (BigN.pred q) == q. +Proof. +intros; apply succ_pred. +intro H'; rewrite H' in H; discriminate. +Qed. + +(** [BigN] is a semi-ring *) + +Lemma BigNring : + semi_ring_theory BigN.zero BigN.one BigN.add BigN.mul BigN.eq. +Proof. +constructor. +exact plus_0_l. +exact plus_comm. +exact plus_assoc. +exact times_1_l. +exact times_0_l. +exact times_comm. +exact times_assoc. +exact times_plus_distr_r. +Qed. + +Add Ring BigNr : BigNring. + +(** Todo: tactic translating from [BigN] to [Z] + omega *) + +(** Todo: micromega *) diff --git a/theories/Numbers/Natural/BigN/NBigN.v b/theories/Numbers/Natural/BigN/NBigN.v deleted file mode 100644 index e933b65780..0000000000 --- a/theories/Numbers/Natural/BigN/NBigN.v +++ /dev/null @@ -1,364 +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$ i*) - -Require Import Nnat. -Require Import NMinus. -Require Export BigN. - -(** * [BigN] implements [NAxiomsSig] *) - -Module BigNAxiomsMod <: NAxiomsSig. -Import BigN. -Open Local Scope bigN_scope. -Module Export NZOrdAxiomsMod <: NZOrdAxiomsSig. -Module Export NZAxiomsMod <: NZAxiomsSig. - -Definition NZ := bigN. -Definition NZeq n m := (to_Z n = to_Z m). -Definition NZ0 := 0. -Definition NZsucc := succ. -Definition NZpred := pred. -Definition NZplus := add. -Definition NZminus := sub. -Definition NZtimes := mul. - -Delimit Scope IntScope with Int. -Bind Scope IntScope with NZ. -Open Local Scope IntScope. -Notation "[ x ]" := (to_Z x). -Notation "x == y" := (NZeq x y) (at level 70) : IntScope. -Notation "x ~= y" := (~ NZeq x y) (at level 70) : IntScope. -Notation "0" := NZ0 : IntScope. -Notation "'S'" := NZsucc : IntScope. -Notation "'P'" := NZpred : IntScope. -Notation "x + y" := (NZplus x y) : IntScope. -Notation "x - y" := (NZminus x y) : IntScope. -Notation "x * y" := (NZtimes x y) : IntScope. - -Theorem NZeq_equiv : equiv NZ NZeq. -Proof. -unfold NZeq; repeat split; repeat red; intros; auto; congruence. -Qed. - -Add Relation NZ NZeq - 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 NZeq ==> NZeq as NZsucc_wd. -Proof. -unfold NZeq; intros; rewrite 2 spec_succ; f_equal; auto. -Qed. - -Add Morphism NZpred with signature NZeq ==> NZeq as NZpred_wd. -Proof. -unfold NZeq; intros. -generalize (spec_pos y) (spec_pos x) (spec_eq_bool x 0). -destruct eq_bool; change (to_Z 0) with 0%Z; intros. -rewrite 2 spec_pred0; congruence. -rewrite 2 spec_pred; f_equal; auto; try omega. -Qed. - -Add Morphism NZplus with signature NZeq ==> NZeq ==> NZeq as NZplus_wd. -Proof. -unfold NZeq; intros; rewrite 2 spec_add; f_equal; auto. -Qed. - -Add Morphism NZminus with signature NZeq ==> NZeq ==> NZeq as NZminus_wd. -Proof. -unfold NZeq; intros x x' Hx y y' Hy. -destruct (Z_lt_le_dec [x] [y]). -rewrite 2 spec_sub0; f_equal; congruence. -rewrite 2 spec_sub; f_equal; congruence. -Qed. - -Add Morphism NZtimes with signature NZeq ==> NZeq ==> NZeq as NZtimes_wd. -Proof. -unfold NZeq; intros; rewrite 2 spec_mul; f_equal; auto. -Qed. - -Theorem NZpred_succ : forall n : NZ, P (S n) == n. -Proof. -unfold NZeq; intros. -rewrite BigN.spec_pred; rewrite BigN.spec_succ. -omega. -generalize (BigN.spec_pos n); omega. -Qed. - -Definition of_Z z := of_N (Zabs_N z). - -Section Induction. - -Variable A : NZ -> Prop. -Hypothesis A_wd : predicate_wd NZeq A. -Hypothesis A0 : A 0. -Hypothesis AS : forall n : NZ, A n <-> A (S n). - -Add Morphism A with signature NZeq ==> iff as A_morph. -Proof. apply A_wd. Qed. - -Let B (z : Z) := A (of_Z z). - -Lemma B0 : B 0. -Proof. -exact A0. -Qed. - -Lemma BS : forall z : Z, 0 <= z -> B z -> B (z + 1). -Proof. -intros z H1 H2. -unfold B in *. apply -> AS in H2. -setoid_replace (of_Z (z + 1)) with (S (of_Z z)); auto. -unfold NZeq. rewrite spec_succ. -unfold of_Z. -rewrite 2 spec_of_N, 2 Z_of_N_abs, 2 Zabs_eq; auto with zarith. -Qed. - -Lemma B_holds : forall z : Z, 0 <= z -> B z. -Proof. -exact (natlike_ind B B0 BS). -Qed. - -Theorem NZinduction : forall n : NZ, A n. -Proof. -intro n. setoid_replace n with (of_Z (to_Z n)). -apply B_holds. apply spec_pos. -red; unfold of_Z. -rewrite spec_of_N, Z_of_N_abs, Zabs_eq; auto. -apply spec_pos. -Qed. - -End Induction. - -Theorem NZplus_0_l : forall n : NZ, 0 + n == n. -Proof. -intros; red; rewrite spec_add; auto with zarith. -Qed. - -Theorem NZplus_succ_l : forall n m : NZ, (S n) + m == S (n + m). -Proof. -intros; red; rewrite spec_add, 2 spec_succ, spec_add; auto with zarith. -Qed. - -Theorem NZminus_0_r : forall n : NZ, n - 0 == n. -Proof. -intros; red; rewrite spec_sub; change [0] with 0%Z; auto with zarith. -apply spec_pos. -Qed. - -Theorem NZminus_succ_r : forall n m : NZ, n - (S m) == P (n - m). -Proof. -intros; red. -destruct (Z_lt_le_dec [n] [S m]) as [H|H]. -rewrite spec_sub0; auto. -rewrite spec_succ in H. -rewrite spec_pred0; auto. -destruct (Z_eq_dec [n] [m]). -rewrite spec_sub; auto with zarith. -rewrite spec_sub0; auto with zarith. - -rewrite spec_sub, spec_succ in *; auto. -rewrite spec_pred, spec_sub; auto with zarith. -rewrite spec_sub; auto with zarith. -Qed. - -Theorem NZtimes_0_l : forall n : NZ, 0 * n == 0. -Proof. -intros; red. -rewrite spec_mul; auto with zarith. -Qed. - -Theorem NZtimes_succ_l : forall n m : NZ, (S n) * m == n * m + m. -Proof. -intros; red. -rewrite spec_add, 2 spec_mul, spec_succ; ring. -Qed. - -End NZAxiomsMod. - -Open Scope bigN_scope. -Open Scope IntScope. - -Definition NZlt n m := (compare n m = Lt). -Definition NZle n m := (compare n m <> Gt). -Definition NZmin n m := match compare n m with Gt => m | _ => n end. -Definition NZmax n m := match compare n m with Lt => m | _ => n end. - -Infix "<=" := NZle : IntScope. -Infix "<" := NZlt : IntScope. - -Lemma spec_compare_alt : forall x y, (x ?= y) = ([x] ?= [y])%Z. -Proof. - intros; generalize (spec_compare x y). - destruct (x ?= y); auto. - intros H; rewrite H; symmetry; apply Zcompare_refl. -Qed. - -Lemma spec_lt : forall x y, (x<y) <-> ([x]<[y])%Z. -Proof. - intros; unfold NZlt, Zlt; rewrite spec_compare_alt; intuition. -Qed. - -Lemma spec_le : forall x y, (x<=y) <-> ([x]<=[y])%Z. -Proof. - intros; unfold NZle, Zle; rewrite spec_compare_alt; intuition. -Qed. - -Lemma spec_min : forall x y, [NZmin x y] = Zmin [x] [y]. -Proof. - intros; unfold NZmin, Zmin. - rewrite spec_compare_alt; destruct Zcompare; auto. -Qed. - -Lemma spec_max : forall x y, [NZmax x y] = Zmax [x] [y]. -Proof. - intros; unfold NZmax, Zmax. - rewrite spec_compare_alt; destruct Zcompare; auto. -Qed. - -Add Morphism compare with signature NZeq ==> NZeq ==> (@eq comparison) as compare_wd. -Proof. -intros x x' Hx y y' Hy. -rewrite 2 spec_compare_alt; rewrite Hx, Hy; intuition. -Qed. - -Add Morphism NZlt with signature NZeq ==> NZeq ==> iff as NZlt_wd. -Proof. -intros x x' Hx y y' Hy; unfold NZlt; rewrite Hx, Hy; intuition. -Qed. - -Add Morphism NZle with signature NZeq ==> NZeq ==> iff as NZle_wd. -Proof. -intros x x' Hx y y' Hy; unfold NZle; rewrite Hx, Hy; intuition. -Qed. - -Add Morphism NZmin with signature NZeq ==> NZeq ==> NZeq as NZmin_wd. -Proof. -intros; red; rewrite 2 spec_min; congruence. -Qed. - -Add Morphism NZmax with signature NZeq ==> NZeq ==> NZeq as NZmax_wd. -Proof. -intros; red; rewrite 2 spec_max; congruence. -Qed. - -Theorem NZlt_eq_cases : forall n m : NZ, n <= m <-> n < m \/ n == m. -Proof. -intros. -unfold NZeq; rewrite spec_lt, spec_le; omega. -Qed. - -Theorem NZlt_irrefl : forall n : NZ, ~ n < n. -Proof. -intros; rewrite spec_lt; auto with zarith. -Qed. - -Theorem NZlt_succ_r : forall n m : NZ, n < (NZsucc m) <-> n <= m. -Proof. -intros; rewrite spec_lt, spec_le, spec_succ; omega. -Qed. - -Theorem NZmin_l : forall n m : NZ, n <= m -> NZmin n m == n. -Proof. -intros n m; unfold NZeq; rewrite spec_le, spec_min. -generalize (Zmin_spec [n] [m]); omega. -Qed. - -Theorem NZmin_r : forall n m : NZ, m <= n -> NZmin n m == m. -Proof. -intros n m; unfold NZeq; rewrite spec_le, spec_min. -generalize (Zmin_spec [n] [m]); omega. -Qed. - -Theorem NZmax_l : forall n m : NZ, m <= n -> NZmax n m == n. -Proof. -intros n m; unfold NZeq; rewrite spec_le, spec_max. -generalize (Zmax_spec [n] [m]); omega. -Qed. - -Theorem NZmax_r : forall n m : NZ, n <= m -> NZmax n m == m. -Proof. -intros n m; unfold NZeq; rewrite spec_le, spec_max. -generalize (Zmax_spec [n] [m]); omega. -Qed. - -End NZOrdAxiomsMod. - -Theorem pred_0 : P 0 == 0. -Proof. -reflexivity. -Qed. - -Definition to_N n := Zabs_N (to_Z n). - -Definition recursion (A : Type) (a : A) (f : NZ -> A -> A) (n : NZ) := - Nrect (fun _ => A) a (fun n a => f (of_N n) a) (to_N n). -Implicit Arguments recursion [A]. - -Theorem recursion_wd : -forall (A : Type) (Aeq : relation A), - forall a a' : A, Aeq a a' -> - forall f f' : NZ -> A -> A, fun2_eq NZeq Aeq Aeq f f' -> - forall x x' : NZ, x == x' -> - Aeq (recursion a f x) (recursion a' f' x'). -Proof. -unfold fun2_wd, NZeq, fun2_eq. -intros A Aeq a a' Eaa' f f' Eff' x x' Exx'. -unfold recursion. -unfold to_N. -rewrite <- Exx'; clear x' Exx'. -replace (Zabs_N [x]) with (N_of_nat (Zabs_nat [x])). -induction (Zabs_nat [x]). -simpl; auto. -rewrite N_of_S, 2 Nrect_step; auto. -destruct [x]; simpl; auto. -change (nat_of_P p) with (nat_of_N (Npos p)); apply N_of_nat_of_N. -change (nat_of_P p) with (nat_of_N (Npos p)); apply N_of_nat_of_N. -Qed. - -Theorem recursion_0 : - forall (A : Type) (a : A) (f : NZ -> A -> A), recursion a f 0 = a. -Proof. -intros A a f; unfold recursion; now rewrite Nrect_base. -Qed. - -Theorem recursion_succ : - forall (A : Type) (Aeq : relation A) (a : A) (f : NZ -> A -> A), - Aeq a a -> fun2_wd NZeq Aeq Aeq f -> - forall n : NZ, Aeq (recursion a f (S n)) (f n (recursion a f n)). -Proof. -unfold NZeq, recursion, fun2_wd; intros A Aeq a f EAaa f_wd n. -replace (to_N (S n)) with (Nsucc (to_N n)). -rewrite Nrect_step. -apply f_wd; auto. -unfold to_N. -rewrite spec_of_N, Z_of_N_abs, Zabs_eq; auto. - apply spec_pos. - -fold (recursion a f n). -apply recursion_wd; auto. -red; auto. -red; auto. -unfold to_N. - -rewrite spec_succ. -change ([n]+1)%Z with (Zsucc [n]). -apply Z_of_N_eq_rev. -rewrite Z_of_N_succ. -rewrite 2 Z_of_N_abs. -rewrite 2 Zabs_eq; auto. -generalize (spec_pos n); auto with zarith. -apply spec_pos; auto. -Qed. - -End BigNAxiomsMod. - -Module Export BigNMinusPropMod := NMinusPropFunct BigNAxiomsMod. diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml index 22a4b200a2..534b680e2a 100644 --- a/theories/Numbers/Natural/BigN/NMake_gen.ml +++ b/theories/Numbers/Natural/BigN/NMake_gen.ml @@ -79,8 +79,9 @@ let _ = pr "Require Import Nbasic."; pr "Require Import Wf_nat."; pr "Require Import StreamMemo."; + pr "Require Import NSig."; pr ""; - pr "Module Make (Import W0:CyclicType)."; + pr "Module Make (Import W0:CyclicType) <: NType."; pr ""; pr " Definition w0 := W0.w."; @@ -163,8 +164,13 @@ let _ = pr " Open Scope Z_scope."; pr " Notation \"[ x ]\" := (to_Z x)."; - pr " "; + pr ""; + pr " Definition to_N x := Zabs_N (to_Z x)."; + pr ""; + + pr " Definition eq x y := (to_Z x = to_Z y)."; + pr ""; pp " (* Regular make op (no karatsuba) *)"; pp " Fixpoint nmake_op (ww:Type) (ww_op: znz_op ww) (n: nat) : "; @@ -1315,6 +1321,12 @@ let _ = pr " comparenm)."; pr ""; + pr " Definition lt n m := compare n m = Lt."; + pr " Definition le n m := compare n m <> Gt."; + pr " Definition min n m := match compare n m with Gt => m | _ => n end."; + pr " Definition max n m := match compare n m with Lt => m | _ => n end."; + pr ""; + for i = 0 to size do pp " Let spec_compare_%i: forall x y," i; pp " match compare_%i x y with " i; @@ -2396,7 +2408,6 @@ let _ = pr " end."; pr ""; - pr " Theorem spec_of_N: forall x,"; pr " [of_N x] = Z_of_N x."; pa " Admitted."; diff --git a/theories/Numbers/Natural/SpecViaZ/NSig.v b/theories/Numbers/Natural/SpecViaZ/NSig.v new file mode 100644 index 0000000000..e53e627eca --- /dev/null +++ b/theories/Numbers/Natural/SpecViaZ/NSig.v @@ -0,0 +1,115 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) +(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) +(************************************************************************) + +(*i $Id$ i*) + +Require Import ZArith Znumtheory. + +Open Scope Z_scope. + +(** * NSig *) + +(** Interface of a rich structure about natural numbers. + Specifications are written via translation to Z. +*) + +Module Type NType. + + Parameter t : Type. + + Parameter to_Z : t -> Z. + Notation "[ x ]" := (to_Z x). + Parameter spec_pos: forall x, 0 <= [x]. + + Parameter of_N : N -> t. + Parameter spec_of_N: forall x, to_Z (of_N x) = Z_of_N x. + Definition to_N n := Zabs_N (to_Z n). + + Definition eq n m := ([n] = [m]). + + Parameter zero : t. + Parameter one : t. + + Parameter spec_0: [zero] = 0. + Parameter spec_1: [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, 0 < [x] -> [pred x] = [x] - 1. + Parameter spec_pred0: forall x, [x] = 0 -> [pred x] = 0. + + Parameter sub : t -> t -> t. + + Parameter spec_sub: forall x y, [y] <= [x] -> [sub x y] = [x] - [y]. + Parameter spec_sub0: forall x y, [x] < [y]-> [sub x y] = 0. + + 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 sqrt : t -> t. + + Parameter spec_sqrt: forall x, [sqrt x] ^ 2 <= [x] < ([sqrt x] + 1) ^ 2. + + Parameter div_eucl : t -> t -> t * t. + + Parameter spec_div_eucl: forall x y, + 0 < [y] -> + 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, 0 < [y] -> [div x y] = [x] / [y]. + + Parameter modulo : t -> t -> t. + + Parameter spec_modulo: + forall x y, 0 < [y] -> [modulo x y] = [x] mod [y]. + + Parameter gcd : t -> t -> t. + + Parameter spec_gcd: forall a b, [gcd a b] = Zgcd (to_Z a) (to_Z b). + +End NType. diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v new file mode 100644 index 0000000000..115f78be0d --- /dev/null +++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v @@ -0,0 +1,356 @@ +(************************************************************************) +(* 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$ i*) + +Require Import ZArith. +Require Import Nnat. +Require Import NAxioms. +Require Import NSig. + +(** * The interface [NSig.NType] implies the interface [NAxiomsSig] *) + +Module NSig_NAxioms (N:NType) <: NAxiomsSig. + +Delimit Scope IntScope with Int. +Bind Scope IntScope with N.t. +Open Local Scope IntScope. +Notation "[ x ]" := (N.to_Z x) : IntScope. +Infix "==" := N.eq (at level 70) : IntScope. +Notation "0" := N.zero : IntScope. +Infix "+" := N.add : IntScope. +Infix "-" := N.sub : IntScope. +Infix "*" := N.mul : IntScope. + +Module Export NZOrdAxiomsMod <: NZOrdAxiomsSig. +Module Export NZAxiomsMod <: NZAxiomsSig. + +Definition NZ := N.t. +Definition NZeq := N.eq. +Definition NZ0 := N.zero. +Definition NZsucc := N.succ. +Definition NZpred := N.pred. +Definition NZplus := N.add. +Definition NZminus := N.sub. +Definition NZtimes := N.mul. + +Theorem NZeq_equiv : equiv N.t N.eq. +Proof. +repeat split; repeat red; intros; auto; congruence. +Qed. + +Add Relation N.t N.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 N.eq ==> N.eq as NZsucc_wd. +Proof. +unfold N.eq; intros; rewrite 2 N.spec_succ; f_equal; auto. +Qed. + +Add Morphism NZpred with signature N.eq ==> N.eq as NZpred_wd. +Proof. +unfold N.eq; intros. +generalize (N.spec_pos y) (N.spec_pos x) (N.spec_eq_bool x 0). +destruct N.eq_bool; rewrite N.spec_0; intros. +rewrite 2 N.spec_pred0; congruence. +rewrite 2 N.spec_pred; f_equal; auto; try omega. +Qed. + +Add Morphism NZplus with signature N.eq ==> N.eq ==> N.eq as NZplus_wd. +Proof. +unfold N.eq; intros; rewrite 2 N.spec_add; f_equal; auto. +Qed. + +Add Morphism NZminus with signature N.eq ==> N.eq ==> N.eq as NZminus_wd. +Proof. +unfold N.eq; intros x x' Hx y y' Hy. +destruct (Z_lt_le_dec [x] [y]). +rewrite 2 N.spec_sub0; f_equal; congruence. +rewrite 2 N.spec_sub; f_equal; congruence. +Qed. + +Add Morphism NZtimes with signature N.eq ==> N.eq ==> N.eq as NZtimes_wd. +Proof. +unfold N.eq; intros; rewrite 2 N.spec_mul; f_equal; auto. +Qed. + +Theorem NZpred_succ : forall n, N.pred (N.succ n) == n. +Proof. +unfold N.eq; intros. +rewrite N.spec_pred; rewrite N.spec_succ. +omega. +generalize (N.spec_pos n); omega. +Qed. + +Definition N_of_Z z := N.of_N (Zabs_N z). + +Section Induction. + +Variable A : N.t -> Prop. +Hypothesis A_wd : predicate_wd N.eq A. +Hypothesis A0 : A 0. +Hypothesis AS : forall n, A n <-> A (N.succ n). + +Add Morphism A with signature N.eq ==> iff as A_morph. +Proof. apply A_wd. Qed. + +Let B (z : Z) := A (N_of_Z z). + +Lemma B0 : B 0. +Proof. +unfold B, N_of_Z; simpl. +rewrite <- (A_wd 0); auto. +red; rewrite N.spec_0, N.spec_of_N; auto. +Qed. + +Lemma BS : forall z : Z, (0 <= z)%Z -> B z -> B (z + 1). +Proof. +intros z H1 H2. +unfold B in *. apply -> AS in H2. +setoid_replace (N_of_Z (z + 1)) with (N.succ (N_of_Z z)); auto. +unfold N.eq. rewrite N.spec_succ. +unfold N_of_Z. +rewrite 2 N.spec_of_N, 2 Z_of_N_abs, 2 Zabs_eq; auto with zarith. +Qed. + +Lemma B_holds : forall z : Z, (0 <= z)%Z -> B z. +Proof. +exact (natlike_ind B B0 BS). +Qed. + +Theorem NZinduction : forall n, A n. +Proof. +intro n. setoid_replace n with (N_of_Z (N.to_Z n)). +apply B_holds. apply N.spec_pos. +red; unfold N_of_Z. +rewrite N.spec_of_N, Z_of_N_abs, Zabs_eq; auto. +apply N.spec_pos. +Qed. + +End Induction. + +Theorem NZplus_0_l : forall n, 0 + n == n. +Proof. +intros; red; rewrite N.spec_add, N.spec_0; auto with zarith. +Qed. + +Theorem NZplus_succ_l : forall n m, (N.succ n) + m == N.succ (n + m). +Proof. +intros; red; rewrite N.spec_add, 2 N.spec_succ, N.spec_add; auto with zarith. +Qed. + +Theorem NZminus_0_r : forall n, n - 0 == n. +Proof. +intros; red; rewrite N.spec_sub; rewrite N.spec_0; auto with zarith. +apply N.spec_pos. +Qed. + +Theorem NZminus_succ_r : forall n m, n - (N.succ m) == N.pred (n - m). +Proof. +intros; red. +destruct (Z_lt_le_dec [n] [N.succ m]) as [H|H]. +rewrite N.spec_sub0; auto. +rewrite N.spec_succ in H. +rewrite N.spec_pred0; auto. +destruct (Z_eq_dec [n] [m]). +rewrite N.spec_sub; auto with zarith. +rewrite N.spec_sub0; auto with zarith. + +rewrite N.spec_sub, N.spec_succ in *; auto. +rewrite N.spec_pred, N.spec_sub; auto with zarith. +rewrite N.spec_sub; auto with zarith. +Qed. + +Theorem NZtimes_0_l : forall n, 0 * n == 0. +Proof. +intros; red. +rewrite N.spec_mul, N.spec_0; auto with zarith. +Qed. + +Theorem NZtimes_succ_l : forall n m, (N.succ n) * m == n * m + m. +Proof. +intros; red. +rewrite N.spec_add, 2 N.spec_mul, N.spec_succ; ring. +Qed. + +End NZAxiomsMod. + +Definition NZlt := N.lt. +Definition NZle := N.le. +Definition NZmin := N.min. +Definition NZmax := N.max. + +Infix "<=" := N.le : IntScope. +Infix "<" := N.lt : IntScope. + +Lemma spec_compare_alt : forall x y, N.compare x y = ([x] ?= [y])%Z. +Proof. + intros; generalize (N.spec_compare x y). + destruct (N.compare x y); auto. + intros H; rewrite H; symmetry; apply Zcompare_refl. +Qed. + +Lemma spec_lt : forall x y, (x<y) <-> ([x]<[y])%Z. +Proof. + intros; unfold N.lt, Zlt; rewrite spec_compare_alt; intuition. +Qed. + +Lemma spec_le : forall x y, (x<=y) <-> ([x]<=[y])%Z. +Proof. + intros; unfold N.le, Zle; rewrite spec_compare_alt; intuition. +Qed. + +Lemma spec_min : forall x y, [N.min x y] = Zmin [x] [y]. +Proof. + intros; unfold N.min, Zmin. + rewrite spec_compare_alt; destruct Zcompare; auto. +Qed. + +Lemma spec_max : forall x y, [N.max x y] = Zmax [x] [y]. +Proof. + intros; unfold N.max, Zmax. + rewrite spec_compare_alt; destruct Zcompare; auto. +Qed. + +Add Morphism N.compare with signature N.eq ==> N.eq ==> (@eq comparison) as compare_wd. +Proof. +intros x x' Hx y y' Hy. +rewrite 2 spec_compare_alt; rewrite Hx, Hy; intuition. +Qed. + +Add Morphism N.lt with signature N.eq ==> N.eq ==> iff as NZlt_wd. +Proof. +intros x x' Hx y y' Hy; unfold N.lt; rewrite Hx, Hy; intuition. +Qed. + +Add Morphism N.le with signature N.eq ==> N.eq ==> iff as NZle_wd. +Proof. +intros x x' Hx y y' Hy; unfold N.le; rewrite Hx, Hy; intuition. +Qed. + +Add Morphism N.min with signature N.eq ==> N.eq ==> N.eq as NZmin_wd. +Proof. +intros; red; rewrite 2 spec_min; congruence. +Qed. + +Add Morphism N.max with signature N.eq ==> N.eq ==> N.eq as NZmax_wd. +Proof. +intros; red; rewrite 2 spec_max; congruence. +Qed. + +Theorem NZlt_eq_cases : forall n m, n <= m <-> n < m \/ n == m. +Proof. +intros. +unfold N.eq; rewrite spec_lt, spec_le; omega. +Qed. + +Theorem NZlt_irrefl : forall n, ~ n < n. +Proof. +intros; rewrite spec_lt; auto with zarith. +Qed. + +Theorem NZlt_succ_r : forall n m, n < (N.succ m) <-> n <= m. +Proof. +intros; rewrite spec_lt, spec_le, N.spec_succ; omega. +Qed. + +Theorem NZmin_l : forall n m, n <= m -> N.min n m == n. +Proof. +intros n m; unfold N.eq; rewrite spec_le, spec_min. +generalize (Zmin_spec [n] [m]); omega. +Qed. + +Theorem NZmin_r : forall n m, m <= n -> N.min n m == m. +Proof. +intros n m; unfold N.eq; rewrite spec_le, spec_min. +generalize (Zmin_spec [n] [m]); omega. +Qed. + +Theorem NZmax_l : forall n m, m <= n -> N.max n m == n. +Proof. +intros n m; unfold N.eq; rewrite spec_le, spec_max. +generalize (Zmax_spec [n] [m]); omega. +Qed. + +Theorem NZmax_r : forall n m, n <= m -> N.max n m == m. +Proof. +intros n m; unfold N.eq; rewrite spec_le, spec_max. +generalize (Zmax_spec [n] [m]); omega. +Qed. + +End NZOrdAxiomsMod. + +Theorem pred_0 : N.pred 0 == 0. +Proof. +red; rewrite N.spec_pred0; rewrite N.spec_0; auto. +Qed. + +Definition recursion (A : Type) (a : A) (f : N.t -> A -> A) (n : N.t) := + Nrect (fun _ => A) a (fun n a => f (N.of_N n) a) (N.to_N n). +Implicit Arguments recursion [A]. + +Theorem recursion_wd : +forall (A : Type) (Aeq : relation A), + forall a a' : A, Aeq a a' -> + forall f f' : N.t -> A -> A, fun2_eq N.eq Aeq Aeq f f' -> + forall x x' : N.t, x == x' -> + Aeq (recursion a f x) (recursion a' f' x'). +Proof. +unfold fun2_wd, N.eq, fun2_eq. +intros A Aeq a a' Eaa' f f' Eff' x x' Exx'. +unfold recursion. +unfold N.to_N. +rewrite <- Exx'; clear x' Exx'. +replace (Zabs_N [x]) with (N_of_nat (Zabs_nat [x])). +induction (Zabs_nat [x]). +simpl; auto. +rewrite N_of_S, 2 Nrect_step; auto. +destruct [x]; simpl; auto. +change (nat_of_P p) with (nat_of_N (Npos p)); apply N_of_nat_of_N. +change (nat_of_P p) with (nat_of_N (Npos p)); apply N_of_nat_of_N. +Qed. + +Theorem recursion_0 : + forall (A : Type) (a : A) (f : N.t -> A -> A), recursion a f 0 = a. +Proof. +intros A a f; unfold recursion, N.to_N; rewrite N.spec_0; simpl; auto. +Qed. + +Theorem recursion_succ : + forall (A : Type) (Aeq : relation A) (a : A) (f : N.t -> A -> A), + Aeq a a -> fun2_wd N.eq Aeq Aeq f -> + forall n, Aeq (recursion a f (N.succ n)) (f n (recursion a f n)). +Proof. +unfold N.eq, recursion, fun2_wd; intros A Aeq a f EAaa f_wd n. +replace (N.to_N (N.succ n)) with (Nsucc (N.to_N n)). +rewrite Nrect_step. +apply f_wd; auto. +unfold N.to_N. +rewrite N.spec_of_N, Z_of_N_abs, Zabs_eq; auto. + apply N.spec_pos. + +fold (recursion a f n). +apply recursion_wd; auto. +red; auto. +red; auto. +unfold N.to_N. + +rewrite N.spec_succ. +change ([n]+1)%Z with (Zsucc [n]). +apply Z_of_N_eq_rev. +rewrite Z_of_N_succ. +rewrite 2 Z_of_N_abs. +rewrite 2 Zabs_eq; auto. +generalize (N.spec_pos n); auto with zarith. +apply N.spec_pos; auto. +Qed. + +End NSig_NAxioms. diff --git a/theories/Numbers/Rational/BigQ/Q0Make.v b/theories/Numbers/Rational/BigQ/Q0Make.v index 4260c954f3..d84efab23c 100644 --- a/theories/Numbers/Rational/BigQ/Q0Make.v +++ b/theories/Numbers/Rational/BigQ/Q0Make.v @@ -24,6 +24,10 @@ Require Import QMake_base. Module Q0. + Import BinInt Zorder. + Open Local Scope Q_scope. + Open Local Scope Qc_scope. + (** The notation of a rational number is either an integer x, interpreted as itself or a pair (x,y) of an integer x and a naturel number y interpreted as x/y. The pairs (x,0) and (0,y) are all diff --git a/theories/Numbers/Rational/BigQ/QbiMake.v b/theories/Numbers/Rational/BigQ/QbiMake.v index 8ce671a73e..e105b36fc3 100644 --- a/theories/Numbers/Rational/BigQ/QbiMake.v +++ b/theories/Numbers/Rational/BigQ/QbiMake.v @@ -24,6 +24,10 @@ Require Import QMake_base. Module Qbi. + Import BinInt Zorder. + Open Local Scope Q_scope. + Open Local Scope Qc_scope. + (** The notation of a rational number is either an integer x, interpreted as itself or a pair (x,y) of an integer x and a naturel number y interpreted as x/y. The pairs (x,0) and (0,y) are all diff --git a/theories/Numbers/Rational/BigQ/QifMake.v b/theories/Numbers/Rational/BigQ/QifMake.v index 436c137585..1c8caa657f 100644 --- a/theories/Numbers/Rational/BigQ/QifMake.v +++ b/theories/Numbers/Rational/BigQ/QifMake.v @@ -24,6 +24,10 @@ Require Import QMake_base. Module Qif. + Import BinInt. + Open Local Scope Q_scope. + Open Local Scope Qc_scope. + (** The notation of a rational number is either an integer x, interpreted as itself or a pair (x,y) of an integer x and a naturel number y interpreted as x/y. The pairs (x,0) and (0,y) are all diff --git a/theories/Numbers/Rational/BigQ/QpMake.v b/theories/Numbers/Rational/BigQ/QpMake.v index db6c5926fe..b9199357ea 100644 --- a/theories/Numbers/Rational/BigQ/QpMake.v +++ b/theories/Numbers/Rational/BigQ/QpMake.v @@ -22,6 +22,9 @@ Require Import Qcanon. Require Import Qpower. Require Import QMake_base. +Notation Nspec_lt := BigNAxiomsMod.NZOrdAxiomsMod.spec_lt. +Notation Nspec_le := BigNAxiomsMod.NZOrdAxiomsMod.spec_le. + Module Qp. (** The notation of a rational number is either an integer x, @@ -186,20 +189,20 @@ Module Qp. rewrite BigZ.spec_div; simpl; rewrite BigN.spec_gcd; auto with zarith. rewrite BigN.spec_div; simpl; rewrite BigN.spec_gcd; auto with zarith. rewrite Zmult_1_r. - rewrite BigN.succ_pred; auto with zarith. + rewrite BigN.succ_pred by (rewrite Nspec_lt, BigN.spec_0; auto). rewrite Z2P_correct; auto with zarith. rewrite spec_to_N; intros; rewrite Zgcd_div_swap; auto. rewrite H; ring. intros H3. red; simpl. rewrite BigZ.spec_div; simpl; rewrite BigN.spec_gcd; auto with zarith. - rewrite BigN.succ_pred; auto with zarith. + rewrite BigN.succ_pred by (rewrite Nspec_lt, BigN.spec_0; auto). assert (F: (0 < BigN.to_Z (q / BigN.gcd (BigZ.to_N p) q)%bigN)%Z). rewrite BigN.spec_div; auto with zarith. rewrite BigN.spec_gcd. apply Zgcd_div_pos; auto. rewrite BigN.spec_gcd; auto. - rewrite BigN.succ_pred; auto with zarith. + rewrite BigN.succ_pred by (rewrite Nspec_lt, BigN.spec_0; auto). rewrite Z2P_correct; auto. rewrite Z2P_correct; auto. rewrite BigN.spec_div; simpl; rewrite BigN.spec_gcd; auto with zarith. @@ -315,7 +318,7 @@ Module Qp. simpl. repeat rewrite BigZ.spec_add. repeat rewrite BigZ.spec_mul; simpl. - rewrite BigN.succ_pred; try apply Qeq_refl; apply spec_succ_pos. + rewrite BigN.succ_pred; try apply Qeq_refl; apply lt_0_succ. intros p1 n p2. match goal with |- [norm ?X ?Y] == _ => apply Qeq_trans with ([Qq X (BigN.pred Y)]); @@ -325,8 +328,8 @@ Module Qp. simpl. repeat rewrite BigZ.spec_add. repeat rewrite BigZ.spec_mul; simpl. - rewrite Zplus_comm. - rewrite BigN.succ_pred; try apply Qeq_refl; apply spec_succ_pos. + rewrite BinInt.Zplus_comm. + rewrite BigN.succ_pred; try apply Qeq_refl; apply lt_0_succ. intros p1 q1 p2 q2. match goal with |- [norm ?X ?Y] == _ => apply Qeq_trans with ([Qq X (BigN.pred Y)]); @@ -391,12 +394,13 @@ Module Qp. apply Qeq_refl; auto. assert (F1:= spec_succ_pos dx). assert (F2:= spec_succ_pos dy). - rewrite BigN.succ_pred; rewrite BigN.spec_mul. - rewrite BigZ.spec_mul. + rewrite BigN.succ_pred. + rewrite BigN.spec_mul; rewrite BigZ.spec_mul. assert (tmp: (forall a b, 0 < a -> 0 < b -> Z2P (a * b) = (Z2P a * Z2P b)%positive)%Z). intros [|a|a] [|b|b]; simpl; auto; intros; apply False_ind; auto with zarith. rewrite tmp; auto; apply Qeq_refl. + rewrite Nspec_lt, BigN.spec_0, BigN.spec_mul; auto. apply Zmult_lt_0_compat; apply spec_succ_pos. Qed. @@ -496,6 +500,7 @@ Module Qp. rewrite (Zmult_comm (BigZ.to_Z p1)). repeat rewrite Zmult_assoc. rewrite Zgcd_div_swap; auto; try ring. + rewrite Nspec_lt, BigN.spec_0; auto. apply False_ind; generalize F1. rewrite (Zdivide_Zdiv_eq (Zgcd (BigN.to_Z (BigZ.to_N p2)) (BigN.to_Z (BigN.succ n))) @@ -556,6 +561,7 @@ Module Qp. rewrite (Zmult_comm (BigZ.to_Z p2)). repeat rewrite Zmult_assoc. rewrite Zgcd_div_swap; auto; try ring. + rewrite Nspec_lt, BigN.spec_0; auto. apply False_ind; generalize F1. rewrite (Zdivide_Zdiv_eq (Zgcd (BigN.to_Z (BigZ.to_N p1)) (BigN.to_Z (BigN.succ n))) @@ -609,7 +615,7 @@ Module Qp. assert (F: (0 < BigN.to_Z x)%Z). case (Zle_lt_or_eq _ _ (BigN.spec_pos x)); auto with zarith. unfold to_Q; rewrite BigZ.spec_1. - rewrite BigN.succ_pred; auto. + rewrite BigN.succ_pred by (rewrite Nspec_lt, BigN.spec_0; auto). red; unfold Qinv; simpl. generalize F; case BigN.to_Z; auto with zarith. intros p Hp; discriminate Hp. @@ -621,7 +627,7 @@ Module Qp. assert (F: (0 < BigN.to_Z x)%Z). case (Zle_lt_or_eq _ _ (BigN.spec_pos x)); auto with zarith. red; unfold Qinv; simpl. - rewrite BigN.succ_pred; auto. + rewrite BigN.succ_pred by (rewrite Nspec_lt, BigN.spec_0; auto). generalize F; case BigN.to_Z; simpl; auto with zarith. intros p Hp; discriminate Hp. match goal with |- context[BigN.eq_bool ?X ?Y] => @@ -632,7 +638,7 @@ Module Qp. assert (F: (0 < BigN.to_Z nx)%Z). case (Zle_lt_or_eq _ _ (BigN.spec_pos nx)); auto with zarith. red; unfold Qinv; simpl. - rewrite BigN.succ_pred; auto. + rewrite BigN.succ_pred by (rewrite Nspec_lt, BigN.spec_0; auto). rewrite BigN.spec_succ; rewrite Z2P_correct; auto with zarith. generalize F; case BigN.to_Z; auto with zarith. intros p Hp; discriminate Hp. @@ -645,12 +651,12 @@ Module Qp. assert (F: (0 < BigN.to_Z nx)%Z). case (Zle_lt_or_eq _ _ (BigN.spec_pos nx)); auto with zarith. red; unfold Qinv; simpl. - rewrite BigN.succ_pred; auto. + rewrite BigN.succ_pred by (rewrite Nspec_lt, BigN.spec_0; auto). rewrite BigN.spec_succ; rewrite Z2P_correct; auto with zarith. generalize F; case BigN.to_Z; auto with zarith. - simpl; intros. + simpl; intros. match goal with |- (?X = Zneg ?Y)%Z => - replace (Zneg Y) with (Zopp (Zpos Y)); + replace (Zneg Y) with (-(Zpos Y))%Z; try rewrite Z2P_correct; auto with zarith end. rewrite Zpos_mult_morphism; @@ -704,7 +710,7 @@ Definition inv_norm x := generalize (BigN.spec_eq_bool X Y); case BigN.eq_bool end; rewrite BigN.spec_1; intros H1. red; simpl. - rewrite BigN.succ_pred; auto. + rewrite BigN.succ_pred by (rewrite Nspec_lt, BigN.spec_0; auto). rewrite Z2P_correct; try rewrite H1; auto with zarith. apply Qeq_refl. match goal with |- context[BigN.eq_bool ?X ?Y] => @@ -717,7 +723,7 @@ Definition inv_norm x := generalize (BigN.spec_eq_bool X Y); case BigN.eq_bool end; rewrite BigN.spec_1; intros H1. red; simpl. - rewrite BigN.succ_pred; auto. + rewrite BigN.succ_pred by (rewrite Nspec_lt, BigN.spec_0; auto). rewrite Z2P_correct; try rewrite H1; auto with zarith. apply Qeq_refl. case nx; clear nx; intros nx. @@ -730,6 +736,7 @@ Definition inv_norm x := end; rewrite BigN.spec_1; intros H1. red; simpl. rewrite BigN.succ_pred; try rewrite H1; auto with zarith. + rewrite Nspec_lt, BigN.spec_0, H1; auto with zarith. apply Qeq_refl. match goal with |- context[BigN.eq_bool ?X ?Y] => generalize (BigN.spec_eq_bool X Y); case BigN.eq_bool @@ -740,6 +747,7 @@ Definition inv_norm x := end; rewrite BigN.spec_1; intros H1. red; simpl. rewrite BigN.succ_pred; try rewrite H1; auto with zarith. + rewrite Nspec_lt, BigN.spec_0, H1; auto with zarith. apply Qeq_refl. Qed. @@ -791,7 +799,7 @@ Definition inv_norm x := assert (F1 : (0 < BigN.to_Z (BigN.square (BigN.succ dx)))%Z). rewrite BigN.spec_square; apply Zmult_lt_0_compat; auto with zarith. - rewrite BigN.succ_pred; auto. + rewrite BigN.succ_pred by (rewrite Nspec_lt, BigN.spec_0; auto). rewrite Zpos_mult_morphism. repeat rewrite Z2P_correct; auto with zarith. repeat rewrite BigN.spec_succ; auto with zarith. @@ -837,7 +845,7 @@ Definition inv_norm x := assert (F2: (0 < BigN.to_Z (BigN.succ dx) ^ ' p)%Z). unfold Zpower; apply Zpower_pos_pos; auto. unfold power_pos; red; simpl. - rewrite BigN.succ_pred; rewrite BigN.spec_power_pos; auto. + rewrite BigN.succ_pred, BigN.spec_power_pos. rewrite Z2P_correct; auto. generalize (Qpower_decomp p (BigZ.to_Z nx) (Z2P (BigN.to_Z (BigN.succ dx)))). @@ -846,6 +854,7 @@ Definition inv_norm x := unfold Qeq; simpl; intros HH. rewrite HH. rewrite BigZ.spec_power_pos; simpl; ring. + rewrite Nspec_lt, BigN.spec_0, BigN.spec_power_pos; auto. Qed. Theorem spec_power_posc x p: [[power_pos x p]] = [[x]] ^ nat_of_P p. diff --git a/theories/Numbers/Rational/BigQ/QvMake.v b/theories/Numbers/Rational/BigQ/QvMake.v index 59da4da6df..3f51e70639 100644 --- a/theories/Numbers/Rational/BigQ/QvMake.v +++ b/theories/Numbers/Rational/BigQ/QvMake.v @@ -24,6 +24,10 @@ Require Import QMake_base. Module Qv. + Import BinInt Zorder. + Open Local Scope Q_scope. + Open Local Scope Qc_scope. + (** The notation of a rational number is either an integer x, interpreted as itself or a pair (x,y) of an integer x and a naturel number y interpreted as x/y. All functions maintain the invariant |