Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
7cc748ed
Commit
7cc748ed
authored
Jun 21, 2011
by
Jean-Christophe Filliâtre
Browse files
restored insertion sort proof (my mistake)
parent
105f6179
Changes
3
Hide whitespace changes
Inline
Side-by-side
examples/programs/insertion_sort/insertion_sort.mlw_InsertionSort_WP_parameter insertion_sort_1.v
0 → 100644
View file @
7cc748ed
(
*
This
file
is
generated
by
Why3
'
s
Coq
driver
*
)
(
*
Beware
!
Only
edit
allowed
sections
below
*
)
Require
Import
ZArith
.
Require
Import
Rbase
.
Definition
unit
:=
unit
.
Parameter
label
:
Type
.
Parameter
at1
:
forall
(
a
:
Type
),
a
->
label
->
a
.
Implicit
Arguments
at1
.
Parameter
old
:
forall
(
a
:
Type
),
a
->
a
.
Implicit
Arguments
old
.
Inductive
ref
(
a
:
Type
)
:=
|
mk_ref
:
a
->
ref
a
.
Implicit
Arguments
mk_ref
.
Definition
contents
(
a
:
Type
)(
u
:
(
ref
a
))
:
a
:=
match
u
with
|
mk_ref
contents1
=>
contents1
end
.
Implicit
Arguments
contents
.
Parameter
map
:
forall
(
a
:
Type
)
(
b
:
Type
),
Type
.
Parameter
get
:
forall
(
a
:
Type
)
(
b
:
Type
),
(
map
a
b
)
->
a
->
b
.
Implicit
Arguments
get
.
Parameter
set
:
forall
(
a
:
Type
)
(
b
:
Type
),
(
map
a
b
)
->
a
->
b
->
(
map
a
b
).
Implicit
Arguments
set
.
Axiom
Select_eq
:
forall
(
a
:
Type
)
(
b
:
Type
),
forall
(
m
:
(
map
a
b
)),
forall
(
a1
:
a
)
(
a2
:
a
),
forall
(
b1
:
b
),
(
a1
=
a2
)
->
((
get
(
set
m
a1
b1
)
a2
)
=
b1
).
Axiom
Select_neq
:
forall
(
a
:
Type
)
(
b
:
Type
),
forall
(
m
:
(
map
a
b
)),
forall
(
a1
:
a
)
(
a2
:
a
),
forall
(
b1
:
b
),
(
~
(
a1
=
a2
))
->
((
get
(
set
m
a1
b1
)
a2
)
=
(
get
m
a2
)).
Parameter
const
:
forall
(
b
:
Type
)
(
a
:
Type
),
b
->
(
map
a
b
).
Set
Contextual
Implicit
.
Implicit
Arguments
const
.
Unset
Contextual
Implicit
.
Axiom
Const
:
forall
(
b
:
Type
)
(
a
:
Type
),
forall
(
b1
:
b
)
(
a1
:
a
),
((
get
(
const
(
b1
)
:
(
map
a
b
))
a1
)
=
b1
).
Inductive
array
(
a
:
Type
)
:=
|
mk_array
:
Z
->
(
map
Z
a
)
->
array
a
.
Implicit
Arguments
mk_array
.
Definition
elts
(
a
:
Type
)(
u
:
(
array
a
))
:
(
map
Z
a
)
:=
match
u
with
|
mk_array
_
elts1
=>
elts1
end
.
Implicit
Arguments
elts
.
Definition
length
(
a
:
Type
)(
u
:
(
array
a
))
:
Z
:=
match
u
with
|
mk_array
length1
_
=>
length1
end
.
Implicit
Arguments
length
.
Definition
get1
(
a
:
Type
)(
a1
:
(
array
a
))
(
i
:
Z
)
:
a
:=
(
get
(
elts
a1
)
i
).
Implicit
Arguments
get1
.
Definition
set1
(
a
:
Type
)(
a1
:
(
array
a
))
(
i
:
Z
)
(
v
:
a
)
:
(
array
a
)
:=
match
a1
with
|
mk_array
xcl0
_
=>
(
mk_array
xcl0
(
set
(
elts
a1
)
i
v
))
end
.
Implicit
Arguments
set1
.
Definition
sorted_sub
(
a
:
(
map
Z
Z
))
(
l
:
Z
)
(
u
:
Z
)
:
Prop
:=
forall
(
i1
:
Z
)
(
i2
:
Z
),
(((
l
<=
i1
)
%
Z
/
\
(
i1
<=
i2
)
%
Z
)
/
\
(
i2
<
u
)
%
Z
)
->
((
get
a
i1
)
<=
(
get
a
i2
))
%
Z
.
Definition
sorted_sub1
(
a
:
(
array
Z
))
(
l
:
Z
)
(
u
:
Z
)
:
Prop
:=
(
sorted_sub
(
elts
a
)
l
u
).
Definition
sorted
(
a
:
(
array
Z
))
:
Prop
:=
(
sorted_sub
(
elts
a
)
0
%
Z
(
length
a
)).
Definition
map_eq_sub
(
a
:
Type
)(
a1
:
(
map
Z
a
))
(
a2
:
(
map
Z
a
))
(
l
:
Z
)
(
u
:
Z
)
:
Prop
:=
forall
(
i
:
Z
),
((
l
<=
i
)
%
Z
/
\
(
i
<
u
)
%
Z
)
->
((
get
a1
i
)
=
(
get
a2
i
)).
Implicit
Arguments
map_eq_sub
.
Definition
exchange
(
a
:
Type
)(
a1
:
(
map
Z
a
))
(
a2
:
(
map
Z
a
))
(
i
:
Z
)
(
j
:
Z
)
:
Prop
:=
((
get
a1
i
)
=
(
get
a2
j
))
/
\
(((
get
a2
i
)
=
(
get
a1
j
))
/
\
forall
(
k
:
Z
),
((
~
(
k
=
i
))
/
\
~
(
k
=
j
))
->
((
get
a1
k
)
=
(
get
a2
k
))).
Implicit
Arguments
exchange
.
Axiom
exchange_set
:
forall
(
a
:
Type
),
forall
(
a1
:
(
map
Z
a
)),
forall
(
i
:
Z
)
(
j
:
Z
),
(
exchange
a1
(
set
(
set
a1
i
(
get
a1
j
))
j
(
get
a1
i
))
i
j
).
Inductive
permut_sub
{
a
:
Type
}
:
(
map
Z
a
)
->
(
map
Z
a
)
->
Z
->
Z
->
Prop
:=
|
permut_refl
:
forall
(
a1
:
(
map
Z
a
))
(
a2
:
(
map
Z
a
)),
forall
(
l
:
Z
)
(
u
:
Z
),
(
map_eq_sub
a1
a2
l
u
)
->
(
permut_sub
a1
a2
l
u
)
|
permut_sym
:
forall
(
a1
:
(
map
Z
a
))
(
a2
:
(
map
Z
a
)),
forall
(
l
:
Z
)
(
u
:
Z
),
(
permut_sub
a1
a2
l
u
)
->
(
permut_sub
a2
a1
l
u
)
|
permut_trans
:
forall
(
a1
:
(
map
Z
a
))
(
a2
:
(
map
Z
a
))
(
a3
:
(
map
Z
a
)),
forall
(
l
:
Z
)
(
u
:
Z
),
(
permut_sub
a1
a2
l
u
)
->
((
permut_sub
a2
a3
l
u
)
->
(
permut_sub
a1
a3
l
u
))
|
permut_exchange
:
forall
(
a1
:
(
map
Z
a
))
(
a2
:
(
map
Z
a
)),
forall
(
l
:
Z
)
(
u
:
Z
)
(
i
:
Z
)
(
j
:
Z
),
((
l
<=
i
)
%
Z
/
\
(
i
<
u
)
%
Z
)
->
(((
l
<=
j
)
%
Z
/
\
(
j
<
u
)
%
Z
)
->
((
exchange
a1
a2
i
j
)
->
(
permut_sub
a1
a2
l
u
))).
Implicit
Arguments
permut_sub
.
Axiom
permut_weakening
:
forall
(
a
:
Type
),
forall
(
a1
:
(
map
Z
a
))
(
a2
:
(
map
Z
a
)),
forall
(
l1
:
Z
)
(
r1
:
Z
)
(
l2
:
Z
)
(
r2
:
Z
),
(((
l1
<=
l2
)
%
Z
/
\
(
l2
<=
r2
)
%
Z
)
/
\
(
r2
<=
r1
)
%
Z
)
->
((
permut_sub
a1
a2
l2
r2
)
->
(
permut_sub
a1
a2
l1
r1
)).
Axiom
permut_eq
:
forall
(
a
:
Type
),
forall
(
a1
:
(
map
Z
a
))
(
a2
:
(
map
Z
a
)),
forall
(
l
:
Z
)
(
u
:
Z
),
(
l
<=
u
)
%
Z
->
((
permut_sub
a1
a2
l
u
)
->
forall
(
i
:
Z
),
((
i
<
l
)
%
Z
\
/
(
u
<=
i
)
%
Z
)
->
((
get
a2
i
)
=
(
get
a1
i
))).
Axiom
permut_exists
:
forall
(
a
:
Type
),
forall
(
a1
:
(
map
Z
a
))
(
a2
:
(
map
Z
a
)),
forall
(
l
:
Z
)
(
u
:
Z
),
(
permut_sub
a1
a2
l
u
)
->
forall
(
i
:
Z
),
((
l
<=
i
)
%
Z
/
\
(
i
<
u
)
%
Z
)
->
exists
j
:
Z
,
((
l
<=
j
)
%
Z
/
\
(
j
<
u
)
%
Z
)
/
\
((
get
a2
i
)
=
(
get
a1
j
)).
Definition
exchange1
(
a
:
Type
)(
a1
:
(
array
a
))
(
a2
:
(
array
a
))
(
i
:
Z
)
(
j
:
Z
)
:
Prop
:=
(
exchange
(
elts
a1
)
(
elts
a2
)
i
j
).
Implicit
Arguments
exchange1
.
Definition
permut_sub1
(
a
:
Type
)(
a1
:
(
array
a
))
(
a2
:
(
array
a
))
(
l
:
Z
)
(
u
:
Z
)
:
Prop
:=
(
permut_sub
(
elts
a1
)
(
elts
a2
)
l
u
).
Implicit
Arguments
permut_sub1
.
Definition
permut
(
a
:
Type
)(
a1
:
(
array
a
))
(
a2
:
(
array
a
))
:
Prop
:=
((
length
a1
)
=
(
length
a2
))
/
\
(
permut_sub
(
elts
a1
)
(
elts
a2
)
0
%
Z
(
length
a1
)).
Implicit
Arguments
permut
.
Axiom
exchange_permut
:
forall
(
a
:
Type
),
forall
(
a1
:
(
array
a
))
(
a2
:
(
array
a
))
(
i
:
Z
)
(
j
:
Z
),
(
exchange1
a1
a2
i
j
)
->
(((
length
a1
)
=
(
length
a2
))
->
(((
0
%
Z
<=
i
)
%
Z
/
\
(
i
<
(
length
a1
))
%
Z
)
->
(((
0
%
Z
<=
j
)
%
Z
/
\
(
j
<
(
length
a1
))
%
Z
)
->
(
permut
a1
a2
)))).
Definition
array_eq_sub
(
a
:
Type
)(
a1
:
(
array
a
))
(
a2
:
(
array
a
))
(
l
:
Z
)
(
u
:
Z
)
:
Prop
:=
(
map_eq_sub
(
elts
a1
)
(
elts
a2
)
l
u
).
Implicit
Arguments
array_eq_sub
.
Definition
array_eq
(
a
:
Type
)(
a1
:
(
array
a
))
(
a2
:
(
array
a
))
:
Prop
:=
((
length
a1
)
=
(
length
a2
))
/
\
(
array_eq_sub
a1
a2
0
%
Z
(
length
a1
)).
Implicit
Arguments
array_eq
.
Axiom
array_eq_sub_permut
:
forall
(
a
:
Type
),
forall
(
a1
:
(
array
a
))
(
a2
:
(
array
a
))
(
l
:
Z
)
(
u
:
Z
),
(
array_eq_sub
a1
a2
l
u
)
->
(
permut_sub1
a1
a2
l
u
).
Axiom
array_eq_permut
:
forall
(
a
:
Type
),
forall
(
a1
:
(
array
a
))
(
a2
:
(
array
a
)),
(
array_eq
a1
a2
)
->
(
permut
a1
a2
).
Theorem
WP_parameter_insertion_sort
:
forall
(
a
:
Z
),
forall
(
a1
:
(
map
Z
Z
)),
let
a2
:=
(
mk_array
a
a1
)
in
((
1
%
Z
<=
(
a
-
1
%
Z
)
%
Z
)
%
Z
->
forall
(
a3
:
(
map
Z
Z
)),
let
a4
:=
(
mk_array
a
a3
)
in
forall
(
i
:
Z
),
((
1
%
Z
<=
i
)
%
Z
/
\
(
i
<=
(
a
-
1
%
Z
)
%
Z
)
%
Z
)
->
(((
sorted_sub
a3
0
%
Z
i
)
/
\
(
permut
a4
a2
))
->
(((
0
%
Z
<=
i
)
%
Z
/
\
(
i
<
a
)
%
Z
)
->
let
result
:=
(
get
a3
i
)
in
((((
0
%
Z
<=
i
)
%
Z
/
\
(
i
<=
i
)
%
Z
)
/
\
((
permut
(
set1
a4
i
result
)
a2
)
/
\
((
forall
(
k1
:
Z
)
(
k2
:
Z
),
(((
0
%
Z
<=
k1
)
%
Z
/
\
(
k1
<=
k2
)
%
Z
)
/
\
(
k2
<=
i
)
%
Z
)
->
((
~
(
k1
=
i
))
->
((
~
(
k2
=
i
))
->
((
get
a3
k1
)
<=
(
get
a3
k2
))
%
Z
)))
/
\
forall
(
k
:
Z
),
(((
i
+
1
%
Z
)
%
Z
<=
k
)
%
Z
/
\
(
k
<=
i
)
%
Z
)
->
(
result
<
(
get
a3
k
))
%
Z
)))
->
forall
(
j
:
Z
),
forall
(
a5
:
(
map
Z
Z
)),
let
a6
:=
(
mk_array
a
a5
)
in
((((
0
%
Z
<=
j
)
%
Z
/
\
(
j
<=
i
)
%
Z
)
/
\
((
permut
(
set1
a6
j
result
)
a2
)
/
\
((
forall
(
k1
:
Z
)
(
k2
:
Z
),
(((
0
%
Z
<=
k1
)
%
Z
/
\
(
k1
<=
k2
)
%
Z
)
/
\
(
k2
<=
i
)
%
Z
)
->
((
~
(
k1
=
j
))
->
((
~
(
k2
=
j
))
->
((
get
a5
k1
)
<=
(
get
a5
k2
))
%
Z
)))
/
\
forall
(
k
:
Z
),
(((
j
+
1
%
Z
)
%
Z
<=
k
)
%
Z
/
\
(
k
<=
i
)
%
Z
)
->
(
result
<
(
get
a5
k
))
%
Z
)))
->
((
0
%
Z
<
j
)
%
Z
->
(((
0
%
Z
<=
(
j
-
1
%
Z
)
%
Z
)
%
Z
/
\
((
j
-
1
%
Z
)
%
Z
<
a
)
%
Z
)
->
((
result
<
(
get
a5
(
j
-
1
%
Z
)
%
Z
))
%
Z
->
(((
0
%
Z
<=
(
j
-
1
%
Z
)
%
Z
)
%
Z
/
\
((
j
-
1
%
Z
)
%
Z
<
a
)
%
Z
)
->
(((
0
%
Z
<=
j
)
%
Z
/
\
(
j
<
a
)
%
Z
)
->
forall
(
a7
:
(
map
Z
Z
)),
let
a8
:=
(
mk_array
a
a7
)
in
((
a7
=
(
set
a5
j
(
get
a5
(
j
-
1
%
Z
)
%
Z
)))
->
((
exchange
match
(
set1
a8
(
j
-
1
%
Z
)
%
Z
result
)
with
|
mk_array
_
elts1
=>
elts1
end
match
(
set1
a6
j
result
)
with
|
mk_array
_
elts1
=>
elts1
end
(
j
-
1
%
Z
)
%
Z
j
)
->
forall
(
j1
:
Z
),
(
j1
=
(
j
-
1
%
Z
)
%
Z
)
->
(
permut
(
set1
a8
j1
result
)
a2
))))))))))))).
(
*
YOU
MAY
EDIT
THE
PROOF
BELOW
*
)
intuition
.
intuition
.
unfold
set1
.
unfold
permut
.
split
.
simpl
.
auto
.
apply
permut_trans
with
(
elts
(
set1
(
mk_array
a
a5
)
j
(
get
a3
i
)));
auto
.
subst
j1
.
apply
permut_exchange
with
(
j
-
1
)
%
Z
j
.
simpl
;
omega
.
simpl
;
omega
.
assumption
.
unfold
permut
in
H17
.
intuition
.
Qed
.
(
*
DO
NOT
EDIT
BELOW
*
)
examples/programs/insertion_sort/insertion_sort.mlw_InsertionSort_WP_parameter insertion_sort_2.v
0 → 100644
View file @
7cc748ed
(
*
This
file
is
generated
by
Why3
'
s
Coq
driver
*
)
(
*
Beware
!
Only
edit
allowed
sections
below
*
)
Require
Import
ZArith
.
Require
Import
Rbase
.
Definition
unit
:=
unit
.
Parameter
label
:
Type
.
Parameter
at1
:
forall
(
a
:
Type
),
a
->
label
->
a
.
Implicit
Arguments
at1
.
Parameter
old
:
forall
(
a
:
Type
),
a
->
a
.
Implicit
Arguments
old
.
Inductive
ref
(
a
:
Type
)
:=
|
mk_ref
:
a
->
ref
a
.
Implicit
Arguments
mk_ref
.
Definition
contents
(
a
:
Type
)(
u
:
(
ref
a
))
:
a
:=
match
u
with
|
mk_ref
contents1
=>
contents1
end
.
Implicit
Arguments
contents
.
Parameter
map
:
forall
(
a
:
Type
)
(
b
:
Type
),
Type
.
Parameter
get
:
forall
(
a
:
Type
)
(
b
:
Type
),
(
map
a
b
)
->
a
->
b
.
Implicit
Arguments
get
.
Parameter
set
:
forall
(
a
:
Type
)
(
b
:
Type
),
(
map
a
b
)
->
a
->
b
->
(
map
a
b
).
Implicit
Arguments
set
.
Axiom
Select_eq
:
forall
(
a
:
Type
)
(
b
:
Type
),
forall
(
m
:
(
map
a
b
)),
forall
(
a1
:
a
)
(
a2
:
a
),
forall
(
b1
:
b
),
(
a1
=
a2
)
->
((
get
(
set
m
a1
b1
)
a2
)
=
b1
).
Axiom
Select_neq
:
forall
(
a
:
Type
)
(
b
:
Type
),
forall
(
m
:
(
map
a
b
)),
forall
(
a1
:
a
)
(
a2
:
a
),
forall
(
b1
:
b
),
(
~
(
a1
=
a2
))
->
((
get
(
set
m
a1
b1
)
a2
)
=
(
get
m
a2
)).
Parameter
const
:
forall
(
b
:
Type
)
(
a
:
Type
),
b
->
(
map
a
b
).
Set
Contextual
Implicit
.
Implicit
Arguments
const
.
Unset
Contextual
Implicit
.
Axiom
Const
:
forall
(
b
:
Type
)
(
a
:
Type
),
forall
(
b1
:
b
)
(
a1
:
a
),
((
get
(
const
(
b1
)
:
(
map
a
b
))
a1
)
=
b1
).
Inductive
array
(
a
:
Type
)
:=
|
mk_array
:
Z
->
(
map
Z
a
)
->
array
a
.
Implicit
Arguments
mk_array
.
Definition
elts
(
a
:
Type
)(
u
:
(
array
a
))
:
(
map
Z
a
)
:=
match
u
with
|
mk_array
_
elts1
=>
elts1
end
.
Implicit
Arguments
elts
.
Definition
length
(
a
:
Type
)(
u
:
(
array
a
))
:
Z
:=
match
u
with
|
mk_array
length1
_
=>
length1
end
.
Implicit
Arguments
length
.
Definition
get1
(
a
:
Type
)(
a1
:
(
array
a
))
(
i
:
Z
)
:
a
:=
(
get
(
elts
a1
)
i
).
Implicit
Arguments
get1
.
Definition
set1
(
a
:
Type
)(
a1
:
(
array
a
))
(
i
:
Z
)
(
v
:
a
)
:
(
array
a
)
:=
match
a1
with
|
mk_array
xcl0
_
=>
(
mk_array
xcl0
(
set
(
elts
a1
)
i
v
))
end
.
Implicit
Arguments
set1
.
Definition
sorted_sub
(
a
:
(
map
Z
Z
))
(
l
:
Z
)
(
u
:
Z
)
:
Prop
:=
forall
(
i1
:
Z
)
(
i2
:
Z
),
(((
l
<=
i1
)
%
Z
/
\
(
i1
<=
i2
)
%
Z
)
/
\
(
i2
<
u
)
%
Z
)
->
((
get
a
i1
)
<=
(
get
a
i2
))
%
Z
.
Definition
sorted_sub1
(
a
:
(
array
Z
))
(
l
:
Z
)
(
u
:
Z
)
:
Prop
:=
(
sorted_sub
(
elts
a
)
l
u
).
Definition
sorted
(
a
:
(
array
Z
))
:
Prop
:=
(
sorted_sub
(
elts
a
)
0
%
Z
(
length
a
)).
Definition
map_eq_sub
(
a
:
Type
)(
a1
:
(
map
Z
a
))
(
a2
:
(
map
Z
a
))
(
l
:
Z
)
(
u
:
Z
)
:
Prop
:=
forall
(
i
:
Z
),
((
l
<=
i
)
%
Z
/
\
(
i
<
u
)
%
Z
)
->
((
get
a1
i
)
=
(
get
a2
i
)).
Implicit
Arguments
map_eq_sub
.
Definition
exchange
(
a
:
Type
)(
a1
:
(
map
Z
a
))
(
a2
:
(
map
Z
a
))
(
i
:
Z
)
(
j
:
Z
)
:
Prop
:=
((
get
a1
i
)
=
(
get
a2
j
))
/
\
(((
get
a2
i
)
=
(
get
a1
j
))
/
\
forall
(
k
:
Z
),
((
~
(
k
=
i
))
/
\
~
(
k
=
j
))
->
((
get
a1
k
)
=
(
get
a2
k
))).
Implicit
Arguments
exchange
.
Axiom
exchange_set
:
forall
(
a
:
Type
),
forall
(
a1
:
(
map
Z
a
)),
forall
(
i
:
Z
)
(
j
:
Z
),
(
exchange
a1
(
set
(
set
a1
i
(
get
a1
j
))
j
(
get
a1
i
))
i
j
).
Inductive
permut_sub
{
a
:
Type
}
:
(
map
Z
a
)
->
(
map
Z
a
)
->
Z
->
Z
->
Prop
:=
|
permut_refl
:
forall
(
a1
:
(
map
Z
a
))
(
a2
:
(
map
Z
a
)),
forall
(
l
:
Z
)
(
u
:
Z
),
(
map_eq_sub
a1
a2
l
u
)
->
(
permut_sub
a1
a2
l
u
)
|
permut_sym
:
forall
(
a1
:
(
map
Z
a
))
(
a2
:
(
map
Z
a
)),
forall
(
l
:
Z
)
(
u
:
Z
),
(
permut_sub
a1
a2
l
u
)
->
(
permut_sub
a2
a1
l
u
)
|
permut_trans
:
forall
(
a1
:
(
map
Z
a
))
(
a2
:
(
map
Z
a
))
(
a3
:
(
map
Z
a
)),
forall
(
l
:
Z
)
(
u
:
Z
),
(
permut_sub
a1
a2
l
u
)
->
((
permut_sub
a2
a3
l
u
)
->
(
permut_sub
a1
a3
l
u
))
|
permut_exchange
:
forall
(
a1
:
(
map
Z
a
))
(
a2
:
(
map
Z
a
)),
forall
(
l
:
Z
)
(
u
:
Z
)
(
i
:
Z
)
(
j
:
Z
),
((
l
<=
i
)
%
Z
/
\
(
i
<
u
)
%
Z
)
->
(((
l
<=
j
)
%
Z
/
\
(
j
<
u
)
%
Z
)
->
((
exchange
a1
a2
i
j
)
->
(
permut_sub
a1
a2
l
u
))).
Implicit
Arguments
permut_sub
.
Axiom
permut_weakening
:
forall
(
a
:
Type
),
forall
(
a1
:
(
map
Z
a
))
(
a2
:
(
map
Z
a
)),
forall
(
l1
:
Z
)
(
r1
:
Z
)
(
l2
:
Z
)
(
r2
:
Z
),
(((
l1
<=
l2
)
%
Z
/
\
(
l2
<=
r2
)
%
Z
)
/
\
(
r2
<=
r1
)
%
Z
)
->
((
permut_sub
a1
a2
l2
r2
)
->
(
permut_sub
a1
a2
l1
r1
)).
Axiom
permut_eq
:
forall
(
a
:
Type
),
forall
(
a1
:
(
map
Z
a
))
(
a2
:
(
map
Z
a
)),
forall
(
l
:
Z
)
(
u
:
Z
),
(
l
<=
u
)
%
Z
->
((
permut_sub
a1
a2
l
u
)
->
forall
(
i
:
Z
),
((
i
<
l
)
%
Z
\
/
(
u
<=
i
)
%
Z
)
->
((
get
a2
i
)
=
(
get
a1
i
))).
Axiom
permut_exists
:
forall
(
a
:
Type
),
forall
(
a1
:
(
map
Z
a
))
(
a2
:
(
map
Z
a
)),
forall
(
l
:
Z
)
(
u
:
Z
),
(
permut_sub
a1
a2
l
u
)
->
forall
(
i
:
Z
),
((
l
<=
i
)
%
Z
/
\
(
i
<
u
)
%
Z
)
->
exists
j
:
Z
,
((
l
<=
j
)
%
Z
/
\
(
j
<
u
)
%
Z
)
/
\
((
get
a2
i
)
=
(
get
a1
j
)).
Definition
exchange1
(
a
:
Type
)(
a1
:
(
array
a
))
(
a2
:
(
array
a
))
(
i
:
Z
)
(
j
:
Z
)
:
Prop
:=
(
exchange
(
elts
a1
)
(
elts
a2
)
i
j
).
Implicit
Arguments
exchange1
.
Definition
permut_sub1
(
a
:
Type
)(
a1
:
(
array
a
))
(
a2
:
(
array
a
))
(
l
:
Z
)
(
u
:
Z
)
:
Prop
:=
(
permut_sub
(
elts
a1
)
(
elts
a2
)
l
u
).
Implicit
Arguments
permut_sub1
.
Definition
permut
(
a
:
Type
)(
a1
:
(
array
a
))
(
a2
:
(
array
a
))
:
Prop
:=
((
length
a1
)
=
(
length
a2
))
/
\
(
permut_sub
(
elts
a1
)
(
elts
a2
)
0
%
Z
(
length
a1
)).
Implicit
Arguments
permut
.
Axiom
exchange_permut
:
forall
(
a
:
Type
),
forall
(
a1
:
(
array
a
))
(
a2
:
(
array
a
))
(
i
:
Z
)
(
j
:
Z
),
(
exchange1
a1
a2
i
j
)
->
(((
length
a1
)
=
(
length
a2
))
->
(((
0
%
Z
<=
i
)
%
Z
/
\
(
i
<
(
length
a1
))
%
Z
)
->
(((
0
%
Z
<=
j
)
%
Z
/
\
(
j
<
(
length
a1
))
%
Z
)
->
(
permut
a1
a2
)))).
Definition
array_eq_sub
(
a
:
Type
)(
a1
:
(
array
a
))
(
a2
:
(
array
a
))
(
l
:
Z
)
(
u
:
Z
)
:
Prop
:=
(
map_eq_sub
(
elts
a1
)
(
elts
a2
)
l
u
).
Implicit
Arguments
array_eq_sub
.
Definition
array_eq
(
a
:
Type
)(
a1
:
(
array
a
))
(
a2
:
(
array
a
))
:
Prop
:=
((
length
a1
)
=
(
length
a2
))
/
\
(
array_eq_sub
a1
a2
0
%
Z
(
length
a1
)).
Implicit
Arguments
array_eq
.
Axiom
array_eq_sub_permut
:
forall
(
a
:
Type
),
forall
(
a1
:
(
array
a
))
(
a2
:
(
array
a
))
(
l
:
Z
)
(
u
:
Z
),
(
array_eq_sub
a1
a2
l
u
)
->
(
permut_sub1
a1
a2
l
u
).
Axiom
array_eq_permut
:
forall
(
a
:
Type
),
forall
(
a1
:
(
array
a
))
(
a2
:
(
array
a
)),
(
array_eq
a1
a2
)
->
(
permut
a1
a2
).
Theorem
WP_parameter_insertion_sort
:
forall
(
a
:
Z
),
forall
(
a1
:
(
map
Z
Z
)),
let
a2
:=
(
mk_array
a
a1
)
in
((
1
%
Z
<=
(
a
-
1
%
Z
)
%
Z
)
%
Z
->
forall
(
a3
:
(
map
Z
Z
)),
let
a4
:=
(
mk_array
a
a3
)
in
forall
(
i
:
Z
),
((
1
%
Z
<=
i
)
%
Z
/
\
(
i
<=
(
a
-
1
%
Z
)
%
Z
)
%
Z
)
->
(((
sorted_sub
a3
0
%
Z
i
)
/
\
(
permut
a4
a2
))
->
(((
0
%
Z
<=
i
)
%
Z
/
\
(
i
<
a
)
%
Z
)
->
let
result
:=
(
get
a3
i
)
in
((((
0
%
Z
<=
i
)
%
Z
/
\
(
i
<=
i
)
%
Z
)
/
\
((
permut
(
set1
a4
i
result
)
a2
)
/
\
((
forall
(
k1
:
Z
)
(
k2
:
Z
),
(((
0
%
Z
<=
k1
)
%
Z
/
\
(
k1
<=
k2
)
%
Z
)
/
\
(
k2
<=
i
)
%
Z
)
->
((
~
(
k1
=
i
))
->
((
~
(
k2
=
i
))
->
((
get
a3
k1
)
<=
(
get
a3
k2
))
%
Z
)))
/
\
forall
(
k
:
Z
),
(((
i
+
1
%
Z
)
%
Z
<=
k
)
%
Z
/
\
(
k
<=
i
)
%
Z
)
->
(
result
<
(
get
a3
k
))
%
Z
)))
->
forall
(
j
:
Z
),
forall
(
a5
:
(
map
Z
Z
)),
let
a6
:=
(
mk_array
a
a5
)
in
((((
0
%
Z
<=
j
)
%
Z
/
\
(
j
<=
i
)
%
Z
)
/
\
((
permut
(
set1
a6
j
result
)
a2
)
/
\
((
forall
(
k1
:
Z
)
(
k2
:
Z
),
(((
0
%
Z
<=
k1
)
%
Z
/
\
(
k1
<=
k2
)
%
Z
)
/
\
(
k2
<=
i
)
%
Z
)
->
((
~
(
k1
=
j
))
->
((
~
(
k2
=
j
))
->
((
get
a5
k1
)
<=
(
get
a5
k2
))
%
Z
)))
/
\
forall
(
k
:
Z
),
(((
j
+
1
%
Z
)
%
Z
<=
k
)
%
Z
/
\
(
k
<=
i
)
%
Z
)
->
(
result
<
(
get
a5
k
))
%
Z
)))
->
((
0
%
Z
<
j
)
%
Z
->
(((
0
%
Z
<=
(
j
-
1
%
Z
)
%
Z
)
%
Z
/
\
((
j
-
1
%
Z
)
%
Z
<
a
)
%
Z
)
->
((
result
<
(
get
a5
(
j
-
1
%
Z
)
%
Z
))
%
Z
->
(((
0
%
Z
<=
(
j
-
1
%
Z
)
%
Z
)
%
Z
/
\
((
j
-
1
%
Z
)
%
Z
<
a
)
%
Z
)
->
(((
0
%
Z
<=
j
)
%
Z
/
\
(
j
<
a
)
%
Z
)
->
forall
(
a7
:
(
map
Z
Z
)),
(
a7
=
(
set
a5
j
(
get
a5
(
j
-
1
%
Z
)
%
Z
)))
->
((
exchange
match
(
set1
(
mk_array
a
a7
)
(
j
-
1
%
Z
)
%
Z
result
)
with
|
mk_array
_
elts1
=>
elts1
end
match
(
set1
a6
j
result
)
with
|
mk_array
_
elts1
=>
elts1
end
(
j
-
1
%
Z
)
%
Z
j
)
->
forall
(
j1
:
Z
),
(
j1
=
(
j
-
1
%
Z
)
%
Z
)
->
forall
(
k1
:
Z
)
(
k2
:
Z
),
(((
0
%
Z
<=
k1
)
%
Z
/
\
(
k1
<=
k2
)
%
Z
)
/
\
(
k2
<=
i
)
%
Z
)
->
((
~
(
k1
=
j1
))
->
((
~
(
k2
=
j1
))
->
((
get
a7
k1
)
<=
(
get
a7
k2
))
%
Z
))))))))))))).
(
*
YOU
MAY
EDIT
THE
PROOF
BELOW
*
)
intuition
.
intuition
.
Qed
.
(
*
DO
NOT
EDIT
BELOW
*
)
examples/programs/insertion_sort/why3session.xml
0 → 100644
View file @
7cc748ed
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session
name=
"examples/programs/insertion_sort/why3session.xml"
>
<file
name=
"../insertion_sort.mlw"
verified=
"false"
expanded=
"true"
>
<theory
name=
"InsertionSort"
verified=
"false"
expanded=
"true"
>
<goal
name=
"WP_parameter insertion_sort"
expl=
"correctness of parameter insertion_sort"
sum=
"57abb18bfe1fef7ae3c780ae9f60e312"
proved=
"false"
expanded=
"true"
>
<transf
name=
"split_goal"
proved=
"false"
expanded=
"true"
>
<goal
name=
"WP_parameter insertion_sort.1"
expl=
"normal postcondition"
sum=
"9a49382bffbb4e30273c672cda27a668"
proved=
"true"
expanded=
"false"
>
<proof
prover=
"alt-ergo"
timelimit=
"30"
edited=
""
obsolete=
"false"
>
<result
status=
"valid"
time=
"0.03"
/>
</proof>
</goal>
<goal
name=
"WP_parameter insertion_sort.2"
expl=
"for loop initialization"
sum=
"809a90194c2e9cab08ec99f5e52fa2a0"
proved=
"true"
expanded=
"false"
>
<proof
prover=
"alt-ergo"
timelimit=
"30"
edited=
""
obsolete=
"false"
>
<result
status=
"valid"
time=
"0.02"
/>
</proof>
</goal>
<goal
name=
"WP_parameter insertion_sort.3"
expl=
"for loop preservation"
sum=
"0bdb9637597f868dccdcec0500ce3e2b"
proved=
"false"
expanded=
"true"
>
<transf
name=
"split_goal"
proved=
"false"
expanded=
"true"
>
<goal
name=
"WP_parameter insertion_sort.3.1"
expl=
"for loop preservation"
sum=
"5ff7b01940011090bc699d53f57737b8"
proved=
"true"
expanded=
"false"
>
<proof
prover=
"alt-ergo"
timelimit=
"30"
edited=
""
obsolete=
"false"
>
<result
status=
"valid"
time=
"0.03"
/>
</proof>
</goal>
<goal
name=
"WP_parameter insertion_sort.3.2"
expl=
"for loop preservation"
sum=
"614edd716a1dc50d6181208b158daeed"
proved=
"true"
expanded=
"false"
>
<proof
prover=
"cvc3"
timelimit=
"10"
edited=
""
obsolete=
"false"
>
<result
status=
"valid"
time=
"0.03"
/>
</proof>
</goal>
<goal
name=
"WP_parameter insertion_sort.3.3"
expl=
"for loop preservation"
sum=
"dbb435aef0a3fa10b328f732128d0eb4"
proved=
"true"
expanded=
"false"
>
<proof
prover=
"cvc3"
timelimit=
"10"
edited=
""
obsolete=
"false"
>
<result
status=
"valid"
time=
"0.03"
/>
</proof>
</goal>
<goal
name=
"WP_parameter insertion_sort.3.4"
expl=
"for loop preservation"
sum=
"911954256f309bee792b3556a15570ec"
proved=
"true"
expanded=
"false"
>
<proof
prover=
"cvc3"
timelimit=
"10"
edited=
""
obsolete=
"false"
>
<result
status=
"valid"
time=
"0.03"
/>
</proof>
</goal>
<goal
name=
"WP_parameter insertion_sort.3.5"
expl=
"for loop preservation"
sum=
"1c6bed13920144fd41a5c29f36060b09"
proved=
"true"
expanded=
"false"
>
<proof
prover=
"alt-ergo"
timelimit=
"30"
edited=
""
obsolete=
"false"
>
<result
status=
"valid"
time=
"0.03"
/>
</proof>
</goal>
<goal
name=
"WP_parameter insertion_sort.3.6"
expl=
"for loop preservation"
sum=
"ab9857e15f3d50af4d6a84a9ef1257dc"
proved=
"true"
expanded=
"false"
>
<proof
prover=
"cvc3"
timelimit=
"10"
edited=
""
obsolete=
"false"
>
<result
status=
"valid"
time=
"0.05"
/>
</proof>
</goal>
<goal
name=
"WP_parameter insertion_sort.3.7"
expl=
"for loop preservation"
sum=
"de17112a27461509c540d3e68db580ee"
proved=
"false"
expanded=
"true"
>
<transf
name=
"split_goal"
proved=
"false"
expanded=
"true"
>
<goal
name=
"WP_parameter insertion_sort.3.7.1"
expl=
"for loop preservation"
sum=
"8aae15882adf5e051121fe7e6238ff63"
proved=
"true"
expanded=
"false"
>
<proof
prover=
"alt-ergo"
timelimit=
"10"
edited=
""
obsolete=
"false"
>
<result
status=
"valid"
time=
"0.03"
/>
</proof>
</goal>
<goal
name=
"WP_parameter insertion_sort.3.7.2"
expl=
"for loop preservation"
sum=
"065d26a4bca6a8c1e291cc31659d10e2"
proved=
"true"
expanded=
"false"
>
<proof
prover=
"alt-ergo"
timelimit=
"10"
edited=
""
obsolete=
"false"
>
<result
status=
"valid"
time=
"0.03"
/>
</proof>
</goal>
<goal
name=
"WP_parameter insertion_sort.3.7.3"
expl=
"for loop preservation"
sum=
"3aa1af1a36f6d647b47b87fbbf9c36d5"
proved=
"true"
expanded=
"false"
>
<proof
prover=
"coq"
timelimit=
"10"
edited=
"insertion_sort.mlw_InsertionSort_WP_parameter insertion_sort_1.v"
obsolete=
"false"
>
<result
status=
"valid"
time=
"0.56"
/>
</proof>
</goal>
<goal
name=
"WP_parameter insertion_sort.3.7.4"
expl=
"for loop preservation"
sum=
"25e0f93b5176e5c428dd7ef607364586"
proved=
"false"
expanded=
"true"
>
<proof
prover=
"coq"
timelimit=
"20"
edited=
"insertion_sort.mlw_InsertionSort_WP_parameter insertion_sort_2.v"
obsolete=
"false"
><undone/>
</proof>
<proof
prover=
"cvc3"
timelimit=
"10"
edited=
""
obsolete=
"false"
>
<result
status=
"timeout"
time=
"20.08"
/>
</proof>
<proof
prover=
"alt-ergo"
timelimit=
"10"
edited=
""
obsolete=
"false"
>
<result
status=
"timeout"
time=
"20.08"
/>
</proof>
<proof
prover=
"z3"
timelimit=
"10"
edited=
""
obsolete=
"false"
>
<result
status=
"timeout"
time=
"20.14"
/>
</proof>
</goal>
<goal
name=
"WP_parameter insertion_sort.3.7.5"
expl=
"for loop preservation"
sum=
"5d5f15aac1f75e53c3d1084719739106"
proved=
"true"
expanded=
"false"
>
<proof
prover=
"cvc3"
timelimit=
"10"
edited=
""
obsolete=
"false"
>
<result
status=
"valid"
time=
"0.04"
/>
</proof>
</goal>
</transf>
</goal>
<goal
name=
"WP_parameter insertion_sort.3.8"
expl=
"for loop preservation"
sum=
"8910aa1a449e6ba4df5144071d6d0557"
proved=
"true"
expanded=
"false"
>
<transf
name=
"split_goal"
proved=
"true"
expanded=
"false"
>
<goal
name=
"WP_parameter insertion_sort.3.8.1"
expl=
"for loop preservation"
sum=
"ab2edede5624001b8a961609b824cac5"
proved=
"true"
expanded=
"false"
>
<proof
prover=
"alt-ergo"
timelimit=
"10"
edited=
""
obsolete=
"false"
>
<result
status=
"valid"
time=
"0.02"
/>
</proof>
</goal>
<goal
name=
"WP_parameter insertion_sort.3.8.2"
expl=
"for loop preservation"
sum=
"55e4224cd75041c848cf78f7500c0a05"
proved=
"true"
expanded=
"false"
>
<proof
prover=
"alt-ergo"
timelimit=
"10"
edited=
""
obsolete=
"false"
>
<result
status=
"valid"
time=
"0.02"
/>
</proof>
</goal>
</transf>
</goal>
<goal
name=
"WP_parameter insertion_sort.3.9"
expl=
"for loop preservation"
sum=
"9844490bb23da5964fe59d1e738f61b3"
proved=
"true"
expanded=
"false"
>
<proof
prover=
"alt-ergo"
timelimit=
"30"
edited=
""
obsolete=
"false"
>
<result
status=
"valid"
time=
"0.02"
/>
</proof>
</goal>
<goal
name=
"WP_parameter insertion_sort.3.10"
expl=
"for loop preservation"
sum=
"5d9c10bee007d5031f0c5fdd17c48651"
proved=
"true"
expanded=
"false"
>
<proof
prover=
"z3"
timelimit=
"10"
edited=
""
obsolete=
"false"
>
<result
status=
"valid"
time=
"0.02"
/>
</proof>
</goal>
<goal
name=
"WP_parameter insertion_sort.3.11"
expl=
"for loop preservation"
sum=
"b0d6b49ac2bbbbbd65a02fe0034cc3b6"
proved=
"true"
expanded=
"false"
>
<proof
prover=
"cvc3"
timelimit=
"10"
edited=
""
obsolete=
"false"
>
<result
status=
"valid"
time=
"0.05"
/>
</proof>
<proof
prover=
"z3"
timelimit=
"10"
edited=
""
obsolete=
"false"
>