diff options
34 files changed, 232 insertions, 298 deletions
diff --git a/theories/Numbers/Cyclic/Abstract/NZCyclic.v b/theories/Numbers/Cyclic/Abstract/NZCyclic.v index e3c14879d..517e48ad9 100644 --- a/theories/Numbers/Cyclic/Abstract/NZCyclic.v +++ b/theories/Numbers/Cyclic/Abstract/NZCyclic.v @@ -43,17 +43,13 @@ Definition add := w_op.(znz_add). Definition sub := w_op.(znz_sub). Definition mul := w_op.(znz_mul). -Delimit Scope NumScope with Num. -Bind Scope NumScope with t. -Local Open Scope NumScope. -Notation "x == y" := (eq x y) (at level 70) : NumScope. -Notation "0" := zero : NumScope. -Notation S := succ. -Notation P := pred. -Notation "x + y" := (add x y) : NumScope. -Notation "x - y" := (sub x y) : NumScope. -Notation "x * y" := (mul x y) : NumScope. - +Local Infix "==" := eq (at level 70). +Local Notation "0" := zero. +Local Notation S := succ. +Local Notation P := pred. +Local Infix "+" := add. +Local Infix "-" := sub. +Local Infix "*" := mul. Hint Rewrite w_spec.(spec_0) w_spec.(spec_succ) w_spec.(spec_pred) w_spec.(spec_add) w_spec.(spec_mul) w_spec.(spec_sub) : w. @@ -129,7 +125,7 @@ rewrite <- pred_mod_wB. replace ([| n |] + 1 - 1)%Z with [| n |] by auto with zarith. apply NZ_to_Z_mod. Qed. -Lemma Z_to_NZ_0 : Z_to_NZ 0%Z == 0%Num. +Lemma Z_to_NZ_0 : Z_to_NZ 0%Z == 0. Proof. unfold NZ_to_Z, Z_to_NZ. wsimpl. rewrite znz_of_Z_correct; auto. diff --git a/theories/Numbers/Integer/Abstract/ZAdd.v b/theories/Numbers/Integer/Abstract/ZAdd.v index 26ba0a8d4..5663408d1 100644 --- a/theories/Numbers/Integer/Abstract/ZAdd.v +++ b/theories/Numbers/Integer/Abstract/ZAdd.v @@ -12,9 +12,8 @@ Require Export ZBase. -Module ZAddPropFunct (Import Z : ZAxiomsSig). +Module ZAddPropFunct (Import Z : ZAxiomsSig'). Include ZBasePropFunct Z. -Local Open Scope NumScope. (** Theorems that are either not valid on N or have different proofs on N and Z *) diff --git a/theories/Numbers/Integer/Abstract/ZAddOrder.v b/theories/Numbers/Integer/Abstract/ZAddOrder.v index 282709c47..de12993f8 100644 --- a/theories/Numbers/Integer/Abstract/ZAddOrder.v +++ b/theories/Numbers/Integer/Abstract/ZAddOrder.v @@ -12,9 +12,8 @@ Require Export ZLt. -Module ZAddOrderPropFunct (Import Z : ZAxiomsSig). +Module ZAddOrderPropFunct (Import Z : ZAxiomsSig'). Include ZOrderPropFunct Z. -Local Open Scope NumScope. (** Theorems that are either not valid on N or have different proofs on N and Z *) diff --git a/theories/Numbers/Integer/Abstract/ZAxioms.v b/theories/Numbers/Integer/Abstract/ZAxioms.v index 4b3d18be4..9158a214d 100644 --- a/theories/Numbers/Integer/Abstract/ZAxioms.v +++ b/theories/Numbers/Integer/Abstract/ZAxioms.v @@ -14,22 +14,25 @@ Require Export NZAxioms. Set Implicit Arguments. -Module Type ZAxiomsSig. -Include Type NZOrdAxiomsSig. -Local Open Scope NumScope. +Module Type Opp (Import T:Typ). + Parameter Inline opp : t -> t. +End Opp. -Parameter Inline opp : t -> t. -Declare Instance opp_wd : Proper (eq==>eq) opp. +Module Type OppNotation (T:Typ)(Import O : Opp T). + Notation "- x" := (opp x) (at level 35, right associativity). +End OppNotation. -Notation "- x" := (opp x) (at level 35, right associativity) : NumScope. -Notation "- 1" := (- (1)) : NumScope. +Module Type Opp' (T:Typ) := Opp T <+ OppNotation T. -(* Integers are obtained by postulating that every number has a predecessor *) +(** We obtain integers by postulating that every number has a predecessor. *) -Axiom succ_pred : forall n, S (P n) == n. +Module Type IsOpp (Import Z : NZAxiomsSig')(Import O : Opp' Z). + Declare Instance opp_wd : Proper (eq==>eq) opp. + Axiom succ_pred : forall n, S (P n) == n. + Axiom opp_0 : - 0 == 0. + Axiom opp_succ : forall n, - (S n) == P (- n). +End IsOpp. -Axiom opp_0 : - 0 == 0. -Axiom opp_succ : forall n, - (S n) == P (- n). - -End ZAxiomsSig. +Module Type ZAxiomsSig := NZOrdAxiomsSig <+ Opp <+ IsOpp. +Module Type ZAxiomsSig' := NZOrdAxiomsSig' <+ Opp' <+ IsOpp. diff --git a/theories/Numbers/Integer/Abstract/ZBase.v b/theories/Numbers/Integer/Abstract/ZBase.v index 64a122c71..9b5a80762 100644 --- a/theories/Numbers/Integer/Abstract/ZBase.v +++ b/theories/Numbers/Integer/Abstract/ZBase.v @@ -14,9 +14,8 @@ Require Export Decidable. Require Export ZAxioms. Require Import NZProperties. -Module ZBasePropFunct (Import Z : ZAxiomsSig). +Module ZBasePropFunct (Import Z : ZAxiomsSig'). Include Type NZPropFunct Z. -Local Open Scope NumScope. (* Theorems that are true for integers but not for natural numbers *) diff --git a/theories/Numbers/Integer/Abstract/ZDivEucl.v b/theories/Numbers/Integer/Abstract/ZDivEucl.v index 914055654..ba79ae24b 100644 --- a/theories/Numbers/Integer/Abstract/ZDivEucl.v +++ b/theories/Numbers/Integer/Abstract/ZDivEucl.v @@ -23,17 +23,18 @@ Require Import ZAxioms ZProperties NZDiv. -Open Scope NumScope. - -Module Type ZDiv (Import Z : ZAxiomsSig). - Include Type NZDivCommon Z. (** div, mod, compat with eq, equation a=bq+r *) +Module Type ZDivSpecific (Import Z : ZAxiomsSig')(Import DM : DivMod' Z). Definition abs z := max z (-z). Axiom mod_always_pos : forall a b, 0 <= a mod b < abs b. -End ZDiv. +End ZDivSpecific. + +Module Type ZDiv (Z:ZAxiomsSig) + := DivMod Z <+ NZDivCommon Z <+ ZDivSpecific Z. Module Type ZDivSig := ZAxiomsSig <+ ZDiv. +Module Type ZDivSig' := ZAxiomsSig' <+ ZDiv <+ DivModNotation. -Module ZDivPropFunct (Import Z : ZDivSig)(Import ZP : ZPropSig Z). +Module ZDivPropFunct (Import Z : ZDivSig')(Import ZP : ZPropSig Z). (** We benefit from what already exists for NZ *) @@ -159,7 +160,7 @@ Qed. Parameter sign : t -> t. Parameter sign_pos : forall t, sign t == 1 <-> 0<t. Parameter sign_0 : forall t, sign t == 0 <-> t==0. -Parameter sign_neg : forall t, sign t == -1 <-> t<0. +Parameter sign_neg : forall t, sign t == -(1) <-> t<0. Parameter sign_abs : forall t, t * sign t == abs t. (** END TODO *) diff --git a/theories/Numbers/Integer/Abstract/ZDivFloor.v b/theories/Numbers/Integer/Abstract/ZDivFloor.v index 611432a6d..99df15f23 100644 --- a/theories/Numbers/Integer/Abstract/ZDivFloor.v +++ b/theories/Numbers/Integer/Abstract/ZDivFloor.v @@ -26,17 +26,18 @@ Require Import ZAxioms ZProperties NZDiv. -Open Scope NumScope. - -Module Type ZDiv (Import Z : ZAxiomsSig). - Include Type NZDivCommon Z. (** div, mod, compat with eq, equation a=bq+r *) +Module Type ZDivSpecific (Import Z:ZAxiomsSig')(Import DM : DivMod' Z). Axiom mod_pos_bound : forall a b, 0 < b -> 0 <= a mod b < b. Axiom mod_neg_bound : forall a b, b < 0 -> b < a mod b <= 0. -End ZDiv. +End ZDivSpecific. + +Module Type ZDiv (Z:ZAxiomsSig) + := DivMod Z <+ NZDivCommon Z <+ ZDivSpecific Z. Module Type ZDivSig := ZAxiomsSig <+ ZDiv. +Module Type ZDivSig' := ZAxiomsSig' <+ ZDiv <+ DivModNotation. -Module ZDivPropFunct (Import Z : ZDivSig)(Import ZP : ZPropSig Z). +Module ZDivPropFunct (Import Z : ZDivSig')(Import ZP : ZPropSig Z). (** We benefit from what already exists for NZ *) diff --git a/theories/Numbers/Integer/Abstract/ZDivTrunc.v b/theories/Numbers/Integer/Abstract/ZDivTrunc.v index c60bf7c6a..0468b3bf5 100644 --- a/theories/Numbers/Integer/Abstract/ZDivTrunc.v +++ b/theories/Numbers/Integer/Abstract/ZDivTrunc.v @@ -26,18 +26,19 @@ Require Import ZAxioms ZProperties NZDiv. -Open Scope NumScope. - -Module Type ZDiv (Import Z : ZAxiomsSig). - Include Type NZDivCommon Z. (** div, mod, compat with eq, equation a=bq+r *) +Module Type ZDivSpecific (Import Z:ZAxiomsSig')(Import DM : DivMod' Z). Axiom mod_bound : forall a b, 0<=a -> 0<b -> 0 <= a mod b < b. Axiom mod_opp_l : forall a b, b ~= 0 -> (-a) mod b == - (a mod b). Axiom mod_opp_r : forall a b, b ~= 0 -> a mod (-b) == a mod b. -End ZDiv. +End ZDivSpecific. + +Module Type ZDiv (Z:ZAxiomsSig) + := DivMod Z <+ NZDivCommon Z <+ ZDivSpecific Z. Module Type ZDivSig := ZAxiomsSig <+ ZDiv. +Module Type ZDivSig' := ZAxiomsSig' <+ ZDiv <+ DivModNotation. -Module ZDivPropFunct (Import Z : ZDivSig)(Import ZP : ZPropSig Z). +Module ZDivPropFunct (Import Z : ZDivSig')(Import ZP : ZPropSig Z). (** We benefit from what already exists for NZ *) diff --git a/theories/Numbers/Integer/Abstract/ZLt.v b/theories/Numbers/Integer/Abstract/ZLt.v index e77f9c453..849bf6b40 100644 --- a/theories/Numbers/Integer/Abstract/ZLt.v +++ b/theories/Numbers/Integer/Abstract/ZLt.v @@ -12,9 +12,8 @@ Require Export ZMul. -Module ZOrderPropFunct (Import Z : ZAxiomsSig). +Module ZOrderPropFunct (Import Z : ZAxiomsSig'). Include ZMulPropFunct Z. -Local Open Scope NumScope. (** Instances of earlier theorems for m == 0 *) @@ -124,10 +123,10 @@ Proof. intro; apply lt_neq; apply lt_pred_l. Qed. -Theorem lt_n1_r : forall n m, n < m -> m < 0 -> n < -1. +Theorem lt_n1_r : forall n m, n < m -> m < 0 -> n < -(1). Proof. intros n m H1 H2. apply -> lt_le_pred in H2. -setoid_replace (P 0) with (-1) in H2. now apply lt_le_trans with m. +setoid_replace (P 0) with (-(1)) in H2. now apply lt_le_trans with m. apply <- eq_opp_r. now rewrite opp_pred, opp_0. Qed. diff --git a/theories/Numbers/Integer/Abstract/ZMul.v b/theories/Numbers/Integer/Abstract/ZMul.v index 4be2ac887..84d840ad2 100644 --- a/theories/Numbers/Integer/Abstract/ZMul.v +++ b/theories/Numbers/Integer/Abstract/ZMul.v @@ -12,9 +12,8 @@ Require Export ZAdd. -Module ZMulPropFunct (Import Z : ZAxiomsSig). +Module ZMulPropFunct (Import Z : ZAxiomsSig'). Include ZAddPropFunct Z. -Local Open Scope NumScope. (** A note on naming: right (correspondingly, left) distributivity happens when the sum is multiplied by a number on the right diff --git a/theories/Numbers/Integer/Abstract/ZMulOrder.v b/theories/Numbers/Integer/Abstract/ZMulOrder.v index bd9a85714..99be58ebd 100644 --- a/theories/Numbers/Integer/Abstract/ZMulOrder.v +++ b/theories/Numbers/Integer/Abstract/ZMulOrder.v @@ -12,9 +12,10 @@ Require Export ZAddOrder. -Module Type ZMulOrderPropFunct (Import Z : ZAxiomsSig). +Module Type ZMulOrderPropFunct (Import Z : ZAxiomsSig'). Include ZAddOrderPropFunct Z. -Local Open Scope NumScope. + +Local Notation "- 1" := (-(1)). Theorem mul_lt_mono_nonpos : forall n m p q, m <= 0 -> n < m -> q <= 0 -> p < q -> m * q < n * p. diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v index 0956f337f..8b5624cdf 100644 --- a/theories/Numbers/Integer/NatPairs/ZNatPairs.v +++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.v @@ -21,7 +21,18 @@ Open Local Scope pair_scope. Module ZPairsAxiomsMod (Import N : NAxiomsSig) <: ZAxiomsSig. Module Import NPropMod := NPropFunct N. (* Get all properties of N *) -Local Open Scope NumScope. +Delimit Scope NScope with N. +Bind Scope NScope with N.t. +Infix "==" := N.eq (at level 70) : NScope. +Notation "x ~= y" := (~ N.eq x y) (at level 70) : NScope. +Notation "0" := N.zero : NScope. +Notation "1" := (N.succ N.zero) : NScope. +Infix "+" := N.add : NScope. +Infix "-" := N.sub : NScope. +Infix "*" := N.mul : NScope. +Infix "<" := N.lt : NScope. +Infix "<=" := N.le : NScope. +Local Open Scope NScope. (** The definitions of functions ([add], [mul], etc.) will be unfolded by the properties functor. Since we don't want [add_comm] to refer @@ -34,8 +45,8 @@ Module Z. Definition t := (N.t * N.t)%type. Definition zero : t := (0, 0). Definition eq (p q : t) := (p#1 + q#2 == q#1 + p#2). -Definition succ (n : t) : t := (S n#1, n#2). -Definition pred (n : t) : t := (n#1, S n#2). +Definition succ (n : t) : t := (N.succ n#1, n#2). +Definition pred (n : t) : t := (n#1, N.succ n#2). Definition opp (n : t) : t := (n#2, n#1). Definition add (n m : t) : t := (n#1 + m#1, n#2 + m#2). Definition sub (n m : t) : t := (n#1 + m#2, n#2 + m#1). @@ -58,20 +69,19 @@ Definition max (n m : t) : t := (max (n#1 + m#2) (m#1 + n#2), n#2 + m#2). End Z. -Delimit Scope IntScope with Int. -Bind Scope IntScope with Z.t. -Notation "x == y" := (Z.eq x y) (at level 70) : IntScope. -Notation "x ~= y" := (~ Z.eq x y) (at level 70) : IntScope. -Notation "0" := Z.zero : IntScope. -Notation "1" := (Z.succ Z.zero) : IntScope. -Notation "x + y" := (Z.add x y) : IntScope. -Notation "x - y" := (Z.sub x y) : IntScope. -Notation "x * y" := (Z.mul x y) : IntScope. -Notation "- x" := (Z.opp x) : IntScope. -Notation "x < y" := (Z.lt x y) : IntScope. -Notation "x <= y" := (Z.le x y) : IntScope. -Notation "x > y" := (Z.lt y x) (only parsing) : IntScope. -Notation "x >= y" := (Z.le y x) (only parsing) : IntScope. +Delimit Scope ZScope with Z. +Bind Scope ZScope with Z.t. +Infix "==" := Z.eq (at level 70) : ZScope. +Notation "x ~= y" := (~ Z.eq x y) (at level 70) : ZScope. +Notation "0" := Z.zero : ZScope. +Notation "1" := (Z.succ Z.zero) : ZScope. +Infix "+" := Z.add : ZScope. +Infix "-" := Z.sub : ZScope. +Infix "*" := Z.mul : ZScope. +Notation "- x" := (Z.opp x) : ZScope. +Infix "<" := Z.lt : ZScope. +Infix "<=" := Z.le : ZScope. +Local Open Scope ZScope. Lemma sub_add_opp : forall n m, Z.sub n m = Z.add n (Z.opp m). Proof. reflexivity. Qed. @@ -82,7 +92,7 @@ split. unfold Reflexive, Z.eq. reflexivity. unfold Symmetric, Z.eq; now symmetry. unfold Transitive, Z.eq. intros (n1,n2) (m1,m2) (p1,p2) H1 H2; simpl in *. -apply (add_cancel_r _ _ (m1+m2)). +apply (add_cancel_r _ _ (m1+m2)%N). rewrite add_shuffle2, H1, add_shuffle1, H2. now rewrite add_shuffle1, (add_comm m1). Qed. @@ -122,10 +132,10 @@ intros n1 m1 H1 n2 m2 H2. rewrite 2 sub_add_opp. apply add_wd, opp_wd; auto. Qed. -Lemma mul_comm : forall n m, (n*m == m*n)%Int. +Lemma mul_comm : forall n m, n*m == m*n. Proof. intros (n1,n2) (m1,m2); compute. -rewrite (add_comm (m1*n2)). +rewrite (add_comm (m1*n2)%N). apply N.add_wd; apply N.add_wd; apply mul_comm. Qed. @@ -133,7 +143,7 @@ Instance mul_wd : Proper (Z.eq ==> Z.eq ==> Z.eq) Z.mul. Proof. assert (forall n, Proper (Z.eq ==> Z.eq) (Z.mul n)). unfold Z.mul, Z.eq. intros (n1,n2) (p1,p2) (q1,q2) H; simpl in *. - rewrite add_shuffle1, (add_comm (n1*p1)). + rewrite add_shuffle1, (add_comm (n1*p1)%N). symmetry. rewrite add_shuffle1. rewrite <- ! mul_add_distr_l. rewrite (add_comm p2), (add_comm q2), H. @@ -152,26 +162,24 @@ Theorem bi_induction : Proof. intros A0 AS n; unfold Z.zero, Z.succ, Z.eq in *. destruct n as [n m]. -cut (forall p, A (p, 0)); [intro H1 |]. -cut (forall p, A (0, p)); [intro H2 |]. +cut (forall p, A (p, 0%N)); [intro H1 |]. +cut (forall p, A (0%N, p)); [intro H2 |]. destruct (add_dichotomy n m) as [[p H] | [p H]]. -rewrite (A_wd (n, m) (0, p)) by (rewrite add_0_l; now rewrite add_comm). +rewrite (A_wd (n, m) (0%N, p)) by (rewrite add_0_l; now rewrite add_comm). apply H2. -rewrite (A_wd (n, m) (p, 0)) by now rewrite add_0_r. apply H1. +rewrite (A_wd (n, m) (p, 0%N)) by now rewrite add_0_r. apply H1. induct p. assumption. intros p IH. -apply -> (A_wd (0, p) (1, S p)) in IH; [| now rewrite add_0_l, add_1_l]. +apply -> (A_wd (0%N, p) (1%N, N.succ p)) in IH; [| now rewrite add_0_l, add_1_l]. now apply <- AS. induct p. assumption. intros p IH. -replace 0 with (snd (p, 0)); [| reflexivity]. -replace (S p) with (S (fst (p, 0))); [| reflexivity]. now apply -> AS. +replace 0%N with (snd (p, 0%N)); [| reflexivity]. +replace (N.succ p) with (N.succ (fst (p, 0%N))); [| reflexivity]. now apply -> AS. Qed. End Induction. (* Time to prove theorems in the language of Z *) -Open Scope IntScope. - Theorem pred_succ : forall n, Z.pred (Z.succ n) == n. Proof. unfold Z.pred, Z.succ, Z.eq; intro n; simpl; now nzsimpl. @@ -221,7 +229,7 @@ Theorem mul_succ_l : forall n m, (Z.succ n) * m == n * m + m. Proof. intros (n1,n2) (m1,m2); unfold Z.mul, Z.succ, Z.eq; simpl; nzsimpl. rewrite <- (add_assoc _ m1), (add_comm m1), (add_assoc _ _ m1). -now rewrite <- (add_assoc _ m2), (add_comm m2), (add_assoc _ (n2*m1)%Num m2). +now rewrite <- (add_assoc _ m2), (add_comm m2), (add_assoc _ (n2*m1)%N m2). Qed. (** Order *) @@ -279,7 +287,7 @@ Proof. assert (forall n, Proper (Z.eq==>iff) (Z.lt n)). intros (n1,n2). apply proper_sym_impl_iff; auto with *. unfold Z.lt, Z.eq; intros (r1,r2) (s1,s2) Eq H; simpl in *. - apply le_lt_add_lt with (r1+r2)%Num (r1+r2)%Num; [apply le_refl; auto with *|]. + apply le_lt_add_lt with (r1+r2)%N (r1+r2)%N; [apply le_refl; auto with *|]. rewrite add_shuffle2, (add_comm s2), Eq. rewrite (add_comm s1 n2), (add_shuffle1 n2), (add_comm n2 r1). now rewrite <- add_lt_mono_r. diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v index f752c1976..666ce5454 100644 --- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v +++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v @@ -16,18 +16,15 @@ Require Import ZSig. Module ZSig_ZAxioms (Z:ZType) <: ZAxiomsSig. -Delimit Scope NumScope with Num. -Bind Scope NumScope with Z.t. -Local Open Scope NumScope. -Local Notation "[ x ]" := (Z.to_Z x) : NumScope. -Local Infix "==" := Z.eq (at level 70) : NumScope. -Local Notation "0" := Z.zero : NumScope. -Local Infix "+" := Z.add : NumScope. -Local Infix "-" := Z.sub : NumScope. -Local Infix "*" := Z.mul : NumScope. -Local Notation "- x" := (Z.opp x) : NumScope. -Local Infix "<=" := Z.le : NumScope. -Local Infix "<" := Z.lt : NumScope. +Local Notation "[ x ]" := (Z.to_Z x). +Local Infix "==" := Z.eq (at level 70). +Local Notation "0" := Z.zero. +Local Infix "+" := Z.add. +Local Infix "-" := Z.sub. +Local Infix "*" := Z.mul. +Local Notation "- x" := (Z.opp x). +Local Infix "<=" := Z.le. +Local Infix "<" := Z.lt. Hint Rewrite Z.spec_0 Z.spec_1 Z.spec_add Z.spec_sub Z.spec_pred Z.spec_succ diff --git a/theories/Numbers/NatInt/NZAdd.v b/theories/Numbers/NatInt/NZAdd.v index bca7c3682..9535cfdb4 100644 --- a/theories/Numbers/NatInt/NZAdd.v +++ b/theories/Numbers/NatInt/NZAdd.v @@ -10,12 +10,10 @@ (*i $Id$ i*) -Require Import NZAxioms. -Require Import NZBase. +Require Import NZAxioms NZBase. Module Type NZAddPropSig - (Import NZ : NZAxiomsSig)(Import NZBase : NZBasePropSig NZ). -Local Open Scope NumScope. + (Import NZ : NZAxiomsSig')(Import NZBase : NZBasePropSig NZ). Hint Rewrite pred_succ add_0_l add_succ_l mul_0_l mul_succ_l sub_0_r sub_succ_r : nz. diff --git a/theories/Numbers/NatInt/NZAddOrder.v b/theories/Numbers/NatInt/NZAddOrder.v index 56982c616..7313c4131 100644 --- a/theories/Numbers/NatInt/NZAddOrder.v +++ b/theories/Numbers/NatInt/NZAddOrder.v @@ -12,9 +12,8 @@ Require Import NZAxioms NZBase NZMul NZOrder. -Module Type NZAddOrderPropSig (Import NZ : NZOrdAxiomsSig). +Module Type NZAddOrderPropSig (Import NZ : NZOrdAxiomsSig'). Include Type NZBasePropSig NZ <+ NZMulPropSig NZ <+ NZOrderPropSig NZ. -Local Open Scope NumScope. Theorem add_lt_mono_l : forall n m p, n < m <-> p + n < p + m. Proof. diff --git a/theories/Numbers/NatInt/NZAxioms.v b/theories/Numbers/NatInt/NZAxioms.v index f6328e249..5b4e16caf 100644 --- a/theories/Numbers/NatInt/NZAxioms.v +++ b/theories/Numbers/NatInt/NZAxioms.v @@ -10,10 +10,7 @@ (*i $Id$ i*) -Require Export DecidableType2 OrderedType2 NumPrelude. - -Delimit Scope NumScope with Num. -Local Open Scope NumScope. +Require Export DecidableType2 OrderedType2 NumPrelude GenericMinMax. (** Axiomatization of a domain with zero, successor, predecessor, and a bi-directional induction principle. We require [P (S n) = n] @@ -22,121 +19,93 @@ Local Open Scope NumScope. for instance [Z/nZ] (See file [NZDomain for a study of that). *) -Module Type NZDomain (Import E : EqualityType). - (** [E] provides [t], [eq], [eq_equiv : Equivalence eq] *) - -Notation "x == y" := (eq x y) (at level 70) : NumScope. -Notation "x ~= y" := (~ eq x y) (at level 70) : NumScope. - -Parameter Inline zero : t. -Parameter Inline succ : t -> t. -Parameter Inline pred : t -> t. - -Notation "0" := zero : NumScope. -Notation S := succ. -Notation P := pred. -Notation "1" := (S 0) : NumScope. - -Declare Instance succ_wd : Proper (eq ==> eq) S. -Declare Instance pred_wd : Proper (eq ==> eq) P. - -Axiom pred_succ : forall n, P (S n) == n. - -Axiom bi_induction : +Module Type ZeroSuccPred (Import T:Typ). + Parameter Inline zero : t. + Parameters Inline succ pred : t -> t. +End ZeroSuccPred. + +Module Type ZeroSuccPredNotation (T:Typ)(Import NZ:ZeroSuccPred T). + Notation "0" := zero. + Notation S := succ. + Notation P := pred. + Notation "1" := (S 0). + Notation "2" := (S 1). +End ZeroSuccPredNotation. + +Module Type ZeroSuccPred' (T:Typ) := + ZeroSuccPred T <+ ZeroSuccPredNotation T. + +Module Type IsNZDomain (Import E:Eq')(Import NZ:ZeroSuccPred' E). + Declare Instance succ_wd : Proper (eq ==> eq) S. + Declare Instance pred_wd : Proper (eq ==> eq) P. + Axiom pred_succ : forall n, P (S n) == n. + Axiom bi_induction : forall A : t -> Prop, Proper (eq==>iff) A -> A 0 -> (forall n, A n <-> A (S n)) -> forall n, A n. +End IsNZDomain. -End NZDomain. - -Module Type NZDomainSig := EqualityType <+ NZDomain. - -(** A version with decidable type *) - -Module Type NZDecDomainSig := DecidableType <+ NZDomain. +Module Type NZDomainSig := EqualityType <+ ZeroSuccPred <+ IsNZDomain. +Module Type NZDomainSig' := EqualityType' <+ ZeroSuccPred' <+ IsNZDomain. (** Axiomatization of basic operations : [+] [-] [*] *) -Module Type NZHasBasicFuns (Import NZ : NZDomainSig). - -Parameter Inline add : t -> t -> t. -Parameter Inline sub : t -> t -> t. -Parameter Inline mul : t -> t -> t. - -Notation "x + y" := (add x y) : NumScope. -Notation "x - y" := (sub x y) : NumScope. -Notation "x * y" := (mul x y) : NumScope. - -Declare Instance add_wd : Proper (eq ==> eq ==> eq) add. -Declare Instance sub_wd : Proper (eq ==> eq ==> eq) sub. -Declare Instance mul_wd : Proper (eq ==> eq ==> eq) mul. - -Axiom add_0_l : forall n, (0 + n) == n. -Axiom add_succ_l : forall n m, (S n) + m == S (n + m). - -Axiom sub_0_r : forall n, n - 0 == n. -Axiom sub_succ_r : forall n m, n - (S m) == P (n - m). - -Axiom mul_0_l : forall n, 0 * n == 0. -Axiom mul_succ_l : forall n m, S n * m == n * m + m. - -End NZHasBasicFuns. - -Module Type NZBasicFunsSig := NZDomainSig <+ NZHasBasicFuns. - +Module Type AddSubMul (Import T:Typ). + Parameters Inline add sub mul : t -> t -> t. +End AddSubMul. + +Module Type AddSubMulNotation (T:Typ)(Import NZ:AddSubMul T). + Notation "x + y" := (add x y). + Notation "x - y" := (sub x y). + Notation "x * y" := (mul x y). +End AddSubMulNotation. + +Module Type AddSubMul' (T:Typ) := AddSubMul T <+ AddSubMulNotation T. + +Module Type IsAddSubMul (Import E:NZDomainSig')(Import NZ:AddSubMul' E). + Declare Instance add_wd : Proper (eq ==> eq ==> eq) add. + Declare Instance sub_wd : Proper (eq ==> eq ==> eq) sub. + Declare Instance mul_wd : Proper (eq ==> eq ==> eq) mul. + Axiom add_0_l : forall n, 0 + n == n. + Axiom add_succ_l : forall n m, (S n) + m == S (n + m). + Axiom sub_0_r : forall n, n - 0 == n. + Axiom sub_succ_r : forall n m, n - (S m) == P (n - m). + Axiom mul_0_l : forall n, 0 * n == 0. + Axiom mul_succ_l : forall n m, S n * m == n * m + m. +End IsAddSubMul. + +Module Type NZBasicFunsSig := NZDomainSig <+ AddSubMul <+ IsAddSubMul. +Module Type NZBasicFunsSig' := NZDomainSig' <+ AddSubMul' <+IsAddSubMul. (** Old name for the same interface: *) Module Type NZAxiomsSig := NZBasicFunsSig. - +Module Type NZAxiomsSig' := NZBasicFunsSig'. (** Axiomatization of order *) -Module Type NZHasOrd (Import NZ : NZDomainSig). - -Parameter Inline lt : t -> t -> Prop. -Parameter Inline le : t -> t -> Prop. +Module Type NZOrd := NZDomainSig <+ HasLt <+ HasLe. +Module Type NZOrd' := NZDomainSig' <+ HasLt <+ HasLe <+ + LtNotation <+ LeNotation <+ LtLeNotation. -Notation "x < y" := (lt x y) : NumScope. -Notation "x <= y" := (le x y) : NumScope. -Notation "x > y" := (lt y x) (only parsing) : NumScope. -Notation "x >= y" := (le y x) (only parsing) : NumScope. +Module Type IsNZOrd (Import NZ : NZOrd'). + Declare Instance lt_wd : Proper (eq ==> eq ==> iff) lt. + Axiom lt_eq_cases : forall n m, n <= m <-> n < m \/ n == m. + Axiom lt_irrefl : forall n, ~ (n < n). + Axiom lt_succ_r : forall n m, n < S m <-> n <= m. +End IsNZOrd. -Notation "x < y < z" := (x<y /\ y<z) : NumScope. -Notation "x <= y <= z" := (x<=y /\ y<=z) : NumScope. -Notation "x <= y < z" := (x<=y /\ y<z) : NumScope. -Notation "x < y <= z" := (x<y /\ y<=z) : NumScope. - -Declare Instance lt_wd : Proper (eq ==> eq ==> iff) lt. -(** Compatibility of [le] can be proved later from [lt_wd] +(** NB: the compatibility of [le] can be proved later from [lt_wd] and [lt_eq_cases] *) -Axiom lt_eq_cases : forall n m, n <= m <-> n < m \/ n == m. -Axiom lt_irrefl : forall n, ~ (n < n). -Axiom lt_succ_r : forall n m, n < S m <-> n <= m. - -End NZHasOrd. - -Module Type NZOrdSig := NZDomainSig <+ NZHasOrd. - - -(** Axiomatization of minimum and maximum *) - -Module Type NZHasMinMax (Import NZ : NZOrdSig). - -Parameter Inline min : t -> t -> t. -Parameter Inline max : t -> t -> t. - -(** Compatibility of [min] and [max] can be proved later *) - -Axiom min_l : forall n m, n <= m -> min n m == n. -Axiom min_r : forall n m, m <= n -> min n m == m. -Axiom max_l : forall n m, m <= n -> max n m == n. -Axiom max_r : forall n m, n <= m -> max n m == m. +Module Type NZOrdSig := NZOrd <+ IsNZOrd. +Module Type NZOrdSig' := NZOrd' <+ IsNZOrd. -End NZHasMinMax. +(** Everything together : *) +Module Type NZOrdAxiomsSig <: NZBasicFunsSig <: NZOrdSig + := NZOrdSig <+ AddSubMul <+ IsAddSubMul <+ HasMinMax. +Module Type NZOrdAxiomsSig' <: NZOrdAxiomsSig + := NZOrdSig' <+ AddSubMul' <+ IsAddSubMul <+ HasMinMax. -Module Type NZOrdAxiomsSig := - NZDomainSig <+ NZHasBasicFuns <+ NZHasOrd <+ NZHasMinMax. diff --git a/theories/Numbers/NatInt/NZBase.v b/theories/Numbers/NatInt/NZBase.v index 04955b3b3..18e3b9b92 100644 --- a/theories/Numbers/NatInt/NZBase.v +++ b/theories/Numbers/NatInt/NZBase.v @@ -12,8 +12,7 @@ Require Import NZAxioms. -Module Type NZBasePropSig (Import NZ : NZDomainSig). -Local Open Scope NumScope. +Module Type NZBasePropSig (Import NZ : NZDomainSig'). Include BackportEq NZ NZ. (** eq_refl, eq_sym, eq_trans *) diff --git a/theories/Numbers/NatInt/NZDiv.v b/theories/Numbers/NatInt/NZDiv.v index da7d62ceb..4acd6540d 100644 --- a/theories/Numbers/NatInt/NZDiv.v +++ b/theories/Numbers/NatInt/NZDiv.v @@ -10,15 +10,20 @@ Require Import NZAxioms NZMulOrder. -Open Scope NumScope. +(** The first signatures will be common to all divisions over NZ, N and Z *) -(** This first signature will be common to all divisions over NZ, N and Z *) +Module Type DivMod (Import T:Typ). + Parameters div modulo : t -> t -> t. +End DivMod. -Module Type NZDivCommon (Import NZ : NZAxiomsSig). - Parameter Inline div : t -> t -> t. - Parameter Inline modulo : t -> t -> t. - Infix "/" := div : NumScope. - Infix "mod" := modulo (at level 40, no associativity) : NumScope. +Module Type DivModNotation (T:Typ)(Import NZ:DivMod T). + Infix "/" := div. + Infix "mod" := modulo (at level 40, no associativity). +End DivModNotation. + +Module Type DivMod' (T:Typ) := DivMod T <+ DivModNotation T. + +Module Type NZDivCommon (Import NZ : NZAxiomsSig')(Import DM : DivMod' NZ). Declare Instance div_wd : Proper (eq==>eq==>eq) div. Declare Instance mod_wd : Proper (eq==>eq==>eq) modulo. Axiom div_mod : forall a b, b ~= 0 -> a == b*(a/b) + (a mod b). @@ -31,15 +36,18 @@ End NZDivCommon. NB: This axiom would also be true for N and Z, but redundant. *) -Module Type NZDiv (Import NZ : NZOrdAxiomsSig). - Include Type NZDivCommon NZ. +Module Type NZDivSpecific (Import NZ : NZOrdAxiomsSig')(Import DM : DivMod' NZ). Axiom mod_bound : forall a b, 0<=a -> 0<b -> 0 <= a mod b < b. -End NZDiv. +End NZDivSpecific. + +Module Type NZDiv (NZ:NZOrdAxiomsSig) + := DivMod NZ <+ NZDivCommon NZ <+ NZDivSpecific NZ. Module Type NZDivSig := NZOrdAxiomsSig <+ NZDiv. +Module Type NZDivSig' := NZOrdAxiomsSig' <+ NZDiv <+ DivModNotation. Module NZDivPropFunct - (Import NZ : NZDivSig)(Import NZP : NZMulOrderPropSig NZ). + (Import NZ : NZDivSig')(Import NZP : NZMulOrderPropSig NZ). (** Uniqueness theorems *) diff --git a/theories/Numbers/NatInt/NZDomain.v b/theories/Numbers/NatInt/NZDomain.v index 6dcc9e91f..eb06cae03 100644 --- a/theories/Numbers/NatInt/NZDomain.v +++ b/theories/Numbers/NatInt/NZDomain.v @@ -55,8 +55,7 @@ Implicit Arguments iter [A]. Local Infix "^" := iter. -Module NZDomainProp (Import NZ:NZDomainSig). -Local Open Scope NumScope. +Module NZDomainProp (Import NZ:NZDomainSig'). (** * Relationship between points thanks to [succ] and [pred]. *) @@ -274,11 +273,11 @@ End NZDomainProp. First, relationship with [0], [succ], [pred]. *) -Module NZOfNat (Import NZ:NZDomainSig). -Local Open Scope NumScope. +Module NZOfNat (Import NZ:NZDomainSig'). Definition ofnat (n : nat) : t := (S^n) 0. -Notation "[ n ]" := (ofnat n) (at level 7) : NumScope. +Notation "[ n ]" := (ofnat n) (at level 7) : ofnat. +Local Open Scope ofnat. Lemma ofnat_zero : [O] == 0. Proof. @@ -306,10 +305,10 @@ End NZOfNat. [ofnat] is injective, and hence that NZ is infinite (i.e. we ban Z/nZ models) *) -Module NZOfNatOrd (Import NZ:NZOrdSig). +Module NZOfNatOrd (Import NZ:NZOrdSig'). Include NZOfNat NZ. Include NZOrderPropFunct NZ. -Local Open Scope NumScope. +Local Open Scope ofnat. Theorem ofnat_S_gt_0 : forall n : nat, 0 < [Datatypes.S n]. @@ -368,9 +367,9 @@ End NZOfNatOrd. (** For basic operations, we can prove correspondance with their counterpart in [nat]. *) -Module NZOfNatOps (Import NZ:NZAxiomsSig). +Module NZOfNatOps (Import NZ:NZAxiomsSig'). Include NZOfNat NZ. -Local Open Scope NumScope. +Local Open Scope ofnat. Lemma ofnat_add_l : forall n m, [n]+m == (S^n) m. Proof. diff --git a/theories/Numbers/NatInt/NZMul.v b/theories/Numbers/NatInt/NZMul.v index e7c9b05e0..3c11024e5 100644 --- a/theories/Numbers/NatInt/NZMul.v +++ b/theories/Numbers/NatInt/NZMul.v @@ -13,9 +13,8 @@ Require Import NZAxioms NZBase NZAdd. Module Type NZMulPropSig - (Import NZ : NZAxiomsSig)(Import NZBase : NZBasePropSig NZ). + (Import NZ : NZAxiomsSig')(Import NZBase : NZBasePropSig NZ). Include Type NZAddPropSig NZ NZBase. -Local Open Scope NumScope. Theorem mul_0_r : forall n, n * 0 == 0. Proof. diff --git a/theories/Numbers/NatInt/NZMulOrder.v b/theories/Numbers/NatInt/NZMulOrder.v index a4d8a3972..18f61de59 100644 --- a/theories/Numbers/NatInt/NZMulOrder.v +++ b/theories/Numbers/NatInt/NZMulOrder.v @@ -13,9 +13,8 @@ Require Import NZAxioms. Require Import NZAddOrder. -Module Type NZMulOrderPropSig (Import NZ : NZOrdAxiomsSig). +Module Type NZMulOrderPropSig (Import NZ : NZOrdAxiomsSig'). Include Type NZAddOrderPropSig NZ. -Local Open Scope NumScope. Theorem mul_lt_pred : forall p q n m, S p == q -> (p * n < p * m <-> q * n + m < q * m + n). diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v index a95de8df7..6697c0b3d 100644 --- a/theories/Numbers/NatInt/NZOrder.v +++ b/theories/Numbers/NatInt/NZOrder.v @@ -13,8 +13,7 @@ Require Import NZAxioms NZBase Decidable OrderTac. Module Type NZOrderPropSig - (Import NZ : NZOrdSig)(Import NZBase : NZBasePropSig NZ). -Local Open Scope NumScope. + (Import NZ : NZOrdSig')(Import NZBase : NZBasePropSig NZ). Instance le_wd : Proper (eq==>eq==>iff) le. Proof. @@ -137,11 +136,7 @@ Module OrderElts. Definition le_lteq := lt_eq_cases. End OrderElts. Module OrderTac := MakeOrderTac OrderElts. -Ltac order := - change eq with OrderElts.eq in *; - change lt with OrderElts.lt in *; - change le with OrderElts.le in *; - OrderTac.order. +Ltac order := OrderTac.order. (** Some direct consequences of [order]. *) @@ -620,29 +615,3 @@ Module NZOrderPropFunct (Import NZ : NZOrdSig). Include Type NZBasePropSig NZ <+ NZOrderPropSig NZ. End NZOrderPropFunct. - -(** To Merge with GenericMinMax ... *) - -Module NZMinMaxPropFunct (Import NZ : NZOrdAxiomsSig). -Include NZOrderPropFunct NZ. - -(** * Compatibility of [min] and [max]. *) - -Instance min_wd : Proper (eq==>eq==>eq) min. -Proof. -intros n n' Hn m m' Hm. -destruct (le_ge_cases n m). -rewrite 2 min_l; auto. now rewrite <-Hn,<-Hm. -rewrite 2 min_r; auto. now rewrite <-Hn,<-Hm. -Qed. - -Instance max_wd : Proper (eq==>eq==>eq) max. -Proof. -intros n n' Hn m m' Hm. -destruct (le_ge_cases n m). -rewrite 2 max_r; auto. now rewrite <-Hn,<-Hm. -rewrite 2 max_l; auto. now rewrite <-Hn,<-Hm. -Qed. - -End NZMinMaxPropFunct. - diff --git a/theories/Numbers/Natural/Abstract/NAdd.v b/theories/Numbers/Natural/Abstract/NAdd.v index c3e1e223e..9f0b54a6a 100644 --- a/theories/Numbers/Natural/Abstract/NAdd.v +++ b/theories/Numbers/Natural/Abstract/NAdd.v @@ -12,11 +12,9 @@ Require Export NBase. -Module NAddPropFunct (Import N : NAxiomsSig). +Module NAddPropFunct (Import N : NAxiomsSig'). Include NBasePropFunct N. -Local Open Scope NumScope. - (** For theorems about [add] that are both valid for [N] and [Z], see [NZAdd] *) (** Now comes theorems valid for natural numbers but not for Z *) diff --git a/theories/Numbers/Natural/Abstract/NAddOrder.v b/theories/Numbers/Natural/Abstract/NAddOrder.v index f48b62e61..0ce04e54e 100644 --- a/theories/Numbers/Natural/Abstract/NAddOrder.v +++ b/theories/Numbers/Natural/Abstract/NAddOrder.v @@ -12,9 +12,8 @@ Require Export NOrder. -Module NAddOrderPropFunct (Import N : NAxiomsSig). +Module NAddOrderPropFunct (Import N : NAxiomsSig'). Include NOrderPropFunct N. -Local Open Scope NumScope. (** Theorems true for natural numbers, not for integers *) diff --git a/theories/Numbers/Natural/Abstract/NAxioms.v b/theories/Numbers/Natural/Abstract/NAxioms.v index 1cb474674..42016ab10 100644 --- a/theories/Numbers/Natural/Abstract/NAxioms.v +++ b/theories/Numbers/Natural/Abstract/NAxioms.v @@ -14,9 +14,7 @@ Require Export NZAxioms. Set Implicit Arguments. -Module Type NAxiomsSig. -Include Type NZOrdAxiomsSig. -Local Open Scope NumScope. +Module Type NAxioms (Import NZ : NZDomainSig'). Axiom pred_0 : P 0 == 0. @@ -34,5 +32,8 @@ Axiom recursion_succ : Aeq a a -> Proper (eq==>Aeq==>Aeq) f -> forall n, Aeq (recursion a f (S n)) (f n (recursion a f n)). -End NAxiomsSig. +End NAxioms. + +Module Type NAxiomsSig := NZOrdAxiomsSig <+ NAxioms. +Module Type NAxiomsSig' := NZOrdAxiomsSig' <+ NAxioms. diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v index 4095fbb50..0d489a16d 100644 --- a/theories/Numbers/Natural/Abstract/NBase.v +++ b/theories/Numbers/Natural/Abstract/NBase.v @@ -14,10 +14,9 @@ Require Export Decidable. Require Export NAxioms. Require Import NZProperties. -Module NBasePropFunct (Import N : NAxiomsSig). +Module NBasePropFunct (Import N : NAxiomsSig'). (** First, we import all known facts about both natural numbers and integers. *) Include Type NZPropFunct N. -Local Open Scope NumScope. (** We prove that the successor of a number is not zero by defining a function (by recursion) that maps 0 to false and the successor to true *) diff --git a/theories/Numbers/Natural/Abstract/NDefOps.v b/theories/Numbers/Natural/Abstract/NDefOps.v index 69dbf656e..8ac7c6f6d 100644 --- a/theories/Numbers/Natural/Abstract/NDefOps.v +++ b/theories/Numbers/Natural/Abstract/NDefOps.v @@ -14,9 +14,8 @@ Require Import Bool. (* To get the orb and negb function *) Require Import RelationPairs. Require Export NStrongRec. -Module NdefOpsPropFunct (Import N : NAxiomsSig). +Module NdefOpsPropFunct (Import N : NAxiomsSig'). Include NStrongRecPropFunct N. -Local Open Scope NumScope. (*****************************************************) (** Addition *) diff --git a/theories/Numbers/Natural/Abstract/NDiv.v b/theories/Numbers/Natural/Abstract/NDiv.v index 9e446dc69..dd033fb76 100644 --- a/theories/Numbers/Natural/Abstract/NDiv.v +++ b/theories/Numbers/Natural/Abstract/NDiv.v @@ -10,16 +10,14 @@ Require Import NAxioms NProperties NZDiv. -Open Scope NumScope. - -Module Type NDiv (Import N : NAxiomsSig). - Include Type NZDivCommon N. (** div, mod, compat with eq, equation a=bq+r *) +Module Type NDivSpecific (Import N : NAxiomsSig')(Import DM : DivMod' N). Axiom mod_upper_bound : forall a b, b ~= 0 -> a mod b < b. -End NDiv. +End NDivSpecific. -Module Type NDivSig := NAxiomsSig <+ NDiv. +Module Type NDivSig := NAxiomsSig <+ DivMod <+ NZDivCommon <+ NDivSpecific. +Module Type NDivSig' := NAxiomsSig' <+ DivMod' <+ NZDivCommon <+ NDivSpecific. -Module NDivPropFunct (Import N : NDivSig)(Import NP : NPropSig N). +Module NDivPropFunct (Import N : NDivSig')(Import NP : NPropSig N). (** We benefit from what already exists for NZ *) diff --git a/theories/Numbers/Natural/Abstract/NIso.v b/theories/Numbers/Natural/Abstract/NIso.v index 13e289c29..47bf38cba 100644 --- a/theories/Numbers/Natural/Abstract/NIso.v +++ b/theories/Numbers/Natural/Abstract/NIso.v @@ -17,10 +17,10 @@ Module Homomorphism (N1 N2 : NAxiomsSig). Local Notation "n == m" := (N2.eq n m) (at level 70, no associativity). Definition homomorphism (f : N1.t -> N2.t) : Prop := - f N1.zero == N2.zero /\ forall n, f (N1.S n) == N2.S (f n). + f N1.zero == N2.zero /\ forall n, f (N1.succ n) == N2.succ (f n). Definition natural_isomorphism : N1.t -> N2.t := - N1.recursion N2.zero (fun (n : N1.t) (p : N2.t) => N2.S p). + N1.recursion N2.zero (fun (n : N1.t) (p : N2.t) => N2.succ p). Instance natural_isomorphism_wd : Proper (N1.eq ==> N2.eq) natural_isomorphism. Proof. @@ -38,7 +38,7 @@ unfold natural_isomorphism; now rewrite N1.recursion_0. Qed. Theorem natural_isomorphism_succ : - forall n : N1.t, natural_isomorphism (N1.S n) == N2.S (natural_isomorphism n). + forall n : N1.t, natural_isomorphism (N1.succ n) == N2.succ (natural_isomorphism n). Proof. unfold natural_isomorphism. intro n. rewrite N1.recursion_succ; auto with *. diff --git a/theories/Numbers/Natural/Abstract/NMulOrder.v b/theories/Numbers/Natural/Abstract/NMulOrder.v index 285d8c104..a2162b137 100644 --- a/theories/Numbers/Natural/Abstract/NMulOrder.v +++ b/theories/Numbers/Natural/Abstract/NMulOrder.v @@ -12,9 +12,8 @@ Require Export NAddOrder. -Module NMulOrderPropFunct (Import N : NAxiomsSig). +Module NMulOrderPropFunct (Import N : NAxiomsSig'). Include NAddOrderPropFunct N. -Local Open Scope NumScope. (** Theorems that are either not valid on Z or have different proofs on N and Z *) diff --git a/theories/Numbers/Natural/Abstract/NOrder.v b/theories/Numbers/Natural/Abstract/NOrder.v index 94c68a186..090c02ecf 100644 --- a/theories/Numbers/Natural/Abstract/NOrder.v +++ b/theories/Numbers/Natural/Abstract/NOrder.v @@ -12,9 +12,8 @@ Require Export NAdd. -Module NOrderPropFunct (Import N : NAxiomsSig). +Module NOrderPropFunct (Import N : NAxiomsSig'). Include NAddPropFunct N. -Local Open Scope NumScope. (* Theorems that are true for natural numbers but not for integers *) diff --git a/theories/Numbers/Natural/Abstract/NStrongRec.v b/theories/Numbers/Natural/Abstract/NStrongRec.v index 7629aa11b..ed867b825 100644 --- a/theories/Numbers/Natural/Abstract/NStrongRec.v +++ b/theories/Numbers/Natural/Abstract/NStrongRec.v @@ -15,9 +15,8 @@ and proves its properties *) Require Export NSub. -Module NStrongRecPropFunct (Import N : NAxiomsSig). +Module NStrongRecPropFunct (Import N : NAxiomsSig'). Include Type NSubPropFunct N. -Local Open Scope NumScope. Section StrongRecursion. diff --git a/theories/Numbers/Natural/Abstract/NSub.v b/theories/Numbers/Natural/Abstract/NSub.v index e027c0be2..bc638cf3b 100644 --- a/theories/Numbers/Natural/Abstract/NSub.v +++ b/theories/Numbers/Natural/Abstract/NSub.v @@ -12,9 +12,8 @@ Require Export NMulOrder. -Module Type NSubPropFunct (Import N : NAxiomsSig). +Module Type NSubPropFunct (Import N : NAxiomsSig'). Include NMulOrderPropFunct N. -Local Open Scope NumScope. Theorem sub_0_l : forall n, 0 - n == 0. Proof. diff --git a/theories/Structures/OrderedType2.v b/theories/Structures/OrderedType2.v index 5b669db4e..1cddfea3b 100644 --- a/theories/Structures/OrderedType2.v +++ b/theories/Structures/OrderedType2.v @@ -32,11 +32,13 @@ Module Type EqLtLe := Typ <+ HasEq <+ HasLt <+ HasLe. Module Type LtNotation (E:EqLt). Infix "<" := E.lt. + Notation "x > y" := (y<x) (only parsing). Notation "x < y < z" := (x<y /\ y<z). End LtNotation. Module Type LeNotation (E:EqLe). Infix "<=" := E.le. + Notation "x >= y" := (y<=x) (only parsing). Notation "x <= y <= z" := (x<=y /\ y<=z). End LeNotation. |