proposition: Theorem int63it_naive a l1 l2 c : int63it _ next l1 l2 a c = naive_int63it l1 l2 a c.
proof: Proof. revert a l1 l2 c. assert (F: forall m p c c1 l1 l2 a, (Z_of_nat m + Zpos p = 63)%Z -> to_Z c1 = to_Z (shiftr63 c (p2t63 p)) -> int63it_aux _ next (S m) p c1 l1 l2 a = naive_int63it_aux m p c l1 l2 a). - intros m; elim m; clear m; auto. + intros p c c1 l1 l2 a H1 H2. unfold int63it_aux, naive_int63it_aux, int63i. assert (F0: (0 < Zpos p)%Z); try (red; auto; fail). unfold Z_of_nat in H1. match goal with |- context[compare ?X ?Y] => set (u := X ?= Y) end. match goal with |- context[compare ?X ?Y] => set (v := compare X Y); replace v with u end. now case u; auto. unfold u; unfold v; apply phi_compare63_compat; auto. repeat rewrite phi_shiftl63; rewrite ?phi1; auto with zarith. * apply f_equal2 with (f := Z.mul); auto. rewrite 2!phi_shiftr63; rewrite ?phi1; auto with zarith. now apply f_equal2 with (f := Z.div); auto. * rewrite phi_shiftr63; rewrite phi1; auto with zarith. change (2^63)%Z with (2^62 * 2 ^1)%Z. apply Zmult_lt_compat_r; auto with zarith. apply Z.div_lt_upper_bound; auto with zarith. change (2 ^ 1 * 2 ^ 62)%Z with (2 ^ 63)%Z. now rewrite <- H2; case (phi_toZ c1); auto. * change (2^63)%Z with (2^62 * 2 ^1)%Z. apply Zmult_lt_compat_r; auto with zarith. rewrite phi_shiftr63; rewrite phi1; auto with zarith. apply Z.div_lt_upper_bound; auto with zarith. change (2 ^ 1 * 2 ^ 62)%Z with (2 ^ 63)%Z. now case (phi_toZ c1); auto. + intros m Hrec p c c1 l1 l2 a H1 H2. assert (Hk: exists k, k = S m); try exists (S m); auto. case Hk; clear Hk; intros k Hk; rewrite <- Hk. simpl int63it_aux; rewrite Hk. rewrite naive_auxS. assert (F0: (0 < Zpos p)%Z); try (red; auto; fail). rewrite inj_S in H1; unfold int63i. assert (HH : to_Z (shiftr63 c1 1) = to_Z (shiftr63 c (p2t63 (Pos.succ p)))). * rewrite phi_shiftr63, H2, !phi_shiftr63; rewrite ?phi_p2t63; rewrite ?Zpos_succ_morphism; rewrite ?phi1; auto with zarith. rewrite Zdiv_Zdiv; auto with zarith. rewrite <- Zpower_exp; auto with zarith. apply f_equal2 with (f := Z.div); auto. now apply f_equal2 with (f := Zpower); auto with zarith. * match goal with |- context[compare ?X ?Y] => set (u := X ?= Y) end. match goal with |- context[compare ?X ?Y] => set (v := compare X Y); replace v with u end. now case u; apply Hrec; auto; rewrite Zpos_succ_morphism; auto with zarith. unfold u; unfold v; apply phi_compare63_compat; auto. repeat rewrite phi_shiftl63; rewrite phi1; auto with zarith. -- apply f_equal2 with (f := Z.mul); auto. rewrite HH, !phi_shiftr63. ++ rewrite Zdiv_Zdiv; auto with zarith. rewrite <- Zpower_exp; auto with zarith. ** apply f_equal2 with (f := Z.div); auto. rewrite !phi_p2t63; rewrite ?phi1, ?Zpos_succ_morphism; auto with zarith. apply f_equal2 with (f := Zpower); auto with zarith. ** now generalize (phi_nonneg (p2t63 p)); auto with zarith. ** now rewrite phi1. ++ now rewrite phi_p2t63; auto with zarith. ++ now rewrite phi1. ++ rewrite phi_p2t63, Zpos_succ_morphism. now rewrite <- H1; auto with zarith. now rewrite Zpos_succ_morphism; auto with zarith. -- change (2^63)%Z with (2^62 * 2 ^1)%Z. apply Zmult_lt_compat_r; auto with zarith. rewrite phi_shiftr63; rewrite phi1; auto with zarith. apply Z.div_lt_upper_bound; auto with zarith. change (2 ^ 1 * 2 ^ 62)%Z with (2 ^ 63)%Z. now case (phi_toZ (shiftr63 c (p2t63 p))); auto. -- change (2^63)%Z with (2^62 * 2 ^1)%Z. apply Zmult_lt_compat_r; auto with zarith. rewrite phi_shiftr63; rewrite phi1; auto with zarith. apply Z.div_lt_upper_bound; auto with zarith. change (2 ^ 1 * 2 ^ 62)%Z with (2 ^ 63)%Z. now case (phi_toZ c1); auto. - intros; apply F; auto with zarith. rewrite phi_shiftr63; auto with zarith. Qed.
imports: PrimInt63 Cyclic63 List BasicRubik