diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-05 13:43:45 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-05 13:43:45 +0000 |
| commit | b1e1be15990aef3fd76b28fad3d52cf6bc36a60b (patch) | |
| tree | d9d4944e0cd7267e99583405a63b6f72c53f6182 | |
| parent | 380a8c4a8e7fb56fa105a76694f60f262d27d1a1 (diff) | |
Restructuration ZArith et déport de la partie sur 'positive' dans NArith, de la partie Omega dans contrib/omega
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4801 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | theories/ZArith/Wf_Z.v | 1 | ||||
| -rw-r--r-- | theories/ZArith/ZArith_base.v | 4 | ||||
| -rw-r--r-- | theories/ZArith/ZArith_dec.v | 1 | ||||
| -rw-r--r-- | theories/ZArith/Zabs.v | 85 | ||||
| -rw-r--r-- | theories/ZArith/Zcomplements.v | 76 | ||||
| -rw-r--r-- | theories/ZArith/Zeven.v | 184 | ||||
| -rw-r--r-- | theories/ZArith/Zhints.v | 4 | ||||
| -rw-r--r-- | theories/ZArith/Zlogarithm.v | 1 | ||||
| -rw-r--r-- | theories/ZArith/Zmin.v | 74 | ||||
| -rw-r--r-- | theories/ZArith/Zmisc.v | 168 | ||||
| -rw-r--r-- | theories/ZArith/Zorder.v | 922 | ||||
| -rw-r--r-- | theories/ZArith/Zsqrt.v | 3 | ||||
| -rw-r--r-- | theories/ZArith/Zsyntax.v | 11 | ||||
| -rw-r--r-- | theories/ZArith/auxiliary.v | 614 | ||||
| -rw-r--r-- | theories/ZArith/fast_integer.v | 1506 | ||||
| -rw-r--r-- | theories/ZArith/zarith_aux.v | 893 |
16 files changed, 1492 insertions, 3055 deletions
diff --git a/theories/ZArith/Wf_Z.v b/theories/ZArith/Wf_Z.v index 56f8485da..452855a11 100644 --- a/theories/ZArith/Wf_Z.v +++ b/theories/ZArith/Wf_Z.v @@ -9,6 +9,7 @@ (*i $Id$ i*) Require fast_integer. +Require Zorder. Require zarith_aux. Require auxiliary. Require Zsyntax. diff --git a/theories/ZArith/ZArith_base.v b/theories/ZArith/ZArith_base.v index e17bcbe2a..3ef24e61e 100644 --- a/theories/ZArith/ZArith_base.v +++ b/theories/ZArith/ZArith_base.v @@ -14,6 +14,10 @@ Require Export fast_integer. Require Export zarith_aux. +Require Export Zorder. +Require Export Zeven. +Require Export Zmin. +Require Export Zabs. Require Export auxiliary. Require Export Zsyntax. Require Export ZArith_dec. diff --git a/theories/ZArith/ZArith_dec.v b/theories/ZArith/ZArith_dec.v index 88e7c325d..5507acdb2 100644 --- a/theories/ZArith/ZArith_dec.v +++ b/theories/ZArith/ZArith_dec.v @@ -11,6 +11,7 @@ Require Sumbool. Require fast_integer. +Require Zorder. Require zarith_aux. Require auxiliary. Require Zsyntax. diff --git a/theories/ZArith/Zabs.v b/theories/ZArith/Zabs.v new file mode 100644 index 000000000..d3d3efac1 --- /dev/null +++ b/theories/ZArith/Zabs.v @@ -0,0 +1,85 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) +(*i $Id$ i*) + +(** Binary Integers (Pierre Crégut (CNET, Lannion, France) *) + +Require Arith. +Require fast_integer. +Require Zorder. + +V7only [Import nat_scope.]. +Open Local Scope Z_scope. + +(**********************************************************************) +(** Properties of absolute value *) + +Lemma Zabs_eq : (x:Z) (Zle ZERO x) -> (Zabs x)=x. +NewDestruct x; Auto with arith. +Compute; Intros; Absurd SUPERIEUR=SUPERIEUR; Trivial with arith. +Qed. + +Lemma Zabs_non_eq : (x:Z) (Zle x ZERO) -> (Zabs x)=(Zopp x). +Proof. +NewDestruct x; Auto with arith. +Compute; Intros; Absurd SUPERIEUR=SUPERIEUR; Trivial with arith. +Qed. + +Definition Zabs_dec : (x:Z){x=(Zabs x)}+{x=(Zopp (Zabs x))}. +Proof. +NewDestruct x;Auto with arith. +Defined. + +Lemma Zabs_pos : (x:Z)(Zle ZERO (Zabs x)). +NewDestruct x;Auto with arith; Compute; Intros H;Inversion H. +Qed. + +Lemma Zsgn_Zabs: (x:Z)(Zmult x (Zsgn x))=(Zabs x). +Proof. +NewDestruct x; Rewrite Zmult_sym; Auto with arith. +Qed. + +Lemma Zabs_Zsgn: (x:Z)(Zmult (Zabs x) (Zsgn x))=x. +Proof. +NewDestruct x; Rewrite Zmult_sym; Auto with arith. +Qed. + +(** absolute value in nat is compatible with order *) + +Lemma absolu_lt : (x,y:Z) (Zle ZERO x)/\(Zlt x y) -> (lt (absolu x) (absolu y)). +Proof. +Intros x y. Case x; Simpl. Case y; Simpl. + +Intro. Absurd (Zlt ZERO ZERO). Compute. Intro H0. Discriminate H0. Intuition. +Intros. Elim (ZL4 p). Intros. Rewrite H0. Auto with arith. +Intros. Elim (ZL4 p). Intros. Rewrite H0. Auto with arith. + +Case y; Simpl. +Intros. Absurd (Zlt (POS p) ZERO). Compute. Intro H0. Discriminate H0. Intuition. +Intros. Change (gt (convert p) (convert p0)). +Apply compare_convert_SUPERIEUR. +Elim H; Auto with arith. Intro. Exact (ZC2 p0 p). + +Intros. Absurd (Zlt (POS p0) (NEG p)). +Compute. Intro H0. Discriminate H0. Intuition. + +Intros. Absurd (Zle ZERO (NEG p)). Compute. Auto with arith. Intuition. +Qed. + +Lemma Zlt_minus : (n,m:Z)(Zlt ZERO m)->(Zlt (Zminus n m) n). +Proof. +Intros n m H; Apply Zsimpl_lt_plus_l with p:=m; Rewrite Zle_plus_minus; +Pattern 1 n ;Rewrite <- (Zero_right n); Rewrite (Zplus_sym m n); +Apply Zlt_reg_l; Assumption. +Qed. + +Lemma Zlt_O_minus_lt : (n,m:Z)(Zlt ZERO (Zminus n m))->(Zlt m n). +Proof. +Intros n m H; Apply Zsimpl_lt_plus_l with p:=(Zopp m); Rewrite Zplus_inverse_l; +Rewrite Zplus_sym;Exact H. +Qed. diff --git a/theories/ZArith/Zcomplements.v b/theories/ZArith/Zcomplements.v index a9c7ebfee..5b3e16968 100644 --- a/theories/ZArith/Zcomplements.v +++ b/theories/ZArith/Zcomplements.v @@ -15,80 +15,8 @@ Require Wf_nat. V7only [Import Z_scope.]. Open Local Scope Z_scope. -(** Multiplication by a number >0 preserves [Zcompare]. It also perserves - [Zle], [Zlt], [Zge], [Zgt] *) - -Set Implicit Arguments. - -Implicit Variable Type x,y,z:Z. - -Lemma Zgt0_le_pred : (y:Z) `y > 0` -> `0 <= (Zpred y)`. -Intro; Unfold Zpred; Omega. -Qed. - -Lemma Zlt_Zplus : - (x1,x2,y1,y2:Z)`x1 < x2` -> `y1 < y2` -> `x1 + y1 < x2 + y2`. -Intros; Omega. -Qed. - -Lemma Zlt_Zmult_right : (x,y,z:Z)`z>0` -> `x < y` -> `x*z < y*z`. - -Intros; Rewrite (Zs_pred z); Generalize (Zgt0_le_pred H); Intro; -Apply natlike_ind with P:=[z:Z]`x*(Zs z) < y*(Zs z)`; -[ Simpl; Do 2 (Rewrite Zmult_n_1); Assumption -| Unfold Zs; Intros x0 Hx0; Do 6 (Rewrite Zmult_plus_distr_r); - Repeat Rewrite Zmult_n_1; - Intro; Apply Zlt_Zplus; Assumption -| Assumption ]. -Qed. - -Lemma Zlt_Zmult_right2 : (x,y,z:Z)`z>0` -> `x*z < y*z` -> `x < y`. -Intros x y z H; Rewrite (Zs_pred z). -Apply natlike_ind with P:=[z:Z]`x*(Zs z) < y*(Zs z)`->`x < y`. -Simpl; Do 2 Rewrite Zmult_n_1; Auto 1. -Unfold Zs. -Intros x0 Hx0; Repeat Rewrite Zmult_plus_distr_r. -Repeat Rewrite Zmult_n_1. -Omega. (* Auto with zarith. *) -Unfold Zpred; Omega. -Qed. - -Lemma Zle_Zmult_right : (x,y,z:Z)`z>0` -> `x <= y` -> `x*z <= y*z`. -Intros x y z Hz Hxy. -Elim (Zle_lt_or_eq x y Hxy). -Intros; Apply Zlt_le_weak. -Apply Zlt_Zmult_right; Trivial. -Intros; Apply Zle_refl. -Rewrite H; Trivial. -Qed. - -Lemma Zle_Zmult_right2 : (x,y,z:Z)`z>0` -> `x*z <= y*z` -> `x <= y`. -Intros x y z Hz Hxy. -Elim (Zle_lt_or_eq `x*z` `y*z` Hxy). -Intros; Apply Zlt_le_weak. -Apply Zlt_Zmult_right2 with z; Trivial. -Intros; Apply Zle_refl. -Apply Zmult_reg_right with z; Omega. -Qed. - -Lemma Zgt_Zmult_right : (x,y,z:Z)`z>0` -> `x > y` -> `x*z > y*z`. - -Intros; Apply Zlt_gt; Apply Zlt_Zmult_right; -[ Assumption | Apply Zgt_lt ; Assumption ]. -Qed. - -Lemma Zlt_Zmult_left : (x,y,z:Z)`z>0` -> `x < y` -> `z*x < z*y`. - -Intros; -Rewrite (Zmult_sym z x); Rewrite (Zmult_sym z y); -Apply Zlt_Zmult_right; Assumption. -Qed. - -Lemma Zgt_Zmult_left : (x,y,z:Z)`z>0` -> `x > y` -> `z*x > z*y`. -Intros; -Rewrite (Zmult_sym z x); Rewrite (Zmult_sym z y); -Apply Zgt_Zmult_right; Assumption. -Qed. +(**********************************************************************) +(* Properties of comparison on Z *) Theorem Zcompare_Zmult_right : (x,y,z:Z)` z>0` -> `x ?= y`=`x*z ?= y*z`. diff --git a/theories/ZArith/Zeven.v b/theories/ZArith/Zeven.v new file mode 100644 index 000000000..38cefa520 --- /dev/null +++ b/theories/ZArith/Zeven.v @@ -0,0 +1,184 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(*i $Id$ i*) + +Require fast_integer. +Require Zsyntax. + +(**********************************************************************) +(** Even and odd predicates on Z, division by 2 on Z *) + +(**********************************************************************) +(** [Zeven], [Zodd], [Zdiv2] and their related properties *) + +Definition Zeven := + [z:Z]Cases z of ZERO => True + | (POS (xO _)) => True + | (NEG (xO _)) => True + | _ => False + end. + +Definition Zodd := + [z:Z]Cases z of (POS xH) => True + | (NEG xH) => True + | (POS (xI _)) => True + | (NEG (xI _)) => True + | _ => False + end. + +Definition Zeven_bool := + [z:Z]Cases z of ZERO => true + | (POS (xO _)) => true + | (NEG (xO _)) => true + | _ => false + end. + +Definition Zodd_bool := + [z:Z]Cases z of ZERO => false + | (POS (xO _)) => false + | (NEG (xO _)) => false + | _ => true + end. + +Definition Zeven_odd_dec : (z:Z) { (Zeven z) }+{ (Zodd z) }. +Proof. + Intro z. Case z; + [ Left; Compute; Trivial + | Intro p; Case p; Intros; + (Right; Compute; Exact I) Orelse (Left; Compute; Exact I) + | Intro p; Case p; Intros; + (Right; Compute; Exact I) Orelse (Left; Compute; Exact I) ]. +Defined. + +Definition Zeven_dec : (z:Z) { (Zeven z) }+{ ~(Zeven z) }. +Proof. + Intro z. Case z; + [ Left; Compute; Trivial + | Intro p; Case p; Intros; + (Left; Compute; Exact I) Orelse (Right; Compute; Trivial) + | Intro p; Case p; Intros; + (Left; Compute; Exact I) Orelse (Right; Compute; Trivial) ]. +Defined. + +Definition Zodd_dec : (z:Z) { (Zodd z) }+{ ~(Zodd z) }. +Proof. + Intro z. Case z; + [ Right; Compute; Trivial + | Intro p; Case p; Intros; + (Left; Compute; Exact I) Orelse (Right; Compute; Trivial) + | Intro p; Case p; Intros; + (Left; Compute; Exact I) Orelse (Right; Compute; Trivial) ]. +Defined. + +Lemma Zeven_not_Zodd : (z:Z)(Zeven z) -> ~(Zodd z). +Proof. + NewDestruct z; [ Idtac | NewDestruct p | NewDestruct p ]; Compute; Trivial. +Qed. + +Lemma Zodd_not_Zeven : (z:Z)(Zodd z) -> ~(Zeven z). +Proof. + NewDestruct z; [ Idtac | NewDestruct p | NewDestruct p ]; Compute; Trivial. +Qed. + +Lemma Zeven_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 Zodd_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 Zeven_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. + +Lemma Zodd_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. + +Hints Unfold Zeven Zodd : zarith. + +(**********************************************************************) +(** [Zdiv2] is defined on all [Z], but notice that for odd negative + integers it is not the euclidean quotient: in that case we have [n = + 2*(n/2)-1] *) + +Definition Zdiv2 := + [z:Z]Cases z of ZERO => ZERO + | (POS xH) => ZERO + | (POS p) => (POS (Zdiv2_pos p)) + | (NEG xH) => ZERO + | (NEG p) => (NEG (Zdiv2_pos p)) + end. + +Lemma Zeven_div2 : (x:Z) (Zeven x) -> `x = 2*(Zdiv2 x)`. +Proof. +NewDestruct x. +Auto with arith. +NewDestruct p; Auto with arith. +Intros. Absurd (Zeven (POS (xI p))); Red; Auto with arith. +Intros. Absurd (Zeven `1`); Red; Auto with arith. +NewDestruct p; Auto with arith. +Intros. Absurd (Zeven (NEG (xI p))); Red; Auto with arith. +Intros. Absurd (Zeven `-1`); Red; Auto with arith. +Qed. + +Lemma Zodd_div2 : (x:Z) `x >= 0` -> (Zodd x) -> `x = 2*(Zdiv2 x)+1`. +Proof. +NewDestruct x. +Intros. Absurd (Zodd `0`); Red; Auto with arith. +NewDestruct p; Auto with arith. +Intros. Absurd (Zodd (POS (xO p))); Red; Auto with arith. +Intros. Absurd `(NEG p) >= 0`; Red; Auto with arith. +Qed. + +Lemma Zodd_div2_neg : (x:Z) `x <= 0` -> (Zodd x) -> `x = 2*(Zdiv2 x)-1`. +Proof. +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. 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 Zeven_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 <- Zplus_Zmult_2 in Hy. +Exists (y,y); Split. +Assumption. +Left; Reflexivity. +Exists (y,`y+1`); Split. +Rewrite Zplus_assoc; Assumption. +Right; Reflexivity. +Qed. diff --git a/theories/ZArith/Zhints.v b/theories/ZArith/Zhints.v index 27e8fd5c2..8dc9069a6 100644 --- a/theories/ZArith/Zhints.v +++ b/theories/ZArith/Zhints.v @@ -27,6 +27,10 @@ (* Lemmas involving positive and compare are not taken into account *) +Require fast_integer. +Require Zorder. +Require Zmin. +Require Zabs. Require zarith_aux. Require auxiliary. Require Zsyntax. diff --git a/theories/ZArith/Zlogarithm.v b/theories/ZArith/Zlogarithm.v index 0fe380e71..2879fefe8 100644 --- a/theories/ZArith/Zlogarithm.v +++ b/theories/ZArith/Zlogarithm.v @@ -8,6 +8,7 @@ (*i $Id$ i*) +(**********************************************************************) (** The integer logarithms with base 2. There are three logarithms, diff --git a/theories/ZArith/Zmin.v b/theories/ZArith/Zmin.v new file mode 100644 index 000000000..b09299466 --- /dev/null +++ b/theories/ZArith/Zmin.v @@ -0,0 +1,74 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) +(*i $Id$ i*) + +(** Binary Integers (Pierre Crégut (CNET, Lannion, France) *) + +Require Arith. +Require fast_integer. +Require Zorder. + +Open Local Scope Z_scope. + +(**********************************************************************) +(** Minimum on binary integer numbers *) + +Definition Zmin := [n,m:Z] + <Z>Cases (Zcompare n m) of + EGAL => n + | INFERIEUR => n + | SUPERIEUR => m + end. + +(** Properties of minimum on binary integer numbers *) + +Lemma Zmin_SS : (n,m:Z)((Zs (Zmin n m))=(Zmin (Zs n) (Zs m))). +Proof. +Intros n m;Unfold Zmin; Rewrite (Zcompare_n_S n m); +(ElimCompare 'n 'm);Intros E;Rewrite E;Auto with arith. +Qed. + +Lemma Zle_min_l : (n,m:Z)(Zle (Zmin n m) n). +Proof. +Intros n m;Unfold Zmin ; (ElimCompare 'n 'm);Intros E;Rewrite -> E; + [ Apply Zle_n | Apply Zle_n | Apply Zlt_le_weak; Apply Zgt_lt;Exact E ]. +Qed. + +Lemma Zle_min_r : (n,m:Z)(Zle (Zmin n m) m). +Proof. +Intros n m;Unfold Zmin ; (ElimCompare 'n 'm);Intros E;Rewrite -> E;[ + Unfold Zle ;Rewrite -> E;Discriminate +| Unfold Zle ;Rewrite -> E;Discriminate +| Apply Zle_n ]. +Qed. + +Lemma Zmin_case : (n,m:Z)(P:Z->Set)(P n)->(P m)->(P (Zmin n m)). +Proof. +Intros n m P H1 H2; Unfold Zmin; Case (Zcompare n m);Auto with arith. +Qed. + +Lemma Zmin_or : (n,m:Z)(Zmin n m)=n \/ (Zmin n m)=m. +Proof. +Unfold Zmin; Intros; Elim (Zcompare n m); Auto. +Qed. + +Lemma Zmin_n_n : (n:Z) (Zmin n n)=n. +Proof. +Unfold Zmin; Intros; Elim (Zcompare n n); Auto. +Qed. + +Lemma Zmin_plus : + (x,y,n:Z)(Zmin (Zplus x n) (Zplus y n))=(Zplus (Zmin x y) n). +Proof. +Intros; Unfold Zmin. +Rewrite (Zplus_sym x n); +Rewrite (Zplus_sym y n); +Rewrite (Zcompare_Zplus_compatible x y n). +Case (Zcompare x y); Apply Zplus_sym. +Qed. + diff --git a/theories/ZArith/Zmisc.v b/theories/ZArith/Zmisc.v index 7e153c8dd..d6d5cd3d3 100644 --- a/theories/ZArith/Zmisc.v +++ b/theories/ZArith/Zmisc.v @@ -224,172 +224,4 @@ Intros; Rewrite iter_convert; Apply iter_nat_invariant; Trivial with arith. Qed. -(**********************************************************************) -(** [Zeven], [Zodd], [Zdiv2] and their related properties *) - -Definition Zeven := - [z:Z]Cases z of ZERO => True - | (POS (xO _)) => True - | (NEG (xO _)) => True - | _ => False - end. - -Definition Zodd := - [z:Z]Cases z of (POS xH) => True - | (NEG xH) => True - | (POS (xI _)) => True - | (NEG (xI _)) => True - | _ => False - end. - -Definition Zeven_bool := - [z:Z]Cases z of ZERO => true - | (POS (xO _)) => true - | (NEG (xO _)) => true - | _ => false - end. - -Definition Zodd_bool := - [z:Z]Cases z of ZERO => false - | (POS (xO _)) => false - | (NEG (xO _)) => false - | _ => true - end. - -Definition Zeven_odd_dec : (z:Z) { (Zeven z) }+{ (Zodd z) }. -Proof. - Intro z. Case z; - [ Left; Compute; Trivial - | Intro p; Case p; Intros; - (Right; Compute; Exact I) Orelse (Left; Compute; Exact I) - | Intro p; Case p; Intros; - (Right; Compute; Exact I) Orelse (Left; Compute; Exact I) ]. -Defined. - -Definition Zeven_dec : (z:Z) { (Zeven z) }+{ ~(Zeven z) }. -Proof. - Intro z. Case z; - [ Left; Compute; Trivial - | Intro p; Case p; Intros; - (Left; Compute; Exact I) Orelse (Right; Compute; Trivial) - | Intro p; Case p; Intros; - (Left; Compute; Exact I) Orelse (Right; Compute; Trivial) ]. -Defined. - -Definition Zodd_dec : (z:Z) { (Zodd z) }+{ ~(Zodd z) }. -Proof. - Intro z. Case z; - [ Right; Compute; Trivial - | Intro p; Case p; Intros; - (Left; Compute; Exact I) Orelse (Right; Compute; Trivial) - | Intro p; Case p; Intros; - (Left; Compute; Exact I) Orelse (Right; Compute; Trivial) ]. -Defined. - -Lemma Zeven_not_Zodd : (z:Z)(Zeven z) -> ~(Zodd z). -Proof. - NewDestruct z; [ Idtac | NewDestruct p | NewDestruct p ]; Compute; Trivial. -Qed. - -Lemma Zodd_not_Zeven : (z:Z)(Zodd z) -> ~(Zeven z). -Proof. - NewDestruct z; [ Idtac | NewDestruct p | NewDestruct p ]; Compute; Trivial. -Qed. - -Lemma Zeven_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 Zodd_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 Zeven_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. - -Lemma Zodd_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. - -Hints Unfold Zeven Zodd : zarith. - -(**********************************************************************) -(** [Zdiv2] is defined on all [Z], but notice that for odd negative - integers it is not the euclidean quotient: in that case we have [n = - 2*(n/2)-1] *) - -Definition Zdiv2 := - [z:Z]Cases z of ZERO => ZERO - | (POS xH) => ZERO - | (POS p) => (POS (Zdiv2_pos p)) - | (NEG xH) => ZERO - | (NEG p) => (NEG (Zdiv2_pos p)) - end. - -Lemma Zeven_div2 : (x:Z) (Zeven x) -> `x = 2*(Zdiv2 x)`. -Proof. -NewDestruct x. -Auto with arith. -NewDestruct p; Auto with arith. -Intros. Absurd (Zeven (POS (xI p))); Red; Auto with arith. -Intros. Absurd (Zeven `1`); Red; Auto with arith. -NewDestruct p; Auto with arith. -Intros. Absurd (Zeven (NEG (xI p))); Red; Auto with arith. -Intros. Absurd (Zeven `-1`); Red; Auto with arith. -Qed. - -Lemma Zodd_div2 : (x:Z) `x >= 0` -> (Zodd x) -> `x = 2*(Zdiv2 x)+1`. -Proof. -NewDestruct x. -Intros. Absurd (Zodd `0`); Red; Auto with arith. -NewDestruct p; Auto with arith. -Intros. Absurd (Zodd (POS (xO p))); Red; Auto with arith. -Intros. Absurd `(NEG p) >= 0`; Red; Auto with arith. -Qed. - -Lemma Zodd_div2_neg : (x:Z) `x <= 0` -> (Zodd x) -> `x = 2*(Zdiv2 x)-1`. -Proof. -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. 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 Zeven_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. diff --git a/theories/ZArith/Zorder.v b/theories/ZArith/Zorder.v new file mode 100644 index 000000000..ccfb9855b --- /dev/null +++ b/theories/ZArith/Zorder.v @@ -0,0 +1,922 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) +(*i $Id$ i*) + +(** Binary Integers (Pierre Crégut (CNET, Lannion, France) *) + +Require fast_integer. +Require Arith. +Require Decidable. +Require Zsyntax. + +V7only [Import nat_scope.]. +Open Local Scope Z_scope. + +Set Implicit Arguments. +V7only [Unset Implicit Arguments.]. + +Implicit Variable Type x,y,z:Z. + +(**********************************************************************) +(** Properties of the order relations on binary integers *) + +(** Trichotomy *) + +Theorem Ztrichotomy_inf : (m,n:Z) {Zlt m n} + {m=n} + {Zgt m n}. +Proof. +Unfold Zgt Zlt; Intros m n; Assert H:=(refl_equal ? (Zcompare m n)). + LetTac x := (Zcompare m n) in 2 H Goal. + NewDestruct x; + [Left; Right;Rewrite Zcompare_EGAL_eq with 1:=H + | Left; Left + | Right ]; Reflexivity. +Qed. + +Theorem Ztrichotomy : (m,n:Z) (Zlt m n) \/ m=n \/ (Zgt m n). +Proof. + Intros m n; NewDestruct (Ztrichotomy_inf m n) as [[Hlt|Heq]|Hgt]; + [Left | Right; Left |Right; Right]; Assumption. +Qed. + +(**********************************************************************) +(** Decidability of equality and order on Z *) + +Theorem dec_eq: (x,y:Z) (decidable (x=y)). +Proof. +Intros x y; Unfold decidable ; Elim (Zcompare_EGAL x y); +Intros H1 H2; Elim (Dcompare (Zcompare x y)); [ + Tauto + | Intros H3; Right; Unfold not ; Intros H4; + Elim H3; Rewrite (H2 H4); Intros H5; Discriminate H5]. +Qed. + +Theorem dec_Zne: (x,y:Z) (decidable (Zne x y)). +Proof. +Intros x y; Unfold decidable Zne ; Elim (Zcompare_EGAL x y). +Intros H1 H2; Elim (Dcompare (Zcompare x y)); + [ Right; Rewrite H1; Auto + | Left; Unfold not; Intro; Absurd (Zcompare x y)=EGAL; + [ Elim H; Intros HR; Rewrite HR; Discriminate + | Auto]]. +Qed. + +Theorem dec_Zle: (x,y:Z) (decidable (Zle x y)). +Proof. +Intros x y; Unfold decidable Zle ; Elim (Zcompare x y); [ + Left; Discriminate + | Left; Discriminate + | Right; Unfold not ; Intros H; Apply H; Trivial with arith]. +Qed. + +Theorem dec_Zgt: (x,y:Z) (decidable (Zgt x y)). +Proof. +Intros x y; Unfold decidable Zgt ; Elim (Zcompare x y); + [ Right; Discriminate | Right; Discriminate | Auto with arith]. +Qed. + +Theorem dec_Zge: (x,y:Z) (decidable (Zge x y)). +Proof. +Intros x y; Unfold decidable Zge ; Elim (Zcompare x y); [ + Left; Discriminate +| Right; Unfold not ; Intros H; Apply H; Trivial with arith +| Left; Discriminate]. +Qed. + +Theorem dec_Zlt: (x,y:Z) (decidable (Zlt x y)). +Proof. +Intros x y; Unfold decidable Zlt ; Elim (Zcompare x y); + [ Right; Discriminate | Auto with arith | Right; Discriminate]. +Qed. + +Theorem not_Zeq : (x,y:Z) ~ x=y -> (Zlt x y) \/ (Zlt y x). +Proof. +Intros x y; Elim (Dcompare (Zcompare x y)); [ + Intros H1 H2; Absurd x=y; [ Assumption | Elim (Zcompare_EGAL x y); Auto with arith] +| Unfold Zlt ; Intros H; Elim H; Intros H1; + [Auto with arith | Right; Elim (Zcompare_ANTISYM x y); Auto with arith]]. +Qed. + +(** Relating strict and large orders *) + +Lemma Zgt_lt : (m,n:Z) (Zgt m n) -> (Zlt n m). +Proof. +Unfold Zgt Zlt ;Intros m n H; Elim (Zcompare_ANTISYM m n); Auto with arith. +Qed. + +Lemma Zlt_gt : (m,n:Z) (Zlt m n) -> (Zgt n m). +Proof. +Unfold Zgt Zlt ;Intros m n H; Elim (Zcompare_ANTISYM n m); Auto with arith. +Qed. + +Lemma Zge_le : (m,n:Z) (Zge m n) -> (Zle n m). +Proof. +Intros m n; Change ~(Zlt m n)-> ~(Zgt n m); +Unfold not; Intros H1 H2; Apply H1; Apply Zgt_lt; Assumption. +Qed. + +Lemma Zle_ge : (m,n:Z) (Zle m n) -> (Zge n m). +Proof. +Intros m n; Change ~(Zgt m n)-> ~(Zlt n m); +Unfold not; Intros H1 H2; Apply H1; Apply Zlt_gt; Assumption. +Qed. + +Lemma Zle_not_gt : (n,m:Z)(Zle n m) -> ~(Zgt n m). +Proof. +Trivial. +Qed. + +Lemma Zgt_not_le : (n,m:Z)(Zgt n m) -> ~(Zle n m). +Proof. +Intros n m H1 H2; Apply H2; Assumption. +Qed. + +Lemma Zle_not_lt : (n,m:Z)(Zle n m) -> ~(Zlt m n). +Proof. +Intros n m H1 H2. +Assert H3:=(Zlt_gt ? ? H2). +Apply Zle_not_gt with n m; Assumption. +Qed. + +Lemma Zlt_not_le : (n,m:Z)(Zlt n m) -> ~(Zle m n). +Proof. +Intros n m H1 H2. +Apply Zle_not_lt with m n; Assumption. +Qed. + +Theorem not_Zge : (x,y:Z) ~(Zge x y) -> (Zlt x y). +Proof. +Unfold Zge Zlt ; Intros x y H; Apply dec_not_not; + [ Exact (dec_Zlt x y) | Assumption]. +Qed. + +Theorem not_Zlt : (x,y:Z) ~(Zlt x y) -> (Zge x y). +Proof. +Unfold Zlt Zge; Auto with arith. +Qed. + +Lemma not_Zgt : (n,m:Z)~(Zgt n m) -> (Zle n m). +Proof. +Trivial. +Qed. + +V7only [Notation Znot_gt_le := not_Zgt.]. + +Theorem not_Zle : (x,y:Z) ~(Zle x y) -> (Zgt x y). +Proof. +Unfold Zle Zgt ; Intros x y H; Apply dec_not_not; + [ Exact (dec_Zgt x y) | Assumption]. +Qed. + +(** Reflexivity *) + +Lemma Zle_n : (n:Z) (Zle n n). +Proof. +Intros n; Unfold Zle; Rewrite (Zcompare_x_x n); Discriminate. +Qed. + +(** Antisymmetry *) + +Lemma Zle_antisym : (n,m:Z)(Zle n m)->(Zle m n)->n=m. +Proof. +Intros n m H1 H2; NewDestruct (Ztrichotomy n m) as [Hlt|[Heq|Hgt]]. + Absurd (Zgt m n); [ Apply Zle_not_gt | Apply Zlt_gt]; Assumption. + Assumption. + Absurd (Zgt n m); [ Apply Zle_not_gt | Idtac]; Assumption. +Qed. + +(** Asymmetry *) + +Lemma Zgt_not_sym : (n,m:Z)(Zgt n m) -> ~(Zgt m n). +Proof. +Unfold Zgt ;Intros n m H; Elim (Zcompare_ANTISYM n m); Intros H1 H2; +Rewrite -> H1; [ Discriminate | Assumption ]. +Qed. + +Lemma Zlt_not_sym : (n,m:Z)(Zlt n m) -> ~(Zlt m n). +Proof. +Intros n m H H1; +Assert H2:(Zgt m n). Apply Zlt_gt; Assumption. +Assert H3: (Zgt n m). Apply Zlt_gt; Assumption. +Apply Zgt_not_sym with m n; Assumption. +Qed. + +(** Irreflexivity *) + +Lemma Zgt_antirefl : (n:Z)~(Zgt n n). +Proof. +Intros n H; Apply (Zgt_not_sym n n H H). +Qed. + +Lemma Zlt_n_n : (n:Z)~(Zlt n n). +Proof. +Intros n H; Apply (Zlt_not_sym n n H H). +Qed. + +(** Large = strict or equal *) + +Lemma Zle_lt_or_eq : (n,m:Z)(Zle n m)->((Zlt n m) \/ n=m). +Proof. +Intros n m H; NewDestruct (Ztrichotomy n m) as [Hlt|[Heq|Hgt]]; [ + Left; Assumption +| Right; Assumption +| Absurd (Zgt n m); [Apply Zle_not_gt|Idtac]; Assumption ]. +Qed. + +Lemma Zlt_le_weak : (n,m:Z)(Zlt n m)->(Zle n m). +Proof. +Intros n m Hlt; Apply Znot_gt_le; Apply Zgt_not_sym; Apply Zlt_gt; Assumption. +Qed. + +(** Dichotomy *) + +Lemma Zle_or_lt : (n,m:Z)(Zle n m)\/(Zlt m n). +Proof. +Intros n m; NewDestruct (Ztrichotomy n m) as [Hlt|[Heq|Hgt]]; [ + Left; Apply Znot_gt_le; Intro Hgt; Assert Hgt':=(Zlt_gt ? ? Hlt); + Apply Zgt_not_sym with m n; Assumption +| Left; Rewrite Heq; Apply Zle_n +| Right; Apply Zgt_lt; Assumption ]. +Qed. + +(** Transitivity of strict orders *) + +Lemma Zgt_trans : (n,m,p:Z)(Zgt n m)->(Zgt m p)->(Zgt n p). +Proof. +Exact Zcompare_trans_SUPERIEUR. +Qed. + +Lemma Zlt_trans : (n,m,p:Z)(Zlt n m)->(Zlt m p)->(Zlt n p). +Proof. +Intros n m p H1 H2; Apply Zgt_lt; Apply Zgt_trans with m:= m; +Apply Zlt_gt; Assumption. +Qed. + +(** Mixed transitivity *) + +Lemma Zle_gt_trans : (n,m,p:Z)(Zle m n)->(Zgt m p)->(Zgt n p). +Proof. +Intros n m p H1 H2; NewDestruct (Zle_lt_or_eq m n H1) as [Hlt|Heq]; [ + Apply Zgt_trans with m; [Apply Zlt_gt; Assumption | Assumption ] +| Rewrite <- Heq; Assumption ]. +Qed. + +Lemma Zgt_le_trans : (n,m,p:Z)(Zgt n m)->(Zle p m)->(Zgt n p). +Proof. +Intros n m p H1 H2; NewDestruct (Zle_lt_or_eq p m H2) as [Hlt|Heq]; [ + Apply Zgt_trans with m; [Assumption|Apply Zlt_gt; Assumption] +| Rewrite Heq; Assumption ]. +Qed. + +Lemma Zlt_le_trans : (n,m,p:Z)(Zlt n m)->(Zle m p)->(Zlt n p). +Intros n m p H1 H2;Apply Zgt_lt;Apply Zle_gt_trans with m:=m; + [ Assumption | Apply Zlt_gt;Assumption ]. +Qed. + +Lemma Zle_lt_trans : (n,m,p:Z)(Zle n m)->(Zlt m p)->(Zlt n p). +Proof. +Intros n m p H1 H2;Apply Zgt_lt;Apply Zgt_le_trans with m:=m; + [ Apply Zlt_gt;Assumption | Assumption ]. +Qed. + +(** Transitivity of large orders *) + +Lemma Zle_trans : (n,m,p:Z)(Zle n m)->(Zle m p)->(Zle n p). +Proof. +Intros n m p H1 H2; Apply Znot_gt_le. +Intro Hgt; Apply Zle_not_gt with n m. Assumption. +Exact (Zgt_le_trans n p m Hgt H2). +Qed. + +Lemma Zge_trans : (n, m, p : Z) (Zge n m) -> (Zge m p) -> (Zge n p). +Proof. +Intros n m p H1 H2. +Apply Zle_ge. +Apply Zle_trans with m; Apply Zge_le; Trivial. +Qed. + +(** Compatibility of successor wrt to order *) + +Lemma Zle_n_S : (n,m:Z) (Zle m n) -> (Zle (Zs m) (Zs n)). +Proof. +Unfold Zle not ;Intros m n H1 H2; Apply H1; +Rewrite <- (Zcompare_Zplus_compatible n m (POS xH)); +Do 2 Rewrite (Zplus_sym (POS xH)); Exact H2. +Qed. + +Lemma Zgt_n_S : (n,m:Z)(Zgt m n) -> (Zgt (Zs m) (Zs n)). +Proof. +Unfold Zgt; Intros n m H; Rewrite Zcompare_n_S; Auto with arith. +Qed. + +(** Simplification of successor wrt to order *) + +Lemma Zgt_S_n : (n,p:Z)(Zgt (Zs p) (Zs n))->(Zgt p n). +Proof. +Unfold Zs Zgt;Intros n p;Do 2 Rewrite -> [m:Z](Zplus_sym m (POS xH)); +Rewrite -> (Zcompare_Zplus_compatible p n (POS xH));Trivial with arith. +Qed. + +Lemma Zle_S_n : (n,m:Z) (Zle (Zs m) (Zs n)) -> (Zle m n). +Proof. +Unfold Zle not ;Intros m n H1 H2;Apply H1; +Unfold Zs ;Do 2 Rewrite <- (Zplus_sym (POS xH)); +Rewrite -> (Zcompare_Zplus_compatible n m (POS xH));Assumption. +Qed. + +(** Compatibility of addition wrt to order *) + +Lemma Zgt_reg_l + : (n,m,p:Z)(Zgt n m)->(Zgt (Zplus p n) (Zplus p m)). +Proof. +Unfold Zgt; Intros n m p H; Rewrite (Zcompare_Zplus_compatible n m p); +Assumption. +Qed. + +Lemma Zgt_reg_r : (n,m,p:Z)(Zgt n m)->(Zgt (Zplus n p) (Zplus m p)). +Proof. +Intros n m p H; Rewrite (Zplus_sym n p); Rewrite (Zplus_sym m p); Apply Zgt_reg_l; Trivial. +Qed. + +Lemma Zle_reg_l : (n,m,p:Z)(Zle n m)->(Zle (Zplus p n) (Zplus p m)). +Proof. +Intros n m p; Unfold Zle not ;Intros H1 H2;Apply H1; +Rewrite <- (Zcompare_Zplus_compatible n m p); Assumption. +Qed. + +Lemma Zle_reg_r : (n,m,p:Z) (Zle n m)->(Zle (Zplus n p) (Zplus m p)). +Proof. +Intros a b c;Do 2 Rewrite [n:Z](Zplus_sym n c); Exact (Zle_reg_l a b c). +Qed. + +Lemma Zlt_reg_l : (n,m,p:Z)(Zlt n m)->(Zlt (Zplus p n) (Zplus p m)). +Proof. +Unfold Zlt ;Intros n m p; Rewrite Zcompare_Zplus_compatible;Trivial with arith. +Qed. + +Lemma Zlt_reg_r : (n,m,p:Z)(Zlt n m)->(Zlt (Zplus n p) (Zplus m p)). +Proof. +Intros n m p H; Rewrite (Zplus_sym n p); Rewrite (Zplus_sym m p); Apply Zlt_reg_l; Trivial. +Qed. + +Lemma Zlt_le_reg : + (a,b,c,d:Z) (Zlt a b)->(Zle c d)->(Zlt (Zplus a c) (Zplus b d)). +Proof. +Intros a b c d H0 H1. +Apply Zlt_le_trans with (Zplus b c). +Apply Zlt_reg_r; Trivial. +Apply Zle_reg_l; Trivial. +Qed. + +Lemma Zle_lt_reg : + (a,b,c,d:Z) (Zle a b)->(Zlt c d)->(Zlt (Zplus a c) (Zplus b d)). +Proof. +Intros a b c d H0 H1. +Apply Zle_lt_trans with (Zplus b c). +Apply Zle_reg_r; Trivial. +Apply Zlt_reg_l; Trivial. +Qed. + +Lemma Zle_plus_plus : + (n,m,p,q:Z) (Zle n m)->(Zle p q)->(Zle (Zplus n p) (Zplus m q)). +Proof. +Intros n m p q; Intros H1 H2;Apply Zle_trans with m:=(Zplus n q); [ + Apply Zle_reg_l;Assumption | Apply Zle_reg_r;Assumption ]. +Qed. + +V7only [Set Implicit Arguments.]. + +Lemma Zlt_Zplus : + (x1,x2,y1,y2:Z)`x1 < x2` -> `y1 < y2` -> `x1 + y1 < x2 + y2`. +Intros; Apply Zle_lt_reg. Apply Zlt_le_weak; Assumption. Assumption. +Qed. + +V7only [Unset Implicit Arguments.]. + +(** Compatibility of addition wrt to being positive *) + +Theorem Zle_0_plus : + (x,y:Z) (Zle ZERO x) -> (Zle ZERO y) -> (Zle ZERO (Zplus x y)). +Proof. +Intros x y H1 H2;Rewrite <- (Zero_left ZERO); Apply Zle_plus_plus; Assumption. +Qed. + +(** Simplification of addition wrt to order *) + +Lemma Zsimpl_gt_plus_l + : (n,m,p:Z)(Zgt (Zplus p n) (Zplus p m))->(Zgt n m). +Proof. +Unfold Zgt; Intros n m p H; + Rewrite <- (Zcompare_Zplus_compatible n m p); Assumption. +Qed. + +Lemma Zsimpl_gt_plus_r + : (n,m,p:Z)(Zgt (Zplus n p) (Zplus m p))->(Zgt n m). +Proof. +Intros n m p H; Apply Zsimpl_gt_plus_l with p. +Rewrite (Zplus_sym p n); Rewrite (Zplus_sym p m); Trivial. +Qed. + +Lemma Zsimpl_le_plus_l : (p,n,m:Z)(Zle (Zplus p n) (Zplus p m))->(Zle n m). +Proof. +Intros p n m; Unfold Zle not ;Intros H1 H2;Apply H1; +Rewrite (Zcompare_Zplus_compatible n m p); Assumption. +Qed. + +Lemma Zsimpl_le_plus_r : (p,n,m:Z)(Zle (Zplus n p) (Zplus m p))->(Zle n m). +Proof. +Intros p n m H; Apply Zsimpl_le_plus_l with p. +Rewrite (Zplus_sym p n); Rewrite (Zplus_sym p m); Trivial. +Qed. + +Lemma Zsimpl_lt_plus_l + : (n,m,p:Z)(Zlt (Zplus p n) (Zplus p m))->(Zlt n m). +Proof. +Unfold Zlt ;Intros n m p; + Rewrite Zcompare_Zplus_compatible;Trivial with arith. +Qed. + +Lemma Zsimpl_lt_plus_r + : (n,m,p:Z)(Zlt (Zplus n p) (Zplus m p))->(Zlt n m). +Proof. +Intros n m p H; Apply Zsimpl_lt_plus_l with p. +Rewrite (Zplus_sym p n); Rewrite (Zplus_sym p m); Trivial. +Qed. + +(** Order, predecessor and successor *) + +Lemma Zgt_Sn_n : (n:Z)(Zgt (Zs n) n). +Proof. +Exact Zcompare_Zs_SUPERIEUR. +Qed. + +Lemma Zgt_le_S : (n,p:Z)(Zgt p n)->(Zle (Zs n) p). +Proof. +Unfold Zgt Zle; Intros n p H; Elim (Zcompare_et_un p n); Intros H1 H2; +Unfold not ;Intros H3; Unfold not in H1; Apply H1; [ + Assumption +| Elim (Zcompare_ANTISYM (Zplus n (POS xH)) p);Intros H4 H5;Apply H4;Exact H3]. +Qed. + +Lemma Zgt_S_le : (n,p:Z)(Zgt (Zs p) n)->(Zle n p). +Proof. +Intros n p H;Apply Zle_S_n; Apply Zgt_le_S; Assumption. +Qed. + +Lemma Zle_S_gt : (n,m:Z) (Zle (Zs n) m) -> (Zgt m n). +Proof. +Intros n m H;Apply Zle_gt_trans with m:=(Zs n); + [ Assumption | Apply Zgt_Sn_n ]. +Qed. + +Lemma Zle_gt_S : (n,p:Z)(Zle n p)->(Zgt (Zs p) n). +Proof. +Intros n p H; Apply Zgt_le_trans with p. + Apply Zgt_Sn_n. + Assumption. +Qed. + +Lemma Zgt_pred + : (n,p:Z)(Zgt p (Zs n))->(Zgt (Zpred p) n). +Proof. +Unfold Zgt Zs Zpred ;Intros n p H; +Rewrite <- [x,y:Z](Zcompare_Zplus_compatible x y (POS xH)); +Rewrite (Zplus_sym p); Rewrite Zplus_assoc; Rewrite [x:Z](Zplus_sym x n); +Simpl; Assumption. +Qed. + +Lemma Zlt_ZERO_pred_le_ZERO : (n:Z) (Zlt ZERO n) -> (Zle ZERO (Zpred n)). +Intros x H. +Rewrite (Zs_pred x) in H. +Apply Zgt_S_le. +Apply Zlt_gt. +Assumption. +Qed. + +V7only [Set Implicit Arguments.]. + +Lemma Zgt0_le_pred : (y:Z) `y > 0` -> `0 <= (Zpred y)`. +Intros; Apply Zlt_ZERO_pred_le_ZERO; Apply Zgt_lt. Assumption. +Qed. + +V7only [Unset Implicit Arguments.]. + +(** Special cases of ordered integers *) + +Lemma Zle_n_Sn : (n:Z)(Zle n (Zs n)). +Proof. +Intros n; Apply Zgt_S_le;Apply Zgt_trans with m:=(Zs n) ;Apply Zgt_Sn_n. +Qed. + +Lemma Zle_pred_n : (n:Z)(Zle (Zpred n) n). +Proof. +Intros n;Pattern 2 n ;Rewrite Zs_pred; Apply Zle_n_Sn. +Qed. + +Lemma POS_gt_ZERO : (p:positive) (Zgt (POS p) ZERO). +Unfold Zgt; Trivial. +Qed. + + (* weaker but useful (in [Zpower] for instance) *) +Lemma ZERO_le_POS : (p:positive) (Zle ZERO (POS p)). +Intro; Unfold Zle; Discriminate. +Qed. + +Lemma NEG_lt_ZERO : (p:positive)(Zlt (NEG p) ZERO). +Unfold Zlt; Trivial. +Qed. + +(** Weakening equality within order *) + +Lemma Zlt_not_eq : (x,y:Z)(Zlt x y) -> ~x=y. +Proof. +Unfold not; Intros x y H H0. +Rewrite H0 in H. +Apply (Zlt_n_n ? H). +Qed. + +Lemma Zle_refl : (n,m:Z) n=m -> (Zle n m). +Proof. +Intros; Rewrite H; Apply Zle_n. +Qed. + +(** Transitivity using successor *) + +Lemma Zgt_trans_S : (n,m,p:Z)(Zgt (Zs n) m)->(Zgt m p)->(Zgt n p). +Proof. +Intros n m p H1 H2;Apply Zle_gt_trans with m:=m; + [ Apply Zgt_S_le; Assumption | Assumption ]. +Qed. + +Lemma Zgt_S : (n,m:Z)(Zgt (Zs n) m)->((Zgt n m)\/(m=n)). +Proof. +Intros n m H. +Assert Hle : (Zle m n). + Apply Zgt_S_le; Assumption. +NewDestruct (Zle_lt_or_eq ? ? Hle) as [Hlt|Heq]. + Left; Apply Zlt_gt; Assumption. + Right; Assumption. +Qed. + +Hints Resolve Zle_n Zle_n_Sn Zle_trans Zle_n_S : zarith. +Hints Immediate Zle_refl : zarith. + +Lemma Zle_trans_S : (n,m:Z)(Zle (Zs n) m)->(Zle n m). +Proof. +Intros n m H;Apply Zle_trans with m:=(Zs n); [ Apply Zle_n_Sn | Assumption ]. +Qed. + +Lemma Zle_Sn_n : (n:Z)~(Zle (Zs n) n). +Proof. +Intros n; Apply Zgt_not_le; Apply Zgt_Sn_n. +Qed. + +Lemma Zlt_n_Sn : (n:Z)(Zlt n (Zs n)). +Proof. +Intro n; Apply Zgt_lt; Apply Zgt_Sn_n. +Qed. + +Lemma Zlt_S : (n,m:Z)(Zlt n m)->(Zlt n (Zs m)). +Intros n m H;Apply Zgt_lt; Apply Zgt_trans with m:=m; [ + Apply Zgt_Sn_n +| Apply Zlt_gt; Assumption ]. +Qed. + +Lemma Zlt_n_S : (n,m:Z)(Zlt n m)->(Zlt (Zs n) (Zs m)). +Proof. +Intros n m H;Apply Zgt_lt;Apply Zgt_n_S;Apply Zlt_gt; Assumption. +Qed. + +Lemma Zlt_S_n : (n,m:Z)(Zlt (Zs n) (Zs m))->(Zlt n m). +Proof. +Intros n m H;Apply Zgt_lt;Apply Zgt_S_n;Apply Zlt_gt; Assumption. +Qed. + +Lemma Zlt_pred : (n,p:Z)(Zlt (Zs n) p)->(Zlt n (Zpred p)). +Proof. +Intros n p H;Apply Zlt_S_n; Rewrite <- Zs_pred; Assumption. +Qed. + +Lemma Zlt_pred_n_n : (n:Z)(Zlt (Zpred n) n). +Proof. +Intros n; Apply Zlt_S_n; Rewrite <- Zs_pred; Apply Zlt_n_Sn. +Qed. + +Lemma Zlt_le_S : (n,p:Z)(Zlt n p)->(Zle (Zs n) p). +Proof. +Intros n p H; Apply Zgt_le_S; Apply Zlt_gt; Assumption. +Qed. + +Lemma Zlt_n_Sm_le : (n,m:Z)(Zlt n (Zs m))->(Zle n m). +Proof. +Intros n m H; Apply Zgt_S_le; Apply Zlt_gt; Assumption. +Qed. + +Lemma Zle_lt_n_Sm : (n,m:Z)(Zle n m)->(Zlt n (Zs m)). +Proof. +Intros n m H; Apply Zgt_lt; Apply Zle_gt_S; Assumption. +Qed. + +Lemma Zle_le_S : (x,y:Z)(Zle x y)->(Zle x (Zs y)). +Proof. +Intros. +Apply Zle_trans with y; Trivial with zarith. +Qed. + +Hints Resolve Zle_le_S : zarith. + +(** Compatibility of multiplication by a positive wrt to order *) + +V7only [Set Implicit Arguments.]. + +Lemma Zle_Zmult_pos_right : + (a,b,c : Z) + (Zle a b) -> (Zle ZERO c) -> (Zle (Zmult a c) (Zmult b c)). +Proof. +Intros; NewDestruct c. + Do 2 Rewrite Zero_mult_right; Assumption. + Rewrite (Zmult_sym a); Rewrite (Zmult_sym b). + Unfold Zle; Rewrite Zcompare_Zmult_compatible; Assumption. + Unfold Zle in H0; Contradiction H0; Reflexivity. +Qed. + +Lemma Zle_Zmult_pos_left : + (a,b,c : Z) + (Zle a b) -> (Zle ZERO c) -> (Zle (Zmult c a) (Zmult c b)). +Proof. +Intros a b c H1 H2; Rewrite (Zmult_sym c a);Rewrite (Zmult_sym c b). +Apply Zle_Zmult_pos_right; Trivial. +Qed. + +Lemma Zlt_Zmult_right : (x,y,z:Z)`z>0` -> `x < y` -> `x*z < y*z`. +Proof. +Intros; NewDestruct z. + Contradiction (Zgt_antirefl `0`). + Rewrite (Zmult_sym x); Rewrite (Zmult_sym y). + Unfold Zlt; Rewrite Zcompare_Zmult_compatible; Assumption. + Discriminate H. +Qed. + +Lemma Zle_Zmult_right : (x,y,z:Z)`z>0` -> `x <= y` -> `x*z <= y*z`. +Proof. +Intros x y z Hz Hxy. +Elim (Zle_lt_or_eq x y Hxy). +Intros; Apply Zlt_le_weak. +Apply Zlt_Zmult_right; Trivial. +Intros; Apply Zle_refl. +Rewrite H; Trivial. +Qed. + +Lemma Zgt_Zmult_right : (x,y,z:Z)`z>0` -> `x > y` -> `x*z > y*z`. +Proof. +Intros; Apply Zlt_gt; Apply Zlt_Zmult_right; +[ Assumption | Apply Zgt_lt ; Assumption ]. +Qed. + +Lemma Zlt_Zmult_left : (x,y,z:Z)`z>0` -> `x < y` -> `z*x < z*y`. +Proof. +Intros; +Rewrite (Zmult_sym z x); Rewrite (Zmult_sym z y); +Apply Zlt_Zmult_right; Assumption. +Qed. + +Lemma Zgt_Zmult_left : (x,y,z:Z)`z>0` -> `x > y` -> `z*x > z*y`. +Proof. +Intros; +Rewrite (Zmult_sym z x); Rewrite (Zmult_sym z y); +Apply Zgt_Zmult_right; Assumption. +Qed. + +Lemma Zge_Zmult_pos_right : + (a,b,c : Z) + (Zge a b) -> (Zge c ZERO) -> (Zge (Zmult a c) (Zmult b c)). +Proof. +Intros a b c H1 H2; Apply Zle_ge. +Apply Zle_Zmult_pos_right; Apply Zge_le; Trivial. +Qed. + +Lemma Zge_Zmult_pos_left : + (a,b,c : Z) + (Zge a b) -> (Zge c ZERO) -> (Zge (Zmult c a) (Zmult c b)). +Proof. +Intros a b c H1 H2; Apply Zle_ge. +Apply Zle_Zmult_pos_left; Apply Zge_le; Trivial. +Qed. + +Lemma Zge_Zmult_pos_compat : + (a,b,c,d : Z) + (Zge a c) -> (Zge b d) -> (Zge c ZERO) -> (Zge d ZERO) + -> (Zge (Zmult a b) (Zmult c d)). +Proof. +Intros a b c d H0 H1 H2 H3. +Apply Zge_trans with (Zmult a d). +Apply Zge_Zmult_pos_left; Trivial. +Apply Zge_trans with c; Trivial. +Apply Zge_Zmult_pos_right; Trivial. +Qed. + +(** Simplification of multiplication by a positive wrt to being positive *) + +Lemma Zlt_Zmult_right2 : (x,y,z:Z)`z>0` -> `x*z < y*z` -> `x < y`. +Proof. +Intros; NewDestruct z. + Contradiction (Zgt_antirefl `0`). + Rewrite (Zmult_sym x) in H0; Rewrite (Zmult_sym y) in H0. + Unfold Zlt in H0; Rewrite Zcompare_Zmult_compatible in H0; Assumption. + Discriminate H. +Qed. + +Lemma Zle_Zmult_right2 : (x,y,z:Z)`z>0` -> `x*z <= y*z` -> `x <= y`. +Proof. +Intros x y z Hz Hxy. +Elim (Zle_lt_or_eq `x*z` `y*z` Hxy). +Intros; Apply Zlt_le_weak. +Apply Zlt_Zmult_right2 with z; Trivial. +Intros; Apply Zle_refl. +Apply Zmult_reg_right with z. + Intro. Rewrite H0 in Hz. Contradiction (Zgt_antirefl `0`). +Assumption. +Qed. + +V7only [Unset Implicit Arguments.]. + +(** Compatibility of multiplication by a positive wrt to being positive *) + +Theorem Zle_ZERO_mult : + (x,y:Z) (Zle ZERO x) -> (Zle ZERO y) -> (Zle ZERO (Zmult x y)). +Proof. +Intros x y; Case x. +Intros; Rewrite Zero_mult_left; Trivial. +Intros p H1; Unfold Zle. + Pattern 2 ZERO ; Rewrite <- (Zero_mult_right (POS p)). + Rewrite Zcompare_Zmult_compatible; Trivial. +Intros p H1 H2; Absurd (Zgt ZERO (NEG p)); Trivial. +Unfold Zgt; Simpl; Auto with zarith. +Qed. + +Lemma Zgt_ZERO_mult: (a,b:Z) (Zgt a ZERO)->(Zgt b ZERO) + ->(Zgt (Zmult a b) ZERO). +Proof. +Intros x y; Case x. +Intros H; Discriminate H. +Intros p H1; Unfold Zgt; +Pattern 2 ZERO ; Rewrite <- (Zero_mult_right (POS p)). + Rewrite Zcompare_Zmult_compatible; Trivial. +Intros p H; Discriminate H. +Qed. + +Theorem Zle_mult: + (x,y:Z) (Zgt x ZERO) -> (Zle ZERO y) -> (Zle ZERO (Zmult y x)). +Proof. +Intros x y H1 H2; Apply Zle_ZERO_mult; Trivial. +Apply Zlt_le_weak; Apply Zgt_lt; Trivial. +Qed. + +(** Simplification of multiplication by a positive wrt to being positive *) + +Theorem Zmult_le: + (x,y:Z) (Zgt x ZERO) -> (Zle ZERO (Zmult y x)) -> (Zle ZERO y). +Proof. +Intros x y; Case x; [ + Simpl; Unfold Zgt ; Simpl; Intros H; Discriminate H +| Intros p H1; Unfold Zle; Rewrite -> Zmult_sym; + Pattern 1 ZERO ; Rewrite <- (Zero_mult_right (POS p)); + Rewrite Zcompare_Zmult_compatible; Auto with arith +| Intros p; Unfold Zgt ; Simpl; Intros H; Discriminate H]. +Qed. + +Theorem Zmult_lt: + (x,y:Z) (Zgt x ZERO) -> (Zlt ZERO (Zmult y x)) -> (Zlt ZERO y). +Proof. +Intros x y; Case x; [ + Simpl; Unfold Zgt ; Simpl; Intros H; Discriminate H +| Intros p H1; Unfold Zlt; Rewrite -> Zmult_sym; + Pattern 1 ZERO ; Rewrite <- (Zero_mult_right (POS p)); + Rewrite Zcompare_Zmult_compatible; Auto with arith +| Intros p; Unfold Zgt ; Simpl; Intros H; Discriminate H]. +Qed. + +Theorem Zmult_gt: + (x,y:Z) (Zgt x ZERO) -> (Zgt (Zmult x y) ZERO) -> (Zgt y ZERO). +Proof. +Intros x y; Case x. + Intros H; Discriminate H. + Intros p H1; Unfold Zgt. + Pattern 1 ZERO ; Rewrite <- (Zero_mult_right (POS p)). + Rewrite Zcompare_Zmult_compatible; Trivial. +Intros p H; Discriminate H. +Qed. + +(** Equivalence between inequalities (used in contrib/graph) *) + +Lemma Zle_plus_swap : (x,y,z:Z) (Zle (Zplus x z) y) <-> (Zle x (Zminus y z)). +Proof. + Intros. Split. Intro. Rewrite <- (Zero_right x). Rewrite <- (Zplus_inverse_r z). + Rewrite Zplus_assoc_l. Exact (Zle_reg_r ? ? ? H). + Intro. Rewrite <- (Zero_right y). Rewrite <- (Zplus_inverse_l z). Rewrite Zplus_assoc_l. + Apply Zle_reg_r. Assumption. +Qed. + +Lemma Zge_iff_le : (x,y:Z) (Zge x y) <-> (Zle y x). +Proof. + Intros. Split. Intro. Apply Zge_le. Assumption. + Intro. Apply Zle_ge. Assumption. +Qed. + +Lemma Zlt_plus_swap : (x,y,z:Z) (Zlt (Zplus x z) y) <-> (Zlt x (Zminus y z)). +Proof. + Intros. Split. Intro. Unfold Zminus. Rewrite Zplus_sym. Rewrite <- (Zero_left x). + Rewrite <- (Zplus_inverse_l z). Rewrite Zplus_assoc_r. Apply Zlt_reg_l. Rewrite Zplus_sym. + Assumption. + Intro. Rewrite Zplus_sym. Rewrite <- (Zero_left y). Rewrite <- (Zplus_inverse_r z). + Rewrite Zplus_assoc_r. Apply Zlt_reg_l. Rewrite Zplus_sym. Assumption. +Qed. + +Lemma Zgt_iff_lt : (x,y:Z) (Zgt x y) <-> (Zlt y x). +Proof. + Intros. Split. Intro. Apply Zgt_lt. Assumption. + Intro. Apply Zlt_gt. Assumption. +Qed. + +Lemma Zeq_plus_swap : (x,y,z:Z) (Zplus x z)=y <-> x=(Zminus y z). +Proof. +Intros. Split. Intro. Apply Zplus_minus. Symmetry. Rewrite Zplus_sym. + Assumption. +Intro. Rewrite H. Unfold Zminus. Rewrite Zplus_assoc_r. + Rewrite Zplus_inverse_l. Apply Zero_right. +Qed. + +(** Reverting [x ?= y] to trichotomy *) + +Lemma rename : (A:Set)(P:A->Prop)(x:A) ((y:A)(x=y)->(P y)) -> (P x). +Proof. +Auto with arith. +Qed. + +Theorem Zcompare_elim : + (c1,c2,c3:Prop)(x,y:Z) + ((x=y) -> c1) ->((Zlt x y) -> c2) ->((Zgt x y)-> c3) + -> Cases (Zcompare x y) of EGAL => c1 | INFERIEUR => c2 | SUPERIEUR => c3 end. +Proof. +Intros. +Apply rename with x:=(Zcompare x y); Intro r; Elim r; +[ Intro; Apply H; Apply (Zcompare_EGAL_eq x y); Assumption +| Unfold Zlt in H0; Assumption +| Unfold Zgt in H1; Assumption ]. +Qed. + +Lemma Zcompare_eq_case : + (c1,c2,c3:Prop)(x,y:Z) c1 -> x=y -> + Cases (Zcompare x y) of EGAL => c1 | INFERIEUR => c2 | SUPERIEUR => c3 end. +Proof. +Intros. +Rewrite H0; Rewrite (Zcompare_x_x). +Assumption. +Qed. + +(** Decompose an egality between two [?=] relations into 3 implications *) + +Theorem Zcompare_egal_dec : + (x1,y1,x2,y2:Z) + ((Zlt x1 y1)->(Zlt x2 y2)) + ->((Zcompare x1 y1)=EGAL -> (Zcompare x2 y2)=EGAL) + ->((Zgt x1 y1)->(Zgt x2 y2))->(Zcompare x1 y1)=(Zcompare x2 y2). +Proof. +Intros x1 y1 x2 y2. +Unfold Zgt; Unfold Zlt; +Case (Zcompare x1 y1); Case (Zcompare x2 y2); Auto with arith; Symmetry; Auto with arith. +Qed. + +(** Relating [x ?= y] to [Zle], [Zlt], [Zge] or [Zgt] *) + +Lemma Zle_Zcompare : + (x,y:Z)(Zle x y) -> + Cases (Zcompare x y) of EGAL => True | INFERIEUR => True | SUPERIEUR => False end. +Proof. +Intros x y; Unfold Zle; Elim (Zcompare x y); Auto with arith. +Qed. + +Lemma Zlt_Zcompare : + (x,y:Z)(Zlt x y) -> + Cases (Zcompare x y) of EGAL => False | INFERIEUR => True | SUPERIEUR => False end. +Proof. +Intros x y; Unfold Zlt; Elim (Zcompare x y); Intros; Discriminate Orelse Trivial with arith. +Qed. + +Lemma Zge_Zcompare : + (x,y:Z)(Zge x y)-> + Cases (Zcompare x y) of EGAL => True | INFERIEUR => False | SUPERIEUR => True end. +Proof. +Intros x y; Unfold Zge; Elim (Zcompare x y); Auto with arith. +Qed. + +Lemma Zgt_Zcompare : + (x,y:Z)(Zgt x y) -> + Cases (Zcompare x y) of EGAL => False | INFERIEUR => False | SUPERIEUR => True end. +Proof. +Intros x y; Unfold Zgt; Elim (Zcompare x y); Intros; Discriminate Orelse Trivial with arith. +Qed. diff --git a/theories/ZArith/Zsqrt.v b/theories/ZArith/Zsqrt.v index 3c895d6db..e5ee2682d 100644 --- a/theories/ZArith/Zsqrt.v +++ b/theories/ZArith/Zsqrt.v @@ -14,6 +14,9 @@ Require Export Omega. V7only [Import Z_scope.]. Open Local Scope Z_scope. +(**********************************************************************) +(** Definition and properties of square root on Z *) + (** The following tactic replaces all instances of (POS (xI ...)) by `2*(POS ...)+1` , but only when ... is not made only with xO, XI, or xH. *) Tactic Definition compute_POS := diff --git a/theories/ZArith/Zsyntax.v b/theories/ZArith/Zsyntax.v index 6c632ea42..001de304b 100644 --- a/theories/ZArith/Zsyntax.v +++ b/theories/ZArith/Zsyntax.v @@ -9,7 +9,6 @@ (*i $Id$ i*) Require Export fast_integer. -Require Export zarith_aux. V7only[ @@ -64,6 +63,16 @@ with expr0 : constr := | expr_num [ number($s) ] -> [$s ] | expr_negnum [ "-" negnumber($n) ] -> [ $n ] | expr_inv [ "-" expr0($c) ] -> [ (Zopp $c) ] +| expr_meta [ zmeta($m) ] -> [ $m ] + +with zmeta := +| rimpl [ "?" ] -> [ ? ] +| rmeta0 [ "?" "0" ] -> [ ?0 ] +| rmeta1 [ "?" "1" ] -> [ ?1 ] +| rmeta2 [ "?" "2" ] -> [ ?2 ] +| rmeta3 [ "?" "3" ] -> [ ?3 ] +| rmeta4 [ "?" "4" ] -> [ ?4 ] +| rmeta5 [ "?" "5" ] -> [ ?5 ] with application : constr := apply [ application($p) expr($c1) ] -> [ ($p $c1) ] diff --git a/theories/ZArith/auxiliary.v b/theories/ZArith/auxiliary.v index aa34a201e..745c5c988 100644 --- a/theories/ZArith/auxiliary.v +++ b/theories/ZArith/auxiliary.v @@ -12,6 +12,7 @@ Require Export Arith. Require fast_integer. +Require Zorder. Require zarith_aux. Require Decidable. Require Peano_dec. @@ -20,9 +21,12 @@ Require Export Compare_dec. Open Local Scope Z_scope. Definition neq := [x,y:nat] ~(x=y). -Definition Zne := [x,y:Z] ~(x=y). + +(**********************************************************************) +(** Properties of the injection from nat into Z *) Theorem inj_S : (y:nat) (inject_nat (S y)) = (Zs (inject_nat y)). +Proof. Induction y; [ Unfold Zs ; Simpl; Trivial with arith | Intros n; Intros H; @@ -32,7 +36,7 @@ Qed. Theorem inj_plus : (x,y:nat) (inject_nat (plus x y)) = (Zplus (inject_nat x) (inject_nat y)). - +Proof. Induction x; Induction y; [ Simpl; Trivial with arith | Simpl; Trivial with arith @@ -44,7 +48,7 @@ Qed. Theorem inj_mult : (x,y:nat) (inject_nat (mult x y)) = (Zmult (inject_nat x) (inject_nat y)). - +Proof. Induction x; [ Simpl; Trivial with arith | Intros n H y; Rewrite -> inj_S; Rewrite <- Zmult_Sm_n; @@ -53,7 +57,7 @@ Qed. Theorem inj_neq: (x,y:nat) (neq x y) -> (Zne (inject_nat x) (inject_nat y)). - +Proof. Unfold neq Zne not ; Intros x y H1 H2; Apply H1; Generalize H2; Case x; Case y; Intros; [ Auto with arith @@ -64,7 +68,7 @@ Qed. Theorem inj_le: (x,y:nat) (le x y) -> (Zle (inject_nat x) (inject_nat y)). - +Proof. Intros x y; Intros H; Elim H; [ Unfold Zle ; Elim (Zcompare_EGAL (inject_nat x) (inject_nat x)); Intros H1 H2; Rewrite H2; [ Discriminate | Trivial with arith] @@ -73,25 +77,30 @@ Intros x y; Intros H; Elim H; [ Qed. Theorem inj_lt: (x,y:nat) (lt x y) -> (Zlt (inject_nat x) (inject_nat y)). +Proof. Intros x y H; Apply Zgt_lt; Apply Zle_S_gt; Rewrite <- inj_S; Apply inj_le; Exact H. Qed. Theorem inj_gt: (x,y:nat) (gt x y) -> (Zgt (inject_nat x) (inject_nat y)). +Proof. Intros x y H; Apply Zlt_gt; Apply inj_lt; Exact H. Qed. Theorem inj_ge: (x,y:nat) (ge x y) -> (Zge (inject_nat x) (inject_nat y)). +Proof. Intros x y H; Apply Zle_ge; Apply inj_le; Apply H. Qed. Theorem inj_eq: (x,y:nat) x=y -> (inject_nat x) = (inject_nat y). +Proof. Intros x y H; Rewrite H; Trivial with arith. Qed. Theorem intro_Z : (x:nat) (EX y:Z | (inject_nat x)=y /\ (Zle ZERO (Zplus (Zmult y (POS xH)) ZERO))). +Proof. Intros x; Exists (inject_nat x); Split; [ Trivial with arith | Rewrite Zmult_sym; Rewrite Zmult_one; Rewrite Zero_right; @@ -101,99 +110,36 @@ Qed. Theorem inj_minus1 : (x,y:nat) (le y x) -> (inject_nat (minus x y)) = (Zminus (inject_nat x) (inject_nat y)). +Proof. Intros x y H; Apply (Zsimpl_plus_l (inject_nat y)); Unfold Zminus ; Rewrite Zplus_permute; Rewrite Zplus_inverse_r; Rewrite <- inj_plus; Rewrite <- (le_plus_minus y x H);Rewrite Zero_right; Trivial with arith. Qed. Theorem inj_minus2: (x,y:nat) (gt y x) -> (inject_nat (minus x y)) = ZERO. +Proof. Intros x y H; Rewrite inj_minus_aux; [ Trivial with arith | Apply gt_not_le; Assumption]. Qed. -Theorem dec_eq: (x,y:Z) (decidable (x=y)). -Intros x y; Unfold decidable ; Elim (Zcompare_EGAL x y); -Intros H1 H2; Elim (Dcompare (Zcompare x y)); [ - Tauto - | Intros H3; Right; Unfold not ; Intros H4; - Elim H3; Rewrite (H2 H4); Intros H5; Discriminate H5]. -Qed. - -Theorem dec_Zne: (x,y:Z) (decidable (Zne x y)). -Intros x y; Unfold decidable Zne ; Elim (Zcompare_EGAL x y). -Intros H1 H2; Elim (Dcompare (Zcompare x y)); - [ Right; Rewrite H1; Auto - | Left; Unfold not; Intro; Absurd (Zcompare x y)=EGAL; - [ Elim H; Intros HR; Rewrite HR; Discriminate - | Auto]]. -Qed. - -Theorem dec_Zle: (x,y:Z) (decidable (Zle x y)). -Intros x y; Unfold decidable Zle ; Elim (Zcompare x y); [ - Left; Discriminate - | Left; Discriminate - | Right; Unfold not ; Intros H; Apply H; Trivial with arith]. -Qed. - -Theorem dec_Zgt: (x,y:Z) (decidable (Zgt x y)). -Intros x y; Unfold decidable Zgt ; Elim (Zcompare x y); - [ Right; Discriminate | Right; Discriminate | Auto with arith]. -Qed. - -Theorem dec_Zge: (x,y:Z) (decidable (Zge x y)). -Intros x y; Unfold decidable Zge ; Elim (Zcompare x y); [ - Left; Discriminate -| Right; Unfold not ; Intros H; Apply H; Trivial with arith -| Left; Discriminate]. -Qed. - -Theorem dec_Zlt: (x,y:Z) (decidable (Zlt x y)). -Intros x y; Unfold decidable Zlt ; Elim (Zcompare x y); - [ Right; Discriminate | Auto with arith | Right; Discriminate]. -Qed. - -Theorem not_Zge : (x,y:Z) ~(Zge x y) -> (Zlt x y). -Unfold Zge Zlt ; Intros x y H; Apply dec_not_not; - [ Exact (dec_Zlt x y) | Assumption]. -Qed. - -Theorem not_Zlt : (x,y:Z) ~(Zlt x y) -> (Zge x y). -Unfold Zlt Zge; Auto with arith. -Qed. - -Theorem not_Zle : (x,y:Z) ~(Zle x y) -> (Zgt x y). -Unfold Zle Zgt ; Intros x y H; Apply dec_not_not; - [ Exact (dec_Zgt x y) | Assumption]. - Qed. - -Theorem not_Zgt : (x,y:Z) ~(Zgt x y) -> (Zle x y). -Unfold Zgt Zle; Auto with arith. -Qed. - -Theorem not_Zeq : (x,y:Z) ~ x=y -> (Zlt x y) \/ (Zlt y x). - -Intros x y; Elim (Dcompare (Zcompare x y)); [ - Intros H1 H2; Absurd x=y; [ Assumption | Elim (Zcompare_EGAL x y); Auto with arith] -| Unfold Zlt ; Intros H; Elim H; Intros H1; - [Auto with arith | Right; Elim (Zcompare_ANTISYM x y); Auto with arith]]. -Qed. - -Lemma new_var: (x:Z) (EX y:Z |(x=y)). -Intros x; Exists x; Trivial with arith. -Qed. +(**********************************************************************) +(** Moving terms from one side to the other of an inequality *) Theorem Zne_left : (x,y:Z) (Zne x y) -> (Zne (Zplus x (Zopp y)) ZERO). +Proof. Intros x y; Unfold Zne; Unfold not; Intros H1 H2; Apply H1; Apply Zsimpl_plus_l with (Zopp y); Rewrite Zplus_inverse_l; Rewrite Zplus_sym; Trivial with arith. Qed. Theorem Zegal_left : (x,y:Z) (x=y) -> (Zplus x (Zopp y)) = ZERO. +Proof. Intros x y H; Apply (Zsimpl_plus_l y);Rewrite -> Zplus_permute; Rewrite -> Zplus_inverse_r;Do 2 Rewrite -> Zero_right;Assumption. Qed. Theorem Zle_left : (x,y:Z) (Zle x y) -> (Zle ZERO (Zplus y (Zopp x))). +Proof. Intros x y H; Replace ZERO with (Zplus x (Zopp x)). Apply Zle_reg_r; Trivial. Apply Zplus_inverse_r. @@ -201,18 +147,21 @@ Qed. Theorem Zle_left_rev : (x,y:Z) (Zle ZERO (Zplus y (Zopp x))) -> (Zle x y). +Proof. Intros x y H; Apply (Zsimpl_le_plus_r (Zopp x)). Rewrite Zplus_inverse_r; Trivial. Qed. Theorem Zlt_left_rev : (x,y:Z) (Zlt ZERO (Zplus y (Zopp x))) -> (Zlt x y). +Proof. Intros x y H; Apply Zsimpl_lt_plus_r with (Zopp x). Rewrite Zplus_inverse_r; Trivial. Qed. Theorem Zlt_left : (x,y:Z) (Zlt x y) -> (Zle ZERO (Zplus (Zplus y (NEG xH)) (Zopp x))). +Proof. Intros x y H; Apply Zle_left; Apply Zle_S_n; Change (Zle (Zs x) (Zs (Zpred y))); Rewrite <- Zs_pred; Apply Zlt_le_S; Assumption. @@ -220,22 +169,26 @@ Qed. Theorem Zlt_left_lt : (x,y:Z) (Zlt x y) -> (Zlt ZERO (Zplus y (Zopp x))). +Proof. Intros x y H; Replace ZERO with (Zplus x (Zopp x)). Apply Zlt_reg_r; Trivial. Apply Zplus_inverse_r. Qed. Theorem Zge_left : (x,y:Z) (Zge x y) -> (Zle ZERO (Zplus x (Zopp y))). +Proof. Intros x y H; Apply Zle_left; Apply Zge_le; Assumption. Qed. Theorem Zgt_left : (x,y:Z) (Zgt x y) -> (Zle ZERO (Zplus (Zplus x (NEG xH)) (Zopp y))). +Proof. Intros x y H; Apply Zlt_left; Apply Zgt_lt; Assumption. Qed. Theorem Zgt_left_gt : (x,y:Z) (Zgt x y) -> (Zgt (Zplus x (Zopp y)) ZERO). +Proof. Intros x y H; Replace ZERO with (Zplus y (Zopp y)). Apply Zgt_reg_r; Trivial. Apply Zplus_inverse_r. @@ -243,12 +196,13 @@ Qed. Theorem Zgt_left_rev : (x,y:Z) (Zgt (Zplus x (Zopp y)) ZERO) -> (Zgt x y). +Proof. Intros x y H; Apply Zsimpl_gt_plus_r with (Zopp y). Rewrite Zplus_inverse_r; Trivial. Qed. (**********************************************************************) -(** Omega lemmas *) +(** Misc lemmas *) Theorem Zred_factor0 : (x:Z) x = (Zmult x (POS xH)). Intro x; Rewrite (Zmult_n_1 x); Reflexivity. @@ -287,66 +241,6 @@ Theorem Zred_factor6 : (x:Z) x = (Zplus x ZERO). Intro; Rewrite Zero_right; Trivial with arith. Qed. -Theorem Zmult_le: - (x,y:Z) (Zgt x ZERO) -> (Zle ZERO (Zmult y x)) -> (Zle ZERO y). - -Intros x y; Case x; [ - Simpl; Unfold Zgt ; Simpl; Intros H; Discriminate H -| Intros p H1; Unfold Zle; Rewrite -> Zmult_sym; - Pattern 1 ZERO ; Rewrite <- (Zero_mult_right (POS p)); - Rewrite Zcompare_Zmult_compatible; Auto with arith -| Intros p; Unfold Zgt ; Simpl; Intros H; Discriminate H]. -Qed. - -Theorem Zle_ZERO_mult : - (x,y:Z) (Zle ZERO x) -> (Zle ZERO y) -> (Zle ZERO (Zmult x y)). -Intros x y; Case x. -Intros; Rewrite Zero_mult_left; Trivial. -Intros p H1; Unfold Zle. - Pattern 2 ZERO ; Rewrite <- (Zero_mult_right (POS p)). - Rewrite Zcompare_Zmult_compatible; Trivial. -Intros p H1 H2; Absurd (Zgt ZERO (NEG p)); Trivial. -Unfold Zgt; Simpl; Auto with zarith. -Qed. - -Lemma Zgt_ZERO_mult: (a,b:Z) (Zgt a ZERO)->(Zgt b ZERO) - ->(Zgt (Zmult a b) ZERO). -Intros x y; Case x. -Intros H; Discriminate H. -Intros p H1; Unfold Zgt; -Pattern 2 ZERO ; Rewrite <- (Zero_mult_right (POS p)). - Rewrite Zcompare_Zmult_compatible; Trivial. -Intros p H; Discriminate H. -Qed. - -Theorem Zle_mult: - (x,y:Z) (Zgt x ZERO) -> (Zle ZERO y) -> (Zle ZERO (Zmult y x)). -Intros x y H1 H2; Apply Zle_ZERO_mult; Trivial. -Apply Zlt_le_weak; Apply Zgt_lt; Trivial. -Qed. - -Theorem Zmult_lt: - (x,y:Z) (Zgt x ZERO) -> (Zlt ZERO (Zmult y x)) -> (Zlt ZERO y). - -Intros x y; Case x; [ - Simpl; Unfold Zgt ; Simpl; Intros H; Discriminate H -| Intros p H1; Unfold Zlt; Rewrite -> Zmult_sym; - Pattern 1 ZERO ; Rewrite <- (Zero_mult_right (POS p)); - Rewrite Zcompare_Zmult_compatible; Auto with arith -| Intros p; Unfold Zgt ; Simpl; Intros H; Discriminate H]. -Qed. - -Theorem Zmult_gt: - (x,y:Z) (Zgt x ZERO) -> (Zgt (Zmult x y) ZERO) -> (Zgt y ZERO). - -Intros x y; Case x. - Intros H; Discriminate H. - Intros p H1; Unfold Zgt. - Pattern 1 ZERO ; Rewrite <- (Zero_mult_right (POS p)). - Rewrite Zcompare_Zmult_compatible; Trivial. -Intros p H; Discriminate H. -Qed. - Theorem Zle_mult_approx: (x,y,z:Z) (Zgt x ZERO) -> (Zgt z ZERO) -> (Zle ZERO y) -> (Zle ZERO (Zplus (Zmult y x) z)). @@ -357,74 +251,6 @@ Intros x y z H1 H2 H3; Apply Zle_trans with m:=(Zmult y x) ; [ Apply Zlt_le_weak; Apply Zgt_lt; Assumption]. Qed. -Lemma Zle_Zmult_pos_right : - (a,b,c : Z) - (Zle a b) -> (Zle ZERO c) -> (Zle (Zmult a c) (Zmult b c)). -Intros a b c H1 H2; Apply Zle_left_rev. -Rewrite Zopp_Zmult_l. -Rewrite <- Zmult_plus_distr_l. -Apply Zle_ZERO_mult; Trivial. -Apply Zle_left; Trivial. -Qed. - -Lemma Zle_Zmult_pos_left : - (a,b,c : Z) - (Zle a b) -> (Zle ZERO c) -> (Zle (Zmult c a) (Zmult c b)). -Intros a b c H1 H2; Rewrite (Zmult_sym c a);Rewrite (Zmult_sym c b). -Apply Zle_Zmult_pos_right; Trivial. -Qed. - -Lemma Zge_Zmult_pos_right : - (a,b,c : Z) - (Zge a b) -> (Zge c ZERO) -> (Zge (Zmult a c) (Zmult b c)). -Intros a b c H1 H2; Apply Zle_ge. -Apply Zle_Zmult_pos_right; Apply Zge_le; Trivial. -Qed. - -Lemma Zge_Zmult_pos_left : - (a,b,c : Z) - (Zge a b) -> (Zge c ZERO) -> (Zge (Zmult c a) (Zmult c b)). -Intros a b c H1 H2; Apply Zle_ge. -Apply Zle_Zmult_pos_left; Apply Zge_le; Trivial. -Qed. - -Lemma Zge_Zmult_pos_compat : - (a,b,c,d : Z) - (Zge a c) -> (Zge b d) -> (Zge c ZERO) -> (Zge d ZERO) - -> (Zge (Zmult a b) (Zmult c d)). -Intros a b c d H0 H1 H2 H3. -Apply Zge_trans with (Zmult a d). -Apply Zge_Zmult_pos_left; Trivial. -Apply Zge_trans with c; Trivial. -Apply Zge_Zmult_pos_right; Trivial. -Qed. - -Lemma Zle_mult_simpl - : (a,b,c:Z) (Zgt c ZERO)->(Zle (Zmult a c) (Zmult b c))->(Zle a b). -Intros a b c H1 H2; Apply Zle_left_rev. -Apply Zmult_le with c; Trivial. -Rewrite Zmult_plus_distr_l. -Rewrite <- Zopp_Zmult_l. -Apply Zle_left; Trivial. -Qed. - - -Lemma Zge_mult_simpl - : (a,b,c:Z) (Zgt c ZERO)->(Zge (Zmult a c) (Zmult b c))->(Zge a b). -Intros a b c H1 H2; Apply Zle_ge; Apply Zle_mult_simpl with c; Trivial. -Apply Zge_le; Trivial. -Qed. - -Lemma Zgt_mult_simpl - : (a,b,c:Z) (Zgt c ZERO)->(Zgt (Zmult a c) (Zmult b c))->(Zgt a b). -Intros a b c H1 H2; Apply Zgt_left_rev. -Apply Zmult_gt with c; Trivial. -Rewrite Zmult_sym. -Rewrite Zmult_plus_distr_l. -Rewrite <- Zopp_Zmult_l. -Apply Zgt_left_gt; Trivial. -Qed. - Lemma Zgt_square_simpl: (x, y : Z) (Zge x ZERO) -> (Zge y ZERO) -> (Zgt (Zmult x x) (Zmult y y)) -> (Zgt x y). @@ -451,383 +277,5 @@ Intros x y z H1 H2 H3; Apply Zlt_n_Sm_le; Apply (Zmult_lt x); [ Qed. -Theorem OMEGA1 : (x,y:Z) (x=y) -> (Zle ZERO x) -> (Zle ZERO y). -Intros x y H; Rewrite H; Auto with arith. -Qed. - -Theorem OMEGA2 : (x,y:Z) (Zle ZERO x) -> (Zle ZERO y) -> (Zle ZERO (Zplus x y)). -Intros x y H1 H2;Rewrite <- (Zero_left ZERO); Apply Zle_plus_plus; Assumption. -Qed. - -Theorem OMEGA3 : - (x,y,k:Z)(Zgt k ZERO)-> (x=(Zmult y k)) -> (x=ZERO) -> (y=ZERO). - -Intros x y k H1 H2 H3; Apply (Zmult_eq k); [ - Unfold not ; Intros H4; Absurd (Zgt k ZERO); [ - Rewrite H4; Unfold Zgt ; Simpl; Discriminate | Assumption] - | Rewrite <- H2; Assumption]. -Qed. - -Theorem OMEGA4 : - (x,y,z:Z)(Zgt x ZERO) -> (Zgt y x) -> ~(Zplus (Zmult z y) x) = ZERO. - -Unfold not ; Intros x y z H1 H2 H3; Cut (Zgt y ZERO); [ - Intros H4; Cut (Zle ZERO (Zplus (Zmult z y) x)); [ - Intros H5; Generalize (Zmult_le_approx y z x H4 H2 H5) ; Intros H6; - Absurd (Zgt (Zplus (Zmult z y) x) ZERO); [ - Rewrite -> H3; Unfold Zgt ; Simpl; Discriminate - | Apply Zle_gt_trans with x ; [ - Pattern 1 x ; Rewrite <- (Zero_left x); Apply Zle_reg_r; - Rewrite -> Zmult_sym; Generalize H4 ; Unfold Zgt; - Case y; [ - Simpl; Intros H7; Discriminate H7 - | Intros p H7; Rewrite <- (Zero_mult_right (POS p)); - Unfold Zle ; Rewrite -> Zcompare_Zmult_compatible; Exact H6 - | Simpl; Intros p H7; Discriminate H7] - | Assumption]] - | Rewrite -> H3; Unfold Zle ; Simpl; Discriminate] - | Apply Zgt_trans with x ; [ Assumption | Assumption]]. -Qed. - -Theorem OMEGA5: (x,y,z:Z)(x=ZERO) -> (y=ZERO) -> (Zplus x (Zmult y z)) = ZERO. - -Intros x y z H1 H2; Rewrite H1; Rewrite H2; Simpl; Trivial with arith. -Qed. -Theorem OMEGA6: - (x,y,z:Z)(Zle ZERO x) -> (y=ZERO) -> (Zle ZERO (Zplus x (Zmult y z))). - -Intros x y z H1 H2; Rewrite H2; Simpl; Rewrite Zero_right; Assumption. -Qed. - -Theorem OMEGA7: - (x,y,z,t:Z)(Zgt z ZERO) -> (Zgt t ZERO) -> (Zle ZERO x) -> (Zle ZERO y) -> - (Zle ZERO (Zplus (Zmult x z) (Zmult y t))). - -Intros x y z t H1 H2 H3 H4; Rewrite <- (Zero_left ZERO); -Apply Zle_plus_plus; Apply Zle_mult; Assumption. -Qed. - -Theorem OMEGA8: - (x,y:Z) (Zle ZERO x) -> (Zle ZERO y) -> x = (Zopp y) -> x = ZERO. - -Intros x y H1 H2 H3; Elim (Zle_lt_or_eq ZERO x H1); [ - Intros H4; Absurd (Zlt ZERO x); [ - Change (Zge ZERO x); Apply Zle_ge; Apply (Zsimpl_le_plus_l y); - Rewrite -> H3; Rewrite Zplus_inverse_r; Rewrite Zero_right; Assumption - | Assumption] -| Intros H4; Rewrite -> H4; Trivial with arith]. -Qed. - -Theorem OMEGA9:(x,y,z,t:Z) y=ZERO -> x = z -> - (Zplus y (Zmult (Zplus (Zopp x) z) t)) = ZERO. - -Intros x y z t H1 H2; Rewrite H2; Rewrite Zplus_inverse_l; -Rewrite Zero_mult_left; Rewrite Zero_right; Assumption. -Qed. -Theorem OMEGA10:(v,c1,c2,l1,l2,k1,k2:Z) - (Zplus (Zmult (Zplus (Zmult v c1) l1) k1) (Zmult (Zplus (Zmult v c2) l2) k2)) - = (Zplus (Zmult v (Zplus (Zmult c1 k1) (Zmult c2 k2))) - (Zplus (Zmult l1 k1) (Zmult l2 k2))). - -Intros; Repeat (Rewrite Zmult_plus_distr_l Orelse Rewrite Zmult_plus_distr_r); -Repeat Rewrite Zmult_assoc; Repeat Elim Zplus_assoc; -Rewrite (Zplus_permute (Zmult l1 k1) (Zmult (Zmult v c2) k2)); Trivial with arith. -Qed. - -Theorem OMEGA11:(v1,c1,l1,l2,k1:Z) - (Zplus (Zmult (Zplus (Zmult v1 c1) l1) k1) l2) - = (Zplus (Zmult v1 (Zmult c1 k1)) (Zplus (Zmult l1 k1) l2)). - -Intros; Repeat (Rewrite Zmult_plus_distr_l Orelse Rewrite Zmult_plus_distr_r); -Repeat Rewrite Zmult_assoc; Repeat Elim Zplus_assoc; Trivial with arith. -Qed. - -Theorem OMEGA12:(v2,c2,l1,l2,k2:Z) - (Zplus l1 (Zmult (Zplus (Zmult v2 c2) l2) k2)) - = (Zplus (Zmult v2 (Zmult c2 k2)) (Zplus l1 (Zmult l2 k2))). - -Intros; Repeat (Rewrite Zmult_plus_distr_l Orelse Rewrite Zmult_plus_distr_r); -Repeat Rewrite Zmult_assoc; Repeat Elim Zplus_assoc; Rewrite Zplus_permute; -Trivial with arith. -Qed. - -Theorem OMEGA13:(v,l1,l2:Z)(x:positive) - (Zplus (Zplus (Zmult v (POS x)) l1) (Zplus (Zmult v (NEG x)) l2)) - = (Zplus l1 l2). - -Intros; Rewrite Zplus_assoc; Rewrite (Zplus_sym (Zmult v (POS x)) l1); -Rewrite (Zplus_assoc_r l1); Rewrite <- Zmult_plus_distr_r; -Rewrite <- Zopp_NEG; Rewrite (Zplus_sym (Zopp (NEG x)) (NEG x)); -Rewrite Zplus_inverse_r; Rewrite Zero_mult_right; Rewrite Zero_right; Trivial with arith. -Qed. - -Theorem OMEGA14:(v,l1,l2:Z)(x:positive) - (Zplus (Zplus (Zmult v (NEG x)) l1) (Zplus (Zmult v (POS x)) l2)) - = (Zplus l1 l2). - -Intros; Rewrite Zplus_assoc; Rewrite (Zplus_sym (Zmult v (NEG x)) l1); -Rewrite (Zplus_assoc_r l1); Rewrite <- Zmult_plus_distr_r; -Rewrite <- Zopp_NEG; Rewrite Zplus_inverse_r; Rewrite Zero_mult_right; -Rewrite Zero_right; Trivial with arith. -Qed. -Theorem OMEGA15:(v,c1,c2,l1,l2,k2:Z) - (Zplus (Zplus (Zmult v c1) l1) (Zmult (Zplus (Zmult v c2) l2) k2)) - = (Zplus (Zmult v (Zplus c1 (Zmult c2 k2))) - (Zplus l1 (Zmult l2 k2))). - -Intros; Repeat (Rewrite Zmult_plus_distr_l Orelse Rewrite Zmult_plus_distr_r); -Repeat Rewrite Zmult_assoc; Repeat Elim Zplus_assoc; -Rewrite (Zplus_permute l1 (Zmult (Zmult v c2) k2)); Trivial with arith. -Qed. - -Theorem OMEGA16: - (v,c,l,k:Z) - (Zmult (Zplus (Zmult v c) l) k) = (Zplus (Zmult v (Zmult c k)) (Zmult l k)). - -Intros; Repeat (Rewrite Zmult_plus_distr_l Orelse Rewrite Zmult_plus_distr_r); -Repeat Rewrite Zmult_assoc; Repeat Elim Zplus_assoc; Trivial with arith. -Qed. - -Theorem OMEGA17: - (x,y,z:Z)(Zne x ZERO) -> (y=ZERO) -> (Zne (Zplus x (Zmult y z)) ZERO). - -Unfold Zne not; Intros x y z H1 H2 H3; Apply H1; -Apply Zsimpl_plus_l with (Zmult y z); Rewrite Zplus_sym; Rewrite H3; -Rewrite H2; Auto with arith. -Qed. - -Theorem OMEGA18: - (x,y,k:Z) (x=(Zmult y k)) -> (Zne x ZERO) -> (Zne y ZERO). - -Unfold Zne not; Intros x y k H1 H2 H3; Apply H2; Rewrite H1; Rewrite H3; Auto with arith. -Qed. - -Theorem OMEGA19: - (x:Z) (Zne x ZERO) -> - (Zle ZERO (Zplus x (NEG xH))) \/ (Zle ZERO (Zplus (Zmult x (NEG xH)) (NEG xH))). - -Unfold Zne ; Intros x H; Elim (Zle_or_lt ZERO x); [ - Intros H1; Elim Zle_lt_or_eq with 1:=H1; [ - Intros H2; Left; Change (Zle ZERO (Zpred x)); Apply Zle_S_n; - Rewrite <- Zs_pred; Apply Zlt_le_S; Assumption - | Intros H2; Absurd x=ZERO; Auto with arith] -| Intros H1; Right; Rewrite <- Zopp_one; Rewrite Zplus_sym; - Apply Zle_left; Apply Zle_S_n; Simpl; Apply Zlt_le_S; Auto with arith]. -Qed. - -Theorem OMEGA20: - (x,y,z:Z)(Zne x ZERO) -> (y=ZERO) -> (Zne (Zplus x (Zmult y z)) ZERO). - -Unfold Zne not; Intros x y z H1 H2 H3; Apply H1; Rewrite H2 in H3; -Simpl in H3; Rewrite Zero_right in H3; Trivial with arith. -Qed. - -Definition fast_Zplus_sym := -[x,y:Z][P:Z -> Prop][H: (P (Zplus y x))] - (eq_ind_r Z (Zplus y x) P H (Zplus x y) (Zplus_sym x y)). - -Definition fast_Zplus_assoc_r := -[n,m,p:Z][P:Z -> Prop][H : (P (Zplus n (Zplus m p)))] - (eq_ind_r Z (Zplus n (Zplus m p)) P H (Zplus (Zplus n m) p) (Zplus_assoc_r n m p)). - -Definition fast_Zplus_assoc_l := -[n,m,p:Z][P:Z -> Prop][H : (P (Zplus (Zplus n m) p))] - (eq_ind_r Z (Zplus (Zplus n m) p) P H (Zplus n (Zplus m p)) - (Zplus_assoc_l n m p)). - -Definition fast_Zplus_permute := -[n,m,p:Z][P:Z -> Prop][H : (P (Zplus m (Zplus n p)))] - (eq_ind_r Z (Zplus m (Zplus n p)) P H (Zplus n (Zplus m p)) - (Zplus_permute n m p)). - -Definition fast_OMEGA10 := -[v,c1,c2,l1,l2,k1,k2:Z][P:Z -> Prop] -[H : (P (Zplus (Zmult v (Zplus (Zmult c1 k1) (Zmult c2 k2))) - (Zplus (Zmult l1 k1) (Zmult l2 k2))))] - (eq_ind_r Z - (Zplus (Zmult v (Zplus (Zmult c1 k1) (Zmult c2 k2))) - (Zplus (Zmult l1 k1) (Zmult l2 k2))) - P H - (Zplus (Zmult (Zplus (Zmult v c1) l1) k1) - (Zmult (Zplus (Zmult v c2) l2) k2)) - (OMEGA10 v c1 c2 l1 l2 k1 k2)). - -Definition fast_OMEGA11 := -[v1,c1,l1,l2,k1:Z][P:Z -> Prop] -[H : (P (Zplus (Zmult v1 (Zmult c1 k1)) (Zplus (Zmult l1 k1) l2)))] - (eq_ind_r Z - (Zplus (Zmult v1 (Zmult c1 k1)) (Zplus (Zmult l1 k1) l2)) - P H - (Zplus (Zmult (Zplus (Zmult v1 c1) l1) k1) l2) - (OMEGA11 v1 c1 l1 l2 k1)). -Definition fast_OMEGA12 := -[v2,c2,l1,l2,k2:Z][P:Z -> Prop] -[H : (P (Zplus (Zmult v2 (Zmult c2 k2)) (Zplus l1 (Zmult l2 k2))))] - (eq_ind_r Z - (Zplus (Zmult v2 (Zmult c2 k2)) (Zplus l1 (Zmult l2 k2))) - P H - (Zplus l1 (Zmult (Zplus (Zmult v2 c2) l2) k2)) - (OMEGA12 v2 c2 l1 l2 k2)). - -Definition fast_OMEGA15 := -[v,c1,c2,l1,l2,k2 :Z][P:Z -> Prop] -[H : (P (Zplus (Zmult v (Zplus c1 (Zmult c2 k2))) (Zplus l1 (Zmult l2 k2))))] - (eq_ind_r Z - (Zplus (Zmult v (Zplus c1 (Zmult c2 k2))) (Zplus l1 (Zmult l2 k2))) - P H - (Zplus (Zplus (Zmult v c1) l1) (Zmult (Zplus (Zmult v c2) l2) k2)) - (OMEGA15 v c1 c2 l1 l2 k2)). -Definition fast_OMEGA16 := -[v,c,l,k :Z][P:Z -> Prop] -[H : (P (Zplus (Zmult v (Zmult c k)) (Zmult l k)))] - (eq_ind_r Z - (Zplus (Zmult v (Zmult c k)) (Zmult l k)) - P H - (Zmult (Zplus (Zmult v c) l) k) - (OMEGA16 v c l k)). - -Definition fast_OMEGA13 := -[v,l1,l2 :Z][x:positive][P:Z -> Prop] -[H : (P (Zplus l1 l2))] - (eq_ind_r Z - (Zplus l1 l2) - P H - (Zplus (Zplus (Zmult v (POS x)) l1) (Zplus (Zmult v (NEG x)) l2)) - (OMEGA13 v l1 l2 x )). - -Definition fast_OMEGA14 := -[v,l1,l2 :Z][x:positive][P:Z -> Prop] -[H : (P (Zplus l1 l2))] - (eq_ind_r Z - (Zplus l1 l2) - P H - (Zplus (Zplus (Zmult v (NEG x)) l1) (Zplus (Zmult v (POS x)) l2)) - (OMEGA14 v l1 l2 x )). -Definition fast_Zred_factor0:= -[x:Z][P:Z -> Prop] -[H : (P (Zmult x (POS xH)) )] - (eq_ind_r Z - (Zmult x (POS xH)) - P H - x - (Zred_factor0 x)). - -Definition fast_Zopp_one := -[x:Z][P:Z -> Prop] -[H : (P (Zmult x (NEG xH)))] - (eq_ind_r Z - (Zmult x (NEG xH)) - P H - (Zopp x) - (Zopp_one x)). - -Definition fast_Zmult_sym := -[x,y :Z][P:Z -> Prop] -[H : (P (Zmult y x))] - (eq_ind_r Z -(Zmult y x) - P H -(Zmult x y) - (Zmult_sym x y )). - -Definition fast_Zopp_Zplus := -[x,y :Z][P:Z -> Prop] -[H : (P (Zplus (Zopp x) (Zopp y)) )] - (eq_ind_r Z - (Zplus (Zopp x) (Zopp y)) - P H - (Zopp (Zplus x y)) - (Zopp_Zplus x y )). - -Definition fast_Zopp_Zopp := -[x:Z][P:Z -> Prop] -[H : (P x )] (eq_ind_r Z x P H (Zopp (Zopp x)) (Zopp_Zopp x)). - -Definition fast_Zopp_Zmult_r := -[x,y:Z][P:Z -> Prop] -[H : (P (Zmult x (Zopp y)))] - (eq_ind_r Z - (Zmult x (Zopp y)) - P H - (Zopp (Zmult x y)) - (Zopp_Zmult_r x y )). - -Definition fast_Zmult_plus_distr := -[n,m,p:Z][P:Z -> Prop] -[H : (P (Zplus (Zmult n p) (Zmult m p)))] - (eq_ind_r Z - (Zplus (Zmult n p) (Zmult m p)) - P H - (Zmult (Zplus n m) p) - (Zmult_plus_distr_l n m p)). -Definition fast_Zmult_Zopp_left:= -[x,y:Z][P:Z -> Prop] -[H : (P (Zmult x (Zopp y)))] - (eq_ind_r Z - (Zmult x (Zopp y)) - P H - (Zmult (Zopp x) y) - (Zmult_Zopp_left x y)). - -Definition fast_Zmult_assoc_r := -[n,m,p :Z][P:Z -> Prop] -[H : (P (Zmult n (Zmult m p)))] - (eq_ind_r Z - (Zmult n (Zmult m p)) - P H - (Zmult (Zmult n m) p) - (Zmult_assoc_r n m p)). - -Definition fast_Zred_factor1 := -[x:Z][P:Z -> Prop] -[H : (P (Zmult x (POS (xO xH))) )] - (eq_ind_r Z - (Zmult x (POS (xO xH))) - P H - (Zplus x x) - (Zred_factor1 x)). - -Definition fast_Zred_factor2 := -[x,y:Z][P:Z -> Prop] -[H : (P (Zmult x (Zplus (POS xH) y)))] - (eq_ind_r Z - (Zmult x (Zplus (POS xH) y)) - P H - (Zplus x (Zmult x y)) - (Zred_factor2 x y)). -Definition fast_Zred_factor3 := -[x,y:Z][P:Z -> Prop] -[H : (P (Zmult x (Zplus (POS xH) y)))] - (eq_ind_r Z - (Zmult x (Zplus (POS xH) y)) - P H - (Zplus (Zmult x y) x) - (Zred_factor3 x y)). - -Definition fast_Zred_factor4 := -[x,y,z:Z][P:Z -> Prop] -[H : (P (Zmult x (Zplus y z)))] - (eq_ind_r Z - (Zmult x (Zplus y z)) - P H - (Zplus (Zmult x y) (Zmult x z)) - (Zred_factor4 x y z)). - -Definition fast_Zred_factor5 := -[x,y:Z][P:Z -> Prop] -[H : (P y)] - (eq_ind_r Z - y - P H - (Zplus (Zmult x ZERO) y) - (Zred_factor5 x y)). - -Definition fast_Zred_factor6 := -[x :Z][P:Z -> Prop] -[H : (P(Zplus x ZERO) )] - (eq_ind_r Z - (Zplus x ZERO) - P H - x - (Zred_factor6 x )). +V7only [Notation OMEGA2 := Zle_0_plus.]. diff --git a/theories/ZArith/fast_integer.v b/theories/ZArith/fast_integer.v index 04bf712a9..ff046ed63 100644 --- a/theories/ZArith/fast_integer.v +++ b/theories/ZArith/fast_integer.v @@ -12,1472 +12,14 @@ (** Binary Integers (Pierre Crégut, CNET, Lannion, France) *) (***********************************************************) -(**********************************************************************) -(** Binary positive numbers *) - -Inductive positive : Set := - xI : positive -> positive -| xO : positive -> positive -| xH : positive. - -(* Declare Scope positive_scope with Key P *) -Delimits Scope positive_scope with positive. - -(* Automatically open scope positive_scope for type positive, xO and xI *) -Bind Scope positive_scope with positive. -Arguments Scope xO [ positive_scope ]. -Arguments Scope xI [ positive_scope ]. - -(** Successor *) - -Fixpoint add_un [x:positive]:positive := - Cases x of - (xI x') => (xO (add_un x')) - | (xO x') => (xI x') - | xH => (xO xH) - end. - -(** Addition *) - -Fixpoint add [x:positive]:positive -> positive := [y:positive] - Cases x y of - | (xI x') (xI y') => (xO (add_carry x' y')) - | (xI x') (xO y') => (xI (add x' y')) - | (xI x') xH => (xO (add_un x')) - | (xO x') (xI y') => (xI (add x' y')) - | (xO x') (xO y') => (xO (add x' y')) - | (xO x') xH => (xI x') - | xH (xI y') => (xO (add_un y')) - | xH (xO y') => (xI y') - | xH xH => (xO xH) - end -with add_carry [x:positive]:positive -> positive := [y:positive] - Cases x y of - | (xI x') (xI y') => (xI (add_carry x' y')) - | (xI x') (xO y') => (xO (add_carry x' y')) - | (xI x') xH => (xI (add_un x')) - | (xO x') (xI y') => (xO (add_carry x' y')) - | (xO x') (xO y') => (xI (add x' y')) - | (xO x') xH => (xO (add_un x')) - | xH (xI y') => (xI (add_un y')) - | xH (xO y') => (xO (add_un y')) - | xH xH => (xI xH) - end. - -V7only [Notation "x + y" := (add x y) : positive_scope.]. -V8Infix "+" add : positive_scope. - -Open Local Scope positive_scope. - -(** From binary positive numbers to Peano natural numbers *) - -Fixpoint positive_to_nat [x:positive]:nat -> nat := - [pow2:nat] - <nat> Cases x of - (xI x') => (plus pow2 (positive_to_nat x' (plus pow2 pow2))) - | (xO x') => (positive_to_nat x' (plus pow2 pow2)) - | xH => pow2 - end. - -Definition convert := [x:positive] (positive_to_nat x (S O)). - -(** From Peano natural numbers to binary positive numbers *) - -Fixpoint anti_convert [n:nat]: positive := - Cases n of - O => xH - | (S x') => (add_un (anti_convert x')) - end. - -(** Subtraction *) - -Fixpoint double_moins_un [x:positive]:positive := - Cases x of - (xI x') => (xI (xO x')) - | (xO x') => (xI (double_moins_un x')) - | xH => xH - end. - -(** Predecessor *) - -Definition sub_un := [x:positive] - Cases x of - (xI x') => (xO x') - | (xO x') => (double_moins_un x') - | xH => xH - end. - -(** An auxiliary type for subtraction *) - -Inductive positive_mask: Set := - IsNul : positive_mask - | IsPos : positive -> positive_mask - | IsNeg : positive_mask. - -(** Operation x -> 2*x+1 *) - -Definition Un_suivi_de_mask := [x:positive_mask] - Cases x of IsNul => (IsPos xH) | IsNeg => IsNeg | (IsPos p) => (IsPos (xI p)) end. - -(** Operation x -> 2*x *) - -Definition Zero_suivi_de_mask := [x:positive_mask] - Cases x of IsNul => IsNul | IsNeg => IsNeg | (IsPos p) => (IsPos (xO p)) end. - -(** Operation x -> 2*x-2 *) - -Definition double_moins_deux := - [x:positive] Cases x of - (xI x') => (IsPos (xO (xO x'))) - | (xO x') => (IsPos (xO (double_moins_un x'))) - | xH => IsNul - end. - -(** Subtraction of binary positive numbers into a positive numbers mask *) - -Fixpoint sub_pos[x,y:positive]:positive_mask := - Cases x y of - | (xI x') (xI y') => (Zero_suivi_de_mask (sub_pos x' y')) - | (xI x') (xO y') => (Un_suivi_de_mask (sub_pos x' y')) - | (xI x') xH => (IsPos (xO x')) - | (xO x') (xI y') => (Un_suivi_de_mask (sub_neg x' y')) - | (xO x') (xO y') => (Zero_suivi_de_mask (sub_pos x' y')) - | (xO x') xH => (IsPos (double_moins_un x')) - | xH xH => IsNul - | xH _ => IsNeg - end -with sub_neg [x,y:positive]:positive_mask := - Cases x y of - (xI x') (xI y') => (Un_suivi_de_mask (sub_neg x' y')) - | (xI x') (xO y') => (Zero_suivi_de_mask (sub_pos x' y')) - | (xI x') xH => (IsPos (double_moins_un x')) - | (xO x') (xI y') => (Zero_suivi_de_mask (sub_neg x' y')) - | (xO x') (xO y') => (Un_suivi_de_mask (sub_neg x' y')) - | (xO x') xH => (double_moins_deux x') - | xH _ => IsNeg - end. - -(** Subtraction of binary positive numbers x and y, returns 1 if x<=y *) - -Definition true_sub := [x,y:positive] - Cases (sub_pos x y) of (IsPos z) => z | _ => xH end. - -V8Infix "-" true_sub : positive_scope. - -(** Multiplication on binary positive numbers *) - -Fixpoint times [x:positive] : positive -> positive:= - [y:positive] - Cases x of - (xI x') => (add y (xO (times x' y))) - | (xO x') => (xO (times x' y)) - | xH => y - end. - -V8Infix "*" times : positive_scope. - -(** Division by 2 rounded below but for 1 *) - -Definition Zdiv2_pos := - [z:positive]Cases z of xH => xH - | (xO p) => p - | (xI p) => p - end. - -V8Infix "/" Zdiv2_pos : positive_scope. - -(**********************************************************************) -(** Comparison on binary positive numbers *) -V7only [Notation relation := Datatypes.relation.]. - -Fixpoint compare [x,y:positive]: relation -> relation := - [r:relation] - Cases x y of - | (xI x') (xI y') => (compare x' y' r) - | (xI x') (xO y') => (compare x' y' SUPERIEUR) - | (xI x') xH => SUPERIEUR - | (xO x') (xI y') => (compare x' y' INFERIEUR) - | (xO x') (xO y') => (compare x' y' r) - | (xO x') xH => SUPERIEUR - | xH (xI y') => INFERIEUR - | xH (xO y') => INFERIEUR - | xH xH => r - end. - -Theorem compare_convert1 : - (x,y:positive) - ~(compare x y SUPERIEUR) = EGAL /\ ~(compare x y INFERIEUR) = EGAL. -Proof. -Induction x;Induction y;Split;Simpl;Auto; - Discriminate Orelse (Elim (H p0); Auto). -Qed. - -Theorem compare_convert_EGAL : (x,y:positive) (compare x y EGAL) = EGAL -> x=y. -Proof. -Induction x;Induction y;Simpl;Auto; [ - Intros z H1 H2; Rewrite (H z); Trivial -| Intros z H1 H2; Absurd (compare p z SUPERIEUR)=EGAL ; - [ Elim (compare_convert1 p z);Auto | Assumption ] -| Intros H1;Discriminate H1 -| Intros z H1 H2; Absurd (compare p z INFERIEUR) = EGAL; - [ Elim (compare_convert1 p z);Auto | Assumption ] -| Intros z H1 H2 ;Rewrite (H z);Auto -| Intros H1;Discriminate H1 -| Intros p H H1;Discriminate H1 -| Intros p H H1;Discriminate H1 ]. -Qed. - -Lemma ZLSI: - (x,y:positive) (compare x y SUPERIEUR) = INFERIEUR -> - (compare x y EGAL) = INFERIEUR. -Proof. -Induction x;Induction y;Simpl;Auto; - Discriminate Orelse Intros H;Discriminate H. -Qed. - -Lemma ZLIS: - (x,y:positive) (compare x y INFERIEUR) = SUPERIEUR -> - (compare x y EGAL) = SUPERIEUR. -Proof. -Induction x;Induction y;Simpl;Auto; - Discriminate Orelse Intros H;Discriminate H. -Qed. - -Lemma ZLII: - (x,y:positive) (compare x y INFERIEUR) = INFERIEUR -> - (compare x y EGAL) = INFERIEUR \/ x = y. -Proof. -(Induction x;Induction y;Simpl;Auto;Try Discriminate); - Intros z H1 H2; Elim (H z H2);Auto; Intros E;Rewrite E; - Auto. -Qed. - -Lemma ZLSS: - (x,y:positive) (compare x y SUPERIEUR) = SUPERIEUR -> - (compare x y EGAL) = SUPERIEUR \/ x = y. -Proof. -(Induction x;Induction y;Simpl;Auto;Try Discriminate); - Intros z H1 H2; Elim (H z H2);Auto; Intros E;Rewrite E; - Auto. -Qed. - -Lemma Dcompare : (r:relation) r=EGAL \/ r = INFERIEUR \/ r = SUPERIEUR. -Proof. -Induction r; Auto. -Qed. - -Tactic Definition ElimPcompare c1 c2:= - Elim (Dcompare (compare c1 c2 EGAL)); [ Idtac | - Let x = FreshId "H" In Intro x; Case x; Clear x ]. - -Theorem convert_compare_EGAL: (x:positive)(compare x x EGAL)=EGAL. -Induction x; Auto. -Qed. - -(**********************************************************************) -(** Miscellaneous properties of binary positive numbers *) - -Lemma ZL11: (x:positive) (x=xH) \/ ~(x=xH). -Proof. -Intros x;Case x;Intros; (Left;Reflexivity) Orelse (Right;Discriminate). -Qed. - -(**********************************************************************) -(** Properties of successor on binary positive numbers *) - -(** Specification of [xI] in term of [Psucc] and [xO] *) - -Lemma xI_add_un_xO : (x:positive)(xI x) = (add_un (xO x)). -Proof. -Reflexivity. -Qed. - -(** Successor and double *) - -Lemma is_double_moins_un : (x:positive) (add_un (double_moins_un x)) = (xO x). -Proof. -NewInduction x as [x IHx|x|]; Simpl; Try Rewrite IHx; Reflexivity. -Qed. - -Lemma double_moins_un_add_un_xI : - (x:positive)(double_moins_un (add_un x))=(xI x). -Proof. -NewInduction x as [x IHx|x|]; Simpl; Try Rewrite IHx; Reflexivity. -Qed. - -Lemma ZL1: (y:positive)(xO (add_un y)) = (add_un (add_un (xO y))). -Proof. -Induction y; Simpl; Auto. -Qed. - -(** Successor and predecessor *) - -Lemma add_un_not_un : (x:positive) (add_un x) <> xH. -Proof. -NewDestruct x as [x|x|]; Discriminate. -Qed. - -Lemma sub_add_one : (x:positive) (sub_un (add_un x)) = x. -Proof. -(Induction x; [Idtac | Idtac | Simpl;Auto]); -(Intros p; Elim p; [Idtac | Idtac | Simpl;Auto]); -Simpl; Intros q H1 H2; Case H2; Simpl; Trivial. -Qed. - -Lemma add_sub_one : (x:positive) (x=xH) \/ (add_un (sub_un x)) = x. -Proof. -Induction x; [ - Simpl; Auto -| Simpl; Intros;Right;Apply is_double_moins_un -| Auto ]. -Qed. - -(** Injectivity of successor *) - -Lemma add_un_inj : (x,y:positive) (add_un x)=(add_un y) -> x=y. -Proof. -NewInduction x; NewDestruct y as [y|y|]; Simpl; - Intro H; Discriminate H Orelse Try (Injection H; Clear H; Intro H). -Rewrite (IHx y H); Reflexivity. -Absurd (add_un x)=xH; [ Apply add_un_not_un | Assumption ]. -Apply f_equal with 1:=H; Assumption. -Absurd (add_un y)=xH; [ Apply add_un_not_un | Symmetry; Assumption ]. -Reflexivity. -Qed. - -(**********************************************************************) -(** Properties of addition on binary positive numbers *) - -(** Specification of [Psucc] in term of [Pplus] *) - -Lemma ZL12: (q:positive) (add_un q) = (add q xH). -Proof. -NewDestruct q; Reflexivity. -Qed. - -Lemma ZL12bis: (q:positive) (add_un q) = (add xH q). -Proof. -NewDestruct q; Reflexivity. -Qed. - -(** Specification of [Pplus_carry] *) - -Theorem ZL13: (x,y:positive)(add_carry x y) = (add_un (add x y)). -Proof. -(Induction x;Induction y;Simpl;Auto); Intros q H1;Rewrite H; - Auto. -Qed. - -(** Commutativity *) - -Theorem add_sym : (x,y:positive) (add x y) = (add y x). -Proof. -Induction x;Induction y;Simpl;Auto; Intros q H1; [ - Clear H1; Do 2 Rewrite ZL13; Rewrite H;Auto -| Rewrite H;Auto | Rewrite H;Auto | Rewrite H;Auto ]. -Qed. - -(** Permutation of [Pplus] and [Psucc] *) - -Theorem ZL14: (x,y:positive)(add x (add_un y)) = (add_un (add x y)). -Proof. -Induction x;Induction y;Simpl;Auto; [ - Intros q H1; Rewrite ZL13; Rewrite H; Auto -| Intros q H1; Rewrite ZL13; Auto -| Elim p;Simpl;Auto -| Intros q H1;Rewrite H;Auto -| Elim p;Simpl;Auto ]. -Qed. - -Theorem ZL14bis: (x,y:positive)(add (add_un x) y) = (add_un (add x y)). -Proof. -Intros x y; Rewrite add_sym; Rewrite add_sym with x:=x; Apply ZL14. -Qed. - -Theorem ZL15: (q,z:positive) ~z=xH -> (add_carry q (sub_un z)) = (add q z). -Proof. -Intros q z H; Elim (add_sub_one z); [ - Intro;Absurd z=xH;Auto -| Intros E;Pattern 2 z ;Rewrite <- E; Rewrite ZL14; Rewrite ZL13; Trivial ]. -Qed. - -(** No neutral for addition on strictly positive numbers *) - -Lemma add_no_neutral : (x,y:positive) ~(add y x)=x. -Proof. -NewInduction x; NewDestruct y as [y|y|]; Simpl; Intro H; - Discriminate H Orelse Injection H; Clear H; Intro H; Apply (IHx y H). -Qed. - -Lemma add_carry_not_add_un : (x,y:positive) ~(add_carry y x)=(add_un x). -Proof. -Intros x y H; Absurd (add y x)=x; - [ Apply add_no_neutral - | Apply add_un_inj; Rewrite <- ZL13; Assumption ]. -Qed. - -(** Simplification *) - -Lemma add_carry_add : - (x,y,z,t:positive) (add_carry x z)=(add_carry y t) -> (add x z)=(add y t). -Proof. -Intros x y z t H; Apply add_un_inj; Do 2 Rewrite <- ZL13; Assumption. -Qed. - -Lemma simpl_add_r : (x,y,z:positive) (add x z)=(add y z) -> x=y. -Proof. -Intros x y z; Generalize x y; Clear x y. -NewInduction z as [z|z|]. - NewDestruct x as [x|x|]; NewDestruct y as [y|y|]; Simpl; Intro H; - Discriminate H Orelse Try (Injection H; Clear H; Intro H). - Rewrite IHz with 1:=(add_carry_add ? ? ? ? H); Reflexivity. - Absurd (add_carry x z)=(add_un z); - [ Apply add_carry_not_add_un | Assumption ]. - Rewrite IHz with 1:=H; Reflexivity. - Symmetry in H; Absurd (add_carry y z)=(add_un z); - [ Apply add_carry_not_add_un | Assumption ]. - Reflexivity. - NewDestruct x as [x|x|]; NewDestruct y as [y|y|]; Simpl; Intro H; - Discriminate H Orelse Try (Injection H; Clear H; Intro H). - Rewrite IHz with 1:=H; Reflexivity. - Absurd (add x z)=z; [ Apply add_no_neutral | Assumption ]. - Rewrite IHz with 1:=H; Reflexivity. - Symmetry in H; Absurd y+z=z; [ Apply add_no_neutral | Assumption ]. - Reflexivity. - Intros H x y; Apply add_un_inj; Do 2 Rewrite ZL12; Assumption. -Qed. - -Lemma simpl_add_carry_r : - (x,y,z:positive) (add_carry x z)=(add_carry y z) -> x=y. -Proof. -Intros x y z H; Apply simpl_add_r with z:=z; Apply add_carry_add; Assumption. -Qed. - -Lemma simpl_add_l : (x,y,z:positive) (add x y)=(add x z) -> y=z. -Proof. -Intros x y z H;Apply simpl_add_r with z:=x; - Rewrite add_sym with x:=z; Rewrite add_sym with x:=y; Assumption. -Qed. - -Lemma simpl_add_carry_l : - (x,y,z:positive) (add_carry x y)=(add_carry x z) -> y=z. -Proof. -Intros x y z H;Apply simpl_add_r with z:=x; -Rewrite add_sym with x:=z; Rewrite add_sym with x:=y; Apply add_carry_add; -Assumption. -Qed. - -(** Addition on positive is associative *) - -Theorem add_assoc: (x,y,z:positive)(add x (add y z)) = (add (add x y) z). -Proof. -Intros x y; Generalize x; Clear x. -NewInduction y as [y|y|]. - NewDestruct x as [x|x|]; NewDestruct z as [z|z|]; Simpl; Repeat Rewrite ZL13; - Repeat Rewrite ZL14; Repeat Rewrite ZL14bis; Reflexivity Orelse - Repeat Apply f_equal with A:=positive; Apply IHy. - NewDestruct x as [x|x|]; NewDestruct z as [z|z|]; Simpl; Repeat Rewrite ZL13; - Repeat Rewrite ZL14; Repeat Rewrite ZL14bis; Reflexivity Orelse - Repeat Apply f_equal with A:=positive; Apply IHy. - Intros x z; Rewrite add_sym with x:=xH; Do 2 Rewrite <- ZL12; Rewrite ZL14bis; Rewrite ZL14; Reflexivity. -Qed. - -(** Commutation of addition with the double of a positive number *) - -Lemma add_xI_double_moins_un : - (p,q:positive)(xO (add p q)) = (add (xI p) (double_moins_un q)). -Proof. -Intros; Change (xI p) with (add (xO p) xH). -Rewrite <- add_assoc; Rewrite <- ZL12bis; Rewrite is_double_moins_un. -Reflexivity. -Qed. - -(* xO_xI_plus_double_moins_un = add_xI_double_moins_un *) - -Lemma double_moins_un_plus_xO_double_moins_un : - (p,q:positive) (double_moins_un (add p q)) = (add (xO p) (double_moins_un q)). -Proof. -NewInduction p as [p IHp|p IHp|]; NewDestruct q as [q|q|]; - Simpl; Try Rewrite ZL13; Try Rewrite double_moins_un_add_un_xI; - Try Rewrite IHp; Try Rewrite add_xI_double_moins_un; Try Reflexivity. - Rewrite <- is_double_moins_un; Rewrite ZL12bis; Reflexivity. -Qed. - -(* double_moins_un_add = double_moins_un_plus_xO_double_moins_un *) - -(** Misc *) - -Lemma add_x_x : (x:positive) (add x x) = (xO x). -Proof. -NewInduction x; Simpl; Try Rewrite ZL13; Try Rewrite IHx; Reflexivity. -Qed. - -(**********************************************************************) -(** Peano induction on binary positive positive numbers *) - -Fixpoint add_iter [x:positive] : positive -> positive := - [y]Cases x of - | xH => (add_un y) - | (xO x) => (add_iter x (add_iter x y)) - | (xI x) => (add_iter x (add_iter x (add_un y))) - end. - -Lemma add_iter_add : (x,y:positive)(add_iter x y)=(add x y). -Proof. -NewInduction x as [p IHp|p IHp|]; NewDestruct y; Simpl; - Reflexivity Orelse Do 2 Rewrite IHp; Rewrite add_assoc; Rewrite add_x_x; - Try Reflexivity. -Rewrite ZL13; Rewrite <- ZL14; Reflexivity. -Rewrite ZL12; Reflexivity. -Qed. - -Lemma add_iter_xO : (x:positive)(add_iter x x)=(xO x). -Proof. -Intro; Rewrite <- add_x_x; Apply add_iter_add. -Qed. - -Lemma add_iter_xI : (x:positive)(add_un (add_iter x x))=(xI x). -Proof. -Intro; Rewrite xI_add_un_xO; Rewrite <- add_x_x; - Apply (f_equal positive); Apply add_iter_add. -Qed. - -Lemma iterate_add : (P:(positive->Type)) - ((n:positive)(P n) ->(P (add_un n)))->(p,n:positive)(P n) -> - (P (add_iter p n)). -Proof. -Intros P H; NewInduction p; Simpl; Intros. -Apply IHp; Apply IHp; Apply H; Assumption. -Apply IHp; Apply IHp; Assumption. -Apply H; Assumption. -Defined. - -(** Peano induction *) - -Theorem Pind : (P:(positive->Prop)) - (P xH) ->((n:positive)(P n) ->(P (add_un n))) ->(n:positive)(P n). -Proof. -Intros P H1 Hsucc; NewInduction n. -Rewrite <- add_iter_xI; Apply Hsucc; Apply iterate_add; Assumption. -Rewrite <- add_iter_xO; Apply iterate_add; Assumption. -Assumption. -Qed. - -(** Peano recursion *) - -Definition Prec : (A:Set)A->(positive->A->A)->positive->A := - [A;a;f]Fix Prec { Prec [p:positive] : A := - Cases p of - | xH => a - | (xO p) => (iterate_add [_]A f p p (Prec p)) - | (xI p) => (f (add_iter p p) (iterate_add [_]A f p p (Prec p))) - end}. - -(** Test *) - -Check - let fact = (Prec positive xH [p;r](times (add_un p) r)) in - let seven = (xI (xI xH)) in - let five_thousand_forty= (xO(xO(xO(xO(xI(xI(xO(xI(xI(xI(xO(xO xH)))))))))))) - in ((refl_equal ? ?) :: (fact seven) = five_thousand_forty). - -(**********************************************************************) -(** Properties of minus on binary positive numbers *) - -(* Properties of subtraction *) - -Lemma ZS: (p:positive_mask) (Zero_suivi_de_mask p) = IsNul -> p = IsNul. -Proof. -NewDestruct p; Simpl; [ Trivial | Discriminate 1 | Discriminate 1 ]. -Qed. - -Lemma US: (p:positive_mask) ~(Un_suivi_de_mask p)=IsNul. -Proof. -Induction p; Intros; Discriminate. -Qed. - -Lemma USH: (p:positive_mask) (Un_suivi_de_mask p) = (IsPos xH) -> p = IsNul. -Proof. -NewDestruct p; Simpl; [ Trivial | Discriminate 1 | Discriminate 1 ]. -Qed. - -Lemma ZSH: (p:positive_mask) ~(Zero_suivi_de_mask p)= (IsPos xH). -Proof. -Induction p; Intros; Discriminate. -Qed. - -Theorem sub_pos_x_x : (x:positive) (sub_pos x x) = IsNul. -Proof. -Induction x; [ - Simpl; Intros p H;Rewrite H;Simpl; Trivial -| Intros p H;Simpl;Rewrite H;Auto -| Auto ]. -Qed. - -Theorem ZL10: (x,y:positive) - (sub_pos x y) = (IsPos xH) -> (sub_neg x y) = IsNul. -Proof. -NewInduction x as [p|p|]; NewDestruct y as [q|q|]; Simpl; Intro H; -Try Discriminate H; [ - Absurd (Zero_suivi_de_mask (sub_pos p q))=(IsPos xH); - [ Apply ZSH | Assumption ] -| Assert Heq : (sub_pos p q)=IsNul; - [ Apply USH;Assumption | Rewrite Heq; Reflexivity ] -| Assert Heq : (sub_neg p q)=IsNul; - [ Apply USH;Assumption | Rewrite Heq; Reflexivity ] -| Absurd (Zero_suivi_de_mask (sub_pos p q))=(IsPos xH); - [ Apply ZSH | Assumption ] -| NewDestruct p; Simpl; [ Discriminate H | Discriminate H | Reflexivity ] ]. -Qed. - -(* Properties valid only for x>y *) - -Theorem sub_pos_SUPERIEUR: - (x,y:positive)(compare x y EGAL)=SUPERIEUR -> - (EX h:positive | (sub_pos x y) = (IsPos h) /\ (add y h) = x /\ - (h = xH \/ (sub_neg x y) = (IsPos (sub_un h)))). -Proof. -NewInduction x as [p|p|];NewDestruct y as [q|q|]; Simpl; Intro H; - Try Discriminate H. - NewDestruct (IHp q H) as [z [H4 [H6 H7]]]; Exists (xO z); Split. - Rewrite H4; Reflexivity. - Split. - Simpl; Rewrite H6; Reflexivity. - Right; Clear H6; NewDestruct (ZL11 z) as [H8|H8]; [ - Rewrite H8; Rewrite H8 in H4; - Rewrite ZL10; [ Reflexivity | Assumption ] - | Clear H4; NewDestruct H7 as [H9|H9]; [ - Absurd z=xH; Assumption - | Rewrite H9; Clear H9; NewDestruct z; - [ Reflexivity | Reflexivity | Absurd xH=xH; Trivial ]]]. - Case ZLSS with 1:=H; [ - Intros H3;Elim (IHp q H3); Intros z H4; Exists (xI z); - Elim H4;Intros H5 H6;Elim H6;Intros H7 H8; Split; [ - Simpl;Rewrite H5;Auto - | Split; [ - Simpl; Rewrite H7; Trivial - | Right; - Change (Zero_suivi_de_mask (sub_pos p q))=(IsPos (sub_un (xI z))); - Rewrite H5; Auto ]] - | Intros H3; Exists xH; Rewrite H3; Split; [ - Simpl; Rewrite sub_pos_x_x; Auto - | Split; Auto ]]. - Exists (xO p); Auto. - NewDestruct (IHp q) as [z [H4 [H6 H7]]]. - Apply ZLIS; Assumption. - NewDestruct (ZL11 z) as [vZ|]; [ - Exists xH; Split; [ - Rewrite ZL10; [ Reflexivity | Rewrite vZ in H4;Assumption ] - | Split; [ - Simpl; Rewrite ZL12; Rewrite <- vZ; Rewrite H6; Trivial - | Auto ]] - | Exists (xI (sub_un z)); NewDestruct H7 as [|H8];[ - Absurd z=xH;Assumption - | Split; [ - Rewrite H8; Trivial - | Split; [ Simpl; Rewrite ZL15; [ - Rewrite H6;Trivial - | Assumption ] - | Right; Rewrite H8; Reflexivity]]]]. - NewDestruct (IHp q H) as [z [H4 [H6 H7]]]. - Exists (xO z); Split; [ - Rewrite H4;Auto - | Split; [ - Simpl;Rewrite H6;Reflexivity - | Right; - Change (Un_suivi_de_mask (sub_neg p q))=(IsPos (double_moins_un z)); - NewDestruct (ZL11 z) as [H8|H8]; [ - Rewrite H8; Simpl; - Assert H9:(sub_neg p q)=IsNul;[ - Apply ZL10;Rewrite <- H8;Assumption - | Rewrite H9;Reflexivity ] - | NewDestruct H7 as [H9|H9]; [ - Absurd z=xH;Auto - | Rewrite H9; NewDestruct z; Simpl; - [ Reflexivity - | Reflexivity - | Absurd xH=xH; [Assumption | Reflexivity]]]]]]. - Exists (double_moins_un p); Split; [ - Reflexivity - | Clear IHp; Split; [ - NewDestruct p; Simpl; [ - Reflexivity - | Rewrite is_double_moins_un; Reflexivity - | Reflexivity ] - | NewDestruct p; [Right|Right|Left]; Reflexivity ]]. -Qed. - -Theorem sub_add: -(x,y:positive) (compare x y EGAL) = SUPERIEUR -> (add y (true_sub x y)) = x. -Proof. -Intros x y H;Elim sub_pos_SUPERIEUR with 1:=H; -Intros z H1;Elim H1;Intros H2 H3; Elim H3;Intros H4 H5; -Unfold true_sub ;Rewrite H2; Exact H4. -Qed. - -(**********************************************************************) -(** Properties of the injection from binary positive numbers to Peano - natural numbers *) - +Require Export BinPos. Require Le. Require Lt. Require Gt. Require Plus. Require Mult. -Require Minus. - -(** [IPN] is a morphism for addition *) - -Lemma convert_add_un : - (x:positive)(m:nat) - (positive_to_nat (add_un x) m) = (plus m (positive_to_nat x m)). -Proof. -Induction x; Simpl; Auto; Intros x' H0 m; Rewrite H0; -Rewrite plus_assoc_l; Trivial. -Qed. - -Theorem convert_add_carry : - (x,y:positive)(m:nat) - (positive_to_nat (add_carry x y) m) = - (plus m (positive_to_nat (add x y) m)). -Proof. -Induction x; Induction y; Simpl; Auto with arith; [ - Intros y' H1 m; Rewrite H; Rewrite plus_assoc_l; Trivial with arith -| Intros y' H1 m; Rewrite H; Rewrite plus_assoc_l; Trivial with arith -| Intros m; Rewrite convert_add_un; Rewrite plus_assoc_l; Trivial with arith -| Intros y' H m; Rewrite convert_add_un; Apply plus_assoc_r ]. -Qed. - -Theorem cvt_carry : - (x,y:positive)(convert (add_carry x y)) = (S (convert (add x y))). -Proof. -Intros;Unfold convert; Rewrite convert_add_carry; Simpl; Trivial with arith. -Qed. - -Theorem add_verif : - (x,y:positive)(m:nat) - (positive_to_nat (add x y) m) = - (plus (positive_to_nat x m) (positive_to_nat y m)). -Proof. -Induction x;Induction y;Simpl;Auto with arith; [ - Intros y' H1 m;Rewrite convert_add_carry; Rewrite H; - Rewrite plus_assoc_r; Rewrite plus_assoc_r; - Rewrite (plus_permute m (positive_to_nat p (plus m m))); Trivial with arith -| Intros y' H1 m; Rewrite H; Apply plus_assoc_l -| Intros m; Rewrite convert_add_un; - Rewrite (plus_sym (plus m (positive_to_nat p (plus m m)))); - Apply plus_assoc_r -| Intros y' H1 m; Rewrite H; Apply plus_permute -| Intros y' H1 m; Rewrite convert_add_un; Apply plus_assoc_r ]. -Qed. - -Theorem convert_add: - (x,y:positive) (convert (add x y)) = (plus (convert x) (convert y)). -Proof. -Intros x y; Exact (add_verif x y (S O)). -Qed. - -(** [IPN_shift] is a morphism for addition wrt the factor *) - -Lemma ZL2: - (y:positive)(m:nat) - (positive_to_nat y (plus m m)) = - (plus (positive_to_nat y m) (positive_to_nat y m)). -Proof. -Induction y; [ - Intros p H m; Simpl; Rewrite H; Rewrite plus_assoc_r; - Rewrite (plus_permute m (positive_to_nat p (plus m m))); - Rewrite plus_assoc_r; Auto with arith -| Intros p H m; Simpl; Rewrite H; Auto with arith -| Intro;Simpl; Trivial with arith ]. -Qed. - -Lemma ZL6: - (p:positive) (positive_to_nat p (S (S O))) = (plus (convert p) (convert p)). -Proof. -Intro p;Change (2) with (plus (S O) (S O)); Rewrite ZL2; Trivial. -Qed. - -(** [IPN] is a morphism for multiplication *) - -Lemma positive_to_nat_mult : (p:positive) (n,m:nat) - (positive_to_nat p (mult m n))=(mult m (positive_to_nat p n)). -Proof. - Induction p. Intros. Simpl. Rewrite mult_plus_distr_r. Rewrite <- (mult_plus_distr_r m n n). - Rewrite (H (plus n n) m). Reflexivity. - Intros. Simpl. Rewrite <- (mult_plus_distr_r m n n). Apply H. - Trivial. -Qed. -Theorem times_convert : - (x,y:positive) (convert (times x y)) = (mult (convert x) (convert y)). -Proof. -Intros x y; NewInduction x as [ x' H | x' H | ]; [ - Change (times (xI x') y) with (add y (xO (times x' y))); Rewrite convert_add; - Unfold 2 3 convert; Simpl; Do 2 Rewrite ZL6; Rewrite H; - Rewrite -> mult_plus_distr; Reflexivity -| Unfold 1 2 convert; Simpl; Do 2 Rewrite ZL6; - Rewrite H; Rewrite mult_plus_distr; Reflexivity -| Simpl; Rewrite <- plus_n_O; Reflexivity ]. -Qed. -V7only [ - Comments "Compatibility with the old version of times and times_convert". - Syntactic Definition times1 := - [x:positive;_:positive->positive;y:positive](times x y). - Syntactic Definition times1_convert := - [x,y:positive;_:positive->positive](times_convert x y). -]. - -(** IPN is strictly positive *) - -Theorem compare_positive_to_nat_O : - (p:positive)(m:nat)(le m (positive_to_nat p m)). -Induction p; Simpl; Auto with arith. -Intros; Apply le_trans with (plus m m); Auto with arith. -Qed. - -Theorem compare_convert_O : (p:positive)(lt O (convert p)). -Intro; Unfold convert; Apply lt_le_trans with (S O); Auto with arith. -Apply compare_positive_to_nat_O. -Qed. - -(** Mapping of 2 and 4 through IPN_shift *) - -Lemma positive_to_nat_2 : (p:positive) - (positive_to_nat p (2))=(mult (2) (positive_to_nat p (1))). -Proof. - Intros. Rewrite <- positive_to_nat_mult. Reflexivity. -Qed. - -Lemma positive_to_nat_4 : (p:positive) - (positive_to_nat p (4))=(mult (2) (positive_to_nat p (2))). -Proof. - Intros. Rewrite <- positive_to_nat_mult. Reflexivity. -Qed. - -(** Mapping of xH, xO and xI through IPN *) - -Lemma convert_xH : (convert xH)=(1). -Proof. - Reflexivity. -Qed. - -Lemma convert_xO : (p:positive) (convert (xO p))=(mult (2) (convert p)). -Proof. - Induction p. Unfold convert. Simpl. Intros. Rewrite positive_to_nat_2. - Rewrite positive_to_nat_4. Rewrite H. Simpl. Rewrite <- plus_Snm_nSm. Reflexivity. - Unfold convert. Simpl. Intros. Rewrite positive_to_nat_2. Rewrite positive_to_nat_4. - Rewrite H. Reflexivity. - Reflexivity. -Qed. - -Lemma convert_xI : (p:positive) (convert (xI p))=(S (mult (2) (convert p))). -Proof. - Induction p. Unfold convert. Simpl. Intro p0. Intro. Rewrite positive_to_nat_2. - Rewrite positive_to_nat_4; Injection H; Intro H1; Rewrite H1; Rewrite <- plus_Snm_nSm; Reflexivity. - Unfold convert. Simpl. Intros. Rewrite positive_to_nat_2. Rewrite positive_to_nat_4. - Injection H; Intro H1; Rewrite H1; Reflexivity. - Reflexivity. -Qed. - -(**********************************************************************) -(** Properties of the shifted injection from Peano natural numbers to - binary positive numbers *) - -(** Composition of [INP] and [IPN] is shifted identity on [nat] *) - -Theorem bij1 : (m:nat) (convert (anti_convert m)) = (S m). -Proof. -Induction m; [ - Unfold convert; Simpl; Trivial -| Unfold convert; Intros n H; Simpl; Rewrite convert_add_un; Rewrite H; Auto ]. -Qed. - -(** Miscellaneous lemmas on [INP] *) - -Lemma ZL3: (x:nat) (add_un (anti_convert (plus x x))) = (xO (anti_convert x)). -Proof. -Induction x; [ - Simpl; Auto with arith -| Intros y H; Simpl; Rewrite plus_sym; Simpl; Rewrite H; Rewrite ZL1;Auto with arith]. -Qed. - -Lemma ZL4: (y:positive) (EX h:nat |(convert y)=(S h)). -Proof. -Induction y; [ - Intros p H;Elim H; Intros x H1; Exists (plus (S x) (S x)); - Unfold convert ;Simpl; Change (2) with (plus (1) (1)); Rewrite ZL2; Unfold convert in H1; - Rewrite H1; Auto with arith -| Intros p H1;Elim H1;Intros x H2; Exists (plus x (S x)); Unfold convert; - Simpl; Change (2) with (plus (1) (1)); Rewrite ZL2;Unfold convert in H2; Rewrite H2; Auto with arith -| Exists O ;Auto with arith ]. -Qed. - -Lemma ZL5: (x:nat) (anti_convert (plus (S x) (S x))) = (xI (anti_convert x)). -Proof. -Induction x;Simpl; [ - Auto with arith -| Intros y H; Rewrite <- plus_n_Sm; Simpl; Rewrite H; Auto with arith]. -Qed. - -(** Composition of [IPN] and [INP] is shifted identity on [positive] *) - -Theorem bij2 : (x:positive) (anti_convert (convert x)) = (add_un x). -Proof. -Induction x; [ - Intros p H; Simpl; Rewrite <- H; Change (2) with (plus (1) (1)); - Rewrite ZL2; Elim (ZL4 p); - Unfold convert; Intros n H1;Rewrite H1; Rewrite ZL3; Auto with arith -| Intros p H; Unfold convert ;Simpl; Change (2) with (plus (1) (1)); - Rewrite ZL2; - Rewrite <- (sub_add_one - (anti_convert - (plus (positive_to_nat p (S O)) (positive_to_nat p (S O))))); - Rewrite <- (sub_add_one (xI p)); - Simpl;Rewrite <- H;Elim (ZL4 p); Unfold convert ;Intros n H1;Rewrite H1; - Rewrite ZL5; Simpl; Trivial with arith -| Unfold convert; Simpl; Auto with arith ]. -Qed. - -(** Composition of [IPN], [INP] and [Ppred] is identity on [positive] *) - -Theorem bij3: (x:positive)(sub_un (anti_convert (convert x))) = x. -Proof. -Intros x; Rewrite bij2; Rewrite sub_add_one; Trivial with arith. -Qed. - -(** Extra lemmas on [lt] on Peano natural numbers *) - -Lemma ZL7: - (m,n:nat) (lt m n) -> (lt (plus m m) (plus n n)). -Proof. -Intros m n H; Apply lt_trans with m:=(plus m n); [ - Apply lt_reg_l with 1:=H -| Rewrite (plus_sym m n); Apply lt_reg_l with 1:=H ]. -Qed. - -Lemma ZL8: - (m,n:nat) (lt m n) -> (lt (S (plus m m)) (plus n n)). -Proof. -Intros m n H; Apply le_lt_trans with m:=(plus m n); [ - Change (lt (plus m m) (plus m n)) ; Apply lt_reg_l with 1:=H -| Rewrite (plus_sym m n); Apply lt_reg_l with 1:=H ]. -Qed. - -(** [IPN] is a morphism from [positive] to [nat] for [lt] (expressed - from [compare] on [positive]) - - Part 1: [lt] on [positive] is finer than [lt] on [nat] -*) - -Theorem compare_convert_INFERIEUR : - (x,y:positive) (compare x y EGAL) = INFERIEUR -> - (lt (convert x) (convert y)). -Proof. -Induction x;Induction y; [ - Intros z H1 H2; Unfold convert ;Simpl; Apply lt_n_S; - Do 2 Rewrite ZL6; Apply ZL7; Apply H; Simpl in H2; Assumption -| Intros q H1 H2; Unfold convert ;Simpl; Do 2 Rewrite ZL6; - Apply ZL8; Apply H;Simpl in H2; Apply ZLSI;Assumption -| Simpl; Intros H1;Discriminate H1 -| Simpl; Intros q H1 H2; Unfold convert ;Simpl;Do 2 Rewrite ZL6; - Elim (ZLII p q H2); [ - Intros H3;Apply lt_S;Apply ZL7; Apply H;Apply H3 - | Intros E;Rewrite E;Apply lt_n_Sn] -| Simpl;Intros q H1 H2; Unfold convert ;Simpl;Do 2 Rewrite ZL6; - Apply ZL7;Apply H;Assumption -| Simpl; Intros H1;Discriminate H1 -| Intros q H1 H2; Unfold convert ;Simpl; Apply lt_n_S; Rewrite ZL6; - Elim (ZL4 q);Intros h H3; Rewrite H3;Simpl; Apply lt_O_Sn -| Intros q H1 H2; Unfold convert ;Simpl; Rewrite ZL6; Elim (ZL4 q);Intros h H3; - Rewrite H3; Simpl; Rewrite <- plus_n_Sm; Apply lt_n_S; Apply lt_O_Sn -| Simpl; Intros H;Discriminate H ]. -Qed. - -(** [IPN] is a morphism from [positive] to [nat] for [gt] (expressed - from [compare] on [positive]) - - Part 1: [gt] on [positive] is finer than [gt] on [nat] -*) - -Theorem compare_convert_SUPERIEUR : - (x,y:positive) (compare x y EGAL)=SUPERIEUR -> (gt (convert x) (convert y)). -Proof. -Unfold gt; Induction x;Induction y; [ - Simpl;Intros q H1 H2; Unfold convert ;Simpl;Do 2 Rewrite ZL6; - Apply lt_n_S; Apply ZL7; Apply H;Assumption -| Simpl;Intros q H1 H2; Unfold convert ;Simpl; Do 2 Rewrite ZL6; - Elim (ZLSS p q H2); [ - Intros H3;Apply lt_S;Apply ZL7;Apply H;Assumption - | Intros E;Rewrite E;Apply lt_n_Sn] -| Intros H1;Unfold convert ;Simpl; Rewrite ZL6;Elim (ZL4 p); - Intros h H3;Rewrite H3;Simpl; Apply lt_n_S; Apply lt_O_Sn -| Simpl;Intros q H1 H2;Unfold convert ;Simpl;Do 2 Rewrite ZL6; - Apply ZL8; Apply H; Apply ZLIS; Assumption -| Simpl;Intros q H1 H2; Unfold convert ;Simpl;Do 2 Rewrite ZL6; - Apply ZL7;Apply H;Assumption -| Intros H1;Unfold convert ;Simpl; Rewrite ZL6; Elim (ZL4 p); - Intros h H3;Rewrite H3;Simpl; Rewrite <- plus_n_Sm;Apply lt_n_S; - Apply lt_O_Sn -| Simpl; Intros q H1 H2;Discriminate H2 -| Simpl; Intros q H1 H2;Discriminate H2 -| Simpl;Intros H;Discriminate H ]. -Qed. - -(** [IPN] is a morphism from [positive] to [nat] for [lt] (expressed - from [compare] on [positive]) - - Part 2: [lt] on [nat] is finer than [lt] on [positive] -*) - -Theorem convert_compare_INFERIEUR : - (x,y:positive)(lt (convert x) (convert y)) -> (compare x y EGAL) = INFERIEUR. -Proof. -Intros x y; Unfold gt; Elim (Dcompare (compare x y EGAL)); [ - Intros E; Rewrite (compare_convert_EGAL x y E); - Intros H;Absurd (lt (convert y) (convert y)); [ Apply lt_n_n | Assumption ] -| Intros H;Elim H; [ - Auto - | Intros H1 H2; Absurd (lt (convert x) (convert y)); [ - Apply lt_not_sym; Change (gt (convert x) (convert y)); - Apply compare_convert_SUPERIEUR; Assumption - | Assumption ]]]. -Qed. - -(** [IPN] is a morphism from [positive] to [nat] for [gt] (expressed - from [compare] on [positive]) - - Part 2: [gt] on [nat] is finer than [gt] on [positive] -*) - -Theorem convert_compare_SUPERIEUR : - (x,y:positive)(gt (convert x) (convert y)) -> (compare x y EGAL) = SUPERIEUR. -Proof. -Intros x y; Unfold gt; Elim (Dcompare (compare x y EGAL)); [ - Intros E; Rewrite (compare_convert_EGAL x y E); - Intros H;Absurd (lt (convert y) (convert y)); [ Apply lt_n_n | Assumption ] -| Intros H;Elim H; [ - Intros H1 H2; Absurd (lt (convert y) (convert x)); [ - Apply lt_not_sym; Apply compare_convert_INFERIEUR; Assumption - | Assumption ] - | Auto]]. -Qed. - -(**********************************************************************) -(** Extra properties of the comparison on binary positive numbers *) - -Lemma ZC1: - (x,y:positive)(compare x y EGAL)=SUPERIEUR -> (compare y x EGAL)=INFERIEUR. -Proof. -Intros x y H;Apply convert_compare_INFERIEUR; -Change (gt (convert x) (convert y));Apply compare_convert_SUPERIEUR; -Assumption. -Qed. - -Lemma ZC2: - (x,y:positive)(compare x y EGAL)=INFERIEUR -> (compare y x EGAL)=SUPERIEUR. -Proof. -Intros x y H;Apply convert_compare_SUPERIEUR;Unfold gt; -Apply compare_convert_INFERIEUR;Assumption. -Qed. - -Lemma ZC3: (x,y:positive)(compare x y EGAL)=EGAL -> (compare y x EGAL)=EGAL. -Proof. -Intros x y H; Rewrite (compare_convert_EGAL x y H); -Apply convert_compare_EGAL. -Qed. - -Lemma ZC4: (x,y:positive) (compare x y EGAL) = (Op (compare y x EGAL)). -Proof. -Intros x y;ElimPcompare y x; -Intros E;Rewrite E;Simpl; [Apply ZC3 | Apply ZC2 | Apply ZC1 ]; Assumption. -Qed. - -(**********************************************************************) -(** Extra properties of the injection from binary positive numbers to Peano - natural numbers *) - -(** [IPN] is a morphism for subtraction on positive numbers *) - -Theorem true_sub_convert: - (x,y:positive) (compare x y EGAL) = SUPERIEUR -> - (convert (true_sub x y)) = (minus (convert x) (convert y)). -Proof. -Intros x y H; Apply (simpl_plus_l (convert y)); -Rewrite le_plus_minus_r; [ - Rewrite <- convert_add; Rewrite sub_add; Auto with arith -| Apply lt_le_weak; Exact (compare_convert_SUPERIEUR x y H)]. -Qed. - -(** [IPN] is injective *) - -Lemma convert_intro : (x,y:positive)(convert x)=(convert y) -> x=y. -Proof. -Intros x y H;Rewrite <- (bij3 x);Rewrite <- (bij3 y); Rewrite H; Trivial with arith. -Qed. - -Lemma ZL16: (p,q:positive)(lt (minus (convert p) (convert q)) (convert p)). -Proof. -Intros p q; Elim (ZL4 p);Elim (ZL4 q); Intros h H1 i H2; -Rewrite H1;Rewrite H2; Simpl;Unfold lt; Apply le_n_S; Apply le_minus. -Qed. - -Lemma ZL17: (p,q:positive)(lt (convert p) (convert (add p q))). -Proof. -Intros p q; Rewrite convert_add;Unfold lt;Elim (ZL4 q); Intros k H;Rewrite H; -Rewrite plus_sym;Simpl; Apply le_n_S; Apply le_plus_r. -Qed. - -(* Comparison and subtraction *) - -Lemma compare_true_sub_right : - (p,q,z:positive) - (compare q p EGAL)=INFERIEUR-> - (compare z p EGAL)=SUPERIEUR-> - (compare z q EGAL)=SUPERIEUR-> - (compare (true_sub z p) (true_sub z q) EGAL)=INFERIEUR. -Proof. -Intros; Apply convert_compare_INFERIEUR; Rewrite true_sub_convert; [ - Rewrite true_sub_convert; [ - Apply simpl_lt_plus_l with p:=(convert q); Rewrite le_plus_minus_r; [ - Rewrite plus_sym; Apply simpl_lt_plus_l with p:=(convert p); - Rewrite plus_assoc_l; Rewrite le_plus_minus_r; [ - Rewrite (plus_sym (convert p)); Apply lt_reg_l; - Apply compare_convert_INFERIEUR; Assumption - | Apply lt_le_weak; Apply compare_convert_INFERIEUR; - Apply ZC1; Assumption ] - | Apply lt_le_weak;Apply compare_convert_INFERIEUR; - Apply ZC1; Assumption ] - | Assumption ] - | Assumption ]. -Qed. - -Lemma compare_true_sub_left : - (p,q,z:positive) - (compare q p EGAL)=INFERIEUR-> - (compare p z EGAL)=SUPERIEUR-> - (compare q z EGAL)=SUPERIEUR-> - (compare (true_sub q z) (true_sub p z) EGAL)=INFERIEUR. -Proof. -Intros; Apply convert_compare_INFERIEUR; Rewrite true_sub_convert; [ - Rewrite true_sub_convert; [ - Unfold gt; Apply simpl_lt_plus_l with p:=(convert z); - Rewrite le_plus_minus_r; [ - Rewrite le_plus_minus_r; [ - Apply compare_convert_INFERIEUR;Assumption - | Apply lt_le_weak; Apply compare_convert_INFERIEUR;Apply ZC1;Assumption] - | Apply lt_le_weak; Apply compare_convert_INFERIEUR;Apply ZC1; Assumption] - | Assumption] -| Assumption]. -Qed. - -(**********************************************************************) -(** Properties of multiplication on binary positive numbers *) - -(** One is right neutral for multiplication *) - -Lemma times_x_1 : (x:positive) (times x xH) = x. -Proof. -NewInduction x; Simpl. - Rewrite IHx; Reflexivity. - Rewrite IHx; Reflexivity. - Reflexivity. -Qed. - -(** Right reduction properties for multiplication *) - -Lemma times_x_double : (x,y:positive) (times x (xO y)) = (xO (times x y)). -Proof. -Intros; NewInduction x; Simpl. - Rewrite IHx; Reflexivity. - Rewrite IHx; Reflexivity. - Reflexivity. -Qed. - -Lemma times_x_double_plus_one : - (x,y:positive) (times x (xI y)) = (add x (xO (times x y))). -Proof. -Intros; NewInduction x; Simpl. - Rewrite IHx; Do 2 Rewrite add_assoc; Rewrite add_sym with x:=y; Reflexivity. - Rewrite IHx; Reflexivity. - Reflexivity. -Qed. - -(** Commutativity of multiplication *) - -Theorem times_sym : (x,y:positive) (times x y) = (times y x). -Proof. -NewInduction y; Simpl. - Rewrite <- IHy; Apply times_x_double_plus_one. - Rewrite <- IHy; Apply times_x_double. - Apply times_x_1. -Qed. - -(** Distributivity of multiplication over addition *) - -Theorem times_add_distr: - (x,y,z:positive) (times x (add y z)) = (add (times x y) (times x z)). -Proof. -Intros; NewInduction x; Simpl. - Rewrite IHx; Rewrite <- add_assoc with y := (xO (times x y)); - Rewrite -> add_assoc with x := (xO (times x y)); - Rewrite -> add_sym with x := (xO (times x y)); - Rewrite <- add_assoc with y := (xO (times x y)); - Rewrite -> add_assoc with y := z; Reflexivity. - Rewrite IHx; Reflexivity. - Reflexivity. -Qed. - -Theorem times_add_distr_l: - (x,y,z:positive) (times (add x y) z) = (add (times x z) (times y z)). -Proof. -Intros x y z; Do 3 Rewrite times_sym with y:=z; Apply times_add_distr. -Qed. - -(** Associativity of multiplication *) - -Theorem times_assoc : - ((x,y,z:positive) (times x (times y z))= (times (times x y) z)). -Proof. -NewInduction x as [x|x|]; Simpl; Intros y z. - Rewrite IHx; Rewrite times_add_distr_l; Reflexivity. - Rewrite IHx; Reflexivity. - Reflexivity. -Qed. - -(** Distributivity of multiplication over subtraction *) - -Theorem times_true_sub_distr: - (x,y,z:positive) (compare y z EGAL) = SUPERIEUR -> - (times x (true_sub y z)) = (true_sub (times x y) (times x z)). -Proof. -Intros x y z H; Apply convert_intro; -Rewrite times_convert; Rewrite true_sub_convert; [ - Rewrite true_sub_convert; [ - Do 2 Rewrite times_convert; - Do 3 Rewrite (mult_sym (convert x));Apply mult_minus_distr - | Apply convert_compare_SUPERIEUR; Do 2 Rewrite times_convert; - Unfold gt; Elim (ZL4 x);Intros h H1;Rewrite H1; Apply lt_mult_left; - Exact (compare_convert_SUPERIEUR y z H) ] -| Assumption ]. -Qed. - -(** Parity properties of multiplication *) - -Theorem times_discr_xO_xI : - (x,y,z:positive)(times (xI x) z)<>(times (xO y) z). -Proof. -NewInduction z as [|z IHz|]; Try Discriminate. -Intro H; Apply IHz; Clear IHz. -Do 2 Rewrite times_x_double in H. -Injection H; Clear H; Intro H; Exact H. -Qed. - -Theorem times_discr_xO : (x,y:positive)(times (xO x) y)<>y. -Proof. -NewInduction y; Try Discriminate. -Rewrite times_x_double; Injection; Assumption. -Qed. - -(** Simplification properties of multiplication *) - -Theorem simpl_times_r : (x,y,z:positive) (times x z)=(times y z) -> x=y. -Proof. -NewInduction x as [p IHp|p IHp|]; NewDestruct y as [q|q|]; Intros z H; - Reflexivity Orelse Apply (f_equal positive) Orelse Apply False_ind. - Simpl in H; Apply IHp with z := (xO z); Simpl; Do 2 Rewrite times_x_double; - Apply simpl_add_l with 1 := H. - Apply times_discr_xO_xI with 1 := H. - Simpl in H; Rewrite add_sym in H; Apply add_no_neutral with 1 := H. - Symmetry in H; Apply times_discr_xO_xI with 1 := H. - Apply IHp with z := (xO z); Simpl; Do 2 Rewrite times_x_double; Assumption. - Apply times_discr_xO with 1:=H. - Simpl in H; Symmetry in H; Rewrite add_sym in H; - Apply add_no_neutral with 1 := H. - Symmetry in H; Apply times_discr_xO with 1:=H. -Qed. - -Theorem simpl_times_l : (x,y,z:positive) (times z x)=(times z y) -> x=y. -Proof. -Intros x y z H; Apply simpl_times_r with z:=z. -Rewrite times_sym with x:=x; Rewrite times_sym with x:=y; Assumption. -Qed. - -(**********************************************************************) -(** Binary natural numbers *) - -Inductive entier: Set := Nul : entier | Pos : positive -> entier. - -(** Operation x -> 2*x+1 *) - -Definition Un_suivi_de := [x] - Cases x of Nul => (Pos xH) | (Pos p) => (Pos (xI p)) end. - -(** Operation x -> 2*x *) - -Definition Zero_suivi_de := - [n] Cases n of Nul => Nul | (Pos p) => (Pos (xO p)) end. - -(** Successor *) - -Definition Nsucc := - [n] Cases n of Nul => (Pos xH) | (Pos p) => (Pos (add_un p)) end. - -(** Addition *) - -Definition Nplus := [n,m] - Cases n m of - | Nul _ => m - | _ Nul => n - | (Pos p) (Pos q) => (Pos (add p q)) - end. - -(** Multiplication *) - -Definition Nmult := [n,m] - Cases n m of - | Nul _ => Nul - | _ Nul => Nul - | (Pos p) (Pos q) => (Pos (times p q)) - end. - -(** Order *) - -Definition Ncompare := [n,m] - Cases n m of - | Nul Nul => EGAL - | Nul (Pos m') => INFERIEUR - | (Pos n') Nul => SUPERIEUR - | (Pos n') (Pos m') => (compare n' m' EGAL) - end. - -(** Peano induction on binary natural numbers *) - -Theorem Nind : (P:(entier ->Prop)) - (P Nul) ->((n:entier)(P n) ->(P (Nsucc n))) ->(n:entier)(P n). -Proof. -NewDestruct n. - Assumption. - Apply Pind with P := [p](P (Pos p)). -Exact (H0 Nul H). -Intro p'; Exact (H0 (Pos p')). -Qed. - -(** Properties of addition *) - -Theorem Nplus_0_l : (n:entier)(Nplus Nul n)=n. -Proof. -Reflexivity. -Qed. - -Theorem Nplus_0_r : (n:entier)(Nplus n Nul)=n. -Proof. -NewDestruct n; Reflexivity. -Qed. - -Theorem Nplus_comm : (n,m:entier)(Nplus n m)=(Nplus m n). -Proof. -Intros. -NewDestruct n; NewDestruct m; Simpl; Try Reflexivity. -Rewrite add_sym; Reflexivity. -Qed. - -Theorem Nplus_assoc_l : - (n,m,p:entier)(Nplus (Nplus n m) p)=(Nplus n (Nplus m p)). -Proof. -Intros. -NewDestruct n; Try Reflexivity. -NewDestruct m; Try Reflexivity. -NewDestruct p; Try Reflexivity. -Simpl; Rewrite add_assoc; Reflexivity. -Qed. - -Theorem Nplus_succ : (n,m:entier)(Nplus (Nsucc n) m)=(Nsucc (Nplus n m)). -Proof. -NewDestruct n; NewDestruct m. - Simpl; Reflexivity. - Unfold Nsucc Nplus; Rewrite <- ZL12bis; Reflexivity. - Simpl; Reflexivity. - Simpl; Rewrite ZL14bis; Reflexivity. -Qed. - -Theorem Nsucc_inj : (n,m:entier)(Nsucc n)=(Nsucc m)->n=m. -Proof. -NewDestruct n; NewDestruct m; Simpl; Intro H; - Reflexivity Orelse Injection H; Clear H; Intro H. - Symmetry in H; Contradiction add_un_not_un with p. - Contradiction add_un_not_un with p. - Rewrite add_un_inj with 1:=H; Reflexivity. -Qed. - -Theorem Nplus_reg_l : (n,m,p:entier)(Nplus n m)=(Nplus n p)->m=p. -Proof. -Intro n; Pattern n; Apply Nind; Clear n; Simpl. - Trivial. - Intros n IHn m p H0; Do 2 Rewrite Nplus_succ in H0. - Apply IHn; Apply Nsucc_inj; Assumption. -Qed. - -(** Properties of multiplication *) - -Theorem Nmult_1_l : (n:entier)(Nmult (Pos xH) n)=n. -Proof. -NewDestruct n; Reflexivity. -Qed. - -Theorem Nmult_1_r : (n:entier)(Nmult n (Pos xH))=n. -Proof. -NewDestruct n; Simpl; Try Reflexivity. -Rewrite times_x_1; Reflexivity. -Qed. - -Theorem Nmult_comm : (n,m:entier)(Nmult n m)=(Nmult m n). -Proof. -Intros. -NewDestruct n; NewDestruct m; Simpl; Try Reflexivity. -Rewrite times_sym; Reflexivity. -Qed. - -Theorem Nmult_assoc_l : - (n,m,p:entier)(Nmult (Nmult n m) p)=(Nmult n (Nmult m p)). -Proof. -Intros. -NewDestruct n; Try Reflexivity. -NewDestruct m; Try Reflexivity. -NewDestruct p; Try Reflexivity. -Simpl; Rewrite times_assoc; Reflexivity. -Qed. - -Theorem Nmult_Nplus_distr_l : - (n,m,p:entier)(Nmult (Nplus n m) p)=(Nplus (Nmult n p) (Nmult m p)). -Proof. -Intros. -NewDestruct n; Try Reflexivity. -NewDestruct m; NewDestruct p; Try Reflexivity. -Simpl; Rewrite times_add_distr_l; Reflexivity. -Qed. - -Theorem Nmult_int_r : (n,m,p:entier) (Nmult n p)=(Nmult m p) -> n=m\/p=Nul. -Proof. -NewDestruct p; Intro H. -Right; Reflexivity. -Left; NewDestruct n; NewDestruct m; Reflexivity Orelse Try Discriminate H. -Injection H; Clear H; Intro H; Rewrite simpl_times_r with 1:=H; Reflexivity. -Qed. - -Theorem Nmult_0_l : (n:entier) (Nmult Nul n) = Nul. -Proof. -Reflexivity. -Qed. - -(** Properties of comparison *) - -Theorem Ncompare_Eq_eq : (n,m:entier) (Ncompare n m) = EGAL -> n = m. -Proof. -NewDestruct n as [|n]; NewDestruct m as [|m]; Simpl; Intro H; - Reflexivity Orelse Try Discriminate H. - Rewrite (compare_convert_EGAL n m H); Reflexivity. -Qed. +V7only [Notation relation := Datatypes.relation.]. (**********************************************************************) (** Binary integer numbers *) @@ -1485,10 +27,10 @@ Qed. Inductive Z : Set := ZERO : Z | POS : positive -> Z | NEG : positive -> Z. -(* Declare Scope Z_scope with Key Z *) +(** Declare Scope Z_scope with Key Z *) Delimits Scope Z_scope with Z. -(* Automatically open scope Z_scope for arguments of type Z, POS and NEG *) +(** Automatically open scope positive_scope for the constructors of Z *) Bind Scope Z_scope with Z. Arguments Scope POS [ positive_scope ]. Arguments Scope NEG [ positive_scope ]. @@ -1622,7 +164,7 @@ Definition Zsgn [z:Z] : Z := | (NEG p) => (NEG xH) end. -(* Easier to handle variants of successor and addition *) +(** Easier to handle variants of successor and addition *) Definition Zs' [x:Z] := Cases x of @@ -1662,7 +204,7 @@ Intros P H0 Hs Hp; NewDestruct z. Apply Pind with P:=[p](P (POS p)). Change (P (Zs' ZERO)); Apply Hs; Apply H0. Intro n; Exact (Hs (POS n)). - Apply Pind with P:=[p](P (NEG p)). + Apply Pind with P:=[p](P (NEG p)). Change (P (Zpred' ZERO)); Apply Hp; Apply H0. Intro n; Exact (Hp (NEG n)). Qed. @@ -2098,7 +640,7 @@ Qed. Hints Local Resolve weak_assoc. -Theorem Zplus_assoc_l : +Theorem Zplus_assoc : (n,m,p:Z) (Zplus n (Zplus m p))= (Zplus (Zplus n m) p). Proof. Intros x y z;Case x;Case y;Case z;Auto with arith; Intros; [ @@ -2125,7 +667,7 @@ Intros x y z;Case x;Case y;Case z;Auto with arith; Intros; [ . Qed. -V7only [Notation Zplus_assoc := Zplus_assoc_l.]. +V7only [Notation Zplus_assoc_l := Zplus_assoc.]. Lemma Zplus_assoc_r : (n,m,p:Z)(Zplus (Zplus n m) p) =(Zplus n (Zplus m p)). Proof. @@ -2368,13 +910,13 @@ Qed. (** Associativity of multiplication *) -Theorem Zmult_assoc_l : - (n,m,p:Z) (Zmult n (Zmult m p))= (Zmult (Zmult n m) p). +Theorem Zmult_assoc : + (x,y,z:Z) (Zmult x (Zmult y z))= (Zmult (Zmult x y) z). Proof. Intros x y z; NewDestruct x; NewDestruct y; NewDestruct z; Simpl; Try Rewrite times_assoc; Reflexivity. Qed. -V7only [Notation Zmult_assoc := Zmult_assoc_l.]. +V7only [Notation Zmult_assoc_l := Zmult_assoc.]. Lemma Zmult_assoc_r : (n,m,p:Z)((Zmult (Zmult n m) p) = (Zmult n (Zmult m p))). Proof. @@ -2559,7 +1101,7 @@ Intros x y H; Rewrite H; Auto with arith. Qed. (**********************************************************************) -(* Comparison on integers *) +(** Comparison on integers *) Lemma Zcompare_x_x : (x:Z) (Zcompare x x) = EGAL. Proof. @@ -2925,12 +1467,15 @@ Qed. Lemma POS_xI : (p:positive) (POS (xI p))=(Zplus (Zmult (POS (xO xH)) (POS p)) (POS xH)). Intro; Apply refl_equal. Qed. + Lemma POS_xO : (p:positive) (POS (xO p))=(Zmult (POS (xO xH)) (POS p)). Intro; Apply refl_equal. Qed. + Lemma NEG_xI : (p:positive) (NEG (xI p))=(Zminus (Zmult (POS (xO xH)) (NEG p)) (POS xH)). Intro; Apply refl_equal. Qed. + Lemma NEG_xO : (p:positive) (NEG (xO p))=(Zmult (POS (xO xH)) (NEG p)). Reflexivity. Qed. @@ -2950,6 +1495,7 @@ Definition Zlt := [x,y:Z](Zcompare x y) = INFERIEUR. Definition Zgt := [x,y:Z](Zcompare x y) = SUPERIEUR. Definition Zle := [x,y:Z]~(Zcompare x y) = SUPERIEUR. Definition Zge := [x,y:Z]~(Zcompare x y) = INFERIEUR. +Definition Zne := [x,y:Z] ~(x=y). V8Infix "<=" Zle : Z_scope. V8Infix "<" Zlt : Z_scope. @@ -2962,6 +1508,23 @@ V8Notation "x < y < z" := (Zlt x y)/\(Zlt y z) :Z_scope. V8Notation "x < y <= z" := (Zlt x y)/\(Zle y z) :Z_scope. (**********************************************************************) +(** Absolute value on integers *) + +Definition absolu [x:Z] : nat := + Cases x of + ZERO => O + | (POS p) => (convert p) + | (NEG p) => (convert p) + end. + +Definition Zabs [z:Z] : Z := + Cases z of + ZERO => ZERO + | (POS p) => (POS p) + | (NEG p) => (POS p) + end. + +(**********************************************************************) (** From [nat] to [Z] *) Definition inject_nat := @@ -2970,9 +1533,10 @@ Definition inject_nat := | (S y) => (POS (anti_convert y)) end. +Require BinNat. + Definition entier_of_Z := [z:Z]Cases z of ZERO => Nul | (POS p) => (Pos p) | (NEG p) => (Pos p) end. Definition Z_of_entier := [x:entier]Cases x of Nul => ZERO | (Pos p) => (POS p) end. - diff --git a/theories/ZArith/zarith_aux.v b/theories/ZArith/zarith_aux.v index 01c346781..5338643ac 100644 --- a/theories/ZArith/zarith_aux.v +++ b/theories/ZArith/zarith_aux.v @@ -7,762 +7,139 @@ (***********************************************************************) (*i $Id$ i*) -(** Binary Integers (Pierre Crégut (CNET, Lannion, France) *) - Require fast_integer. -Require Arith. - -V7only [Import nat_scope.]. -Open Local Scope Z_scope. - -(**********************************************************************) -(** Properties of the order relations on binary integers *) - -(** Trichotomy *) - -Theorem Ztrichotomy_inf : (m,n:Z) {Zlt m n} + {m=n} + {Zgt m n}. -Proof. -Unfold Zgt Zlt; Intros m n; Assert H:=(refl_equal ? (Zcompare m n)). - LetTac x := (Zcompare m n) in 2 H Goal. - NewDestruct x; - [Left; Right;Rewrite Zcompare_EGAL_eq with 1:=H - | Left; Left - | Right ]; Reflexivity. -Qed. - -Theorem Ztrichotomy : (m,n:Z) (Zlt m n) \/ m=n \/ (Zgt m n). -Proof. - Intros m n; NewDestruct (Ztrichotomy_inf m n) as [[Hlt|Heq]|Hgt]; - [Left | Right; Left |Right; Right]; Assumption. -Qed. - -(** Relating strict and large orders *) - -Lemma Zgt_lt : (m,n:Z) (Zgt m n) -> (Zlt n m). -Proof. -Unfold Zgt Zlt ;Intros m n H; Elim (Zcompare_ANTISYM m n); Auto with arith. -Qed. - -Lemma Zlt_gt : (m,n:Z) (Zlt m n) -> (Zgt n m). -Proof. -Unfold Zgt Zlt ;Intros m n H; Elim (Zcompare_ANTISYM n m); Auto with arith. -Qed. - -Lemma Zge_le : (m,n:Z) (Zge m n) -> (Zle n m). -Proof. -Intros m n; Change ~(Zlt m n)-> ~(Zgt n m); -Unfold not; Intros H1 H2; Apply H1; Apply Zgt_lt; Assumption. -Qed. - -Lemma Zle_ge : (m,n:Z) (Zle m n) -> (Zge n m). -Proof. -Intros m n; Change ~(Zgt m n)-> ~(Zlt n m); -Unfold not; Intros H1 H2; Apply H1; Apply Zlt_gt; Assumption. -Qed. - -Lemma Zle_not_gt : (n,m:Z)(Zle n m) -> ~(Zgt n m). -Proof. -Trivial. -Qed. - -Lemma Znot_gt_le : (n,m:Z)~(Zgt n m) -> (Zle n m). -Proof. -Trivial. -Qed. - -Lemma Zgt_not_le : (n,m:Z)(Zgt n m) -> ~(Zle n m). -Proof. -Intros n m H1 H2; Apply H2; Assumption. -Qed. - -Lemma Zle_not_lt : (n,m:Z)(Zle n m) -> ~(Zlt m n). -Proof. -Intros n m H1 H2. -Assert H3:=(Zlt_gt ? ? H2). -Apply Zle_not_gt with n m; Assumption. -Qed. - -Lemma Zlt_not_le : (n,m:Z)(Zlt n m) -> ~(Zle m n). -Proof. -Intros n m H1 H2. -Apply Zle_not_lt with m n; Assumption. -Qed. - -(** Reflexivity *) - -Lemma Zle_n : (n:Z) (Zle n n). -Proof. -Intros n; Unfold Zle; Rewrite (Zcompare_x_x n); Discriminate. -Qed. - -(** Antisymmetry *) - -Lemma Zle_antisym : (n,m:Z)(Zle n m)->(Zle m n)->n=m. -Proof. -Intros n m H1 H2; NewDestruct (Ztrichotomy n m) as [Hlt|[Heq|Hgt]]. - Absurd (Zgt m n); [ Apply Zle_not_gt | Apply Zlt_gt]; Assumption. - Assumption. - Absurd (Zgt n m); [ Apply Zle_not_gt | Idtac]; Assumption. -Qed. - -(** Asymmetry *) - -Lemma Zgt_not_sym : (n,m:Z)(Zgt n m) -> ~(Zgt m n). -Proof. -Unfold Zgt ;Intros n m H; Elim (Zcompare_ANTISYM n m); Intros H1 H2; -Rewrite -> H1; [ Discriminate | Assumption ]. -Qed. - -Lemma Zlt_not_sym : (n,m:Z)(Zlt n m) -> ~(Zlt m n). -Proof. -Intros n m H H1; -Assert H2:(Zgt m n). Apply Zlt_gt; Assumption. -Assert H3: (Zgt n m). Apply Zlt_gt; Assumption. -Apply Zgt_not_sym with m n; Assumption. -Qed. - -(** Irreflexivity *) - -Lemma Zgt_antirefl : (n:Z)~(Zgt n n). -Proof. -Intros n H; Apply (Zgt_not_sym n n H H). -Qed. - -Lemma Zlt_n_n : (n:Z)~(Zlt n n). -Proof. -Intros n H; Apply (Zlt_not_sym n n H H). -Qed. - -(** Large = strict or equal *) - -Lemma Zle_lt_or_eq : (n,m:Z)(Zle n m)->((Zlt n m) \/ n=m). -Proof. -Intros n m H; NewDestruct (Ztrichotomy n m) as [Hlt|[Heq|Hgt]]; [ - Left; Assumption -| Right; Assumption -| Absurd (Zgt n m); [Apply Zle_not_gt|Idtac]; Assumption ]. -Qed. - -Lemma Zlt_le_weak : (n,m:Z)(Zlt n m)->(Zle n m). -Proof. -Intros n m Hlt; Apply Znot_gt_le; Apply Zgt_not_sym; Apply Zlt_gt; Assumption. -Qed. - -(** Dichotomy *) - -Lemma Zle_or_lt : (n,m:Z)(Zle n m)\/(Zlt m n). -Proof. -Intros n m; NewDestruct (Ztrichotomy n m) as [Hlt|[Heq|Hgt]]; [ - Left; Apply Znot_gt_le; Intro Hgt; Assert Hgt':=(Zlt_gt ? ? Hlt); - Apply Zgt_not_sym with m n; Assumption -| Left; Rewrite Heq; Apply Zle_n -| Right; Apply Zgt_lt; Assumption ]. -Qed. - -(** Transitivity of strict orders *) - -Lemma Zgt_trans : (n,m,p:Z)(Zgt n m)->(Zgt m p)->(Zgt n p). -Proof. -Exact Zcompare_trans_SUPERIEUR. -Qed. - -Lemma Zlt_trans : (n,m,p:Z)(Zlt n m)->(Zlt m p)->(Zlt n p). -Proof. -Intros n m p H1 H2; Apply Zgt_lt; Apply Zgt_trans with m:= m; -Apply Zlt_gt; Assumption. -Qed. - -(** Mixed transitivity *) - -Lemma Zle_gt_trans : (n,m,p:Z)(Zle m n)->(Zgt m p)->(Zgt n p). -Proof. -Intros n m p H1 H2; NewDestruct (Zle_lt_or_eq m n H1) as [Hlt|Heq]; [ - Apply Zgt_trans with m; [Apply Zlt_gt; Assumption | Assumption ] -| Rewrite <- Heq; Assumption ]. -Qed. - -Lemma Zgt_le_trans : (n,m,p:Z)(Zgt n m)->(Zle p m)->(Zgt n p). -Proof. -Intros n m p H1 H2; NewDestruct (Zle_lt_or_eq p m H2) as [Hlt|Heq]; [ - Apply Zgt_trans with m; [Assumption|Apply Zlt_gt; Assumption] -| Rewrite Heq; Assumption ]. -Qed. - -Lemma Zlt_le_trans : (n,m,p:Z)(Zlt n m)->(Zle m p)->(Zlt n p). -Intros n m p H1 H2;Apply Zgt_lt;Apply Zle_gt_trans with m:=m; - [ Assumption | Apply Zlt_gt;Assumption ]. -Qed. - -Lemma Zle_lt_trans : (n,m,p:Z)(Zle n m)->(Zlt m p)->(Zlt n p). -Proof. -Intros n m p H1 H2;Apply Zgt_lt;Apply Zgt_le_trans with m:=m; - [ Apply Zlt_gt;Assumption | Assumption ]. -Qed. - -(** Transitivity of large orders *) - -Lemma Zle_trans : (n,m,p:Z)(Zle n m)->(Zle m p)->(Zle n p). -Proof. -Intros n m p H1 H2; Apply Znot_gt_le. -Intro Hgt; Apply Zle_not_gt with n m. Assumption. -Exact (Zgt_le_trans n p m Hgt H2). -Qed. - -Lemma Zge_trans : (n, m, p : Z) (Zge n m) -> (Zge m p) -> (Zge n p). -Proof. -Intros n m p H1 H2. -Apply Zle_ge. -Apply Zle_trans with m; Apply Zge_le; Trivial. -Qed. - -(** Compatibility of operations wrt to order *) - -Lemma Zgt_S_n : (n,p:Z)(Zgt (Zs p) (Zs n))->(Zgt p n). -Proof. -Unfold Zs Zgt;Intros n p;Do 2 Rewrite -> [m:Z](Zplus_sym m (POS xH)); -Rewrite -> (Zcompare_Zplus_compatible p n (POS xH));Trivial with arith. -Qed. - -Lemma Zle_S_n : (n,m:Z) (Zle (Zs m) (Zs n)) -> (Zle m n). -Proof. -Unfold Zle not ;Intros m n H1 H2;Apply H1; -Unfold Zs ;Do 2 Rewrite <- (Zplus_sym (POS xH)); -Rewrite -> (Zcompare_Zplus_compatible n m (POS xH));Assumption. -Qed. - -Lemma Zle_n_S : (n,m:Z) (Zle m n) -> (Zle (Zs m) (Zs n)). -Proof. -Unfold Zle not ;Intros m n H1 H2; Apply H1; -Rewrite <- (Zcompare_Zplus_compatible n m (POS xH)); -Do 2 Rewrite (Zplus_sym (POS xH)); Exact H2. -Qed. - -Lemma Zgt_n_S : (n,m:Z)(Zgt m n) -> (Zgt (Zs m) (Zs n)). -Proof. -Unfold Zgt; Intros n m H; Rewrite Zcompare_n_S; Auto with arith. -Qed. - -Lemma Zsimpl_gt_plus_l - : (n,m,p:Z)(Zgt (Zplus p n) (Zplus p m))->(Zgt n m). -Proof. -Unfold Zgt; Intros n m p H; - Rewrite <- (Zcompare_Zplus_compatible n m p); Assumption. -Qed. - -Lemma Zsimpl_gt_plus_r - : (n,m,p:Z)(Zgt (Zplus n p) (Zplus m p))->(Zgt n m). -Proof. -Intros n m p H; Apply Zsimpl_gt_plus_l with p. -Rewrite (Zplus_sym p n); Rewrite (Zplus_sym p m); Trivial. -Qed. - -Lemma Zgt_reg_l - : (n,m,p:Z)(Zgt n m)->(Zgt (Zplus p n) (Zplus p m)). -Proof. -Unfold Zgt; Intros n m p H; Rewrite (Zcompare_Zplus_compatible n m p); -Assumption. -Qed. - -Lemma Zgt_reg_r : (n,m,p:Z)(Zgt n m)->(Zgt (Zplus n p) (Zplus m p)). -Proof. -Intros n m p H; Rewrite (Zplus_sym n p); Rewrite (Zplus_sym m p); Apply Zgt_reg_l; Trivial. -Qed. - -(** Order, predecessor and successor *) - -Lemma Zgt_Sn_n : (n:Z)(Zgt (Zs n) n). -Proof. -Exact Zcompare_Zs_SUPERIEUR. -Qed. - -Lemma Zgt_le_S : (n,p:Z)(Zgt p n)->(Zle (Zs n) p). -Proof. -Unfold Zgt Zle; Intros n p H; Elim (Zcompare_et_un p n); Intros H1 H2; -Unfold not ;Intros H3; Unfold not in H1; Apply H1; [ - Assumption -| Elim (Zcompare_ANTISYM (Zplus n (POS xH)) p);Intros H4 H5;Apply H4;Exact H3]. -Qed. - -Lemma Zgt_S_le : (n,p:Z)(Zgt (Zs p) n)->(Zle n p). -Proof. -Intros n p H;Apply Zle_S_n; Apply Zgt_le_S; Assumption. -Qed. - -Lemma Zle_S_gt : (n,m:Z) (Zle (Zs n) m) -> (Zgt m n). -Proof. -Intros n m H;Apply Zle_gt_trans with m:=(Zs n); - [ Assumption | Apply Zgt_Sn_n ]. -Qed. - -Lemma Zle_gt_S : (n,p:Z)(Zle n p)->(Zgt (Zs p) n). -Proof. -Intros n p H; Apply Zgt_le_trans with p. - Apply Zgt_Sn_n. - Assumption. -Qed. - -Lemma Zgt_pred - : (n,p:Z)(Zgt p (Zs n))->(Zgt (Zpred p) n). -Proof. -Unfold Zgt Zs Zpred ;Intros n p H; -Rewrite <- [x,y:Z](Zcompare_Zplus_compatible x y (POS xH)); -Rewrite (Zplus_sym p); Rewrite Zplus_assoc; Rewrite [x:Z](Zplus_sym x n); -Simpl; Assumption. -Qed. - -Lemma Zlt_ZERO_pred_le_ZERO : (n:Z) (Zlt ZERO n) -> (Zle ZERO (Zpred n)). -Intros x H. -Rewrite (Zs_pred x) in H. -Apply Zgt_S_le. -Apply Zlt_gt. -Assumption. -Qed. - -(** Special cases of ordered integers *) - -Lemma Zle_n_Sn : (n:Z)(Zle n (Zs n)). -Proof. -Intros n; Apply Zgt_S_le;Apply Zgt_trans with m:=(Zs n) ;Apply Zgt_Sn_n. -Qed. - -Lemma Zle_pred_n : (n:Z)(Zle (Zpred n) n). -Proof. -Intros n;Pattern 2 n ;Rewrite Zs_pred; Apply Zle_n_Sn. -Qed. - -Lemma POS_gt_ZERO : (p:positive) (Zgt (POS p) ZERO). -Unfold Zgt; Trivial. -Qed. - - (* weaker but useful (in [Zpower] for instance) *) -Lemma ZERO_le_POS : (p:positive) (Zle ZERO (POS p)). -Intro; Unfold Zle; Discriminate. -Qed. - -Lemma NEG_lt_ZERO : (p:positive)(Zlt (NEG p) ZERO). -Unfold Zlt; Trivial. -Qed. - -(** Weakening equality within order *) - -Lemma Zlt_not_eq : (x,y:Z)(Zlt x y) -> ~x=y. -Proof. -Unfold not; Intros x y H H0. -Rewrite H0 in H. -Apply (Zlt_n_n ? H). -Qed. - -Lemma Zle_refl : (n,m:Z) n=m -> (Zle n m). -Proof. -Intros; Rewrite H; Apply Zle_n. -Qed. - -(** Transitivity using successor *) - -Lemma Zgt_trans_S : (n,m,p:Z)(Zgt (Zs n) m)->(Zgt m p)->(Zgt n p). -Proof. -Intros n m p H1 H2;Apply Zle_gt_trans with m:=m; - [ Apply Zgt_S_le; Assumption | Assumption ]. -Qed. - -Lemma Zgt_S : (n,m:Z)(Zgt (Zs n) m)->((Zgt n m)\/(m=n)). -Proof. -Intros n m H. -Assert Hle : (Zle m n). - Apply Zgt_S_le; Assumption. -NewDestruct (Zle_lt_or_eq ? ? Hle) as [Hlt|Heq]. - Left; Apply Zlt_gt; Assumption. - Right; Assumption. -Qed. - -Hints Resolve Zle_n Zle_n_Sn Zle_trans Zle_n_S : zarith. -Hints Immediate Zle_refl : zarith. - -Lemma Zle_trans_S : (n,m:Z)(Zle (Zs n) m)->(Zle n m). -Proof. -Intros n m H;Apply Zle_trans with m:=(Zs n); [ Apply Zle_n_Sn | Assumption ]. -Qed. - -Lemma Zle_Sn_n : (n:Z)~(Zle (Zs n) n). -Proof. -Intros n; Apply Zgt_not_le; Apply Zgt_Sn_n. -Qed. - -Lemma Zlt_n_Sn : (n:Z)(Zlt n (Zs n)). -Proof. -Intro n; Apply Zgt_lt; Apply Zgt_Sn_n. -Qed. - -Lemma Zlt_S : (n,m:Z)(Zlt n m)->(Zlt n (Zs m)). -Intros n m H;Apply Zgt_lt; Apply Zgt_trans with m:=m; [ - Apply Zgt_Sn_n -| Apply Zlt_gt; Assumption ]. -Qed. - -Lemma Zlt_n_S : (n,m:Z)(Zlt n m)->(Zlt (Zs n) (Zs m)). -Proof. -Intros n m H;Apply Zgt_lt;Apply Zgt_n_S;Apply Zlt_gt; Assumption. -Qed. - -Lemma Zlt_S_n : (n,m:Z)(Zlt (Zs n) (Zs m))->(Zlt n m). -Proof. -Intros n m H;Apply Zgt_lt;Apply Zgt_S_n;Apply Zlt_gt; Assumption. -Qed. - -Lemma Zlt_pred : (n,p:Z)(Zlt (Zs n) p)->(Zlt n (Zpred p)). -Proof. -Intros n p H;Apply Zlt_S_n; Rewrite <- Zs_pred; Assumption. -Qed. - -Lemma Zlt_pred_n_n : (n:Z)(Zlt (Zpred n) n). -Proof. -Intros n; Apply Zlt_S_n; Rewrite <- Zs_pred; Apply Zlt_n_Sn. -Qed. - -Lemma Zlt_le_S : (n,p:Z)(Zlt n p)->(Zle (Zs n) p). -Proof. -Intros n p H; Apply Zgt_le_S; Apply Zlt_gt; Assumption. -Qed. - -Lemma Zlt_n_Sm_le : (n,m:Z)(Zlt n (Zs m))->(Zle n m). -Proof. -Intros n m H; Apply Zgt_S_le; Apply Zlt_gt; Assumption. -Qed. - -Lemma Zle_lt_n_Sm : (n,m:Z)(Zle n m)->(Zlt n (Zs m)). -Proof. -Intros n m H; Apply Zgt_lt; Apply Zle_gt_S; Assumption. -Qed. - -Lemma Zle_le_S : (x,y:Z)(Zle x y)->(Zle x (Zs y)). -Proof. -Intros. -Apply Zle_trans with y; Trivial with zarith. -Qed. - -Hints Resolve Zle_le_S : zarith. - -(** Simplification and compatibility *) - -Lemma Zsimpl_le_plus_l : (p,n,m:Z)(Zle (Zplus p n) (Zplus p m))->(Zle n m). -Proof. -Intros p n m; Unfold Zle not ;Intros H1 H2;Apply H1; -Rewrite (Zcompare_Zplus_compatible n m p); Assumption. -Qed. - -Lemma Zsimpl_le_plus_r : (p,n,m:Z)(Zle (Zplus n p) (Zplus m p))->(Zle n m). -Proof. -Intros p n m H; Apply Zsimpl_le_plus_l with p. -Rewrite (Zplus_sym p n); Rewrite (Zplus_sym p m); Trivial. -Qed. - -Lemma Zle_reg_l : (n,m,p:Z)(Zle n m)->(Zle (Zplus p n) (Zplus p m)). -Proof. -Intros n m p; Unfold Zle not ;Intros H1 H2;Apply H1; -Rewrite <- (Zcompare_Zplus_compatible n m p); Assumption. -Qed. - -Lemma Zle_reg_r : (n,m,p:Z) (Zle n m)->(Zle (Zplus n p) (Zplus m p)). -Proof. -Intros a b c;Do 2 Rewrite [n:Z](Zplus_sym n c); Exact (Zle_reg_l a b c). -Qed. - -Lemma Zle_plus_plus : - (n,m,p,q:Z) (Zle n m)->(Zle p q)->(Zle (Zplus n p) (Zplus m q)). -Proof. -Intros n m p q; Intros H1 H2;Apply Zle_trans with m:=(Zplus n q); [ - Apply Zle_reg_l;Assumption | Apply Zle_reg_r;Assumption ]. -Qed. - -Lemma Zsimpl_lt_plus_l - : (n,m,p:Z)(Zlt (Zplus p n) (Zplus p m))->(Zlt n m). -Proof. -Unfold Zlt ;Intros n m p; - Rewrite Zcompare_Zplus_compatible;Trivial with arith. -Qed. - -Lemma Zsimpl_lt_plus_r - : (n,m,p:Z)(Zlt (Zplus n p) (Zplus m p))->(Zlt n m). -Proof. -Intros n m p H; Apply Zsimpl_lt_plus_l with p. -Rewrite (Zplus_sym p n); Rewrite (Zplus_sym p m); Trivial. -Qed. - -Lemma Zlt_reg_l : (n,m,p:Z)(Zlt n m)->(Zlt (Zplus p n) (Zplus p m)). -Proof. -Unfold Zlt ;Intros n m p; Rewrite Zcompare_Zplus_compatible;Trivial with arith. -Qed. - -Lemma Zlt_reg_r : (n,m,p:Z)(Zlt n m)->(Zlt (Zplus n p) (Zplus m p)). -Proof. -Intros n m p H; Rewrite (Zplus_sym n p); Rewrite (Zplus_sym m p); Apply Zlt_reg_l; Trivial. -Qed. - -Lemma Zlt_le_reg : - (a,b,c,d:Z) (Zlt a b)->(Zle c d)->(Zlt (Zplus a c) (Zplus b d)). -Proof. -Intros a b c d H0 H1. -Apply Zlt_le_trans with (Zplus b c). -Apply Zlt_reg_r; Trivial. -Apply Zle_reg_l; Trivial. -Qed. - -Lemma Zle_lt_reg : - (a,b,c,d:Z) (Zle a b)->(Zlt c d)->(Zlt (Zplus a c) (Zplus b d)). -Proof. -Intros a b c d H0 H1. -Apply Zle_lt_trans with (Zplus b c). -Apply Zle_reg_r; Trivial. -Apply Zlt_reg_l; Trivial. -Qed. - -(** Equivalence between inequalities (used in contrib/graph) *) - -Lemma Zle_plus_swap : (x,y,z:Z) (Zle (Zplus x z) y) <-> (Zle x (Zminus y z)). -Proof. - Intros. Split. Intro. Rewrite <- (Zero_right x). Rewrite <- (Zplus_inverse_r z). - Rewrite Zplus_assoc_l. Exact (Zle_reg_r ? ? ? H). - Intro. Rewrite <- (Zero_right y). Rewrite <- (Zplus_inverse_l z). Rewrite Zplus_assoc_l. - Apply Zle_reg_r. Assumption. -Qed. - -Lemma Zge_iff_le : (x,y:Z) (Zge x y) <-> (Zle y x). -Proof. - Intros. Split. Intro. Apply Zge_le. Assumption. - Intro. Apply Zle_ge. Assumption. -Qed. - -Lemma Zlt_plus_swap : (x,y,z:Z) (Zlt (Zplus x z) y) <-> (Zlt x (Zminus y z)). -Proof. - Intros. Split. Intro. Unfold Zminus. Rewrite Zplus_sym. Rewrite <- (Zero_left x). - Rewrite <- (Zplus_inverse_l z). Rewrite Zplus_assoc_r. Apply Zlt_reg_l. Rewrite Zplus_sym. - Assumption. - Intro. Rewrite Zplus_sym. Rewrite <- (Zero_left y). Rewrite <- (Zplus_inverse_r z). - Rewrite Zplus_assoc_r. Apply Zlt_reg_l. Rewrite Zplus_sym. Assumption. -Qed. - -Lemma Zgt_iff_lt : (x,y:Z) (Zgt x y) <-> (Zlt y x). -Proof. - Intros. Split. Intro. Apply Zgt_lt. Assumption. - Intro. Apply Zlt_gt. Assumption. -Qed. - -Lemma Zeq_plus_swap : (x,y,z:Z) (Zplus x z)=y <-> x=(Zminus y z). -Proof. - Intros. Split. Intro. Rewrite <- H. Unfold Zminus. Rewrite Zplus_assoc_r. - Rewrite Zplus_inverse_r. Apply sym_eq. Apply Zero_right. - Intro. Rewrite H. Unfold Zminus. Rewrite Zplus_assoc_r. Rewrite Zplus_inverse_l. - Apply Zero_right. -Qed. - -(** Reverting [x ?= y] to trichotomy *) - -Lemma rename : (A:Set)(P:A->Prop)(x:A) ((y:A)(x=y)->(P y)) -> (P x). -Auto with arith. -Qed. - -Theorem Zcompare_elim : - (c1,c2,c3:Prop)(x,y:Z) - ((x=y) -> c1) ->((Zlt x y) -> c2) ->((Zgt x y)-> c3) - -> Cases (Zcompare x y) of EGAL => c1 | INFERIEUR => c2 | SUPERIEUR => c3 end. -Proof. -Intros. -Apply rename with x:=(Zcompare x y); Intro r; Elim r; -[ Intro; Apply H; Apply (Zcompare_EGAL_eq x y); Assumption -| Unfold Zlt in H0; Assumption -| Unfold Zgt in H1; Assumption ]. -Qed. - -Lemma Zcompare_eq_case : - (c1,c2,c3:Prop)(x,y:Z) c1 -> x=y -> - Cases (Zcompare x y) of EGAL => c1 | INFERIEUR => c2 | SUPERIEUR => c3 end. -Intros. -Rewrite H0; Rewrite (Zcompare_x_x). -Assumption. -Qed. - -(** Decompose an egality between two [?=] relations into 3 implications *) - -Theorem Zcompare_egal_dec : - (x1,y1,x2,y2:Z) - ((Zlt x1 y1)->(Zlt x2 y2)) - ->((Zcompare x1 y1)=EGAL -> (Zcompare x2 y2)=EGAL) - ->((Zgt x1 y1)->(Zgt x2 y2))->(Zcompare x1 y1)=(Zcompare x2 y2). -Intros x1 y1 x2 y2. -Unfold Zgt; Unfold Zlt; -Case (Zcompare x1 y1); Case (Zcompare x2 y2); Auto with arith; Symmetry; Auto with arith. -Qed. - -(** Relating [x ?= y] to [Zle], [Zlt], [Zge] or [Zgt] *) - -Lemma Zle_Zcompare : - (x,y:Z)(Zle x y) -> - Cases (Zcompare x y) of EGAL => True | INFERIEUR => True | SUPERIEUR => False end. -Intros x y; Unfold Zle; Elim (Zcompare x y); Auto with arith. -Qed. - -Lemma Zlt_Zcompare : - (x,y:Z)(Zlt x y) -> - Cases (Zcompare x y) of EGAL => False | INFERIEUR => True | SUPERIEUR => False end. -Intros x y; Unfold Zlt; Elim (Zcompare x y); Intros; Discriminate Orelse Trivial with arith. -Qed. - -Lemma Zge_Zcompare : - (x,y:Z)(Zge x y)-> - Cases (Zcompare x y) of EGAL => True | INFERIEUR => False | SUPERIEUR => True end. -Intros x y; Unfold Zge; Elim (Zcompare x y); Auto with arith. -Qed. - -Lemma Zgt_Zcompare : - (x,y:Z)(Zgt x y) -> - Cases (Zcompare x y) of EGAL => False | INFERIEUR => False | SUPERIEUR => True end. -Intros x y; Unfold Zgt; Elim (Zcompare x y); Intros; Discriminate Orelse Trivial with arith. -Qed. - -(**********************************************************************) -(** Minimum on binary integer numbers *) - -Definition Zmin := [n,m:Z] - <Z>Cases (Zcompare n m) of - EGAL => n - | INFERIEUR => n - | SUPERIEUR => m - end. - -(** Properties of minimum on binary integer numbers *) - -Lemma Zmin_SS : (n,m:Z)((Zs (Zmin n m))=(Zmin (Zs n) (Zs m))). -Proof. -Intros n m;Unfold Zmin; Rewrite (Zcompare_n_S n m); -(ElimCompare 'n 'm);Intros E;Rewrite E;Auto with arith. -Qed. - -Lemma Zle_min_l : (n,m:Z)(Zle (Zmin n m) n). -Proof. -Intros n m;Unfold Zmin ; (ElimCompare 'n 'm);Intros E;Rewrite -> E; - [ Apply Zle_n | Apply Zle_n | Apply Zlt_le_weak; Apply Zgt_lt;Exact E ]. -Qed. - -Lemma Zle_min_r : (n,m:Z)(Zle (Zmin n m) m). -Proof. -Intros n m;Unfold Zmin ; (ElimCompare 'n 'm);Intros E;Rewrite -> E;[ - Unfold Zle ;Rewrite -> E;Discriminate -| Unfold Zle ;Rewrite -> E;Discriminate -| Apply Zle_n ]. -Qed. - -Lemma Zmin_case : (n,m:Z)(P:Z->Set)(P n)->(P m)->(P (Zmin n m)). -Proof. -Intros n m P H1 H2; Unfold Zmin; Case (Zcompare n m);Auto with arith. -Qed. - -Lemma Zmin_or : (n,m:Z)(Zmin n m)=n \/ (Zmin n m)=m. -Proof. -Unfold Zmin; Intros; Elim (Zcompare n m); Auto. -Qed. - -Lemma Zmin_n_n : (n:Z) (Zmin n n)=n. -Proof. -Unfold Zmin; Intros; Elim (Zcompare n n); Auto. -Qed. - -Lemma Zmin_plus : - (x,y,n:Z)(Zmin (Zplus x n) (Zplus y n))=(Zplus (Zmin x y) n). -Proof. -Intros; Unfold Zmin. -Rewrite (Zplus_sym x n); -Rewrite (Zplus_sym y n); -Rewrite (Zcompare_Zplus_compatible x y n). -Case (Zcompare x y); Apply Zplus_sym. -Qed. - -(**********************************************************************) -(* Absolute value on integers *) - -Definition absolu [x:Z] : nat := - Cases x of - ZERO => O - | (POS p) => (convert p) - | (NEG p) => (convert p) - end. - -Definition Zabs [z:Z] : Z := - Cases z of - ZERO => ZERO - | (POS p) => (POS p) - | (NEG p) => (POS p) - end. - -(** Properties of absolute value *) - -Lemma Zabs_eq : (x:Z) (Zle ZERO x) -> (Zabs x)=x. -NewDestruct x; Auto with arith. -Compute; Intros; Absurd SUPERIEUR=SUPERIEUR; Trivial with arith. -Qed. - -Lemma Zabs_non_eq : (x:Z) (Zle x ZERO) -> (Zabs x)=(Zopp x). -Proof. -NewDestruct x; Auto with arith. -Compute; Intros; Absurd SUPERIEUR=SUPERIEUR; Trivial with arith. -Qed. - -Definition Zabs_dec : (x:Z){x=(Zabs x)}+{x=(Zopp (Zabs x))}. -Proof. -NewDestruct x;Auto with arith. -Defined. - -Lemma Zabs_pos : (x:Z)(Zle ZERO (Zabs x)). -NewDestruct x;Auto with arith; Compute; Intros H;Inversion H. -Qed. - -Lemma Zsgn_Zabs: (x:Z)(Zmult x (Zsgn x))=(Zabs x). -Proof. -NewDestruct x; Rewrite Zmult_sym; Auto with arith. -Qed. - -Lemma Zabs_Zsgn: (x:Z)(Zmult (Zabs x) (Zsgn x))=x. -Proof. -NewDestruct x; Rewrite Zmult_sym; Auto with arith. -Qed. - -(** absolute value in nat is compatible with order *) - -Lemma absolu_lt : (x,y:Z) (Zle ZERO x)/\(Zlt x y) -> (lt (absolu x) (absolu y)). -Proof. -Intros x y. Case x; Simpl. Case y; Simpl. - -Intro. Absurd (Zlt ZERO ZERO). Compute. Intro H0. Discriminate H0. Intuition. -Intros. Elim (ZL4 p). Intros. Rewrite H0. Auto with arith. -Intros. Elim (ZL4 p). Intros. Rewrite H0. Auto with arith. - -Case y; Simpl. -Intros. Absurd (Zlt (POS p) ZERO). Compute. Intro H0. Discriminate H0. Intuition. -Intros. Change (gt (convert p) (convert p0)). -Apply compare_convert_SUPERIEUR. -Elim H; Auto with arith. Intro. Exact (ZC2 p0 p). - -Intros. Absurd (Zlt (POS p0) (NEG p)). -Compute. Intro H0. Discriminate H0. Intuition. - -Intros. Absurd (Zle ZERO (NEG p)). Compute. Auto with arith. Intuition. -Qed. - -Lemma Zlt_minus : (n,m:Z)(Zlt ZERO m)->(Zlt (Zminus n m) n). -Proof. -Intros n m H; Apply Zsimpl_lt_plus_l with p:=m; Rewrite Zle_plus_minus; -Pattern 1 n ;Rewrite <- (Zero_right n); Rewrite (Zplus_sym m n); -Apply Zlt_reg_l; Assumption. -Qed. - -Lemma Zlt_O_minus_lt : (n,m:Z)(Zlt ZERO (Zminus n m))->(Zlt m n). -Proof. -Intros n m H; Apply Zsimpl_lt_plus_l with p:=(Zopp m); Rewrite Zplus_inverse_l; -Rewrite Zplus_sym;Exact H. -Qed. - -(** Just for compatibility with previous versions. - Use [Zmult_plus_distr_r] and [Zmult_plus_distr_l] rather than - their synomymous *) - -Definition Zmult_Zplus_distr := Zmult_plus_distr_r. -Definition Zmult_plus_distr := Zmult_plus_distr_l. +Require Export Zorder. +Require Export Zmin. +Require Export Zabs. + +V7only [ +Notation Zlt := Zlt. +Notation Zgt := Zgt. +Notation Zle := Zle. +Notation Zge := Zge. +Notation Zsgn := Zsgn. +Notation absolu := absolu. +Notation Zabs := Zabs. +Notation Zabs_eq := Zabs_eq. +Notation Zabs_non_eq := Zabs_non_eq. +Notation Zabs_dec := Zabs_dec. +Notation Zabs_pos := Zabs_pos. +Notation Zsgn_Zabs := Zsgn_Zabs. +Notation Zabs_Zsgn := Zabs_Zsgn. +Notation inject_nat := inject_nat. +Notation Zs := Zs. +Notation Zpred := Zpred. +Notation Zgt_Sn_n := Zgt_Sn_n. +Notation Zle_gt_trans := Zle_gt_trans. +Notation Zgt_le_trans := Zgt_le_trans. +Notation Zle_S_gt := Zle_S_gt. +Notation Zcompare_n_S := Zcompare_n_S. +Notation Zgt_n_S := Zgt_n_S. +Notation Zle_not_gt := Zle_not_gt. +Notation Zgt_antirefl := Zgt_antirefl. +Notation Zgt_not_sym := Zgt_not_sym. +Notation Zgt_not_le := Zgt_not_le. +Notation Zgt_trans := Zgt_trans. +Notation Zle_gt_S := Zle_gt_S. +Notation Zgt_pred := Zgt_pred. +Notation Zsimpl_gt_plus_l := Zsimpl_gt_plus_l. +Notation Zsimpl_gt_plus_r := Zsimpl_gt_plus_r. +Notation Zgt_reg_l := Zgt_reg_l. +Notation Zgt_reg_r := Zgt_reg_r. +Notation Zcompare_et_un := Zcompare_et_un. +Notation Zgt_S_n := Zgt_S_n. +Notation Zle_S_n := Zle_S_n. +Notation Zgt_le_S := Zgt_le_S. +Notation Zgt_S_le := Zgt_S_le. +Notation Zgt_S := Zgt_S. +Notation Zgt_trans_S := Zgt_trans_S. +Notation Zeq_S := Zeq_S. +Notation Zpred_Sn := Zpred_Sn. +Notation Zeq_add_S := Zeq_add_S. +Notation Znot_eq_S := Znot_eq_S. +Notation Zsimpl_plus_l := Zsimpl_plus_l. +Notation Zn_Sn := Zn_Sn. +Notation Zplus_n_O := Zplus_n_O. +Notation Zplus_unit_left := Zplus_unit_left. +Notation Zplus_unit_right := Zplus_unit_right. +Notation Zplus_n_Sm := Zplus_n_Sm. +Notation Zmult_n_O := Zmult_n_O. +Notation Zmult_n_Sm := Zmult_n_Sm. +Notation Zle_n := Zle_n. +Notation Zle_refl := Zle_refl. +Notation Zle_trans := Zle_trans. +Notation Zle_n_Sn := Zle_n_Sn. +Notation Zle_n_S := Zle_n_S. +Notation Zs_pred := Zs_pred. +Notation Zle_pred_n := Zle_pred_n. +Notation Zle_trans_S := Zle_trans_S. +Notation Zle_Sn_n := Zle_Sn_n. +Notation Zle_antisym := Zle_antisym. +Notation Zgt_lt := Zgt_lt. +Notation Zlt_gt := Zlt_gt. +Notation Zge_le := Zge_le. +Notation Zle_ge := Zle_ge. +Notation Zge_trans := Zge_trans. +Notation Zlt_n_Sn := Zlt_n_Sn. +Notation Zlt_S := Zlt_S. +Notation Zlt_n_S := Zlt_n_S. +Notation Zlt_S_n := Zlt_S_n. +Notation Zlt_n_n := Zlt_n_n. +Notation Zlt_pred := Zlt_pred. +Notation Zlt_pred_n_n := Zlt_pred_n_n. +Notation Zlt_le_S := Zlt_le_S. +Notation Zlt_n_Sm_le := Zlt_n_Sm_le. +Notation Zle_lt_n_Sm := Zle_lt_n_Sm. +Notation Zlt_le_weak := Zlt_le_weak. +Notation Zlt_trans := Zlt_trans. +Notation Zlt_le_trans := Zlt_le_trans. +Notation Zle_lt_trans := Zle_lt_trans. +Notation Zle_lt_or_eq := Zle_lt_or_eq. +Notation Zle_or_lt := Zle_or_lt. +Notation Zle_not_lt := Zle_not_lt. +Notation Zlt_not_le := Zlt_not_le. +Notation Zlt_not_sym := Zlt_not_sym. +Notation Zle_le_S := Zle_le_S. +Notation Zmin := Zmin. +Notation Zmin_SS := Zmin_SS. +Notation Zle_min_l := Zle_min_l. +Notation Zle_min_r := Zle_min_r. +Notation Zmin_case := Zmin_case. +Notation Zmin_or := Zmin_or. +Notation Zmin_n_n := Zmin_n_n. +Notation Zplus_assoc_l := Zplus_assoc_l. +Notation Zplus_assoc_r := Zplus_assoc_r. +Notation Zplus_permute := Zplus_permute. +Notation Zsimpl_le_plus_l := Zsimpl_le_plus_l. +Notation Zsimpl_le_plus_r := Zsimpl_le_plus_r. +Notation Zle_reg_l := Zle_reg_l. +Notation Zle_reg_r := Zle_reg_r. +Notation Zle_plus_plus := Zle_plus_plus. +Notation Zplus_Snm_nSm := Zplus_Snm_nSm. +Notation Zsimpl_lt_plus_l := Zsimpl_lt_plus_l. +Notation Zsimpl_lt_plus_r := Zsimpl_lt_plus_r. +Notation Zlt_reg_l := Zlt_reg_l. +Notation Zlt_reg_r := Zlt_reg_r. +Notation Zlt_le_reg := Zlt_le_reg. +Notation Zle_lt_reg := Zle_lt_reg. +Notation Zminus := Zminus. +Notation Zminus_plus_simpl := Zminus_plus_simpl. +Notation Zminus_n_O := Zminus_n_O. +Notation Zminus_n_n := Zminus_n_n. +Notation Zplus_minus := Zplus_minus. +Notation Zminus_plus := Zminus_plus. +Notation Zle_plus_minus := Zle_plus_minus. +Notation Zminus_Sn_m := Zminus_Sn_m. +Notation Zlt_minus := Zlt_minus. +Notation Zlt_O_minus_lt := Zlt_O_minus_lt. +Notation Zmult_plus_distr_l := Zmult_plus_distr_l. +Notation Zmult_minus_distr := Zmult_minus_distr. +Notation Zmult_assoc_r := Zmult_assoc_r. +Notation Zmult_assoc_l := Zmult_assoc_l. +Notation Zmult_permute := Zmult_permute. +Notation Zmult_1_n := Zmult_1_n. +Notation Zmult_n_1 := Zmult_n_1. +Notation Zmult_Sm_n := Zmult_Sm_n. +Notation Zmult_Zplus_distr := Zmult_plus_distr_r. +Notation Zmult_plus_distr := Zmult_plus_distr_l. +]. |