quelques adaptations de Zarith en vu de la nouvelle librarie FSet

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

5 files changed, 144 insertions, 7 deletions

diff --git a/.depend.coq b/.depend.coq
index 8e9049fad..df150c945 100644
--- a/.depend.coq
+++ b/.depend.coq
@@ -107,7 +107,7 @@ theories/Bool/DecBool.vo: theories/Bool/DecBool.v
 theories/Bool/Sumbool.vo: theories/Bool/Sumbool.v
 theories/Bool/BoolEq.vo: theories/Bool/BoolEq.v theories/Bool/Bool.vo
 theories/Bool/Bvector.vo: theories/Bool/Bvector.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Arith/Arith.vo
-theories/ZArith/Wf_Z.vo: theories/ZArith/Wf_Z.v theories/ZArith/fast_integer.vo theories/ZArith/zarith_aux.vo theories/ZArith/auxiliary.vo theories/ZArith/Zsyntax.vo
+theories/ZArith/Wf_Z.vo: theories/ZArith/Wf_Z.v theories/ZArith/fast_integer.vo theories/ZArith/zarith_aux.vo theories/ZArith/auxiliary.vo theories/ZArith/Zsyntax.vo theories/ZArith/Zmisc.vo theories/Arith/Wf_nat.vo
 theories/ZArith/Zsyntax.vo: theories/ZArith/Zsyntax.v theories/ZArith/fast_integer.vo theories/ZArith/zarith_aux.vo
 theories/ZArith/ZArith.vo: theories/ZArith/ZArith.v theories/ZArith/ZArith_base.vo theories/ZArith/Zcomplements.vo theories/ZArith/Zsqrt.vo theories/ZArith/Zpower.vo theories/ZArith/Zdiv.vo theories/ZArith/Zlogarithm.vo theories/ZArith/Zbool.vo
 theories/ZArith/auxiliary.vo: theories/ZArith/auxiliary.v theories/Arith/Arith.vo theories/ZArith/fast_integer.vo theories/ZArith/zarith_aux.vo theories/Logic/Decidable.vo theories/Arith/Peano_dec.vo theories/Arith/Compare_dec.vo
@@ -118,7 +118,7 @@ theories/ZArith/zarith_aux.vo: theories/ZArith/zarith_aux.v theories/Arith/Arith
 theories/ZArith/Zhints.vo: theories/ZArith/Zhints.v theories/ZArith/zarith_aux.vo theories/ZArith/auxiliary.vo theories/ZArith/Zsyntax.vo theories/ZArith/Zmisc.vo theories/ZArith/Wf_Z.vo
 theories/ZArith/Zlogarithm.vo: theories/ZArith/Zlogarithm.v theories/ZArith/ZArith_base.vo contrib/omega/Omega.vo theories/ZArith/Zcomplements.vo theories/ZArith/Zpower.vo
 theories/ZArith/Zpower.vo: theories/ZArith/Zpower.v theories/ZArith/ZArith_base.vo contrib/omega/Omega.vo theories/ZArith/Zcomplements.vo
-theories/ZArith/Zcomplements.vo: theories/ZArith/Zcomplements.v theories/ZArith/ZArith_base.vo contrib/ring/ZArithRing.vo contrib/omega/Omega.vo theories/Arith/Wf_nat.vo
+theories/ZArith/Zcomplements.vo: theories/ZArith/Zcomplements.v theories/ZArith/ZArith_base.vo contrib/ring/ZArithRing.vo contrib/omega/Omega.vo theories/Arith/Wf_nat.vo theories/Lists/PolyList.vo
 theories/ZArith/Zdiv.vo: theories/ZArith/Zdiv.v theories/ZArith/ZArith_base.vo contrib/omega/Omega.vo contrib/ring/ZArithRing.vo theories/ZArith/Zcomplements.vo
 theories/ZArith/Zsqrt.vo: theories/ZArith/Zsqrt.v theories/ZArith/ZArith_base.vo contrib/ring/ZArithRing.vo contrib/omega/Omega.vo
 theories/ZArith/Zwf.vo: theories/ZArith/Zwf.v theories/ZArith/ZArith_base.vo theories/Arith/Wf_nat.vo contrib/omega/Omega.vo
diff --git a/.depend.newcoq b/.depend.newcoq
index f9a76e286..9cdc3b1da 100644
--- a/.depend.newcoq
+++ b/.depend.newcoq
@@ -107,7 +107,7 @@ newtheories/Bool/DecBool.vo: newtheories/Bool/DecBool.v
 newtheories/Bool/Sumbool.vo: newtheories/Bool/Sumbool.v
 newtheories/Bool/BoolEq.vo: newtheories/Bool/BoolEq.v newtheories/Bool/Bool.vo
 newtheories/Bool/Bvector.vo: newtheories/Bool/Bvector.v newtheories/Bool/Bool.vo newtheories/Bool/Sumbool.vo newtheories/Arith/Arith.vo
-newtheories/ZArith/Wf_Z.vo: newtheories/ZArith/Wf_Z.v newtheories/ZArith/fast_integer.vo newtheories/ZArith/zarith_aux.vo newtheories/ZArith/auxiliary.vo newtheories/ZArith/Zsyntax.vo
+newtheories/ZArith/Wf_Z.vo: newtheories/ZArith/Wf_Z.v newtheories/ZArith/fast_integer.vo newtheories/ZArith/zarith_aux.vo newtheories/ZArith/auxiliary.vo newtheories/ZArith/Zsyntax.vo newtheories/ZArith/Zmisc.vo newtheories/Arith/Wf_nat.vo
 newtheories/ZArith/Zsyntax.vo: newtheories/ZArith/Zsyntax.v newtheories/ZArith/fast_integer.vo newtheories/ZArith/zarith_aux.vo
 newtheories/ZArith/ZArith.vo: newtheories/ZArith/ZArith.v newtheories/ZArith/ZArith_base.vo newtheories/ZArith/Zcomplements.vo newtheories/ZArith/Zsqrt.vo newtheories/ZArith/Zpower.vo newtheories/ZArith/Zdiv.vo newtheories/ZArith/Zlogarithm.vo newtheories/ZArith/Zbool.vo
 newtheories/ZArith/auxiliary.vo: newtheories/ZArith/auxiliary.v newtheories/Arith/Arith.vo newtheories/ZArith/fast_integer.vo newtheories/ZArith/zarith_aux.vo newtheories/Logic/Decidable.vo newtheories/Arith/Peano_dec.vo newtheories/Arith/Compare_dec.vo
@@ -118,7 +118,7 @@ newtheories/ZArith/zarith_aux.vo: newtheories/ZArith/zarith_aux.v newtheories/Ar
 newtheories/ZArith/Zhints.vo: newtheories/ZArith/Zhints.v newtheories/ZArith/zarith_aux.vo newtheories/ZArith/auxiliary.vo newtheories/ZArith/Zsyntax.vo newtheories/ZArith/Zmisc.vo newtheories/ZArith/Wf_Z.vo
 newtheories/ZArith/Zlogarithm.vo: newtheories/ZArith/Zlogarithm.v newtheories/ZArith/ZArith_base.vo newcontrib/omega/Omega.vo newtheories/ZArith/Zcomplements.vo newtheories/ZArith/Zpower.vo
 newtheories/ZArith/Zpower.vo: newtheories/ZArith/Zpower.v newtheories/ZArith/ZArith_base.vo newcontrib/omega/Omega.vo newtheories/ZArith/Zcomplements.vo
-newtheories/ZArith/Zcomplements.vo: newtheories/ZArith/Zcomplements.v newtheories/ZArith/ZArith_base.vo newcontrib/ring/ZArithRing.vo newcontrib/omega/Omega.vo newtheories/Arith/Wf_nat.vo
+newtheories/ZArith/Zcomplements.vo: newtheories/ZArith/Zcomplements.v newtheories/ZArith/ZArith_base.vo newcontrib/ring/ZArithRing.vo newcontrib/omega/Omega.vo newtheories/Arith/Wf_nat.vo newtheories/Lists/PolyList.vo
 newtheories/ZArith/Zdiv.vo: newtheories/ZArith/Zdiv.v newtheories/ZArith/ZArith_base.vo newcontrib/omega/Omega.vo newcontrib/ring/ZArithRing.vo newtheories/ZArith/Zcomplements.vo
 newtheories/ZArith/Zsqrt.vo: newtheories/ZArith/Zsqrt.v newtheories/ZArith/ZArith_base.vo newcontrib/ring/ZArithRing.vo newcontrib/omega/Omega.vo
 newtheories/ZArith/Zwf.vo: newtheories/ZArith/Zwf.v newtheories/ZArith/ZArith_base.vo newtheories/Arith/Wf_nat.vo newcontrib/omega/Omega.vo
diff --git a/theories/ZArith/Wf_Z.v b/theories/ZArith/Wf_Z.v
index 035e16f22..5dfc8ac8e 100644
--- a/theories/ZArith/Wf_Z.v
+++ b/theories/ZArith/Wf_Z.v
@@ -12,6 +12,8 @@ Require fast_integer.
 Require zarith_aux.
 Require auxiliary.
 Require Zsyntax.
