(* AUTEURS / AUTHORS :                          *)
(* Judicaël Courant,   Jean-François Monin      *)
(* VERIMAG, Université Joseph Fourier, Grenoble *)
(*                                         2006 *)

Require Import MoreZArith.
Require Import Words.
Require Import GenericTactics.

Open Local Scope Z_scope.

Definition continuous f := forall u x,
  {f (u::x) - f u = 1 }+{ f (u::x) = f u }+{ f (u::x) - f u = -1}.

Lemma continuous_gt_ge :
  forall f u x z, continuous f -> f (u :: x) > z -> f u >= z.
intros f u x z Hc.
generalize (Hc u x).
splitsolve0 (0%nat). (* NOTE : limitation de omega : marche pas avec les hypothèses dans Set *)
Qed.

Inductive step_up (f : word -> Z) (z : Z) : word -> Set :=
| Cstep_up : forall u x v,
  f u = z -> f (u :: x) = z + 1 -> step_up f z (u @ [x] @ v).

Lemma step_up_snoc : forall f u x z, step_up f z u -> step_up f z (u::x).
induction 1 as [ u x0 v H H0 ].
change (step_up f z (u @ [x0] @ (v :: x))).
constructor;trivial.
Qed.

Lemma step_up_snocEps : forall f u x z, f u = z -> f (u::x) = z+1 -> 
  step_up f z (u::x).
intros; change (step_up f z (u @ [x] @ Eps)).
constructor;trivial.
Qed.

Lemma step_up_charact : forall f u x z,
  step_up f z u + { f u = z /\ f (u::x) = z + 1 }  -> 
    step_up f z (u::x).
generalize step_up_snoc step_up_snocEps.
splitsolve0 (1%nat).
Qed.

Ltac progress1 g := match goal with
  | [ |- step_up ?f ?z (?u::?x) ] => apply step_up_charact
  | [ H : continuous ?f |- _ ] => unfold continuous in H
  end
  || progress0 g.

Ltac splitsolve1 n := splitsolve progress1 split0 noni0 n 0.

Theorem int_val: forall f z u, continuous f -> f Eps <= z < f u ->step_up f z u.
induction u as [ | v IHu x ];intros.
  (** - 
  The case $u=\emp$ is trivial since the hypothesis [f(Eps) <= z < f(u)]
  is absurd then: *)
  splitsolve1 0%nat...
  (** - 
  We now consider the case [u = v :: x]: *)
  assert ({ z = f v }+{ z < f v }).
    (** -- 
    The above claim automatically resolves by continuity of $f$ and
    since %\\% [z < f(v :: x)]: *)
    splitsolve1 2%nat...
    (** --
    The main case is now trivial: either [f(v) = z] and [f(v :: x) = z+1] and we
    are done, or [z < f(v)] and we conclude thanks to the induction hypothesis: *)
    splitsolve1 3%nat...
Qed.