Cyclic31: proofs for addmuldiv31, tail031 and head031. Only two Admitted left !

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

1 files changed, 291 insertions, 24 deletions

diff --git a/theories/Numbers/Cyclic/Int31/Cyclic31.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v
index e5975efa4..c1e444fb7 100644
--- a/theories/Numbers/Cyclic/Int31/Cyclic31.v
+++ b/theories/Numbers/Cyclic/Int31/Cyclic31.v
@@ -156,6 +156,12 @@ Section Basics.
  Proof.
  destruct x; simpl; auto.
  Qed.
+
+ Lemma firstl_firstr : 
+  forall x, firstl x = firstr (nshiftr (pred size) x).
+ Proof.
+ destruct x; simpl; auto.
+ Qed.
  
  (** More advanced results about [nshiftr] *)
 
@@ -462,6 +468,42 @@ Section Basics.
  apply phibis_aux_bounded; auto.
  Qed.
 
+ Lemma phibis_aux_lowerbound : 
+  forall n x, firstr (nshiftr n x) = D1 -> 
+  (2 ^ Z_of_nat n <= phibis_aux (S n) x)%Z.
+ Proof.
+ induction n.
+ intros.
+ unfold nshiftr in H; simpl in *.
+ unfold phibis_aux, recrbis_aux.
+ rewrite H, Zdouble_plus_one_mult; omega.
+
+ intros.
+ remember (S n) as m.
+ unfold phibis_aux, recrbis_aux; fold recrbis_aux; 
+  fold (phibis_aux m (shiftr x)).
+ subst m.
+ rewrite inj_S, Zpower_Zsucc; auto with zarith.
+ assert (2^(Z_of_nat n) <= phibis_aux (S n) (shiftr x))%Z.
+  apply IHn.
+  rewrite <- nshiftr_S_tail; auto.
+ destruct (firstr x).
+ change (Zdouble (phibis_aux (S n) (shiftr x))) with 
+        (2*(phibis_aux (S n) (shiftr x)))%Z.
+ omega.
+ rewrite Zdouble_plus_one_mult; omega.
+ Qed.
+
+ Lemma phi_lowerbound : 
+  forall x, firstl x = D1 -> (2^(Z_of_nat (pred size)) <= phi x)%Z.
+ Proof.
+ intros.
+ generalize (phibis_aux_lowerbound (pred size) x).
+ rewrite <- firstl_firstr.
+ change (S (pred size)) with size; auto.
+ rewrite phibis_aux_equiv; auto.
+ Qed.
+
  (** * Equivalence modulo [2^n] *)
 
  Section EqShiftL.
@@ -1539,17 +1581,33 @@ Section Int31_Spec.
  change (Zabs_nat 1) with 1%nat; omega.
  Qed.
 
- Lemma spec_add_mul_div : forall x y p,
-       [|p|] <= Zpos 31 ->
-       [| addmuldiv31 p x y |] =
-         ([|x|] * (2 ^ [|p|]) +
-          [|y|] / (2 ^ ((Zpos 31) - [|p|]))) mod wB.
- Proof.
- Admitted. (* TODO !! *)
+ Fixpoint addmuldiv31_alt n i j := 
+  match n with 
+    | O => i 
+    | S n => addmuldiv31_alt n (sneakl (firstl j) i) (shiftl j)
+  end.
 
-(* (* don't work yet (not enough information in IHn) *)
+ Lemma addmuldiv31_equiv : forall p x y, 
+  addmuldiv31 p x y = addmuldiv31_alt (Zabs_nat [|p|]) x y.
+ Proof.
+ intros.
  unfold addmuldiv31.
- intros; rewrite iter_int31_iter_nat.
+ rewrite iter_int31_iter_nat.
+ set (n:=Zabs_nat [|p|]); clearbody n; clear p.
+ revert x y; induction n.
+ simpl; auto.
+ intros.
+ simpl addmuldiv31_alt.
+ replace (S n) with (n+1)%nat by (rewrite plus_comm; auto).
+ rewrite iter_nat_plus; simpl; auto.
+ Qed.
+
+ Lemma spec_add_mul_div : forall x y p, [|p|] <= Zpos 31 ->
+   [| addmuldiv31 p x y |] = 
+   ([|x|] * (2 ^ [|p|]) + [|y|] / (2 ^ ((Zpos 31) - [|p|]))) mod wB.
+ Proof.
+ intros.
+ rewrite addmuldiv31_equiv.
  assert ([|p|] = Z_of_nat (Zabs_nat [|p|])).
   rewrite inj_Zabs_nat; symmetry; apply Zabs_eq.
   destruct (phi_bounded p); auto.
@@ -1557,29 +1615,54 @@ Section Int31_Spec.
  set (n := Zabs_nat [|p|]) in *; clearbody n.
  assert (n <= 31)%nat.
   rewrite inj_le_iff; auto with zarith.
- clear H.
+ clear p H; revert x y.
 
  induction n.
- simpl.
+ simpl; intros.
  change (Zpower_pos 2 31) with (2^31).
  rewrite Zmult_1_r.
  replace ([|y|] / 2^31) with 0.
  rewrite Zplus_0_r.
  symmetry; apply Zmod_small; apply phi_bounded.
  symmetry; apply Zdiv_small; apply phi_bounded.
+
+ simpl addmuldiv31_alt; intros.
+ rewrite IHn; [ | omega ].
+ case_eq (firstl y); intros.
+
+ rewrite phi_twice, Zdouble_mult.
+ rewrite phi_twice_firstl; auto.
+ change (Zdouble [|y|]) with (2*[|y|]).
+ rewrite inj_S, Zpower_Zsucc; auto with zarith.
+ rewrite Zplus_mod; rewrite Zmult_mod_idemp_l; rewrite <- Zplus_mod.
+ f_equal.
+ apply Zplus_eq_compat.
+ ring.
+ replace (31-Z_of_nat n) with (Zsucc(31-Zsucc(Z_of_nat n))) by ring.
+ rewrite Zpower_Zsucc, <- Zdiv_Zdiv; auto with zarith.
+ rewrite Zmult_comm, Z_div_mult; auto with zarith.
  
- simpl iter_nat.
- destruct (iter_nat n (int31 * int31)
-                (fun ij : int31 * int31 =>
-                 let (i, j) := ij in (sneakl (firstl j) i, shiftl j)) 
-                (x, y)).
- case_eq (firstl i0); intros; rewrite ?phi_twice,?phi_twice_plus_one; 
-  rewrite ?Zdouble_mult, ?Zdouble_plus_one_mult; 
-  rewrite IHn; try omega.
+ rewrite phi_twice_plus_one, Zdouble_plus_one_mult.
+ rewrite phi_twice; auto.
+ change (Zdouble [|y|]) with (2*[|y|]).
  rewrite inj_S, Zpower_Zsucc; auto with zarith.
- rewrite Zmult_mod_idemp_r, Zmult_plus_distr_r.
-
-*)
+ rewrite Zplus_mod; rewrite Zmult_mod_idemp_l; rewrite <- Zplus_mod.
+ rewrite Zmult_plus_distr_l, Zmult_1_l, <- Zplus_assoc.
+ f_equal.
+ apply Zplus_eq_compat.
+ ring.
+ assert ((2*[|y|]) mod wB = 2*[|y|] - wB).
+  admit.
+ rewrite H1.
+ replace wB with (2^(Z_of_nat n)*2^(31-Z_of_nat n)) by  
+  (rewrite <- Zpower_exp; auto with zarith; f_equal; unfold size; ring).
+ unfold Zminus; rewrite Zopp_mult_distr_l.
+ rewrite Z_div_plus; auto with zarith.
+ ring_simplify.
+ replace (31+-Z_of_nat n) with (Zsucc(31-Zsucc(Z_of_nat n))) by ring.
+ rewrite Zpower_Zsucc, <- Zdiv_Zdiv; auto with zarith.
+ rewrite Zmult_comm, Z_div_mult; auto with zarith.
+ Qed.
 
  Let w_pos_mod     := int31_op.(znz_pos_mod).
 
@@ -1627,9 +1710,106 @@ Section Int31_Spec.
   intros H'; rewrite <- H'.
   simpl; auto.
  Qed.
+
+ Fixpoint head031_alt n x := 
+  match n with 
+    | O => 0%nat
+    | S n => match firstl x with 
+               | D0 => S (head031_alt n (shiftl x))
+               | D1 => 0%nat
+             end
+  end.
+
+ Lemma head031_equiv : 
+   forall x, [|head031 x|] = Z_of_nat (head031_alt size x).
+ Proof.
+ intros.
+ case_eq (iszero x); intros.
+ rewrite (iszero_eq0 _ H).
+ simpl; auto.
+
+ unfold head031, recl.
+ change On with (phi_inv (Z_of_nat (31-size))).
+ replace (head031_alt size x) with 
+   (head031_alt size x + (31 - size))%nat by (apply plus_0_r; auto).
+ assert (size <= 31)%nat by auto with arith.
+ 
+ revert x H; induction size; intros.
+ simpl; auto.
+ unfold recl_aux; fold recl_aux.
+ unfold head031_alt; fold head031_alt.
+ rewrite H.
+ assert ([|phi_inv (Z_of_nat (31-S n))|] = Z_of_nat (31 - S n)).
+  rewrite phi_phi_inv.
+  apply Zmod_small.
+  split.
+  change 0 with (Z_of_nat O); apply inj_le; omega.
+  apply Zle_lt_trans with (Z_of_nat 31).
+  apply inj_le; omega.
+  compute; auto.
+ case_eq (firstl x); intros; auto.
+ rewrite plus_Sn_m, plus_n_Sm.
+ replace (S (31 - S n)) with (31 - n)%nat by omega.
+ rewrite <- IHn; [ | omega | ].
+ f_equal; f_equal.
+ unfold add31.
+ rewrite H1.
+ f_equal.
+ change [|In|] with 1.
+ replace (31-n)%nat with (S (31 - S n))%nat by omega.
+ rewrite inj_S; ring.
+ 
+ clear - H H2.
+ rewrite (sneakr_shiftl x) in H.
+ rewrite H2 in H.
+ case_eq (iszero (shiftl x)); intros; auto.
+ rewrite (iszero_eq0 _ H0) in H; discriminate.
+ Qed.
+
+ Lemma phi_nz : forall x, 0 < [|x|] <-> x <> 0%int31.
+ Proof.
+ split; intros.
+ red; intro; subst x; discriminate.
+ assert ([|x|]<>0%Z).
+ contradict H.
+ rewrite <- (phi_inv_phi x); rewrite H; auto.
+ generalize (phi_bounded x); auto with zarith.
+ Qed.
+
  Lemma spec_head0  : forall x,  0 < [|x|] ->
 	 wB/ 2 <= 2 ^ ([|head031 x|]) * [|x|] < wB.
- Admitted. (* TODO !! *)
+ Proof.
+ intros.
+ rewrite head031_equiv.
+ assert (nshiftl size x = 0%int31).
+  apply nshiftl_size.
+ revert x H H0.
+ unfold size at 2 5.
+ induction size.
+ simpl Z_of_nat.
+ intros.
+ compute in H0; rewrite H0 in H; discriminate.
+
+ intros.
+ simpl head031_alt.
+ case_eq (firstl x); intros.
+ rewrite (inj_S (head031_alt n (shiftl x))), Zpower_Zsucc; auto with zarith.
+ rewrite <- Zmult_assoc, Zmult_comm, <- Zmult_assoc, <-(Zmult_comm 2).
+ rewrite <- Zdouble_mult, <- (phi_twice_firstl _ H1).
+ apply IHn.
+
+ rewrite phi_nz; rewrite phi_nz in H; contradict H.
+ change twice with shiftl in H.
+ rewrite (sneakr_shiftl x), H1, H; auto.
+
+ rewrite <- nshiftl_S_tail; auto.
+ 
+ change (2^(Z_of_nat 0)) with 1; rewrite Zmult_1_l.
+ generalize (phi_bounded x); unfold size; split; auto with zarith.
+ change (2^(Z_of_nat 31)/2) with (2^(Z_of_nat (pred size))).
+ apply phi_lowerbound; auto.
+ Qed.
+
  Lemma spec_tail00:  forall x, [|x|] = 0 -> [|tail031 x|] = Zpos 31.
  Proof.
   intros.
@@ -1638,9 +1818,96 @@ Section Int31_Spec.
   intros H'; rewrite <- H'.
   simpl; auto.
  Qed.
+
+ Fixpoint tail031_alt n x := 
+  match n with 
+    | O => 0%nat
+    | S n => match firstr x with 
+               | D0 => S (tail031_alt n (shiftr x))
+               | D1 => 0%nat
+             end
+  end.
+
+ Lemma tail031_equiv : 
+   forall x, [|tail031 x|] = Z_of_nat (tail031_alt size x).
+ Proof.
+ intros.
+ case_eq (iszero x); intros.
+ rewrite (iszero_eq0 _ H).
+ simpl; auto.
+
+ unfold tail031, recr.
+ change On with (phi_inv (Z_of_nat (31-size))).
+ replace (tail031_alt size x) with 
+   (tail031_alt size x + (31 - size))%nat by (apply plus_0_r; auto).
+ assert (size <= 31)%nat by auto with arith.
+ 
+ revert x H; induction size; intros.
+ simpl; auto.
+ unfold recr_aux; fold recr_aux.
+ unfold tail031_alt; fold tail031_alt.
+ rewrite H.
+ assert ([|phi_inv (Z_of_nat (31-S n))|] = Z_of_nat (31 - S n)).
+  rewrite phi_phi_inv.
+  apply Zmod_small.
+  split.
+  change 0 with (Z_of_nat O); apply inj_le; omega.
+  apply Zle_lt_trans with (Z_of_nat 31).
+  apply inj_le; omega.
+  compute; auto.
+ case_eq (firstr x); intros; auto.
+ rewrite plus_Sn_m, plus_n_Sm.
+ replace (S (31 - S n)) with (31 - n)%nat by omega.
+ rewrite <- IHn; [ | omega | ].
+ f_equal; f_equal.
+ unfold add31.
+ rewrite H1.
+ f_equal.
+ change [|In|] with 1.
+ replace (31-n)%nat with (S (31 - S n))%nat by omega.
+ rewrite inj_S; ring.
+ 
+ clear - H H2.
+ rewrite (sneakl_shiftr x) in H.
+ rewrite H2 in H.
+ case_eq (iszero (shiftr x)); intros; auto.
+ rewrite (iszero_eq0 _ H0) in H; discriminate.
+ Qed.
+
  Lemma spec_tail0  : forall x, 0 < [|x|] -> 
          exists y, 0 <= y /\ [|x|] = (2 * y + 1) * (2 ^ [|tail031 x|]).
- Admitted. (* TODO !! *)
+ Proof.
+ intros.
+ rewrite tail031_equiv.
+ assert (nshiftr size x = 0%int31).
+  apply nshiftr_size.
+ revert x H H0.
+ induction size.
+ simpl Z_of_nat.
+ intros.
+ compute in H0; rewrite H0 in H; discriminate.
+
+ intros.
+ simpl tail031_alt.
+ case_eq (firstr x); intros.
+ rewrite (inj_S (tail031_alt n (shiftr x))), Zpower_Zsucc; auto with zarith.
+ destruct (IHn (shiftr x)) as {y,Hy1,Hy2}.
+ 
+ rewrite phi_nz; rewrite phi_nz in H; contradict H.
+ rewrite (sneakl_shiftr x), H1, H; auto.
+
+ rewrite <- nshiftr_S_tail; auto.
+ 
+ exists y; split; auto.
+ rewrite phi_eqn1; auto.
+ rewrite Zdouble_mult, Hy2; ring.
+ 
+ exists [|shiftr x|].
+ split.
+ generalize (phi_bounded (shiftr x)); auto with zarith.
+ rewrite phi_eqn2; auto.
+ rewrite Zdouble_plus_one_mult; simpl; ring.
+ Qed.
     
  (* Sqrt *)