Require Import Minimisation ExtractionConsts Omega.

Set Implicit Arguments.
Unset Strict Implicit.

Definition abs_x_minus_y_squared (x y : nat) :=
  Def ((x - y*y) + (y*y - x)).

Definition perfect_sqrt (x:nat) := mu abs_x_minus_y_squared x 0.

Extraction "perfsqrt.ml" perfect_sqrt.

Lemma compute_perfect_sqrt_36 : perfect_sqrt 36 = Def 6.
unfold perfect_sqrt; unfold mu.
apply iter_Def_eq_fixp_2 with (n:=7).
reflexivity.
Qed.

Lemma perfect_sqrt_Undef_iter :
  forall n x y, (forall z:nat, ~ x = z*z) ->
    FixedPoint.iter (mono_mu abs_x_minus_y_squared) n x y = Undef.
induction n.
reflexivity.
simpl; unfold f_mu; simpl.
intros x y Hxneq.
case_eq (x - y * y + (y * y - x)).
intro Heq0.
assert (Hcontr: x = y*y) by omega.
contradiction (Hxneq y Hcontr).
intros _ _.
apply (IHn x (S y) Hxneq).
Qed.

Lemma perfect_sqrt_Undef :
  forall x:nat, (forall y:nat, ~ x = y*y) -> perfect_sqrt x = Undef.
intros x Hx.
unfold perfect_sqrt, mu.
destruct (fixp_flat_witness_2 (@cont_mu nat abs_x_minus_y_squared) x 0) as [n Hn].
rewrite Hn.
apply perfect_sqrt_Undef_iter with (1:=Hx).
Qed.