Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
7
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Open sidebar
Why3
why3
Commits
fd3c9391
Commit
fd3c9391
authored
May 23, 2018
by
Jean-Christophe Filliâtre
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
lagrange_inequality: removed a Coq proof
parent
1bc757e2
Changes
2
Hide whitespace changes
Inline
Side-by-side
Showing
2 changed files
with
0 additions
and
57 deletions
+0
-57
examples/logic/lagrange_inequality/lagrange_inequality_CauchySchwarzInequality_sqr_le_sqrt_1.v
...grange_inequality_CauchySchwarzInequality_sqr_le_sqrt_1.v
+0
-56
examples/logic/lagrange_inequality/why3session.xml
examples/logic/lagrange_inequality/why3session.xml
+0
-1
No files found.
examples/logic/lagrange_inequality/lagrange_inequality_CauchySchwarzInequality_sqr_le_sqrt_1.v
deleted
100644 → 0
View file @
1bc757e2
(
*
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
.
Require
Import
Why3
.
Ltac
ae
:=
why3
"Alt-Ergo,0.99.1,"
timelimit
3
;
admit
.
Import
R_sqrt
.
Open
Scope
R_scope
.
(
*
Why3
goal
*
)
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
.
*
)
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
.
Admitted
.
examples/logic/lagrange_inequality/why3session.xml
View file @
fd3c9391
...
...
@@ -31,7 +31,6 @@
<proof
prover=
"11"
><result
status=
"valid"
time=
"0.00"
/></proof>
</goal>
<goal
name=
"sqr_le_sqrt"
proved=
"true"
>
<proof
prover=
"0"
edited=
"lagrange_inequality_CauchySchwarzInequality_sqr_le_sqrt_1.v"
><result
status=
"valid"
time=
"0.97"
/></proof>
<proof
prover=
"6"
><result
status=
"valid"
time=
"0.04"
/></proof>
</goal>
<goal
name=
"CauchySchwarz"
proved=
"true"
>
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment