diff options
Diffstat (limited to 'theories7/ZArith/Zdiv.v')
| -rw-r--r-- | theories7/ZArith/Zdiv.v | 432 |
1 files changed, 432 insertions, 0 deletions
diff --git a/theories7/ZArith/Zdiv.v b/theories7/ZArith/Zdiv.v new file mode 100644 index 00000000..84d53931 --- /dev/null +++ b/theories7/ZArith/Zdiv.v @@ -0,0 +1,432 @@ +(************************************************************************) +(* 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. + |