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|z] k _ Ezx; try discriminate. unfold MtoP. unfold EtoZ in Ezx; rewrite Ezx; simpl Z.to_pos; clear z Ezx. case (Pos.succ_pred_or x); intro Hx. rewrite Hx. now destruct y; destruct k. 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; simpl Z.to_pos. replace (mantissa_shrp_aux y x) with (mantissa_shrp_aux (xO y) (Pos.succ x)); last first. simpl. now rewrite Pos.pred_succ; destruct x. rewrite mantissa_shrp_aux_correct. 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. rewrite Pos.compare_xO_xO; try easy. 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. Qed.
imports: Coq(ZArith Reals Psatz Bool) Flocq(Zaux Raux) Basic Generic Generic_proof Specific_sig