Update on numbers.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9947 85f007b7-540e-0410-9357-904b9bb8a0f7

22 files changed, 201 insertions, 284 deletions

diff --git a/theories/Numbers/Integer/Axioms/ZAxioms.v b/theories/Numbers/Integer/Axioms/ZAxioms.v
index 4f0eab8e3..b73410256 100644
--- a/theories/Numbers/Integer/Axioms/ZAxioms.v
+++ b/theories/Numbers/Integer/Axioms/ZAxioms.v
@@ -3,12 +3,13 @@ Require Import ZDomain.
 
 Module Type IntSignature.
 Declare Module Export DomainModule : DomainSignature.
+Open Local Scope ZScope.
 
 Parameter Inline O : Z.
 Parameter Inline S : Z -> Z.
 Parameter Inline P : Z -> Z.
 
-Notation "0" := O.
+Notation "0" := O : ZScope.
 
 Add Morphism S with signature E ==> E as S_wd.
 Add Morphism P with signature E ==> E as P_wd.
@@ -26,8 +27,8 @@ End IntSignature.
 
 
 Module IntProperties (Export IntModule : IntSignature).
-
 Module Export DomainPropertiesModule := DomainProperties DomainModule.
+Open Local Scope ZScope.
 
 Ltac induct n :=
   try intros until n;
diff --git a/theories/Numbers/Integer/Axioms/ZDomain.v b/theories/Numbers/Integer/Axioms/ZDomain.v
index 00eab8842..b48684ba8 100644
--- a/theories/Numbers/Integer/Axioms/ZDomain.v
+++ b/theories/Numbers/Integer/Axioms/ZDomain.v
@@ -15,12 +15,15 @@ Add Relation Z E
  transitivity proved by (proj1 (proj2 E_equiv))
 as E_rel.
 
-Notation "x == y" := (E x y) (at level 70).
-Notation "x # y" := (~ E x y) (at level 70).
+Delimit Scope ZScope with Int.
+Bind Scope ZScope with Z.
+Notation "x == y" := (E x y) (at level 70) : ZScope.
+Notation "x # y" := (~ E x y) (at level 70) : ZScope.
 
 End DomainSignature.
 
 Module DomainProperties (Export DomainModule : DomainSignature).
+Open Local Scope ZScope.
 
 Add Morphism e with signature E ==> E ==> eq_bool as e_wd.
 Proof.
diff --git a/theories/Numbers/Integer/Axioms/ZOrder.v b/theories/Numbers/Integer/Axioms/ZOrder.v
index b1983d6f7..3bf4d61f5 100644
--- a/theories/Numbers/Integer/Axioms/ZOrder.v
+++ b/theories/Numbers/Integer/Axioms/ZOrder.v
@@ -1,18 +1,18 @@
 Require Import NumPrelude.
 Require Import ZDomain.
 Require Import ZAxioms.
-Require Import Coq.ZArith.Zmisc. (* for iter_nat *)
 
 Module Type OrderSignature.
 Declare Module Export IntModule : IntSignature.
+Open Local Scope ZScope.
 
 Parameter Inline lt : Z -> Z -> bool.
 Parameter Inline le : Z -> Z -> bool.
 Add Morphism lt with signature E ==> E ==> eq_bool as lt_wd.
 Add Morphism le with signature E ==> E ==> eq_bool as le_wd.
 
-Notation "n <  m" := (lt n m).
-Notation "n <= m" := (le n m).
+Notation "n <  m" := (lt n m) : ZScope.
+Notation "n <= m" := (le n m) : ZScope.
 
 Axiom le_lt : forall n m, n <= m <-> n < m \/ n == m.
 Axiom lt_irr : forall n, ~ (n < n).
@@ -23,6 +23,7 @@ End OrderSignature.
 
 Module OrderProperties (Export OrderModule : OrderSignature).
 Module Export IntPropertiesModule := IntProperties IntModule.
+Open Local Scope ZScope.
 
 Ltac le_intro1 := rewrite le_lt; left.
 Ltac le_intro2 := rewrite le_lt; right.
@@ -294,31 +295,36 @@ Proof.
 intros n H. apply S_wd in H. rewrite S_P in H. now apply neq_Sn_n with (n := n).
 Qed.
 
-Lemma lt_n_Skn :
-  forall (n : Z) (k : nat), n < iter_nat (Datatypes.S k) Z S n.
+Definition nth_S (n : nat) (m : Z) :=
+  nat_rec (fun _ => Z) m (fun _ l => S l) n.
+Definition nth_P (n : nat) (m : Z) :=
+  nat_rec (fun _ => Z) m (fun _ l => P l) n.
+
+Lemma lt_m_Skm :
+  forall (n : nat) (m : Z), m < nth_S (Datatypes.S n) m.
 Proof.
-intro n; induction k as [| k IH]; simpl in *.
+intros n m; induction n as [| n IH]; simpl in *.
 apply lt_n_Sn. now apply lt_n_Sm.
 Qed.
 
-Lemma lt_Pkn_n :
-  forall (n : Z) (k : nat), iter_nat (Datatypes.S k) Z P n < n.
+Lemma lt_Pkm_m :
+  forall (n : nat) (m : Z), nth_P (Datatypes.S n) m < m.
 Proof.
-intro n; induction k as [| k IH]; simpl in *.
+intros n m; induction n as [| n IH]; simpl in *.
 apply lt_Pn_n. now apply lt_Pn_m.
 Qed.
 
-Theorem neq_n_Skn :
-  forall (n : Z) (k : nat), iter_nat (Datatypes.S k) Z S n # n.
+Theorem neq_m_Skm :
+  forall (n : nat) (m : Z), nth_S (Datatypes.S n) m # m.
 Proof.
-intros n k H. pose proof (lt_n_Skn n k) as H1. rewrite H in H1.
+intros n m H. pose proof (lt_m_Skm n m) as H1. rewrite H in H1.
 false_hyp H1 lt_irr.
 Qed.
 
-Theorem neq_Pkn_n :
-  forall (n : Z) (k : nat), iter_nat (Datatypes.S k) Z P n # n.
+Theorem neq_Pkm_m :
+  forall (n : nat) (m : Z), nth_P (Datatypes.S n) m # m.
 Proof.
-intros n k H. pose proof (lt_Pkn_n n k) as H1. rewrite H in H1.
+intros n m H. pose proof (lt_Pkm_m n m) as H1. rewrite H in H1.
 false_hyp H1 lt_irr.
 Qed.
 
diff --git a/theories/Numbers/Integer/Axioms/ZPlus.v b/theories/Numbers/Integer/Axioms/ZPlus.v
index 1b5aa73fb..f455400b7 100644
--- a/theories/Numbers/Integer/Axioms/ZPlus.v
+++ b/theories/Numbers/Integer/Axioms/ZPlus.v
@@ -4,14 +4,15 @@ Require Import ZAxioms.
 
 Module Type PlusSignature.
 Declare Module Export IntModule : IntSignature.
+Open Local Scope ZScope.
 
 Parameter Inline plus : Z -> Z -> Z.
 Parameter Inline minus : Z -> Z -> Z.
 Parameter Inline uminus : Z -> Z.
 
-Notation "x + y" := (plus x y).
-Notation "x - y" := (minus x y).
-Notation "- x" := (uminus x).
+Notation "x + y" := (plus x y) : ZScope.
+Notation "x - y" := (minus x y) : ZScope.
+Notation "- x" := (uminus x) : ZScope.
 
 Add Morphism plus with signature E ==> E ==> E as plus_wd.
 Add Morphism minus with signature E ==> E ==> E as minus_wd.
@@ -29,8 +30,8 @@ Axiom uminus_S : forall n, - (S n) == P (- n).
 End PlusSignature.
 
 Module PlusProperties (Export PlusModule : PlusSignature).
-
 Module Export IntPropertiesModule := IntProperties IntModule.
+Open Local Scope ZScope.
 
 Theorem plus_P : forall n m, P n + m == P (n + m).
 Proof.
diff --git a/theories/Numbers/Integer/Axioms/ZPlusOrder.v b/theories/Numbers/Integer/Axioms/ZPlusOrder.v
index abaaa664f..4f677355b 100644
--- a/theories/Numbers/Integer/Axioms/ZPlusOrder.v
+++ b/theories/Numbers/Integer/Axioms/ZPlusOrder.v
@@ -1,13 +1,14 @@
 Require Import ZOrder.
 Require Import ZPlus.
-(* Warning: Trying to mask the absolute name "Plus"!!! *)
 
 Module PlusOrderProperties (Export PlusModule : PlusSignature)
                            (Export OrderModule : OrderSignature with
                              Module IntModule := PlusModule.IntModule).
-
+(* Warning: Notation _ == _ was already used in scope ZScope !!! *)
 Module Export PlusPropertiesModule := PlusProperties PlusModule.
 Module Export OrderPropertiesModule := OrderProperties OrderModule.
+(* <W> Grammar extension: in [tactic:simple_tactic], some rule has been masked !!! *)
+Open Local Scope ZScope.
 
 Theorem plus_lt_compat_l : forall n m p, n < m <-> p + n < p + m.
 Proof.
diff --git a/theories/Numbers/Integer/Axioms/ZTimes.v b/theories/Numbers/Integer/Axioms/ZTimes.v
index 3f9c7c4ce..ff0de6196 100644
--- a/theories/Numbers/Integer/Axioms/ZTimes.v
+++ b/theories/Numbers/Integer/Axioms/ZTimes.v
@@ -5,10 +5,11 @@ Require Import ZPlus.
 
 Module Type TimesSignature.
 Declare Module Export PlusModule : PlusSignature.
+Open Local Scope ZScope.
 
 Parameter Inline times : Z -> Z -> Z.
 
-Notation "x * y" := (times x y).
+Notation "x * y" := (times x y) : ZScope.
 
 Add Morphism times with signature E ==> E ==> E as times_wd.
 
@@ -31,8 +32,8 @@ French (deux fois trois) and Russian (dvazhdy tri) implies 3 + 3, not
 End TimesSignature.
 
 Module TimesProperties (Export TimesModule : TimesSignature).
-
 Module Export PlusPropertiesModule := PlusProperties PlusModule.
+Open Local Scope ZScope.
 
 Theorem times_P : forall n m, n * (P m) == n * m - n.
 Proof.
diff --git a/theories/Numbers/Integer/Axioms/ZTimesOrder.v b/theories/Numbers/Integer/Axioms/ZTimesOrder.v
index 1f8b0a947..460a13bf4 100644
--- a/theories/Numbers/Integer/Axioms/ZTimesOrder.v
+++ b/theories/Numbers/Integer/Axioms/ZTimesOrder.v
@@ -1,7 +1,6 @@
 Require Import ZPlus.
 Require Import ZTimes.
 Require Import ZOrder.
-(* Warning: Trying to mask the absolute name "Plus"!!! *)
 Require Import ZPlusOrder.
 
 Module TimesOrderProperties (Export TimesModule : TimesSignature)
@@ -11,6 +10,7 @@ Module TimesOrderProperties (Export TimesModule : TimesSignature)
 Module Export TimesPropertiesModule := TimesProperties TimesModule.
 Module Export PlusOrderPropertiesModule :=
   PlusOrderProperties TimesModule.PlusModule OrderModule.
+Open Local Scope ZScope.
 
 Theorem mult_lt_compat_r : forall n m p, 0 < p -> n < m -> n * p < m * p.
 Proof.
