Attention une mise à jour du serveur va être effectuée le vendredi 16 avril entre 12h et 12h30. Cette mise à jour va générer une interruption du service de quelques minutes.

lagrange_inequality: removed a Coq proof

parent 25b8177c
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require Reals.R_sqrt.
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 *)
Definition norm2 (x1:R) (x2:R): R :=
((Reals.RIneq.Rsqr x1) + (Reals.RIneq.Rsqr x2))%R.
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
a2) * (norm2 b1 b2))%R = ((Reals.RIneq.Rsqr (dot a1 a2 b1
b2)) + (Reals.RIneq.Rsqr ((a1 * b2)%R - (a2 * b1)%R)%R))%R).
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.
(* Why3 assumption *)
Definition norm (x1:R) (x2:R): R := (Reals.R_sqrt.sqrt (norm2 x1 x2)).
Axiom norm_pos : forall (x1:R) (x2:R), (0%R <= (norm x1 x2))%R.
Axiom sqr_le_sqrt : forall (x:R) (y:R), ((Reals.RIneq.Rsqr x) <= y)%R ->
(x <= (Reals.R_sqrt.sqrt y))%R.
Require Import Why3.
Ltac ae := why3 "Alt-Ergo,0.99.1," timelimit 3; admit.
(* Why3 goal *)
Theorem CauchySchwarz : forall (x1:R) (x2:R) (y1:R) (y2:R), ((dot x1 x2 y1
y2) <= ((norm x1 x2) * (norm y1 y2))%R)%R.
(* Why3 intros x1 x2 y1 y2. *)
intros x1 x2 y1 y2.
unfold norm.
rewrite <- R_sqrt.sqrt_mult.
apply sqr_le_sqrt.
ae.
ae.
ae.
Admitted.
......@@ -2,9 +2,10 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Coq" version="8.7.1" timelimit="5" steplimit="0" memlimit="4000"/>
<prover id="0" name="Coq" version="8.7.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="CVC3" version="2.4.1" timelimit="3" steplimit="0" memlimit="1000"/>
<prover id="4" name="Eprover" version="2.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="5" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="6" name="MetiTarski" version="2.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="11" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/>
......@@ -34,7 +35,7 @@
<proof prover="6"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="CauchySchwarz" proved="true">
<proof prover="0" edited="lagrange_inequality_CauchySchwarzInequality_CauchySchwarz_1.v"><result status="valid" time="0.59"/></proof>
<proof prover="4"><result status="valid" time="0.10"/></proof>
</goal>
</theory>
<theory name="TriangleInequality" proved="true">
......@@ -47,7 +48,7 @@
<proof prover="6"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="triangle" proved="true">
<proof prover="0" memlimit="1000" edited="lagrange_inequality_TriangleInequality_triangle_1.v"><result status="valid" time="0.33"/></proof>
<proof prover="0" edited="lagrange_inequality_TriangleInequality_triangle_1.v"><result status="valid" time="0.33"/></proof>
</goal>
</theory>
</file>
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment