diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-06-13 10:55:34 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-06-13 10:55:34 +0000 |
commit | 4ea5e9e7a3c08adabb0fb5113f849ffdd48ed172 (patch) | |
tree | 9732e425092cf8accb6de78bc7b0a70aef84ffe2 /theories/ZArith | |
parent | 10ce67c81ae6da0e1c895a5b7ef500f724a34c1a (diff) |
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
Diffstat (limited to 'theories/ZArith')
-rw-r--r-- | theories/ZArith/Wf_Z.v | 40 | ||||
-rw-r--r-- | theories/ZArith/Zcomplements.v | 44 | ||||
-rw-r--r-- | theories/ZArith/Zmisc.v | 59 |
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 *) |