lagrange_inequality_CauchySchwarzInequality_sqr_le_sqrt_1.v 1.41 KB
Newer Older
1
(* This file is generated by Why3's Coq 8.4 driver *)
MARCHE Claude's avatar
MARCHE Claude committed
2 3
(* Beware! Only edit allowed sections below    *)
Require Import BuiltIn.
4
Require Reals.R_sqrt.
MARCHE Claude's avatar
MARCHE Claude committed
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 *)
14 15
Definition norm2 (x1:R) (x2:R): R :=
  ((Reals.RIneq.Rsqr x1) + (Reals.RIneq.Rsqr x2))%R.
MARCHE Claude's avatar
MARCHE Claude committed
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
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's avatar
MARCHE Claude committed
22

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's avatar
MARCHE Claude committed
26 27

(* Why3 assumption *)
28
Definition norm (x1:R) (x2:R): R := (Reals.R_sqrt.sqrt (norm2 x1 x2)).
MARCHE Claude's avatar
MARCHE Claude committed
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.
34
Import R_sqrt.
MARCHE Claude's avatar
MARCHE Claude committed
35 36 37 38

Open Scope R_scope.

(* Why3 goal *)
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's avatar
MARCHE Claude committed
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.