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.