+Require Zmisc.
+Require Wf_nat.
 V7only [Import Z_scope.].
 Open Local Scope Z_scope.
 
@@ -122,6 +124,44 @@ Intros; Apply inject_nat_set;
 | Assumption].
 Qed.
 
+Section natlike_rec2. 
+(** [natlike_rec2] is the same as [natlike_rec], but with a different proof, designed 
+     to give a better extracted term. *)
+
+Local R := [a,b:Z]`0<=a`/\`a=(Zpred b)`.
+
+Local R_wf : (well_founded Z R).
+Proof.
+LetTac f := [z]Cases z of (POS p) => (convert p) | ZERO => O | (NEG _) => O end.
+Apply  well_founded_lt_compat with f.
+Unfold R f.
+Intros x y; Case x.
+Intuition; Rewrite (Zs_pred y); Rewrite <- H1; Simpl; Apply compare_convert_O.
+Case y; Intuition; Try Solve [ Simpl in H2; Inversion H2 ].
+Assert (POS p) = (POS (add_un p0)).
+ Rewrite add_un_Zs; Rewrite H2; Auto with zarith.
+Inversion_clear H0; Unfold convert; Rewrite convert_add_un.
+Change 1 (positive_to_nat p0 (1)) with (plus (0) (positive_to_nat p0 (1))).
+Apply lt_reg_r; Auto.
+Intuition; Elim H1; Simpl; Trivial.
+Qed.
+
+Lemma Z_rec : (P:Z->Type)(P `0`) -> 
+        ((z:Z)`0<z` -> (P (Zpred z)) -> (P z)) -> (z:Z)`0<=z` -> (P z).
+Proof.
+Intros P Ho Hrec z; Pattern z; Apply (well_founded_induction_type Z R R_wf).
+Intro x; Case x.
+Trivial.
+Intros; Apply Hrec.
+Unfold Zlt; Simpl; Trivial.
+Assert `0<=(Zpred (POS p))`.
+Apply Zlt_ZERO_pred_le_ZERO; Unfold Zlt; Simpl; Trivial.
+Apply X; Unfold R; Intuition.
+Intros; Elim H; Simpl; Trivial.
+Qed.
+
+End natlike_rec2.
+
 Lemma Z_lt_induction : 
   (P:Z->Prop)
      ((x:Z)((y:Z)`0 <= y < x`->(P y))->(P x))
diff --git a/theories/ZArith/Zcomplements.v b/theories/ZArith/Zcomplements.v
index 954347d89..e49131a4c 100644
--- a/theories/ZArith/Zcomplements.v
+++ b/theories/ZArith/Zcomplements.v
@@ -283,3 +283,47 @@ Apply Zge_Zmult_pos_compat; Omega.
 Ring.
 Omega.
 Save.
+
+(** A list length in Z, tail recursive.  *)
+Require PolyList.
+
+Fixpoint Zlength_aux [acc: Z; A: Set; l:(list A)] : Z := Cases l of 
+    nil => acc
+  | (cons _ l) => (Zlength_aux (Zs acc) A l)
+end. 
+
+Definition Zlength := (Zlength_aux 0).
+Implicits Zlength [1].
+
+Lemma Zlength_correct : (A:Set)(l:(list A))(Zlength l)=(inject_nat (length l)).
+Proof.
+Assert (A:Set)(l:(list A))(acc:Z)(Zlength_aux acc A l)=acc+(inject_nat (length l)). 
+Induction l.
+Simpl; Auto with zarith.
+Intros; Simpl (length (cons a l0)); Rewrite inj_S.
+Simpl; Rewrite H; Auto with zarith.
+Unfold Zlength; Intros; Rewrite H; Auto.
+Qed.
+Implicits Zlength_correct [1].
+
+Lemma Zlength_nil : (A:Set)(x:A)(l:(list A))(Zlength (nil A))=0.
+Proof.
+Auto.
+Qed.
+
+Lemma Zlength_cons : (A:Set)(x:A)(l:(list A))(Zlength (cons x l))=(Zs (Zlength l)).
+Proof.
+Intros; Do 2 Rewrite Zlength_correct.
+Simpl (length (cons x l)); Rewrite inj_S; Auto.
+Qed.
+Implicits Zlength_cons [1].
+
+Lemma Zlength_nil_inv : (A:Set)(l:(list A))(Zlength l)=0 -> l=(nil ?).
+Proof.
+Intros A l; Rewrite Zlength_correct.
+Case l; Auto.
+Intros x l'; Simpl (length (cons x l')).
+Rewrite inj_S.
+Intros; ElimType False; Generalize (ZERO_le_inj (length l')); Omega.
+Qed.
+Implicits Zlength_nil_inv [1].
diff --git a/theories/ZArith/Zmisc.v b/theories/ZArith/Zmisc.v
index 414a230f0..9b5eb9260 100644
--- a/theories/ZArith/Zmisc.v
+++ b/theories/ZArith/Zmisc.v
@@ -298,6 +298,30 @@ Proof.
   NewDestruct z; [ Idtac | NewDestruct p | NewDestruct p  ]; Compute; Trivial.
 Qed.
 
+Lemma Zeven_Sn : (z:Z)(Zeven z) -> (Zodd (Zs z)).
+Proof.
+ NewDestruct z; Unfold Zs; [ Idtac | NewDestruct p | NewDestruct p  ]; Simpl; Trivial. 
+ Unfold double_moins_un; Case p; Simpl; Auto.
+Qed.
+
+Lemma Zodd_Sn : (z:Z)(Zodd z) -> (Zeven (Zs z)).
+Proof.
+ NewDestruct z; Unfold Zs; [ Idtac | NewDestruct p | NewDestruct p  ]; Simpl; Trivial. 
+ Unfold double_moins_un; Case p; Simpl; Auto.
+Qed.
+
+Lemma Zeven_pred : (z:Z)(Zeven z) -> (Zodd (Zpred z)).
+Proof.
+ NewDestruct z; Unfold Zpred; [ Idtac | NewDestruct p | NewDestruct p  ]; Simpl; Trivial. 
+ Unfold double_moins_un; Case p; Simpl; Auto.
+Qed.
+
+Lemma Zodd_pred : (z:Z)(Zodd z) -> (Zeven (Zpred z)).
+Proof.
+ NewDestruct z; Unfold Zpred; [ Idtac | NewDestruct p | NewDestruct p  ]; Simpl; Trivial. 
+ Unfold double_moins_un; Case p; Simpl; Auto.
+Qed.
+
 Hints Unfold Zeven Zodd : zarith.
 
 (** [Zdiv2] is defined on all [Z], but notice that for odd negative integers
@@ -338,12 +362,41 @@ Intros. Absurd (Zodd (POS (xO p))); Red; Auto with arith.
 Intros. Absurd `(NEG p) >= 0`; Red; Auto with arith.
 Qed.
 
-Lemma Z_modulo_2 : (x:Z) `x >= 0` -> { y:Z | `x=2*y` }+{ y:Z | `x=2*y+1` }.
+Lemma Zodd_div2_neg : (x:Z) `x <= 0` -> (Zodd x) -> `x = 2*(Zdiv2 x)-1`.
 Proof.
-Intros x Hx.
+NewDestruct x.
+Intros. Absurd (Zodd `0`); Red; Auto with arith.
+Intros. Absurd `(NEG p) >= 0`; Red; Auto with arith.
+NewDestruct p; Auto with arith.
+Intros. Absurd (Zodd (NEG (xO p))); Red; Auto with arith.
+Qed.
+
+Lemma Z_modulo_2 : (x:Z) { y:Z | `x=2*y` }+{ y:Z | `x=2*y+1` }.
+Proof.
+Intros x.
 Elim (Zeven_odd_dec x); Intro.
 Left. Split with (Zdiv2 x). Exact (Zeven_div2 x a).
-Right. Split with (Zdiv2 x). Exact (Zodd_div2 x Hx b).
+Right. Generalize b; Clear b; Case x.
+Intro b; Inversion b.
+Intro p; Split with (Zdiv2 (POS p)). Apply (Zodd_div2 (POS p)); Trivial.
+Unfold Zge Zcompare; Simpl; Discriminate.
+Intro p; Split with (Zdiv2 (Zpred (NEG p))).
+Pattern 1 (NEG p); Rewrite (Zs_pred (NEG p)).
+Pattern 1 (Zpred (NEG p)); Rewrite (Zeven_div2 (Zpred (NEG p))).
+Reflexivity.
+Apply Zodd_pred; Assumption.
+Qed.
+
+Lemma Zsplit2 :  (x:Z) { p : Z*Z | let (x1,x2)=p in (`x=x1+x2` /\ (x1=x2 \/ `x2=x1+1`)) }.
+Proof.
+Intros x.
+Elim (Z_modulo_2 x); Intros (y,Hy); Rewrite Zmult_sym in Hy; Rewrite <- Zred_factor1 in Hy.
+Exists (y,y); Split. 
+Assumption.
+Left; Reflexivity.
+Exists (y,y+`1`); Split.
+Rewrite Zplus_assoc; Assumption.
+Right; Reflexivity.
 Qed.
 
 (* Very simple *)