proposition: Lemma float_array_max_partial_correct : forall a, finite_array a = true -> forall i, (Uint63.to_Z i <= Uint63.to_Z (PArray.length a))%Z -> let f := float_array_max_partial a (Uint63.to_Z i) in ((0 < Uint63.to_Z i)%Z -> is_finite (Prim2B f) = true) /\ forall j, (0 <= Uint63.to_Z j < Uint63.to_Z i)%Z -> PrimFloat.leb a.[j] f = true.
proof: Proof. intros a fina_a i bnd_i. generalize (Uint63.to_Z_bounded i). intros Hi. destruct (Uint63.to_Z i); [split; lia | | lia]. unfold float_array_max_partial. simpl. set (P := fun p '(n, x) => (Z.pos p <= Uint63.to_Z (PArray.length a))%Z -> n = Z.pos p /\ is_finite (Prim2B x) = true /\ forall j, (0 <= Uint63.to_Z j < n)%Z -> PrimFloat.leb a.[j] x = true). set (f := fun '(n, x) => (Z.succ n, float_max x a.[of_Z n])). assert (non_empty_a : (0 < Uint63.to_Z (PArray.length a))%Z) by lia. revert bnd_i. cut (forall p', P p' (Pos.iter f (0%Z, neg_infinity) p')). 2: { apply Pos.iter_ind. { unfold P, f, float_max. simpl. intros _. split; [easy |]. rewrite ltb_spec. cbn -[Uint63.to_Z]. unfold SFltb, SFcompare. generalize (finite_array_correct a fina_a 0 non_empty_a). intros fin_a_0. generalize fin_a_0. rewrite <-is_finite_SF_B2SF, B2SF_Prim2B. split; [now destruct Prim2SF; [| destruct s | |] |]. intros j bnd_j. rewrite <-(Uint63.of_to_Z j). replace (Uint63.to_Z j) with 0%Z by lia. assert (a_0_leb_self : PrimFloat.leb a.[0] a.[0] = true). { now rewrite leb_equiv, Bleb_correct, Rle_bool_true; [| apply Rle_refl | ..]. } revert fin_a_1. now destruct Prim2SF; [| destruct s | |]; clear -a_0_leb_self. } intros p' [n x]. unfold P, f, float_max. simpl. intros IHp' bnd_p'. rewrite Pos2Z.inj_succ in bnd_p' |- *. split; [lia |]. destruct IHp' as [eq_n [fin_x a_j_le_x']]; [lia |]. rewrite ltb_equiv. assert (fin_a_n : is_finite (Prim2B a.[of_Z n]) = true). { apply finite_array_correct; [easy |]. generalize (Uint63.to_Z_bounded (PArray.length a)). intros Haux. rewrite Uint63.of_Z_spec, Z.mod_small; lia. } split. { now rewrite (Bltb_correct prec emax (Prim2B x) (Prim2B a.[of_Z n])); [destruct Rlt_bool | |]. } intros j [bnd_j_0 bnd_j_1]. apply Z.lt_succ_r, Zle_lt_or_eq in bnd_j_1. destruct bnd_j_1 as [bnd_j_1 | bnd_j_1]. - rewrite Bltb_correct by easy. assert (fin_a_j : is_finite (Prim2B a.[j]) = true) by (now apply finite_array_correct; [| lia]). assert (a_j_le_x : (a.[j] <=? x)%float = true) by (now apply a_j_le_x'; split). clear a_j_le_x'. case Rlt_bool_spec; intros comp_x; [| apply a_j_le_x]. rewrite leb_equiv, Bleb_correct in a_j_le_x |- * by easy. apply Rle_bool_true. destruct (Rle_or_lt (B2R (Prim2B a.[j])) (B2R (Prim2B x))) as [Haux | Haux]; [lra |]. apply Rle_bool_false in Haux. rewrite a_j_le_x in Haux. lia. - rewrite <-(Uint63.of_to_Z j), bnd_j_1. rewrite Bltb_correct by easy. case Rlt_bool_spec; intros comp_x; rewrite leb_equiv, Bleb_correct by easy; apply Rle_bool_true; [apply Rle_refl | easy]. } intros Haux. destruct Uint63.to_Z as [| p' |] eqn:Hlen; [lia | | lia]. clear non_empty_a. intros comp_p_p'. generalize Haux. intros Haux'. specialize (Haux p). specialize (Haux' p'). unfold P in Haux. revert Haux. destruct (Pos.iter _ _ p) as [p'' x] eqn:H. simpl. intros H'. apply H' in comp_p_p'. destruct comp_p_p' as [-> [fin_x prop_x]]. now split. Qed.
imports: Coq(PrimInt63 Sint63 Floats PArray) Coq(Bool List Reals Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations)