Processor integers + Print assumption (see coqdev mailing list for the

details).




git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9821 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 452 insertions, 0 deletions

diff --git a/theories/Ints/Z/ZDivModAux.v b/theories/Ints/Z/ZDivModAux.v
new file mode 100644
index 0000000000..d07b92d80e
--- /dev/null
+++ b/theories/Ints/Z/ZDivModAux.v
@@ -0,0 +1,452 @@
+
+(*************************************************************)
+(*      This file is distributed under the terms of the      *)
+(*      GNU Lesser General Public License Version 2.1        *)
+(*************************************************************)
+(*    Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr      *)
+(*************************************************************)
+
+(**********************************************************************
+     ZDivModAux.v                                                              
+                                                                               
+     Auxillary functions & Theorems for Zdiv and Zmod                          
+ **********************************************************************)
+
+Require Export ZArith.
+Require Export Znumtheory.
+Require Export Tactic.
+Require Import ZAux.
+Require Import ZPowerAux.
+
+Open Local Scope Z_scope. 
+
+Hint  Extern 2 (Zle _ _) => 
+ (match goal with
+  |- Zpos _ <= Zpos _ => exact (refl_equal _)
+  | H: _ <=  ?p |- _ <= ?p => apply Zle_trans with (2 := H)
+  | H: _ <  ?p |- _ <= ?p => 
+   apply Zlt_le_weak; apply Zle_lt_trans with (2 := H)
+  end).
+
+Hint  Extern 2 (Zlt _ _) => 
+ (match goal with
+   |- Zpos _ < Zpos _ => exact (refl_equal _)
+|      H: _ <=  ?p |- _ <= ?p => apply Zlt_le_trans with (2 := H)
+|   H: _ <  ?p |- _ <= ?p => apply Zle_lt_trans with (2 := H)
+  end).
+
+Hint Resolve Zlt_gt Zle_ge: zarith.
+
+(************************************** 
+  Properties Zmod 
+**************************************)
+ 
+ Theorem Zmod_mult:
+   forall a b n, 0 < n ->  (a * b) mod n = ((a mod n) * (b mod n)) mod n.
+ Proof.
+  intros a b n H.
+  pattern a at 1; rewrite (Z_div_mod_eq a n); auto with zarith.
+  pattern b at 1; rewrite (Z_div_mod_eq b n); auto with zarith.
+  replace ((n * (a / n) + a mod n) * (n * (b / n) + b mod n)) with
+   ((a mod n) * (b mod n) +
+   (((n*(a/n)) * (b/n) + (b mod n)*(a / n)) + (a mod n) * (b / n)) * n);
+   auto with zarith.
+  apply Z_mod_plus; auto with zarith.
+  ring.
+ Qed.
+
+ Theorem Zmod_plus:
+    forall a b n, 0 < n ->  (a + b) mod n = (a mod n + b mod n) mod n.
+ Proof.
+  intros a b n H.
+  pattern a at 1; rewrite (Z_div_mod_eq a n); auto with zarith.
+  pattern b at 1; rewrite (Z_div_mod_eq b n); auto with zarith.
+  replace ((n * (a / n) + a mod n) + (n * (b / n) + b mod n))
+     with ((a mod n + b mod n) + (a / n + b / n) * n); auto with zarith.
+  apply Z_mod_plus; auto with zarith.
+  ring.
+ Qed.
+ 
+ Theorem Zmod_mod: forall a n, 0 < n -> (a mod n) mod n = a mod n.
+ Proof.
+  intros a n H.
+  pattern a at 2; rewrite (Z_div_mod_eq a n); auto with zarith.
+  rewrite Zplus_comm; rewrite Zmult_comm.
+  apply sym_equal; apply Z_mod_plus; auto with zarith.
+ Qed.
+ 
+ Theorem Zmod_def_small: forall a n, 0 <= a < n  ->  a mod n = a.
+ Proof.
+  intros a n [H1 H2]; unfold Zmod.
+  generalize (Z_div_mod a n); case (Zdiv_eucl a n).
+  intros q r H3; case H3; clear H3; auto with zarith.
+  intros H4 [H5 H6].
+  case (Zle_or_lt q (- 1)); intros H7.
+  contradict H1; apply Zlt_not_le.
+  subst a.
+  apply Zle_lt_trans with (n * - 1 + r); auto with zarith.
+  case (Zle_lt_or_eq 0 q); auto with zarith; intros H8.
+  contradict H2; apply Zle_not_lt.
+  apply Zle_trans with (n * 1 + r); auto with zarith.
+  rewrite H4; auto with zarith.
+  subst a; subst q; auto with zarith.
+ Qed.
+
+ Theorem Zmod_minus: 
+     forall a b n, 0 < n -> (a - b) mod n = (a mod n - b mod n) mod n.
+ Proof.
+  intros a b n H; replace (a - b) with (a + (-1) * b); auto with zarith.
+  replace (a mod n - b mod n) with (a mod n + (-1)*(b mod n));auto with zarith.
+  rewrite Zmod_plus; auto with zarith.
+  rewrite Zmod_mult; auto with zarith.
+  rewrite (fun x y => Zmod_plus x  ((-1) * y)); auto with zarith.
+  rewrite Zmod_mult; auto with zarith.
+  rewrite (fun x => Zmod_mult x (b mod n)); auto with zarith.
+  repeat rewrite Zmod_mod; auto.
+ Qed.
+
+ Theorem Zmod_le: forall a n, 0 < n -> 0 <= a -> (Zmod a n) <= a.
+ Proof.
+  intros a n H1 H2; case (Zle_or_lt n  a); intros H3.
+  case (Z_mod_lt a n); auto with zarith.
+  rewrite Zmod_def_small; auto with zarith.
+ Qed.
+
+ Theorem Zmod_le_first: forall a b, 0 <= a -> 0 < b -> 0 <= a mod b <= a.
+ Proof.
+  intros a b H H1;case (Z_mod_lt a b);auto with zarith;intros H2 H3;split;auto.
+  case (Zle_or_lt b a); intros H4; auto with zarith.
+  rewrite Zmod_def_small; auto with zarith.
+ Qed.
+
+
+(**************************************
+ Properties of Zdivide
+**************************************)
+ 
+ Theorem Zdiv_pos: forall a b, 0 < b -> 0 <= a -> 0 <= a / b.
+ Proof.
+  intros; apply Zge_le; apply Z_div_ge0; auto with zarith.
+ Qed. 
+ Hint Resolve Zdiv_pos: zarith.
+
+ Theorem Zdiv_mult_le:
+   forall a b c, 0 <= a -> 0 < b -> 0 <= c -> c * (a/b) <= (c * a)/ b.
+ Proof.
+  intros a b c H1 H2 H3.
+  case (Z_mod_lt a b); auto with zarith; intros Hu1 Hu2.
+  case (Z_mod_lt c b); auto with zarith; intros Hv1 Hv2.
+  apply Zmult_le_reg_r with b; auto with zarith.
+  rewrite <- Zmult_assoc.
+  replace (a / b * b) with (a - a mod b).
+  replace (c * a / b * b) with (c * a - (c * a) mod b).
+  rewrite Zmult_minus_distr_l.
+  unfold Zminus; apply Zplus_le_compat_l.
+  match goal with |- - ? X <= -?Y => assert (Y <= X); auto with zarith end.
+  apply Zle_trans with ((c mod b) * (a mod b)); auto with zarith.
+  rewrite Zmod_mult; case (Zmod_le_first ((c mod b) * (a mod b)) b); 
+    auto with zarith.
+  apply Zmult_le_compat_r; auto with zarith.
+  case (Zmod_le_first c b); auto.
+  pattern (c * a) at 1; rewrite (Z_div_mod_eq (c * a) b); try ring; 
+    auto with zarith.
+  pattern a at 1; rewrite (Z_div_mod_eq a b); try ring; auto with zarith.
+ Qed.
+
+ Theorem Zdiv_unique:
+   forall n d q r, 0 < d -> ( 0 <= r < d ) -> n = d * q + r ->  q = n / d.
+ Proof.
+  intros n d q r H H0 H1.
+  assert (H2: n = d * (n / d) + n mod d).
+  apply Z_div_mod_eq; auto with zarith.
+  assert (H3:  0 <= n mod d < d ).
+  apply Z_mod_lt; auto with zarith.
+  case (Ztrichotomy q (n / d)); auto.
+  intros H4.
+  absurd (n < n); auto with zarith.
+  pattern n at 1; rewrite H1; rewrite H2.
+  apply Zlt_le_trans with (d * (q + 1)); auto with zarith.
+  rewrite Zmult_plus_distr_r; auto with zarith.
+  apply Zle_trans with (d * (n / d)); auto with zarith.
+  intros tmp; case tmp; auto; intros H4; clear tmp.
+  absurd (n < n); auto with zarith.
+  pattern n at 2; rewrite H1; rewrite H2.
+  apply Zlt_le_trans with (d * (n / d + 1)); auto with zarith.
+  rewrite Zmult_plus_distr_r; auto with zarith.
+  apply Zle_trans with (d * q); auto with zarith.
+ Qed.
+
+ Theorem Zmod_unique:
+   forall n d q r, 0 < d -> ( 0 <= r < d ) -> n = d * q + r ->  r = n mod d.
+ Proof.
+  intros n d q r H H0 H1.
+  assert (H2: n = d * (n / d) + n mod d).
+  apply Z_div_mod_eq; auto with zarith.
+  rewrite (Zdiv_unique n d q r) in H1; auto.
+  apply (Zplus_reg_l (d * (n / d))); auto with zarith.
+ Qed.
+
+ Theorem Zmod_Zmult_compat_l: forall a b c, 
+   0 < b -> 0 < c -> c * a  mod (c * b) = c * (a mod b).
+ Proof.
+  intros a b c H2 H3.
+  pattern a at 1; rewrite (Z_div_mod_eq a b); auto with zarith.
+  rewrite Zplus_comm; rewrite Zmult_plus_distr_r.
+  rewrite Zmult_assoc; rewrite (Zmult_comm (c * b)).
+  rewrite Z_mod_plus; auto with zarith.
+  apply Zmod_def_small; split; auto with zarith.
+  apply Zmult_le_0_compat; auto with zarith.
+  destruct (Z_mod_lt a b);auto with zarith.
+  apply Zmult_lt_compat_l; auto with zarith.
+  destruct (Z_mod_lt a b);auto with zarith.
+ Qed.
+
+ Theorem Zdiv_Zmult_compat_l: 
+   forall a b c, 0 <= a -> 0 < b -> 0 < c -> c * a / (c * b) = a / b.
+ Proof.
+  intros a b c H1 H2 H3; case (Z_mod_lt a b); auto with zarith; intros H4 H5.
+  apply Zdiv_unique with (a mod b); auto with zarith.
+  apply Zmult_reg_l with c; auto with zarith.
+  rewrite Zmult_plus_distr_r; rewrite <- Zmod_Zmult_compat_l; auto with zarith.
+  rewrite Zmult_assoc; apply Z_div_mod_eq; auto with zarith.
+ Qed.
+
+ Theorem Zdiv_0: forall a, 0 < a -> 0 / a = 0.
+ Proof.
+  intros a H;apply sym_equal;apply Zdiv_unique with (r := 0); auto with zarith.
+ Qed.
+
+ Theorem Zdiv_le_upper_bound: 
+   forall a b q, 0 <= a -> 0 < b -> a <= q * b -> a / b <= q.
+ Proof.
+  intros a b q H1 H2 H3.
+  apply Zmult_le_reg_r with b; auto with zarith.
+  apply Zle_trans with (2 := H3).
+  pattern a at 2; rewrite (Z_div_mod_eq a b); auto with zarith.
+  rewrite (Zmult_comm b); case (Z_mod_lt a b); auto with zarith.
+ Qed.
+
+ Theorem Zdiv_lt_upper_bound: 
+   forall a b q, 0 <= a -> 0 < b -> a < q * b -> a / b < q.
+ Proof.
+  intros a b q H1 H2 H3.
+  apply Zmult_lt_reg_r with b; auto with zarith.
+  apply Zle_lt_trans with (2 := H3).
+  pattern a at 2; rewrite (Z_div_mod_eq a b); auto with zarith.
+  rewrite (Zmult_comm b); case (Z_mod_lt a b); auto with zarith.
+ Qed.
+
+ Theorem Zdiv_le_lower_bound: 
+   forall a b q, 0 <= a -> 0 < b -> q * b <= a -> q <= a / b.
+ Proof.
+  intros a b q H1 H2 H3.
+  assert (q < a / b + 1); auto with zarith.
+  apply Zmult_lt_reg_r with b; auto with zarith.
+  apply Zle_lt_trans with (1 := H3).
+  pattern a at 1; rewrite (Z_div_mod_eq a b); auto with zarith.
+  rewrite Zmult_plus_distr_l; rewrite (Zmult_comm b); case (Z_mod_lt a b);
+   auto with zarith.
+ Qed.
+
+ Theorem Zmult_mod_distr_l: 
+   forall a b c, 0 < a -> 0 < c -> (a * b) mod (a * c) = a * (b mod c).
+ Proof.
+  intros a b c H Hc.
+  apply sym_equal; apply Zmod_unique with (b / c); auto with zarith.
+  apply Zmult_lt_0_compat; auto.
+  case (Z_mod_lt b c); auto with zarith; intros; split; auto with zarith.
+  apply Zmult_lt_compat_l; auto.
+  rewrite <- Zmult_assoc; rewrite <- Zmult_plus_distr_r.
+  rewrite <- Z_div_mod_eq; auto with zarith.
+ Qed.
+
+
+ Theorem Zmod_distr: forall a b r t, 0 <= a <= b -> 0 <= r -> 0 <= t < 2 ^a ->
+  (2 ^a * r + t) mod (2 ^ b) = (2 ^a * r) mod (2 ^ b) + t.
+ Proof.
+  intros a b r t (H1, H2) H3 (H4, H5).
+  assert (t < 2 ^ b).
+  apply Zlt_le_trans with (1:= H5); auto with zarith.
+  apply Zpower_le_monotone; auto with zarith.
+  rewrite Zmod_plus; auto with zarith.
+  rewrite Zmod_def_small with (a := t); auto with zarith.
+  apply Zmod_def_small; auto with zarith.
+  split; auto with zarith.
+  assert (0 <= 2 ^a * r); auto with zarith.
+  apply Zplus_le_0_compat; auto with zarith.
+  match goal with |- context [?X mod ?Y] => case (Z_mod_lt X Y) end;
+   auto with zarith.
+  pattern (2 ^ b) at 2; replace (2 ^ b) with ((2 ^ b - 2 ^a) + 2 ^ a);
+    try ring.
+  apply Zplus_le_lt_compat; auto with zarith.
+  replace b with ((b - a) + a); try ring.
+  rewrite Zpower_exp; auto with zarith.
+  pattern (2 ^a) at 4; rewrite <- (Zmult_1_l (2 ^a)); 
+   try rewrite <- Zmult_minus_distr_r.
+  rewrite (Zmult_comm (2 ^(b - a))); rewrite  Zmult_mod_distr_l; 
+   auto with zarith.
+  rewrite (Zmult_comm (2 ^a)); apply Zmult_le_compat_r; auto with zarith.
+  match goal with |- context [?X mod ?Y] => case (Z_mod_lt X Y) end;
+   auto with zarith.
+ Qed.
+
+ Theorem Zmult_mod_distr_r:
+   forall a b c : Z, 0 < a -> 0 < c -> (b * a) mod (c * a) = (b mod c) * a.
+ Proof.
+  intros; repeat rewrite (fun x => (Zmult_comm x a)).
+  apply Zmult_mod_distr_l; auto.
+ Qed.
+
+ Theorem Z_div_plus_l: forall a b c : Z, 0 < b -> (a * b + c) / b = a  + c / b.
+ Proof.
+  intros a b c H; rewrite Zplus_comm; rewrite Z_div_plus;
+   try apply Zplus_comm; auto with zarith. 
+ Qed.
+
+ Theorem Zmod_shift_r:
+   forall a b r t, 0 <= a <= b -> 0 <= r -> 0 <= t < 2 ^a ->
+     (r * 2 ^a + t) mod (2 ^ b) = (r * 2 ^a) mod (2 ^ b) + t.
+ Proof.
+  intros a b r t (H1, H2) H3 (H4, H5).
+  assert (t < 2 ^ b).
+  apply Zlt_le_trans with (1:= H5); auto with zarith.
+  apply Zpower_le_monotone; auto with zarith.
+  rewrite Zmod_plus; auto with zarith.
+  rewrite Zmod_def_small with (a := t); auto with zarith.
+  apply Zmod_def_small; auto with zarith.
+  split; auto with zarith.
+  assert (0 <= 2 ^a * r); auto with zarith.
+  apply Zplus_le_0_compat; auto with zarith.
+  match goal with |- context [?X mod ?Y] => case (Z_mod_lt X Y) end; 
+   auto with zarith.
+  pattern (2 ^ b) at 2;replace (2 ^ b) with ((2 ^ b - 2 ^a) + 2 ^ a); try ring.
+  apply Zplus_le_lt_compat; auto with zarith.
+  replace b with ((b - a) + a); try ring.
+  rewrite Zpower_exp; auto with zarith.
+  pattern (2 ^a) at 4; rewrite <- (Zmult_1_l (2 ^a)); 
+   try rewrite <- Zmult_minus_distr_r.
+  repeat rewrite (fun x => Zmult_comm x (2 ^ a)); rewrite Zmult_mod_distr_l;
+   auto with zarith.
+  apply Zmult_le_compat_l; auto with zarith.
+  match goal with |- context [?X mod ?Y] => case (Z_mod_lt X Y) end; 
+   auto with zarith.
+ Qed.
+
+  Theorem Zdiv_lt_0: forall a b, 0 <= a < b -> a / b = 0.
+  intros a b H; apply sym_equal; apply Zdiv_unique with a; auto with zarith.
+  Qed.
+
+  Theorem Zmod_mult_0: forall a b, 0 < b  -> (a * b) mod b = 0.
+  Proof.
+   intros a b H; rewrite <- (Zplus_0_l (a * b)); rewrite Z_mod_plus;
+    auto with zarith.
+  Qed.
+
+  Theorem Zdiv_shift_r: 
+    forall a b r t, 0 <= a <= b -> 0 <= r -> 0 <= t < 2 ^a ->
+      (r * 2 ^a + t) /  (2 ^ b) = (r * 2 ^a) / (2 ^ b).
+  Proof.
+   intros a b r t (H1, H2) H3 (H4, H5).
+   assert (Eq: t < 2 ^ b); auto with zarith.
+   apply Zlt_le_trans with (1 := H5); auto with zarith.
+   apply Zpower_le_monotone; auto with zarith.
+   pattern (r * 2 ^ a) at 1; rewrite Z_div_mod_eq with (b := 2 ^ b);
+    auto with zarith.
+   rewrite <- Zplus_assoc.
+   rewrite <- Zmod_shift_r; auto with zarith.
+   rewrite (Zmult_comm (2 ^ b)); rewrite Z_div_plus_l; auto with zarith.
+   rewrite (fun x y => @Zdiv_lt_0 (x mod y)); auto with zarith.
+   match goal with |- context [?X mod ?Y] => case (Z_mod_lt X Y) end; 
+    auto with zarith.
+  Qed.
+
+
+  Theorem Zpos_minus: 
+     forall a b, Zpos a < Zpos b -> Zpos (b- a) = Zpos b - Zpos a.
+  Proof.
+   intros a b H.
+   repeat rewrite Zpos_eq_Z_of_nat_o_nat_of_P; autorewrite with pos_morph;
+     auto with zarith.
+   rewrite inj_minus1; auto with zarith.
+   match goal with |- (?X <= ?Y)%nat =>
+    case (le_or_lt X Y); auto; intro tmp; absurd (Z_of_nat X < Z_of_nat Y); 
+        try apply Zle_not_lt; auto with zarith
+    end.
+   repeat rewrite <- Zpos_eq_Z_of_nat_o_nat_of_P; auto with zarith.
+   generalize (Zlt_gt _ _ H); auto.
+ Qed.
+
+  Theorem Zdiv_Zmult_compat_r:
+     forall a b c : Z, 0 <= a -> 0 < b -> 0 < c -> a * c / (b * c) = a / b.
+  Proof.
+   intros a b c H H1 H2; repeat rewrite (fun x => Zmult_comm x c); 
+    apply Zdiv_Zmult_compat_l; auto.
+  Qed.
+
+
+ Lemma shift_unshift_mod : forall n p a,
+     0 <= a < 2^n ->
+     0 < p < n ->
+     a * 2^p = a / 2^(n - p) * 2^n + (a*2^p) mod 2^n.
+ Proof.
+  intros n p a H1 H2.
+  pattern (a*2^p) at 1;replace (a*2^p) with 
+     (a*2^p/2^n * 2^n + a*2^p mod 2^n). 
+  2:symmetry;rewrite (Zmult_comm (a*2^p/2^n));apply Z_div_mod_eq.
+  replace (a * 2 ^ p / 2 ^ n) with (a / 2 ^ (n - p));trivial.
+  replace (2^n) with (2^(n-p)*2^p).
+  symmetry;apply Zdiv_Zmult_compat_r.
+  destruct H1;trivial.
+  apply Zpower_lt_0;auto with zarith.
+  apply Zpower_lt_0;auto with zarith.
+  rewrite <- Zpower_exp.
+  replace (n-p+p) with n;trivial. ring.
+  omega. omega.
+  apply Zlt_gt. apply Zpower_lt_0;auto with zarith.
+ Qed.
+
+ Lemma Zdiv_Zdiv : forall a b c, 0 < b -> 0 < c -> (a/b)/c = a / (b*c).
+ Proof.
+  intros a b c H H0.
+  pattern a at 2;rewrite (Z_div_mod_eq a b);auto with zarith.
+  pattern (a/b) at 2;rewrite (Z_div_mod_eq (a/b) c);auto with zarith.
+  replace (b * (c * (a / b / c) + (a / b) mod c) + a mod b) with
+    ((a / b / c)*(b * c)  + (b * ((a / b) mod c) + a mod b));try ring.
+  rewrite Z_div_plus_l;auto with zarith.
+  rewrite (Zdiv_lt_0 (b * ((a / b) mod c) + a mod b)).
+  ring.
+  split.
+  apply Zplus_le_0_compat;auto with zarith.
+  apply Zmult_le_0_compat;auto with zarith.
+  destruct (Z_mod_lt (a/b) c);auto with zarith.
+  destruct (Z_mod_lt a b);auto with zarith.
+  apply Zle_lt_trans with (b * ((a / b) mod c) + (b-1)).
+  destruct (Z_mod_lt a b);auto with zarith.
+  apply Zle_lt_trans with (b * (c-1) + (b - 1)).
+  apply Zplus_le_compat;auto with zarith.
+  destruct (Z_mod_lt (a/b) c);auto with zarith.
+  replace (b * (c - 1) + (b - 1)) with (b*c-1);try ring;auto with zarith.
+  apply Zmult_lt_0_compat;auto with zarith.
+ Qed.
+
+ Lemma div_le_0 : forall p x, 0 <= x -> 0 <= x / 2 ^ p.
+ Proof.
+  intros p x Hle;destruct (Z_le_gt_dec 0 p).
+  apply  Zdiv_le_lower_bound;auto with zarith. 
+  replace (2^p) with 0.
+  destruct x;compute;intro;discriminate.
+  destruct p;trivial;discriminate z.
+ Qed.
+ 
+ Lemma div_lt : forall p x y, 0 <= x < y -> x / 2^p < y.
+ Proof.
+  intros p x y H;destruct (Z_le_gt_dec 0 p).
+  apply Zdiv_lt_upper_bound;auto with zarith. 
+  apply Zlt_le_trans with y;auto with zarith.
+  rewrite <- (Zmult_1_r y);apply Zmult_le_compat;auto with zarith.
+  assert (0 < 2^p);auto with zarith.
+  replace (2^p) with 0.
+  destruct x;change (0<y);auto with zarith.
+  destruct p;trivial;discriminate z.
+ Qed.
+