(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
Require tacticext.
Require boolprop.
Require funs.
Require dataset.
Require natprop.
Require znat.
Require frac.
Require real.
Require realsyntax.
Require realprop.
Require Setoid.

Set Implicit Arguments.

Definition sqrt [R : real_structure; x : R] : R :=
  `sup {y | y * y <= x}`.

Grammar constr real_expr1 : constr :=
  real_sqrt ["sqrt" real_expr1($x)] -> [(sqrt $x)]
| real_sqr [real_expr0($x) "^" "2"] -> [(mulr $x $x)].

Syntax constr
  level 0: top_sqrt [(sqrt $x)] -> ["`" [<hov 0> (REXP 1 <<(sqrt $x)>>)] "`"];
  level 10: top_sqrt_explicit [(sqrt 1!$r)] -> ["sqrt 1!" $r:L];
  level 1: sqrt [<<(REXP $_ <<(sqrt $x)>>)>>] -> ["sqrt" [1 0] (REXP 1 $x)]
         | sqr [<<(REXP $_ <<(mulr $x $x)>>)>>] -> [ (REXP 0 $x):L "^2" ];
  level 0: sqrt_explicit [<<(REXP $_ <<(sqrt 1!$r)>>)>>] ->
           ["[" [<hov 0> <<(sqrt 1!$r)>>] "]"].

Section Sqrt.

Variable R : real_model.

(* patch for v7.3.1 Setoid Prop rewrite at root bug *)
Local xProp [P : Prop] : Prop := P.
Remark xPropE : (P : Prop) (xProp P) -> P. Proof. Done. Qed.
Add Morphism xProp : dedekind_xProp_morphism. Proof. Tauto. Qed.
Tactic Definition IP := Apply xPropE.

Local RR : Type := R.
Local isR [x : RR] : RR := x.
Local eqR : RR -> RR -> Prop := (!eqr ?).
Local leqR : RR -> RR -> Prop := (locked (!leqr ?)).
Local addR : RR -> RR -> RR := (locked (!addr ?)).
Local oppR : RR -> RR := (locked (!oppr ?)).
Local mulR : RR -> RR -> RR := (locked (!mulr ?)).

Remark rwR : (x1, x2 : R) `x1 = x2` -> (eqR (isR x1) (isR x2)).
Proof. Done. Qed. 

Remark leqRI : (x1, x2 : R) `x1 <= x2` == (leqR (isR x1) (isR x2)).
Proof. By Unlock leqR. Qed.

Remark eqRI : (x1, x2 : R) `x1 = x2` == (eqR (isR x1) (isR x2)).
Proof. By Unlock eqR. Qed.

Remark addRI : (x1, x2 : R) `x1 + x2` == (addR (isR x1) (isR x2)).
Proof. By Unlock addR. Qed.

Remark oppRI : (x : R) `-x` == (oppR (isR x)).
Proof. By Unlock oppR. Qed.

Remark mulRI : (x1, x2 : R) `x1 * x2` == (mulR (isR x1) (isR x2)).
Proof. By Unlock mulR. Qed.

Add Setoid RR eqR (eqr_theory R).

Hints Unfold eqR.

Remark eqR_refl : (x : R) (eqR x x). Proof. Apply: (!eqr_refl). Qed.
Hints Resolve eqr_refl eqR_refl leqrr ltrW ltr01 ltr02.

Syntactic Definition ltr01 := (ltr01 R).

Add Morphism isR : sqrt_isr_morphism. Proof. Done. Qed.

Add Morphism leqR : sqrt_leqr_morphism. Proof. Exact (!leqR_morphism ?). Qed.

Add Morphism addR : sqrt_addr_morphism. Proof. Exact (!addR_morphism ?). Qed.

Add Morphism oppR : sqrt_oppr_morphism. Proof. Exact (!oppR_morphism ?). Qed.

Add Morphism mulR : sqrt_mulr_morphism. Proof. Exact (!mulR_morphism ?). Qed.

Remark has_sqrt : (x : R) `x >= 0` -> (has_supr [y]`y^2 <= x`).
Proof.
Move=> x Hx; Split; LeftBy Exists `0%R`; Rewrite: leqRI (rwR (mulr0 `0`)) -leqRI.
Exists (maxr x `1`); Move=> y Hyx; Case: (leqr_total y `1`) => [Hy].
  Apply: (leqr_trans Hy); Apply leqr_maxr.
Apply: (leqr_trans (leqr_trans ? Hyx)); RightBy Apply leqr_maxl.
Move: {}Hy; Rewrite: -(leqr_pmul2l  `1` y (ltr_leq_trans ltr01 Hy)).
By Apply: leqr_trans; Case: (mulr1 y).
Qed.

Lemma square_sqrt : (x : R) `x >= 0` -> `(sqrt x)^2 = x`.
Proof.
Move=> x Hx; Pose rx := `sqrt x`; Def: Hx2 := (has_sqrt Hx).
Step Hx0: `(0)^2 <= x` By Rewrite: leqRI (rwR (mulr0 `0`)) -leqRI.
Step Hrx0: `0 <= rx` By Apply: ubr_sup; Case Hx2.
Case: (reals_classic R `rx^2 = x`); LeftDone; Case/ltr_total=> [Hrx].
  Pose dh := `rx + (rx + 1)`; Pose nh := `x - rx^2`; Pose h := `(minr 1 nh/dh)`.
  Step Hdh0: `dh > 0`.
    Apply: (ltr_leq_trans ltr01); Move: Hrx0.
    Rewrite: -`(leqr_add2r 1 0 rx)` leqRI (rwR `(add0r 1%R)`) -leqRI; Move=> Hrx1.
    By Apply: (leqr_trans Hrx1); IP; Rewrite: /dh `(leqr_add2l rx 1 rx + 1)`.
  Step Hh0 : `h > 0`.
    Move: Hrx; Rewrite: `(leqr_sub0 x rx^2)`; Move=> Hrx.
    IP; Rewrite: /h `(ltr_min 1 nh/dh 0)`; Split; Auto.
    By Rewrite: /nh (posr_pmull `1/dh` Hrx); Apply posr_inv.
  Case Hh0; IP; Rewrite: -`(leqr_add2l rx h 0)` leqRI (rwR (addr0 rx)) -leqRI.
  Apply: ubr_sup; LeftBy Case Hx2.
  Rewrite: leqRI (rwR `(mulr_addl rx + h rx h)`) addRI (rwR (mulr_addr rx rx h)).
  Rewrite: addRI (rwR (mulrC rx h)) -!addRI.
  Rewrite: -(rwR `(addrA rx^2 h * rx h * (rx + h))`) addRI.
  Rewrite: -(rwR `(mulr_addr h rx rx + h)`); Pose dh' := `rx + (rx + h)`.
  Rewrite: -(rwR (addr_inv `rx^2` x)) (rwR `(addrCA (-rx^2) rx^2 x)`) addRI.
  Rewrite: (rwR `(addrC (-rx^2) x)`) -/nh -!addRI -leqRI.
  IP; Rewrite: `(leqr_add2l rx^2 h * dh' nh)` /xProp.
  Apply leqr_trans with `h * dh`.
    IP; Rewrite: `(leqr_pmul2l dh' dh Hh0)` /dh /dh'.
    Rewrite: `(leqr_add2l rx rx + h rx + 1)` `(leqr_add2l rx h 1)`.
    Apply: leqr_minl.
  Rewrite: leqRI (rwR (mulrC h dh)) -(rwR (pmulr_inv nh Hdh0)).
  Rewrite: (rwR `(mulrCA 1/dh dh nh)`) 2!mulRI (rwR `(mulrC 1/dh nh)`) -!mulRI.
  IP; Rewrite: -leqRI `(leqr_pmul2l h nh/dh Hdh0)`; Apply: leqr_minr.
Pose dh := `rx + rx`; Pose nh := `rx^2 - x`; Pose h := `(minr rx nh/dh)`.
Step Hrx0': `0 < rx`.
  Move: {}Hrx0; Rewrite: `(leqr_eqVlt 0 rx)`; Case; RightDone.
  By Move=> Drx; Case Hrx; Rewrite: leqRI mulRI -(rwR Drx) -mulRI -leqRI. 
Step Hdh0: `dh > 0`.
  Apply: (ltr_leq_trans Hrx0'); Rewrite: leqRI -(rwR (addr0 rx)) -leqRI.
  By IP; Rewrite: /dh `(leqr_add2l rx 0 rx)`.
Step Hh0 : `h > 0`.
  Move: Hrx; Rewrite: `(leqr_sub0 rx^2 x)` -/nh; Move=> Hnh.
  IP; Rewrite: /h `(ltr_min rx nh/dh 0)`; Split; Auto.
  By Rewrite: (posr_pmull `1/dh` Hnh); Apply posr_inv.
Case: (supr_total `rx - h` Hx2) => [[y Hyx Hhy] | Hrx']; Case Hh0.
  IP; Rewrite: -`(leqr_pmul2l h 0 Hh0)`.
  Rewrite: -`(leqr_add2l rx^2 - h * dh h^2 h * 0)` /xProp leqRI.
  Rewrite: !addRI {1}/dh {2 oppr}lock oppRI -lock (rwR `(mulr_addr h rx rx)`).
  Rewrite: (rwR (mulr0 h)) -oppRI (rwR `(oppr_add h * rx h * rx)`) addRI.
  Rewrite: {2 oppr}lock -(rwR (mulr_oppl h rx)) -lock -(rwR (mulr_oppr h rx)).
  Rewrite: (rwR (mulrC `-h` rx)) {1 addR}lock -2!addRI -lock.
  Rewrite: (rwR `(addrA rx^2 rx * -h h * -rx)`) -addRI.
  Rewrite: -(rwR `(addrA rx^2 + rx * -h h * -rx h^2)`) addRI.
  Rewrite: -(rwR (mulr_addr rx rx `-h`)) -(rwR (mulr_addr h `-rx` h)).
  Rewrite: {1 mulr}lock mulRI -lock -(rwR (oppr_opp h)) -mulRI.
  Rewrite: (rwR (mulr_oppl `-h` `-rx + h`)) -(rwR (mulr_oppr `-h` `-rx + h`)).
  Rewrite: 2!mulRI (rwR (oppr_add `-rx` h)) 2!addRI (rwR (oppr_opp rx)) -!addRI.
  Rewrite: -!mulRI -(rwR (mulr_addl `rx - h` rx `-h`)).
  Rewrite: (rwR (addr0 `rx^2 - h * dh`)) -leqRI.
  Apply: (leqr_trans (leqr_trans ? Hyx)).
    Step Hrx': `rx - h >= 0`.
      IP; Rewrite: -(leqr_0sub h rx); Apply: leqr_minl.
    Apply: (leqr_trans (mulr_monotony R Hrx' Hhy)).
    Rewrite: leqRI (rwR (mulrC `rx - h` y)) -leqRI.
    By Apply: (mulr_monotony R (leqr_trans Hrx' Hhy)).
  IP; Rewrite: (leqr_0sub x `rx^2 - h * dh`) leqRI.
  Rewrite: -(rwR (addrA `rx^2` `-(h * dh)` `-x`)).
  Rewrite: addRI (rwR (addrC `-(h * dh)` `-x`)) -addRI.
  Rewrite: (rwR (addrA `rx^2` `-x` `-(h * dh)`)) -/nh -leqRI.
  Rewrite: -(leqr_0sub `h * dh` nh) leqRI.
  Rewrite: -(rwR (pmulr_inv nh Hdh0)) (rwR (mulrC h dh)).
  Rewrite: (rwR `(mulrC 1/dh dh * nh)`) -(rwR `(mulrA dh nh 1/dh)`) -leqRI.
  Rewrite: `(leqr_pmul2l h nh/dh Hdh0)`; Apply: leqr_minr.
IP; Rewrite: `(leqr_0sub h 0)` -`(leqr_add2l rx 0 0 - h)` leqRI.
By Rewrite: (rwR (addr0 rx)) addRI (rwR (add0r `-h`)) -addRI -leqRI.
Qed.

Lemma sqrt_square : (x : R) `x >= 0` -> `sqrt x^2 = x`.
Proof.
Move=> x Hx; Step Hx2: `x^2 >= 0`.
  By Rewrite: leqRI -(rwR (mulr0 x)) -leqRI; Apply (mulr_monotony R).
Move/has_sqrt: Hx2 => Hx2; Split.
  Apply: leqr_sup_ub; LeftBy Case Hx2.
  Move=> y Hyx2; Case: (reals_classic R `y <= x`); Auto.
  Move=> Hxy; IP; Rewrite: -(leqr_pmul2l y x (leqr_lt_trans Hx Hxy)).
  Apply: (leqr_trans Hyx2); Rewrite: leqRI (rwR (mulrC y x)) -leqRI.
  By Apply (mulr_monotony R); RightBy Apply ltrW.
By Apply: ubr_sup; [Case Hx2 | Apply leqrr].
Qed.

Lemma sqrt_morphism : (x, y : R) `x >= 0` -> `x = y` -> `sqrt x = sqrt y`.
Proof.
Move=> x y Hx0 Dx; Apply: (supr_morphism (has_sqrt Hx0)) => [z].
Rewrite: leqRI (rwR Dx) -leqRI; Tauto.
Qed.

Lemma sqrt_def : (x, y : R)
  (`x >= 0` /\ `y = sqrt x`) <-> (`y >= 0` /\ `y^2 = x`).
Proof.
Move=> x y; Split.
  Move=> [Hx Dy]; Split.
    Rewrite: leqRI (rwR Dy) -leqRI; Apply: ubr_sup; LeftBy Case (has_sqrt Hx).
    By Rewrite: leqRI (rwR (mulr0 `0`)) -leqRI.
  By Rewrite: eqRI mulRI (rwR Dy) -mulRI; Apply: square_sqrt.
Move=> [Hy Dx]; Step Hy2: `y^2 >= 0`.
  By Rewrite: leqRI -(rwR (mulr0 y)) -leqRI; Apply: (mulr_monotony R).
Split; LeftBy Rewrite: leqRI -(rwR Dx) -leqRI.
By Rewrite: eqRI -(rwR (sqrt_square Hy)) -eqRI; Apply: sqrt_morphism.
Qed.

End Sqrt.

Section Sqrt2.

Variable R : real_model.
Coercion Local fracR := (fracr R).

Theorem sqrt2_irrational : ~(EX f : frac | `f = sqrt 2`).
Proof.
Move=> [f Df]; Step [Hf22 H2f2]: `(mulf f f) = F2`.
  Apply: (eqr_trans (fracr_mul ? ? ?)); Apply: eqr_trans (fracrz R (Znat 2)).
  By Apply: eqr_trans (square_sqrt (ltrW (ltr02 R))); Apply mulr_morphism.
Step Df2: (eqf F2 (mulf f f)) By Apply/andP; Split; Apply/(fracr_leqPx R ? ?).
Move: f Df2 {Hf22 H2f2 Df} => [d m]; Rewrite: /eqf /= -eqz_leq; Move/eqP.
Rewrite: scalez_mul -scalez_scale scalez_mul mulzC {-1 Zpos}lock /= -lock.
Step []: (Zpos (S d)) = (scalez d (Znat 1)).
  By Apply esym; Apply: eqP; Rewrite scalez_pos; Elim d.
Step [n []]: (EX n | (mulz (Zpos n) (Zpos n)) = (mulz m m)).
  Case: m => [n | n]; LeftBy Exists n.
  By Exists (S n); Rewrite: -{1 (Zneg n)}oppz_opp mulz_oppl -mulz_oppr.
Pose i := (addn (S d) n); Move: (leqnn i) {m}; Rewrite: {1}/i.
Elim: i n d => // [i Hrec] n d Hi Dn2; Move/esym: Dn2 Hi.
Rewrite: -{n}odd_double_half double_addnn !zpos_addn; Move/half: n (odd n) => n.
Case; [Move/((congr oddz) ? ?) | Move/((congr halfz) ? ?)].
  By Rewrite: !mulz_addr oddz_add mulzC !mulz_addr oddz_add !oddz_double.
Rewrite: add0n addnC -addnA add0z mulz_addr !halfz_double mulzC mulz_addr.
Case: n => [|n] Dn2 Hi; LeftBy Rewrite: !mulz_nat in Dn2.
Apply: Hrec Dn2; Apply: (leq_trans 3!i) Hi; Apply: leq_addl.
Qed.

End Sqrt2.

Unset Implicit Arguments.