proposition: Theorem new_location_even_correct : Z.even nb_steps = true -> forall x k l, (0 <= k < nb_steps)%Z -> inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x l -> inbetween start (start + IZR nb_steps * step) x (new_location_even k l).
proof: Proof. intros He x k l Hk Hx. unfold new_location_even. destruct (Zeq_bool_spec k 0) as [Hk0|Hk0]. rewrite Hk0 in Hx. rewrite Rmult_0_l, Rplus_0_r, Rmult_1_l in Hx. set (l' := match l with loc_Exact => l | _ => loc_Inexact Lt end). assert ((l = loc_Exact /\ l' = loc_Exact) \/ (l <> loc_Exact /\ l' = loc_Inexact Lt)). unfold l' ; case l ; try (now left) ; right ; now split. destruct H as [(H1,H2)|(H1,H2)] ; rewrite H2. constructor. rewrite H1 in Hx. now inversion_clear Hx. now apply inbetween_step_Lo_not_Eq with (2 := H1). destruct (Zcompare_spec (2 * k) nb_steps) as [Hk1|Hk1|Hk1]. apply inbetween_step_Lo with (1 := Hx). lia. destruct (Zeven_ex nb_steps). rewrite He in H. lia. set (l' := match l with loc_Exact => Eq | _ => Gt end). assert ((l = loc_Exact /\ l' = Eq) \/ (l <> loc_Exact /\ l' = Gt)). unfold l' ; case l ; try (now left) ; right ; now split. destruct H as [(H1,H2)|(H1,H2)] ; rewrite H2. rewrite H1 in Hx. now apply inbetween_step_Mi_Mi_even with (1 := Hx). now apply inbetween_step_Hi_Mi_even with (1 := Hx). apply inbetween_step_Hi with (1 := Hx). exact Hk1. apply Hk. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Float_prop