Section Arithmetic.

(* Dichotomic research on array of [Z]. *)

Check Z.
Check Zdiv.

Variable Array : Type -> Z -> Type.
Variable Array_read : forall A n, Array A n -> Z -> maybe A.
Hypothesis Array_read_ok : forall A n m (a : Array A n),
  m < n -> is_defined _ (Array_read _ _ a m) = true.

Check Array_read_ok.


Inductive state : Type :=
  | state_cons : forall n,
    Z (* goal *) -> Array Z n -> Z (* min *) -> Z (* max *) -> state.


Definition is_final (s : state) : Prop :=
  match s with
  | state_cons _ _ a min max =>
    (* ... *)
  end.

Definition next (s : state) : maybe state :=
  match s with
  | state_cons _ goal a min max =>
    (* ... *)
  end.


Lemma always_in_bounds : forall n goal (a : Array Z n) min max s,
  min < n -> max < n ->
  s = state_cons _ goal a min max ->
  ~ is_final s ->
  exists min' max',
  min' < n /\ max' < n /\
  next s =
    defined _ (state_cons _ goal a min' max').
Proof.
    (* ... *)
Qed.

Print always_in_bounds.

End Arithmetic.