(* (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)] -> ["`" [ (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)>>)>>] -> ["[" [ <<(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.