Update on numbers.

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

9 files changed, 93 insertions, 224 deletions

diff --git a/theories/Numbers/Integer/Axioms/ZAxioms.v b/theories/Numbers/Integer/Axioms/ZAxioms.v
index 4f0eab8e35..b734102563 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 00eab8842f..b48684ba88 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 b1983d6f7f..3bf4d61f5a 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 1b5aa73fb2..f455400b78 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 abaaa664f7..4f677355bc 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 3f9c7c4ce6..ff0de61960 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 1f8b0a9478..460a13bf41 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 673a1fe50d..0000000000
--- 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 d2634970db..02f73f4d1e 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).