proposition: Lemma mantissa_shrp_correct : forall x y z k, valid_mantissa y -> EtoZ z = Zpos x -> (Zpower radix (Zpos x - 1) <= Zpos (MtoP y) < Zpos (shift radix 1 x))%Z -> let l := mantissa_shrp y z k in l = adjust_pos (Zpos (MtoP y)) (shift radix 1 x) k.
proof: Proof. intros x y z k [v Hv] Ezx. unfold mantissa_shrp. case (Pos.succ_pred_or x); intro Hx. rewrite Hx. intros Hl; simpl in Hl. assert (MtoP y = 1%positive) by lia. rewrite H. unfold MtoP in H; rewrite Hv in H. destruct k; simpl; try easy. unfold EtoZ in Ezx. case BigN.compare_spec; try easy; intro H1; red in H1; rewrite !BigN.spec_shiftl, spec_to_Z, Ezx in H1; simpl Z.sgn in H1; rewrite Hx, Hv,H in H1; cbv in H1; inversion H1. rewrite <- Hx at 1. rewrite Pos2Z.inj_succ. replace (Z.succ (Z.pos (Pos.pred x)) - 1)%Z with (Z.pos (Pos.pred x)) by lia. intros [Hl _]. unfold mantissa_shrp. replace (shift radix 1 x) with (xO ((Z.to_pos radix) ^ (Pos.pred x))); last first. apply Pos2Z.inj. rewrite <- (Pos.mul_1_r (_ ^ _)), <- (Pos.mul_xO_r _ xH). rewrite Pos.mul_comm, <- Pos.pow_succ_r, Hx, shift_correct. rewrite !Z.pow_pos_fold, Pos2Z.inj_pow, radix_to_pos; lia. simpl. replace (BigN.shiftl y 1 ?= BigN.shiftl 1 (BigZ.to_N z))%bigN with (MtoP y ?= 2 ^ Pos.pred x)%positive. revert Hl. rewrite <-Z.pow_pos_fold, <- radix_to_pos, <- Pos2Z.inj_pow_pos. simpl. case Pos.compare_spec; try easy. intro H; lia. now destruct k. rewrite BigN.spec_compare, !BigN.spec_shiftl. rewrite Z.shiftl_1_l. unfold EtoZ in Ezx. rewrite spec_to_Z, Ezx. unfold MtoP; rewrite Hv. rewrite Z.mul_1_l. rewrite <- Hx at 2. rewrite Pos2Z.inj_succ. rewrite Z.pow_succ_r, Z.mul_comm; try lia. replace (Z.shiftl (Z.pos v) (BigN.to_Z 1)) with (Zpos v * 2)%Z by (cbn; lia). rewrite <- Pos2Z.inj_pow; try easy. now rewrite <- Zmult_compare_compat_r. Qed.
imports: Coq(Bool ZArith Reals Psatz) Bignums(BigN BigZ) Flocq(Zaux Raux Digits) Basic Generic Generic_proof Specific_sig