3 files changed, 140 insertions, 3 deletions

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 *)