diff --git a/theories/Numbers/Integer/NatPairs/CommRefl.v b/theories/Numbers/Integer/NatPairs/CommRefl.v
deleted file mode 100644
index 673a1fe50..000000000
--- a/theories/Numbers/Integer/NatPairs/CommRefl.v
+++ /dev/null
@@ -1,185 +0,0 @@
-Require Import Arith.
-Require Import List.
-Require Import Setoid.
-
-Inductive bin : Set := node : bin->bin->bin | leaf : nat->bin.
-
-Fixpoint flatten_aux (t fin:bin){struct t} : bin :=
-  match t with
-  | node t1 t2 => flatten_aux t1 (flatten_aux t2 fin)
-  | x => node x fin
-  end.
-
-Fixpoint flatten (t:bin) : bin :=
-  match t with
-  | node t1 t2 => flatten_aux t1 (flatten t2)
-  | x => x
-  end.
-
-Fixpoint nat_le_bool (n m:nat){struct m} : bool :=
-  match n, m with
-  | O, _ => true
-  | S _, O => false
-  | S n, S m => nat_le_bool n m
-  end.
-
-Fixpoint insert_bin (n:nat)(t:bin){struct t} : bin :=
-  match t with
-  | leaf m => match nat_le_bool n m with
-              | true => node (leaf n)(leaf m)
-              | false => node (leaf m)(leaf n)
-              end
-  | node (leaf m) t' => match nat_le_bool n m with
-                        | true => node (leaf n) t
-                        | false => 
-                            node (leaf m)(insert_bin n t')
-                        end
-  | t => node (leaf n) t
-  end.
-
-Fixpoint sort_bin (t:bin) : bin :=
-  match t with
-  | node (leaf n) t' => insert_bin n (sort_bin t')
-  | t => t
-  end.
-
-Section commut_eq.
-Variable A : Set.
-Variable E : relation A.
-Variable f : A -> A -> A.
-
-Hypothesis E_equiv : equiv A E.
-Hypothesis comm : forall x y : A, f x y = f y x.
-Hypothesis assoc : forall x y z : A, f x (f y z) = f (f x y) z.
-
-Notation "x == y" := (E x y) (at level 70).
-
-Add Relation A E
- reflexivity proved by (proj1 E_equiv)
- symmetry proved by (proj2 (proj2 E_equiv))
- transitivity proved by (proj1 (proj2 E_equiv))
-as E_rel.
-
-Fixpoint bin_A (l:list A)(def:A)(t:bin){struct t} : A :=
-  match t with
-  | node t1 t2 => f (bin_A l def t1)(bin_A l def t2)
-  | leaf n => nth n l def
-  end.
- Theorem flatten_aux_valid_A :
- forall (l:list A)(def:A)(t t':bin),
-  f (bin_A l def t)(bin_A l def t') == bin_A l def (flatten_aux t t').
-Proof.
- intros l def t; elim t; simpl; auto.
- intros t1 IHt1 t2 IHt2 t'.  rewrite <- IHt1; rewrite <- IHt2.
- symmetry; apply assoc.
-Qed.
- Theorem flatten_valid_A :
- forall (l:list A)(def:A)(t:bin),
-   bin_A l def t == bin_A l def (flatten t).
-Proof.
- intros l def t; elim t; simpl; trivial.
- intros t1 IHt1 t2 IHt2; rewrite <- flatten_aux_valid_A; rewrite <- IHt2.
- trivial.
-Qed.
-
-Theorem flatten_valid_A_2 :
- forall (t t':bin)(l:list A)(def:A),
-   bin_A l def (flatten t) == bin_A l def (flatten t')->
-   bin_A l def t == bin_A l def t'. 
-Proof.
- intros t t' l def Heq.
- rewrite (flatten_valid_A l def t); rewrite (flatten_valid_A l def t').
- trivial.
-Qed.
-
-Theorem insert_is_f : forall (l:list A)(def:A)(n:nat)(t:bin),
-   bin_A l def (insert_bin n t) == 
-   f (nth n l def) (bin_A l def t).
-Proof.
- intros l def n t; elim t.
- intros t1; case t1.
- intros t1' t1'' IHt1 t2 IHt2.
- simpl.
- auto.
- intros n0 IHt1 t2 IHt2.
- simpl.
- case (nat_le_bool n n0).
- simpl.
- auto.
- simpl.
- rewrite IHt2.
- repeat rewrite assoc; rewrite (comm (nth n l def)); auto.
- simpl.
- intros n0; case (nat_le_bool n n0); auto.
- rewrite comm; auto.
-Qed.
-
-Theorem sort_eq : forall (l:list A)(def:A)(t:bin),
-    bin_A l def (sort_bin t) == bin_A l def t.  
-Proof.
- intros l def t; elim t.
- intros t1 IHt1; case t1.
- auto.
- intros n t2 IHt2; simpl; rewrite insert_is_f.
- rewrite IHt2; auto.
- auto.
-Qed.
-
-
-Theorem sort_eq_2 :
- forall (l:list A)(def:A)(t1 t2:bin),
-   bin_A l def (sort_bin t1) == bin_A l def (sort_bin t2)->
-   bin_A l def t1 == bin_A l def t2.  
-Proof.
- intros l def t1 t2.
- rewrite <- (sort_eq l def t1); rewrite <- (sort_eq l def t2).
- trivial.
-Qed.
-
-End commut_eq.
-
-
-Ltac term_list f l v :=
-  match v with
-  | (f ?X1 ?X2) =>
-    let l1 := term_list f l X2 in term_list f l1 X1
-  | ?X1 => constr:(cons X1 l)
-  end.
-
-Ltac compute_rank l n v :=
-  match l with
-  | (cons ?X1 ?X2) =>
-    let tl := constr:X2 in
-    match constr:(X1 == v) with
-    | (?X1 == ?X1) => n
-    | _ => compute_rank tl (S n) v
-    end
-  end.
-
-Ltac model_aux l f v :=
-  match v with
-  | (f ?X1 ?X2) =>
-    let r1 := model_aux l f X1 with r2 := model_aux l f X2 in
-      constr:(node r1 r2)
-  | ?X1 => let n := compute_rank l 0 X1 in constr:(leaf n)
-  | _ => constr:(leaf 0)
-  end.
-
-Ltac comm_eq A f assoc_thm comm_thm :=
-  match goal with
-  | [ |- (?X1 == ?X2 :>A) ] =>
-    let l := term_list f (nil (A:=A)) X1 in
-    let term1 := model_aux l f X1 
-    with term2 := model_aux l f X2 in
-    (change (bin_A A f l X1 term1 == bin_A A f l X1 term2);
-      apply flatten_valid_A_2 with (1 := assoc_thm);
-      apply sort_eq_2 with (1 := comm_thm)(2 := assoc_thm); 
-      auto)
-  end.
-
-(*
-Theorem reflection_test4 : forall x y z:nat, x+(y+z) = (z+x)+y.
-Proof.
- intros x y z. comm_eq nat plus plus_assoc plus_comm.
-Qed.
-*)
\ No newline at end of file
diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
index d2634970d..02f73f4d1 100644
--- a/theories/Numbers/Integer/NatPairs/ZNatPairs.v
+++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
@@ -14,14 +14,14 @@ Require Import ZOrder.
 Require Import ZPlusOrder.
 Require Import ZTimesOrder.
 
-Module NatPairsDomain (Export PlusModule : NPlus.PlusSignature) <:
+Module NatPairsDomain (NPlusModule : NPlus.PlusSignature) <:
   ZDomain.DomainSignature.
-
-Module Export PlusPropertiesModule := NPlus.PlusProperties PlusModule.
+Module Export NPlusPropertiesModule := NPlus.PlusProperties NPlusModule.
 
 Definition Z : Set := (N * N)%type.
-Definition E (p1 p2 : Z) := (fst p1) + (snd p2) == (fst p2) + (snd p1).
-Definition e (p1 p2 : Z) := e ((fst p1) + (snd p2)) ((fst p2) + (snd p1)).
+
+Definition E (p1 p2 : Z) := ((fst p1) + (snd p2) == (fst p2) + (snd p1))%Nat.
+Definition e (p1 p2 : Z) := e ((fst p1) + (snd p2)) ((fst p2) + (snd p1))%Nat.
 
 Theorem E_equiv_e : forall x y : Z, E x y <-> e x y.
 Proof.
@@ -31,15 +31,56 @@ Qed.
 Theorem E_equiv : equiv Z E.
 Proof.
 split; [| split]; unfold reflexive, symmetric, transitive, E.
-now intro x.
+(* reflexivity *)
+now intro.
+(* transitivity *)
 intros x y z H1 H2.
-comm_eq N 
+apply plus_cancel_l with (p := fst y + snd y).
+rewrite (plus_shuffle2 (fst y) (snd y) (fst x) (snd z)).
+rewrite (plus_shuffle2 (fst y) (snd y) (fst z) (snd x)).
+rewrite plus_comm. rewrite (plus_comm (snd y) (fst x)).
+rewrite (plus_comm (snd y) (fst z)). now apply plus_wd.
+(* symmetry *)
+now intros.
+Qed.
+
+Add Relation Z E                                                                                 
+ reflexivity proved by (proj1 E_equiv)                                                           
+ symmetry proved by (proj2 (proj2 E_equiv))                                                      
+ transitivity proved by (proj1 (proj2 E_equiv))                                                  
+as E_rel.
+
+End NatPairsDomain.
+
+
+Module NatPairsInt (Export NPlusModule : NPlus.PlusSignature) <: IntSignature.
+
+Module Export ZDomainModule := NatPairsDomain NPlusModule.
+
+Definition O := (0, 0).
+Definition S (n : Z) := (NatModule.S (fst n), snd n).
+Definition P (n : Z) := (fst n, NatModule.S (snd n)).
+(* Unfortunately, we do not have P (S n) = n but only P (S n) == n.
+It could be possible to consider as "canonical" only pairs where one of
+the elements is 0, and make all operations convert canonical values into
+other canonical values. We do not do this because this is more complex
+and because we do not have the predecessor function on N at this point. *)
+
+Add Morphism S with signature E ==> E as S_wd.
+Proof.
+unfold S, E; intros n m H; simpl.
+do 2 rewrite plus_Sn_m; now rewrite H.
+Qed.
+
+Add Morphism P with signature E ==> E as P_wd.
+Proof.
+unfold P, E; intros n m H; simpl.
+do 2 rewrite plus_n_Sm; now rewrite H.
+Qed.
 
+Theorem S_inj : forall x y : Z, S x == S y -> x == y.
 
 
-assert (H : ((fst x) + (snd y)) + ((fst y) + (snd z)) ==
-            ((fst y) + (snd x)) + ((fst z) + (snd y))); [now apply plus_wd |].
-assert (H : (fst y) + (snd y) + (fst x) + (snd z) ==
-            (fst y) + (snd y) + (snd x) + (fst z)).
 
+Definition N_Z (n : nat) := nat_rec (fun _ : nat => Z) 0 (fun _ p => S p).
 
diff --git a/theories/Numbers/Natural/Axioms/NAxioms.v b/theories/Numbers/Natural/Axioms/NAxioms.v
index 55f07eb89..7d8fb573a 100644
--- a/theories/Numbers/Natural/Axioms/NAxioms.v
+++ b/theories/Numbers/Natural/Axioms/NAxioms.v
@@ -6,12 +6,20 @@ Require Export NDomain.
 
 Module Type NatSignature.
 Declare Module Export DomainModule : DomainSignature.
+(* We use Export in the previous line to make sure that if we import a
+module of type NatSignature, then we also import (i.e., get access
+without path qualifiers to) DomainModule. For example, the functor
+NatProperties below, which accepts an implementation of NatSignature
+as an argument and imports it, will have access to N. Indeed, it does
+not make sense to get unqualified access to O and S but not to N. *)
+
+Open Local Scope NScope.
 
 Parameter Inline O : N.
 Parameter Inline S : N -> N.
 
-Notation "0" := O.
-Notation "1" := (S O).
+Notation "0" := O : NScope.
+Notation "1" := (S O) : NScope.
 
 Add Morphism S with signature E ==> E as S_wd.
 
@@ -166,9 +174,9 @@ Implicit Arguments recursion_S [A].
 
 End NatSignature.
 
-Module NatProperties (Export NatModule : NatSignature).
-
-Module Export  DomainPropertiesModule := DomainProperties DomainModule.
+Module NatProperties (Import NatModule : NatSignature).
+Module Export DomainPropertiesModule := DomainProperties DomainModule.
+Open Local Scope NScope.
 
 (* This tactic applies the induction axioms and solves the resulting
 goal "pred_wd E P" *)
diff --git a/theories/Numbers/Natural/Axioms/NDepRec.v b/theories/Numbers/Natural/Axioms/NDepRec.v
index 7da105f5b..1d35bfbc4 100644
--- a/theories/Numbers/Natural/Axioms/NDepRec.v
+++ b/theories/Numbers/Natural/Axioms/NDepRec.v
@@ -8,11 +8,12 @@ n) must coincide with (A n') whenever n == n'. However, it is possible
 to try to use arbitrary domain and require that n == n' -> A n = A n'. *)
 
 Module Type DepRecSignature.
-Declare Module DomainModule : DomainEqSignature.
+Declare Module Export DomainModule : DomainEqSignature.
 Declare Module Export NatModule : NatSignature with
   Module DomainModule := DomainModule.
 (* Instead of these two lines, I would like to say
-Declare Module Export Nat : NatSignature with Module Domain : NatDomainEq. *)
+Declare Module Export Nat : NatSignature with Module Domain : NatEqDomain. *)
+Open Local Scope NScope.
 
 Parameter Inline dep_recursion :
   forall A : N -> Set, A 0 -> (forall n, A n -> A (S n)) -> forall n, A n.
@@ -27,11 +28,11 @@ Axiom dep_recursion_S :
 
 End DepRecSignature.
 
-Module DepRecTimesProperties (Export DepRecModule : DepRecSignature)
-                             (Export TimesModule : TimesSignature
+Module DepRecTimesProperties (Import DepRecModule : DepRecSignature)
+                             (Import TimesModule : TimesSignature
                                 with Module PlusModule.NatModule := DepRecModule.NatModule).
-
 Module Export TimesPropertiesModule := TimesProperties TimesModule.
+Open Local Scope NScope.
 
 Theorem not_0_implies_S_dep : forall n, n # O -> {m : N | n == S m}.
 Proof.
diff --git a/theories/Numbers/Natural/Axioms/NDomain.v b/theories/Numbers/Natural/Axioms/NDomain.v
index ebc692d5b..9dc8e4078 100644
--- a/theories/Numbers/Natural/Axioms/NDomain.v
+++ b/theories/Numbers/Natural/Axioms/NDomain.v
@@ -28,8 +28,10 @@ Add Relation N E
  transitivity proved by (proj1 (proj2 E_equiv))
 as E_rel.
 
-Notation "x == y" := (E x y) (at level 70).
-Notation "x # y" := (~ E x y) (at level 70).
+Delimit Scope NScope with Nat.
+Bind Scope NScope with N.
+Notation "x == y" := (E x y) (at level 70) : NScope.
+Notation "x # y" := (~ E x y) (at level 70) : NScope.
 
 End DomainSignature.
 
@@ -51,14 +53,17 @@ Add Relation N E
  transitivity proved by (proj1 (proj2 E_equiv))
 as E_rel.
 
-Notation "x == y" := (E x y) (at level 70).
-Notation "x # y" := ((E x y) -> False) (at level 70).
+Delimit Scope NScope with Nat.
+Bind Scope NScope with N.
+Notation "x == y" := (E x y) (at level 70) : NScope.
+Notation "x # y" := ((E x y) -> False) (at level 70) : NScope.
 (* Why do we need a new notation for Leibniz equality? See DepRec.v *)
 
 End DomainEqSignature.
 
-Module DomainProperties (Export DomainModule : DomainSignature).
+Module DomainProperties (Import DomainModule : DomainSignature).
 (* It also accepts module of type NatDomainEq *)
+Open Local Scope NScope.
 
 (* The following easily follows from transitivity of e and E, but
 we need to deal with the coercion *)
diff --git a/theories/Numbers/Natural/Axioms/NIso.v b/theories/Numbers/Natural/Axioms/NIso.v
index 41d7d6145..fdf3418ed 100644
--- a/theories/Numbers/Natural/Axioms/NIso.v
+++ b/theories/Numbers/Natural/Axioms/NIso.v
@@ -2,8 +2,8 @@ Require Import NAxioms.
 
 Module Homomorphism (Nat1 Nat2 : NatSignature).
 
-Module Import DomainProperties1 := DomainProperties Nat1.DomainModule.
-Module Import DomainProperties2 := DomainProperties Nat2.DomainModule.
+(*Module Import DomainProperties1 := DomainProperties Nat1.DomainModule.
+Module Import DomainProperties2 := DomainProperties Nat2.DomainModule.*)
 (* This registers Nat1.Domain.E and Nat2.Domain.E as setoid relations *)
 
 Notation Local N1 := Nat1.DomainModule.N.
diff --git a/theories/Numbers/Natural/Axioms/NLt.v b/theories/Numbers/Natural/Axioms/NLt.v
index 210786bba..a70b3f95b 100644
--- a/theories/Numbers/Natural/Axioms/NLt.v
+++ b/theories/Numbers/Natural/Axioms/NLt.v
@@ -2,10 +2,11 @@ Require Export NAxioms.
 
 Module Type LtSignature.
 Declare Module Export NatModule : NatSignature.
+Open Local Scope NScope.
 
 Parameter Inline lt : N -> N -> bool.
 
-Notation "x < y" := (lt x y).
+Notation "x < y" := (lt x y) : NScope.
 
 Add Morphism lt with signature E ==> E ==> eq_bool as lt_wd.
 
@@ -13,9 +14,9 @@ Axiom lt_0 : forall x, ~ (x < 0).
 Axiom lt_S : forall x y, x < S y <-> x < y \/ x == y.
 End LtSignature.
 
-Module LtProperties (Export LtModule : LtSignature).
-
-Module Export NatPropertiesModule := NatProperties NatModule.
+Module LtProperties (Import LtModule : LtSignature).
+Module Import NatPropertiesModule := NatProperties NatModule.
+Open Local Scope NScope.
 
 Theorem lt_n_Sn : forall n, n < S n.
 Proof.
diff --git a/theories/Numbers/Natural/Axioms/NMiscFunct.v b/theories/Numbers/Natural/Axioms/NMiscFunct.v
index 5f9b7b1d1..03f3cd86e 100644
--- a/theories/Numbers/Natural/Axioms/NMiscFunct.v
+++ b/theories/Numbers/Natural/Axioms/NMiscFunct.v
@@ -10,6 +10,7 @@ Require Import NTimesLt.
 Module MiscFunctFunctor (NatMod : NatSignature).
 Module Export NatPropertiesModule := NatProperties NatMod.
 Module Export StrongRecPropertiesModule := StrongRecProperties NatMod.
+Open Local Scope NScope.
 
 (*****************************************************)
 (**                   Addition                       *)
@@ -317,7 +318,7 @@ Qed.
 End DefaultPlusModule.
 
 Module DefaultTimesModule <: TimesSignature.
-Module Export PlusModule := DefaultPlusModule.
+Module Import PlusModule := DefaultPlusModule.
 
 Definition times := times.
 
@@ -360,11 +361,11 @@ Qed.
 
 End DefaultLtModule.
 
-Module Export DefaultPlusProperties := PlusProperties DefaultPlusModule.
-Module Export DefaultTimesProperties := TimesProperties DefaultTimesModule.
-Module Export DefaultLtProperties := LtProperties DefaultLtModule.
-Module Export DefaultPlusLtProperties := PlusLtProperties DefaultPlusModule DefaultLtModule.
-Module Export DefaultTimesLtProperties := TimesLtProperties DefaultTimesModule DefaultLtModule.
+Module Import DefaultPlusProperties := PlusProperties DefaultPlusModule.
+Module Import DefaultTimesProperties := TimesProperties DefaultTimesModule.
+Module Import DefaultLtProperties := LtProperties DefaultLtModule.
+Module Import DefaultPlusLtProperties := PlusLtProperties DefaultPlusModule DefaultLtModule.
+Module Import DefaultTimesLtProperties := TimesLtProperties DefaultTimesModule DefaultLtModule.
 
 (*Opaque MiscFunctFunctor.plus.
 Check plus_comm. (* This produces the following *)
diff --git a/theories/Numbers/Natural/Axioms/NOtherInd.v b/theories/Numbers/Natural/Axioms/NOtherInd.v
index e37669bad..6f51330f3 100644
--- a/theories/Numbers/Natural/Axioms/NOtherInd.v
+++ b/theories/Numbers/Natural/Axioms/NOtherInd.v
@@ -1,5 +1,6 @@
 Require Export NDomain.
 Declare Module Export DomainModule : DomainSignature.
+Open Local Scope NScope.
 
 Parameter O : N.
 Parameter S : N -> N.
diff --git a/theories/Numbers/Natural/Axioms/NPlus.v b/theories/Numbers/Natural/Axioms/NPlus.v
index 29b65e3f4..d2ef81018 100644
--- a/theories/Numbers/Natural/Axioms/NPlus.v
+++ b/theories/Numbers/Natural/Axioms/NPlus.v
@@ -2,10 +2,13 @@ Require Export NAxioms.
 
 Module Type PlusSignature.
 Declare Module Export NatModule : NatSignature.
+(* We use Export here because if we have an access to plus,
+then we need also an access to S and N *)
+Open Local Scope NScope.
 
 Parameter Inline plus : N -> N -> N.
 
-Notation "x + y" := (plus x y).
+Notation "x + y" := (plus x y) : NScope.
 
 Add Morphism plus with signature E ==> E ==> E as plus_wd.
 
@@ -14,11 +17,11 @@ Axiom plus_Sn_m : forall n m, (S n) + m == S (n + m).
 
 End PlusSignature.
 
-Module PlusProperties (Export PlusModule : PlusSignature).
-
+Module PlusProperties (Import PlusModule : PlusSignature).
 Module Export NatPropertiesModule := NatProperties NatModule.
+Open Local Scope NScope.
 
-Lemma plus_0_r : forall n, n + 0 == n.
+Theorem plus_0_r : forall n, n + 0 == n.
 Proof.
 induct n.
 now rewrite plus_0_n.
@@ -27,13 +30,13 @@ rewrite plus_Sn_m.
 now rewrite IH.
 Qed.
 
-Lemma plus_0_l : forall n, 0 + n == n.
+Theorem plus_0_l : forall n, 0 + n == n.
 Proof.
 intro n.
 now rewrite plus_0_n.
 Qed.
 
-Lemma plus_n_Sm : forall n m, n + S m == S (n + m).
+Theorem plus_n_Sm : forall n m, n + S m == S (n + m).
 Proof.
 intros n m; generalize n; clear n. induct n.
 now repeat rewrite plus_0_n.
@@ -41,13 +44,13 @@ intros x IH.
 repeat rewrite plus_Sn_m; now rewrite IH.
 Qed.
 
-Lemma plus_Sn_m : forall n m, S n + m == S (n + m).
+Theorem plus_Sn_m : forall n m, S n + m == S (n + m).
 Proof.
 intros.
 now rewrite plus_Sn_m.
 Qed.
 
-Lemma plus_comm : forall n m, n + m == m + n.
+Theorem plus_comm : forall n m, n + m == m + n.
 Proof.
 intros n m; generalize n; clear n. induct n.
 rewrite plus_0_l; now rewrite plus_0_r.
@@ -55,7 +58,7 @@ intros x IH.
 rewrite plus_Sn_m; rewrite plus_n_Sm; now rewrite IH.
 Qed.
 
-Lemma plus_assoc : forall n m p, n + (m + p) == (n + m) + p.
+Theorem plus_assoc : forall n m p, n + (m + p) == (n + m) + p.
 Proof.
 intros n m p; generalize n; clear n. induct n.
 now repeat rewrite plus_0_l.
@@ -63,24 +66,39 @@ intros x IH.
 repeat rewrite plus_Sn_m; now rewrite IH.
 Qed.
 
-Lemma plus_1_l : forall n, 1 + n == S n.
+Theorem plus_shuffle1 : forall n m p q, (n + m) + (p + q) == (n + p) + (m + q).
+Proof.
+intros n m p q.
+rewrite <- (plus_assoc n m (p + q)). rewrite (plus_comm m (p + q)).
+rewrite <- (plus_assoc p q m). rewrite (plus_assoc n p (q + m)).
+now rewrite (plus_comm q m).
+Qed.
+
+Theorem plus_shuffle2 : forall n m p q, (n + m) + (p + q) == (n + q) + (m + p).
+Proof.
+intros n m p q.
+rewrite <- (plus_assoc n m (p + q)). rewrite (plus_assoc m p q).
+rewrite (plus_comm (m + p) q). now rewrite <- (plus_assoc n q (m + p)).
+Qed.
+
+Theorem plus_1_l : forall n, 1 + n == S n.
 Proof.
 intro n; rewrite plus_Sn_m; now rewrite plus_0_n.
 Qed.
 
-Lemma plus_1_r : forall n, n + 1 == S n.
+Theorem plus_1_r : forall n, n + 1 == S n.
 Proof.
 intro n; rewrite plus_comm; apply plus_1_l.
 Qed.
 
-Lemma plus_cancel_l : forall n m p, p + n == p + m -> n == m.
+Theorem plus_cancel_l : forall n m p, p + n == p + m -> n == m.
 Proof.
 induct p.
 do 2 rewrite plus_0_n; trivial.
 intros p IH H. do 2 rewrite plus_Sn_m in H. apply S_inj in H. now apply IH.
 Qed.
 
-Lemma plus_cancel_r : forall n m p, n + p == m + p -> n == m.
+Theorem plus_cancel_r : forall n m p, n + p == m + p -> n == m.
 Proof.
 intros n m p.
 rewrite plus_comm.
@@ -88,7 +106,7 @@ set (k := p + n); rewrite plus_comm; unfold k.
 apply plus_cancel_l.
 Qed.
 
-Lemma plus_eq_0 : forall n m, n + m == 0 -> n == 0 /\ m == 0.
+Theorem plus_eq_0 : forall n m, n + m == 0 -> n == 0 /\ m == 0.
 Proof.
 intros n m; induct n.
 rewrite plus_0_n; now split.
@@ -96,7 +114,7 @@ intros n IH H. rewrite plus_Sn_m in H.
 absurd_hyp H; [|assumption]. unfold not; apply S_0.
 Qed.
 
-Lemma succ_plus_discr : forall n m, m # S (n + m).
+Theorem succ_plus_discr : forall n m, m # S (n + m).
 Proof.
 intro n; induct m.
 intro H. apply S_0 with (n := (n + 0)). now apply (proj2 (proj2 E_equiv)). (* symmetry *)
@@ -104,19 +122,19 @@ intros m IH H. apply S_inj in H. rewrite plus_n_Sm in H.
 unfold not in IH; now apply IH.
 Qed.
 
-Lemma n_SSn : forall n, n # S (S n).
+Theorem n_SSn : forall n, n # S (S n).
 Proof.
 intro n. pose proof (succ_plus_discr 1 n) as H.
 rewrite plus_Sn_m in H; now rewrite plus_0_n in H.
 Qed.
 
-Lemma n_SSSn : forall n, n # S (S (S n)).
+Theorem n_SSSn : forall n, n # S (S (S n)).
 Proof.
 intro n. pose proof (succ_plus_discr (S (S 0)) n) as H.
 do 2 rewrite plus_Sn_m in H. now rewrite plus_0_n in H.
 Qed.
 
-Lemma n_SSSSn : forall n, n # S (S (S (S n))).
+Theorem n_SSSSn : forall n, n # S (S (S (S n))).
 Proof.
 intro n. pose proof (succ_plus_discr (S (S (S 0))) n) as H.
 do 3 rewrite plus_Sn_m in H. now rewrite plus_0_n in H.
@@ -138,7 +156,7 @@ Qed.
 
 Definition plus_eq_1_dec (m n : N) : bool := recursion true (fun _ _ => false) m.
 
-Lemma plus_eq_1_dec_step_wd : fun2_wd E eq_bool eq_bool (fun _ _ => false).
+Theorem plus_eq_1_dec_step_wd : fun2_wd E eq_bool eq_bool (fun _ _ => false).
 Proof.
 unfold fun2_wd; intros. unfold eq_bool. reflexivity.
 Qed.
@@ -153,13 +171,13 @@ unfold eq_fun2; unfold eq_bool; reflexivity.
 assumption.
 Qed.
 
-Lemma plus_eq_1_dec_0 : forall n, plus_eq_1_dec 0 n = true.
+Theorem plus_eq_1_dec_0 : forall n, plus_eq_1_dec 0 n = true.
 Proof.
 intro n. unfold plus_eq_1_dec.
 now apply recursion_0.
 Qed.
 
-Lemma plus_eq_1_dec_S : forall m n, plus_eq_1_dec (S n) m = false.
+Theorem plus_eq_1_dec_S : forall m n, plus_eq_1_dec (S n) m = false.
 Proof.
 intros n m. unfold plus_eq_1_dec.
 now rewrite (recursion_S eq_bool);
diff --git a/theories/Numbers/Natural/Axioms/NPlusLt.v b/theories/Numbers/Natural/Axioms/NPlusLt.v
index ac322a8f2..77bd80012 100644
--- a/theories/Numbers/Natural/Axioms/NPlusLt.v
+++ b/theories/Numbers/Natural/Axioms/NPlusLt.v
@@ -1,12 +1,12 @@
 Require Export NPlus.
 Require Export NLt.
 
-Module PlusLtProperties (Export PlusModule : PlusSignature)
-                        (Export LtModule : LtSignature with
+Module PlusLtProperties (Import PlusModule : PlusSignature)
+                        (Import LtModule : LtSignature with
                            Module NatModule := PlusModule.NatModule).
-
 Module Export PlusPropertiesModule := PlusProperties PlusModule.
 Module Export LtPropertiesModule := LtProperties LtModule.
+Open Local Scope NScope.
 
 (* Print All locks up here !!! *)
 Theorem lt_plus_trans : forall n m p, n < m -> n < m + p.
diff --git a/theories/Numbers/Natural/Axioms/NStrongRec.v b/theories/Numbers/Natural/Axioms/NStrongRec.v
index a97dca9a5..5e8223108 100644
--- a/theories/Numbers/Natural/Axioms/NStrongRec.v
+++ b/theories/Numbers/Natural/Axioms/NStrongRec.v
@@ -1,7 +1,8 @@
 Require Import NAxioms.
 
-Module StrongRecProperties (Export NatModule : NatSignature).
+Module StrongRecProperties (Import NatModule : NatSignature).
 Module Export DomainPropertiesModule := DomainProperties NatModule.DomainModule.
+Open Local Scope NScope.
 
 Section StrongRecursion.
 
diff --git a/theories/Numbers/Natural/Axioms/NTimes.v b/theories/Numbers/Natural/Axioms/NTimes.v
index a47070083..6a7e9ba39 100644
--- a/theories/Numbers/Natural/Axioms/NTimes.v
+++ b/theories/Numbers/Natural/Axioms/NTimes.v
@@ -2,10 +2,11 @@ Require Export NPlus.
 
 Module Type TimesSignature.
 Declare Module Export PlusModule : PlusSignature.
+Open Local Scope NScope.
 
 Parameter Inline times : N -> N -> N.
 
-Notation "x * y" := (times x y).
+Notation "x * y" := (times x y) : NScope.
 
 Add Morphism times with signature E ==> E ==> E as times_wd.
 
@@ -14,9 +15,9 @@ Axiom times_Sn_m : forall n m, (S n) * m == m + n * m.
 
 End TimesSignature.
 
-Module TimesProperties (Export TimesModule : TimesSignature).
-
+Module TimesProperties (Import TimesModule : TimesSignature).
 Module Export PlusPropertiesModule := PlusProperties PlusModule.
+Open Local Scope NScope.
 
 Theorem mult_0_r : forall n, n * 0 == 0.
 Proof.
diff --git a/theories/Numbers/Natural/Axioms/NTimesLt.v b/theories/Numbers/Natural/Axioms/NTimesLt.v
index e67b5bb2a..c728f05a8 100644
--- a/theories/Numbers/Natural/Axioms/NTimesLt.v
+++ b/theories/Numbers/Natural/Axioms/NTimesLt.v
@@ -2,13 +2,13 @@ Require Export NLt.
 Require Export NTimes.
 Require Export NPlusLt.
 
-Module TimesLtProperties (Export TimesModule : TimesSignature)
-                         (Export LtModule : LtSignature with
+Module TimesLtProperties (Import TimesModule : TimesSignature)
+                         (Import LtModule : LtSignature with
                             Module NatModule := TimesModule.PlusModule.NatModule).
-
 Module Export TimesPropertiesModule := TimesProperties TimesModule.
 Module Export LtPropertiesModule := LtProperties LtModule.
 Module Export PlusLtPropertiesModule := PlusLtProperties TimesModule.PlusModule LtModule.
+Open Local Scope NScope.
 
 Lemma mult_S_lt_compat_l : forall n m p, m < p -> S n * m < S n * p.
 Proof.
diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v
index 403521e7c..057a0e5ac 100644
--- a/theories/Numbers/Natural/Peano/NPeano.v
+++ b/theories/Numbers/Natural/Peano/NPeano.v
@@ -6,7 +6,10 @@ Require Import NPlusLt.
 Require Import NTimesLt.
 Require Import NMiscFunct.
 
-Module PeanoDomain <: DomainEqSignature.
+Module PeanoDomain : DomainEqSignature
+  with Definition N := nat
+  with Definition E := (@eq nat)
+  with Definition e := eq_nat_bool.
 
 Definition N := nat.
 Definition E := (@eq nat).
@@ -28,14 +31,22 @@ Add Relation N E
 as E_rel.
 
 End PeanoDomain.
+Open Scope NScope.
+Import PeanoDomain.
 
 Module PeanoNat <: NatSignature.
-
 Module Export DomainModule := PeanoDomain.
 
 Definition O := 0.
 Definition S := S.
 
+(* For the following line, it is important that we declared
+PeanoDomain module above to be transparent, i.e., we used "<:"
+operator intead of ":". If we used ":", then the value of N, i.e.,
+nat, would not be visible here. Therefore, the type of E, which is
+N -> N -> Prop, would not be coercible to nat -> nat -> Prop.
+So we would not be able to claim that S is a morphism with respect
+to E. The same goes for defining * in terms of +, etc. *)
 Add Morphism S with signature E ==> E as S_wd.
 Proof.
 congruence.