Require Import ZArith.
Require Import Omega.
Require Import ZArithRing.
Open Scope Z_scope.

Lemma calculatoire : forall r0 r' s', 
 0 <= r0 < 4 ->
 s' * s' <= s' * s' + r' < (s' + 1) * (s' + 1) ->
 {s : Z & {r : Z |
     4 * (s' * s' + r') + r0 = s * s + r /\
     s * s <= 4 * (s' * s' + r') + r0 < (s + 1) * (s + 1)}}.
Proof.
intros r0 r' s' Hr Hcmp.
replace (4*(s'*s'+r')+r0) with (4*(s'*s')+(4*r'+r0)).
destruct (Z_lt_ge_dec (4*r'+r0) (4*s'+1)) as [H|H].

  exists (2*s'). exists (4*r'+r0).
  split. ring.
  replace (2*s'*(2*s')) with (4*(s'*s')).
  replace ((2*s'+1)*(2*s'+1)) with (4*(s'*s')+4*s' +1).
  omega. ring. ring.

  exists (2*s'+1). exists (4*r'+r0-4*s'-1). 
  split. ring.
  replace ((2*s'+1)*(2*s'+1)) with (4*(s'*s')+4*s' +1).
  replace  ((2*s'+1+1)*(2*s'+1+1)) with (4*((s'+1)*(s'+1))).
  omega. ring. ring.

ring.
Qed.


Theorem int_sqrt_aux : forall (p:positive),
 {s:Z & {r:Z | Zpos p = s*s+r /\
               s*s <= Zpos p < (s+1)*(s+1)}} *
 {s:Z & {r:Z | Zpos (xO p) = s*s+r /\
               s*s <= Zpos (xO p) < (s+1)*(s+1)}} *
 {s:Z & {r:Z | Zpos (xI p) = s*s+r /\
               s*s <= Zpos (xI p) < (s+1)*(s+1)}}.
Proof.
induction p ;
try (destruct IHp as [[IH IHO] IHI] ;
     destruct IH as [s' [r' [Heq Hcmp]]] ;
     rewrite Heq in Hcmp) ;
split ; try split ;
try assumption ;

  (* Les cas triviaux sont éliminés. Il reste : *)
  (*   - les quatre cas de récurrence           *)
  (*   - les trois cas de base                  *)

  (* Cas de récurrence *)
  try (replace (Zpos (xO (xO p))) with (4*(Zpos p)+0) ;
       replace (Zpos (xO (xI p))) with (4*(Zpos p)+2) ;
       replace (Zpos (xI (xI p))) with (4*(Zpos p)+3) ;
       replace (Zpos (xI (xO p))) with (4*(Zpos p)+1)) ;
  try (rewrite Heq ;
       apply calculatoire ; omega ; assumption);
  try (simpl ; reflexivity).

  (* Cas de base *)
  exists 1. exists 0. omega.
  exists 1. exists 1. omega.
  exists 1. exists 2. omega.
Qed.

Lemma int_sqrt : forall (p:positive), {s:Z & {r:Z | Zpos p = s*s+r /\
                                                    s*s <= Zpos p < (s+1)*(s+1)}}.
Proof.
intro p.
destruct (int_sqrt_aux p) as [[H _] _].
exact H.
Qed.


(* Démonstration alternative : ou la puissance de la tactique refine... *)
Lemma int_sqrt2 : forall (p:positive), {s:Z & {r:Z | Zpos p = s*s+r /\
                                                    s*s <= Zpos p < (s+1)*(s+1)}}.
Proof.
refine (fix f (p:positive) :=
        match p return {s:Z & {r:Z | Zpos p = s*s+r /\ s*s <= Zpos p < (s+1)*(s+1)}} with
          | xH => _
          | xO xH => _
          | xI xH => _
          | xO (xO q) => _
          | xO (xI q) => _
          | xI (xI q) => _
          | xI (xO q) => _
        end).

(* Cas xI xI *)
destruct (f q) as [s' [r' [Heq Hcmp]]].
replace (Zpos (xI (xI q))) with (4*(Zpos q)+3).
rewrite Heq. rewrite Heq in Hcmp.
apply calculatoire. omega. assumption.
simpl. reflexivity.

(* Cas xI xO *)
destruct (f q) as [s' [r' [Heq Hcmp]]].
replace (Zpos (xI (xO q))) with (4*(Zpos q)+1).
rewrite Heq. rewrite Heq in Hcmp.
apply calculatoire. omega. assumption.
simpl. reflexivity.

(* Cas 3 *)
exists 1. exists 2. omega.

(* Cas xO xI *)
destruct (f q) as [s' [r' [Heq Hcmp]]].
replace (Zpos (xO (xI q))) with (4*(Zpos q)+2).
rewrite Heq. rewrite Heq in Hcmp.
apply calculatoire. omega. assumption.
simpl. reflexivity.

(* Cas xO xO *)
destruct (f q) as [s' [r' [Heq Hcmp]]].
replace (Zpos (xO (xO q))) with (4*(Zpos q)+0).
rewrite Heq. rewrite Heq in Hcmp.
apply calculatoire. omega. assumption.
simpl. reflexivity.

(* Cas 2 *)
exists 1. exists 1. omega.

(* Cas 1 *)
exists 1. exists 0. omega.
Qed.