diff options
Diffstat (limited to 'theories7/ZArith/Zdiv.v')
| -rw-r--r-- | theories7/ZArith/Zdiv.v | 432 |
1 files changed, 0 insertions, 432 deletions
diff --git a/theories7/ZArith/Zdiv.v b/theories7/ZArith/Zdiv.v deleted file mode 100644 index 84d53931..00000000 --- a/theories7/ZArith/Zdiv.v +++ /dev/null @@ -1,432 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(*i $Id: Zdiv.v,v 1.1.2.1 2004/07/16 19:31:43 herbelin Exp $ i*) - -(* Contribution by Claude Marché and Xavier Urbain *) - -(** - -Euclidean Division - -Defines first of function that allows Coq to normalize. -Then only after proves the main required property. - -*) - -Require Export ZArith_base. -Require Zbool. -Require Omega. -Require ZArithRing. -Require Zcomplements. -V7only [Import Z_scope.]. -Open Local Scope Z_scope. - -(** - - Euclidean division of a positive by a integer - (that is supposed to be positive). - - total function than returns an arbitrary value when - divisor is not positive - -*) - -Fixpoint Zdiv_eucl_POS [a:positive] : Z -> Z*Z := [b:Z] - Cases a of - | xH => if `(Zge_bool b 2)` then `(0,1)` else `(1,0)` - | (xO a') => - let (q,r) = (Zdiv_eucl_POS a' b) in - [r':=`2*r`] if `(Zgt_bool b r')` then `(2*q,r')` else `(2*q+1,r'-b)` - | (xI a') => - let (q,r) = (Zdiv_eucl_POS a' b) in - [r':=`2*r+1`] if `(Zgt_bool b r')` then `(2*q,r')` else `(2*q+1,r'-b)` - end. - - -(** - - Euclidean division of integers. - - Total function than returns (0,0) when dividing by 0. - -*) - -(* - - The pseudo-code is: - - if b = 0 : (0,0) - - if b <> 0 and a = 0 : (0,0) - - if b > 0 and a < 0 : let (q,r) = div_eucl_pos (-a) b in - if r = 0 then (-q,0) else (-(q+1),b-r) - - if b < 0 and a < 0 : let (q,r) = div_eucl (-a) (-b) in (q,-r) - - if b < 0 and a > 0 : let (q,r) = div_eucl a (-b) in - if r = 0 then (-q,0) else (-(q+1),b+r) - - In other word, when b is non-zero, q is chosen to be the greatest integer - smaller or equal to a/b. And sgn(r)=sgn(b) and |r| < |b|. - -*) - -Definition Zdiv_eucl [a,b:Z] : Z*Z := - Cases a b of - | ZERO _ => `(0,0)` - | _ ZERO => `(0,0)` - | (POS a') (POS _) => (Zdiv_eucl_POS a' b) - | (NEG a') (POS _) => - let (q,r) = (Zdiv_eucl_POS a' b) in - Cases r of - | ZERO => `(-q,0)` - | _ => `(-(q+1),b-r)` - end - | (NEG a') (NEG b') => - let (q,r) = (Zdiv_eucl_POS a' (POS b')) in `(q,-r)` - | (POS a') (NEG b') => - let (q,r) = (Zdiv_eucl_POS a' (POS b')) in - Cases r of - | ZERO => `(-q,0)` - | _ => `(-(q+1),b+r)` - end - end. - - -(** Division and modulo are projections of [Zdiv_eucl] *) - -Definition Zdiv [a,b:Z] : Z := let (q,_) = (Zdiv_eucl a b) in q. - -Definition Zmod [a,b:Z] : Z := let (_,r) = (Zdiv_eucl a b) in r. - -(* Tests: - -Eval Compute in `(Zdiv_eucl 7 3)`. - -Eval Compute in `(Zdiv_eucl (-7) 3)`. - -Eval Compute in `(Zdiv_eucl 7 (-3))`. - -Eval Compute in `(Zdiv_eucl (-7) (-3))`. - -*) - - -(** - - Main division theorem. - - First a lemma for positive - -*) - -Lemma Z_div_mod_POS : (b:Z)`b > 0` -> (a:positive) - let (q,r)=(Zdiv_eucl_POS a b) in `(POS a) = b*q + r`/\`0<=r<b`. -Proof. -Induction a; Unfold Zdiv_eucl_POS; Fold Zdiv_eucl_POS. - -Intro p; Case (Zdiv_eucl_POS p b); Intros q r (H0,H1). -Generalize (Zgt_cases b `2*r+1`). -Case (Zgt_bool b `2*r+1`); -(Rewrite POS_xI; Rewrite H0; Split ; [ Ring | Omega ]). - -Intros p; Case (Zdiv_eucl_POS p b); Intros q r (H0,H1). -Generalize (Zgt_cases b `2*r`). -Case (Zgt_bool b `2*r`); - Rewrite POS_xO; Change (POS (xO p)) with `2*(POS p)`; - Rewrite H0; (Split; [Ring | Omega]). - -Generalize (Zge_cases b `2`). -Case (Zge_bool b `2`); (Intros; Split; [Ring | Omega ]). -Omega. -Qed. - - -Theorem Z_div_mod : (a,b:Z)`b > 0` -> - let (q,r) = (Zdiv_eucl a b) in `a = b*q + r` /\ `0<=r<b`. -Proof. -Intros a b; Case a; Case b; Try (Simpl; Intros; Omega). -Unfold Zdiv_eucl; Intros; Apply Z_div_mod_POS; Trivial. - -Intros; Discriminate. - -Intros. -Generalize (Z_div_mod_POS (POS p) H p0). -Unfold Zdiv_eucl. -Case (Zdiv_eucl_POS p0 (POS p)). -Intros z z0. -Case z0. - -Intros [H1 H2]. -Split; Trivial. -Replace (NEG p0) with `-(POS p0)`; [ Rewrite H1; Ring | Trivial ]. - -Intros p1 [H1 H2]. -Split; Trivial. -Replace (NEG p0) with `-(POS p0)`; [ Rewrite H1; Ring | Trivial ]. -Generalize (POS_gt_ZERO p1); Omega. - -Intros p1 [H1 H2]. -Split; Trivial. -Replace (NEG p0) with `-(POS p0)`; [ Rewrite H1; Ring | Trivial ]. -Generalize (NEG_lt_ZERO p1); Omega. - -Intros; Discriminate. -Qed. - -(** Existence theorems *) - -Theorem Zdiv_eucl_exist : (b:Z)`b > 0` -> (a:Z) - { qr:Z*Z | let (q,r)=qr in `a=b*q+r` /\ `0 <= r < b` }. -Proof. -Intros b Hb a. -Exists (Zdiv_eucl a b). -Exact (Z_div_mod a b Hb). -Qed. - -Implicits Zdiv_eucl_exist. - -Theorem Zdiv_eucl_extended : (b:Z)`b <> 0` -> (a:Z) - { qr:Z*Z | let (q,r)=qr in `a=b*q+r` /\ `0 <= r < |b|` }. -Proof. -Intros b Hb a. -Elim (Z_le_gt_dec `0` b);Intro Hb'. -Cut `b>0`;[Intro Hb''|Omega]. -Rewrite Zabs_eq;[Apply Zdiv_eucl_exist;Assumption|Assumption]. -Cut `-b>0`;[Intro Hb''|Omega]. -Elim (Zdiv_eucl_exist Hb'' a);Intros qr. -Elim qr;Intros q r Hqr. -Exists (pair ? ? `-q` r). -Elim Hqr;Intros. -Split. -Rewrite <- Zmult_Zopp_left;Assumption. -Rewrite Zabs_non_eq;[Assumption|Omega]. -Qed. - -Implicits Zdiv_eucl_extended. - -(** Auxiliary lemmas about [Zdiv] and [Zmod] *) - -Lemma Z_div_mod_eq : (a,b:Z)`b > 0` -> `a = b * (Zdiv a b) + (Zmod a b)`. -Proof. -Unfold Zdiv Zmod. -Intros a b Hb. -Generalize (Z_div_mod a b Hb). -Case (Zdiv_eucl); Tauto. -Save. - -Lemma Z_mod_lt : (a,b:Z)`b > 0` -> `0 <= (Zmod a b) < b`. -Proof. -Unfold Zmod. -Intros a b Hb. -Generalize (Z_div_mod a b Hb). -Case (Zdiv_eucl a b); Tauto. -Save. - -Lemma Z_div_POS_ge0 : (b:Z)(a:positive) - let (q,_) = (Zdiv_eucl_POS a b) in `q >= 0`. -Proof. -Induction a; Unfold Zdiv_eucl_POS; Fold Zdiv_eucl_POS. -Intro p; Case (Zdiv_eucl_POS p b). -Intros; Case (Zgt_bool b `2*z0+1`); Intros; Omega. -Intro p; Case (Zdiv_eucl_POS p b). -Intros; Case (Zgt_bool b `2*z0`); Intros; Omega. -Case (Zge_bool b `2`); Simpl; Omega. -Save. - -Lemma Z_div_ge0 : (a,b:Z)`b > 0` -> `a >= 0` -> `(Zdiv a b) >= 0`. -Proof. -Intros a b Hb; Unfold Zdiv Zdiv_eucl; Case a; Simpl; Intros. -Case b; Simpl; Trivial. -Generalize Hb; Case b; Try Trivial. -Auto with zarith. -Intros p0 Hp0; Generalize (Z_div_POS_ge0 (POS p0) p). -Case (Zdiv_eucl_POS p (POS p0)); Simpl; Tauto. -Intros; Discriminate. -Elim H; Trivial. -Save. - -Lemma Z_div_lt : (a,b:Z)`b >= 2` -> `a > 0` -> `(Zdiv a b) < a`. -Proof. -Intros. Cut `b > 0`; [Intro Hb | Omega]. -Generalize (Z_div_mod a b Hb). -Cut `a >= 0`; [Intro Ha | Omega]. -Generalize (Z_div_ge0 a b Hb Ha). -Unfold Zdiv; Case (Zdiv_eucl a b); Intros q r H1 [H2 H3]. -Cut `a >= 2*q` -> `q < a`; [ Intro h; Apply h; Clear h | Intros; Omega ]. -Apply Zge_trans with `b*q`. -Omega. -Auto with zarith. -Save. - -(** Syntax *) - -V7only[ -Grammar znatural expr2 : constr := - expr_div [ expr2($p) "/" expr2($c) ] -> [ (Zdiv $p $c) ] -| expr_mod [ expr2($p) "%" expr2($c) ] -> [ (Zmod $p $c) ] -. - -Syntax constr - level 6: - Zdiv [ (Zdiv $n1 $n2) ] - -> [ [<hov 0> "`"(ZEXPR $n1):E "/" [0 0] (ZEXPR $n2):L "`"] ] - | Zmod [ (Zmod $n1 $n2) ] - -> [ [<hov 0> "`"(ZEXPR $n1):E "%" [0 0] (ZEXPR $n2):L "`"] ] - | Zdiv_inside - [ << (ZEXPR <<(Zdiv $n1 $n2)>>) >> ] - -> [ (ZEXPR $n1):E "/" [0 0] (ZEXPR $n2):L ] - | Zmod_inside - [ << (ZEXPR <<(Zmod $n1 $n2)>>) >> ] - -> [ (ZEXPR $n1):E " %" [1 0] (ZEXPR $n2):L ] -. -]. - - -Infix 3 "/" Zdiv (no associativity) : Z_scope V8only. -Infix 3 "mod" Zmod (no associativity) : Z_scope. - -(** Other lemmas (now using the syntax for [Zdiv] and [Zmod]). *) - -Lemma Z_div_ge : (a,b,c:Z)`c > 0`->`a >= b`->`a/c >= b/c`. -Proof. -Intros a b c cPos aGeb. -Generalize (Z_div_mod_eq a c cPos). -Generalize (Z_mod_lt a c cPos). -Generalize (Z_div_mod_eq b c cPos). -Generalize (Z_mod_lt b c cPos). -Intros. -Elim (Z_ge_lt_dec `a/c` `b/c`); Trivial. -Intro. -Absurd `b-a >= 1`. -Omega. -Rewrite -> H0. -Rewrite -> H2. -Assert `c*(b/c)+b % c-(c*(a/c)+a % c) = c*(b/c - a/c) + b % c - a % c`. -Ring. -Rewrite H3. -Assert `c*(b/c-a/c) >= c*1`. -Apply Zge_Zmult_pos_left. -Omega. -Omega. -Assert `c*1=c`. -Ring. -Omega. -Save. - -Lemma Z_mod_plus : (a,b,c:Z)`c > 0`->`(a+b*c) % c = a % c`. -Proof. -Intros a b c cPos. -Generalize (Z_div_mod_eq a c cPos). -Generalize (Z_mod_lt a c cPos). -Generalize (Z_div_mod_eq `a+b*c` c cPos). -Generalize (Z_mod_lt `a+b*c` c cPos). -Intros. - -Assert `(a+b*c) % c - a % c = c*(b+a/c - (a+b*c)/c)`. -Replace `(a+b*c) % c` with `a+b*c - c*((a+b*c)/c)`. -Replace `a % c` with `a - c*(a/c)`. -Ring. -Omega. -Omega. -LetTac q := `b+a/c-(a+b*c)/c`. -Apply (Zcase_sign q); Intros. -Assert `c*q=0`. -Rewrite H4; Ring. -Rewrite H5 in H3. -Omega. - -Assert `c*q >= c`. -Pattern 2 c; Replace c with `c*1`. -Apply Zge_Zmult_pos_left; Omega. -Ring. -Omega. - -Assert `c*q <= -c`. -Replace `-c` with `c*(-1)`. -Apply Zle_Zmult_pos_left; Omega. -Ring. -Omega. -Save. - -Lemma Z_div_plus : (a,b,c:Z)`c > 0`->`(a+b*c)/c = a/c+b`. -Proof. -Intros a b c cPos. -Generalize (Z_div_mod_eq a c cPos). -Generalize (Z_mod_lt a c cPos). -Generalize (Z_div_mod_eq `a+b*c` c cPos). -Generalize (Z_mod_lt `a+b*c` c cPos). -Intros. -Apply Zmult_reg_left with c. Omega. -Replace `c*((a+b*c)/c)` with `a+b*c-(a+b*c) % c`. -Rewrite (Z_mod_plus a b c cPos). -Pattern 1 a; Rewrite H2. -Ring. -Pattern 1 `a+b*c`; Rewrite H0. -Ring. -Save. - -Lemma Z_div_mult : (a,b:Z)`b > 0`->`(a*b)/b = a`. -Intros; Replace `a*b` with `0+a*b`; Auto. -Rewrite Z_div_plus; Auto. -Save. - -Lemma Z_mult_div_ge : (a,b:Z)`b>0`->`b*(a/b) <= a`. -Proof. -Intros a b bPos. -Generalize (Z_div_mod_eq `a` ? bPos); Intros. -Generalize (Z_mod_lt `a` ? bPos); Intros. -Pattern 2 a; Rewrite H. -Omega. -Save. - -Lemma Z_mod_same : (a:Z)`a>0`->`a % a=0`. -Proof. -Intros a aPos. -Generalize (Z_mod_plus `0` `1` a aPos). -Replace `0+1*a` with `a`. -Intros. -Rewrite H. -Compute. -Trivial. -Ring. -Save. - -Lemma Z_div_same : (a:Z)`a>0`->`a/a=1`. -Proof. -Intros a aPos. -Generalize (Z_div_plus `0` `1` a aPos). -Replace `0+1*a` with `a`. -Intros. -Rewrite H. -Compute. -Trivial. -Ring. -Save. - -Lemma Z_div_exact_1 : (a,b:Z)`b>0` -> `a = b*(a/b)` -> `a%b = 0`. -Intros a b Hb; Generalize (Z_div_mod a b Hb); Unfold Zmod Zdiv. -Case (Zdiv_eucl a b); Intros q r; Omega. -Save. - -Lemma Z_div_exact_2 : (a,b:Z)`b>0` -> `a%b = 0` -> `a = b*(a/b)`. -Intros a b Hb; Generalize (Z_div_mod a b Hb); Unfold Zmod Zdiv. -Case (Zdiv_eucl a b); Intros q r; Omega. -Save. - -Lemma Z_mod_zero_opp : (a,b:Z)`b>0` -> `a%b = 0` -> `(-a)%b = 0`. -Intros a b Hb. -Intros. -Rewrite Z_div_exact_2 with a b; Auto. -Replace `-(b*(a/b))` with `0+(-(a/b))*b`. -Rewrite Z_mod_plus; Auto. -Ring. -Save. - |