lagrange_inequality_CauchySchwarzInequality_sqr_le_sqrt_1.v 1.41 KB
 Guillaume Melquiond committed Mar 05, 2014 1 ``````(* This file is generated by Why3's Coq 8.4 driver *) `````` MARCHE Claude committed Mar 12, 2013 2 3 ``````(* Beware! Only edit allowed sections below *) Require Import BuiltIn. `````` Guillaume Melquiond committed Mar 05, 2014 4 ``````Require Reals.R_sqrt. `````` MARCHE Claude committed Mar 12, 2013 5 6 7 8 9 10 11 12 13 ``````Require BuiltIn. Require real.Real. Require real.Square. (* Why3 assumption *) Definition dot (x1:R) (x2:R) (y1:R) (y2:R): R := ((x1 * y1)%R + (x2 * y2)%R)%R. (* Why3 assumption *) `````` Guillaume Melquiond committed Mar 05, 2014 14 15 ``````Definition norm2 (x1:R) (x2:R): R := ((Reals.RIneq.Rsqr x1) + (Reals.RIneq.Rsqr x2))%R. `````` MARCHE Claude committed Mar 12, 2013 16 17 18 19 `````` Axiom norm2_pos : forall (x1:R) (x2:R), (0%R <= (norm2 x1 x2))%R. Axiom Lagrange : forall (a1:R) (a2:R) (b1:R) (b2:R), (((norm2 a1 `````` Guillaume Melquiond committed Mar 05, 2014 20 21 `````` a2) * (norm2 b1 b2))%R = ((Reals.RIneq.Rsqr (dot a1 a2 b1 b2)) + (Reals.RIneq.Rsqr ((a1 * b2)%R - (a2 * b1)%R)%R))%R). `````` MARCHE Claude committed Mar 12, 2013 22 `````` `````` Guillaume Melquiond committed Mar 05, 2014 23 24 25 ``````Axiom CauchySchwarz_aux : forall (x1:R) (x2:R) (y1:R) (y2:R), ((Reals.RIneq.Rsqr (dot x1 x2 y1 y2)) <= ((norm2 x1 x2) * (norm2 y1 y2))%R)%R. `````` MARCHE Claude committed Mar 12, 2013 26 27 `````` (* Why3 assumption *) `````` Guillaume Melquiond committed Mar 05, 2014 28 ``````Definition norm (x1:R) (x2:R): R := (Reals.R_sqrt.sqrt (norm2 x1 x2)). `````` MARCHE Claude committed Mar 12, 2013 29 30 31 32 33 `````` Axiom norm_pos : forall (x1:R) (x2:R), (0%R <= (norm x1 x2))%R. Require Import Why3. Ltac ae := why3 "Alt-Ergo,0.95.1," timelimit 3. `````` Guillaume Melquiond committed Mar 05, 2014 34 ``````Import R_sqrt. `````` MARCHE Claude committed Mar 12, 2013 35 36 37 38 `````` Open Scope R_scope. (* Why3 goal *) `````` Guillaume Melquiond committed Mar 05, 2014 39 40 41 ``````Theorem sqr_le_sqrt : forall (x:R) (y:R), ((Reals.RIneq.Rsqr x) <= y)%R -> (x <= (Reals.R_sqrt.sqrt y))%R. (* Why3 intros x y h1. *) `````` MARCHE Claude committed Mar 12, 2013 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 ``````intros x y h1. assert (0 <= Rsqr x) by ae. assert (0 <= y) by ae. assert (h : (x < 0 \/ x >= 0)%R). ae. destruct h. ae. replace x with (sqrt (Rsqr x)). apply sqrt_le_1. ae. ae. ae. ae. Qed. ``````