proposition: Lemma finite_array_correct : forall a, finite_array a = true -> forall i, (Uint63.to_Z i < Uint63.to_Z (PArray.length a))%Z -> is_finite (Prim2B a.[i]) = true.
proof: Proof. intros a fina_a i bnd_i. unfold finite_array in fina_a. set (P := fun n '(i, b) => (Z.of_N n <= Uint63.to_Z (PArray.length a))%Z -> b = true -> i = Z.of_N n /\ forall j, (0 <= j < Z.of_N n)%Z -> is_finite (Prim2B a.[of_Z j]) = true). set (f := fun '(i, b) => (Z.succ i, b && is_finite_SF (Prim2SF a.[of_Z i]))). cut (forall n, P n (N.iter n f (0%Z, true))). 2: { apply N.iter_ind; [intros _ _; split; [easy | lia] |]. intros n [i' b]. simpl. intros IHn H1 H2. destruct IHn as [IHn_1 IHn_2]; [lia | now apply andb_prop in H2 |]. split; [lia |]. intros j Hj'. rewrite IHn_1 in H2. rewrite <-B2SF_Prim2B, is_finite_SF_B2SF in H2. assert (Hj : (0 <= j < Z.of_N n)%Z \/ j = Z.of_N n) by lia. clear Hj'. now destruct Hj as [Hj | ->]; [now apply IHn_2 | now apply andb_prop in H2]. } intros Haux. specialize (Haux (Z.to_N (Uint63.to_Z (PArray.length a)))). unfold P in Haux. revert fina_a Haux. destruct N.iter as [i' b]. simpl. intros -> He. rewrite <-(Uint63.of_to_Z i). generalize (Uint63.to_Z_bounded (PArray.length a)). intros Hy. apply He; [lia | easy |]. generalize (Uint63.to_Z_bounded i). lia. Qed.
imports: Coq(PrimInt63 Sint63 Floats PArray) Coq(Bool List Reals Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations)