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
c053d61f
Commit
c053d61f
authored
Sep 08, 2011
by
Jean-Christophe Filliâtre
Browse files
find: updated proof
parent
0481a32c
Changes
4
Expand all
Hide whitespace changes
Inline
Side-by-side
examples/programs/find/find_WP_FIND_WP_parameter_find_1.v
deleted
100644 → 0
View file @
0481a32c
(
*
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
mark
:
Type
.
Parameter
at1
:
forall
(
a
:
Type
),
a
->
mark
->
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
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
).
Parameter
usN
:
Z
.
Parameter
f
:
Z
.
Axiom
f_N_range
:
(
1
%
Z
<=
(
f
))
%
Z
/
\
((
f
)
<=
(
usN
))
%
Z
.
Definition
found
(
a
:
(
array
Z
))
:
Prop
:=
forall
(
p
:
Z
)
(
q
:
Z
),
((((
1
%
Z
<=
p
)
%
Z
/
\
(
p
<=
(
f
))
%
Z
)
/
\
((
f
)
<=
q
)
%
Z
)
/
\
(
q
<=
(
usN
))
%
Z
)
->
(((
get1
a
p
)
<=
(
get1
a
(
f
)))
%
Z
/
\
((
get1
a
(
f
))
<=
(
get1
a
q
))
%
Z
).
Definition
m_invariant
(
m
:
Z
)
(
a
:
(
array
Z
))
:
Prop
:=
(
m
<=
(
f
))
%
Z
/
\
forall
(
p
:
Z
)
(
q
:
Z
),
((((
1
%
Z
<=
p
)
%
Z
/
\
(
p
<
m
)
%
Z
)
/
\
(
m
<=
q
)
%
Z
)
/
\
(
q
<=
(
usN
))
%
Z
)
->
((
get1
a
p
)
<=
(
get1
a
q
))
%
Z
.
Definition
n_invariant
(
n
:
Z
)
(
a
:
(
array
Z
))
:
Prop
:=
((
f
)
<=
n
)
%
Z
/
\
forall
(
p
:
Z
)
(
q
:
Z
),
((((
1
%
Z
<=
p
)
%
Z
/
\
(
p
<=
n
)
%
Z
)
/
\
(
n
<
q
)
%
Z
)
/
\
(
q
<=
(
usN
))
%
Z
)
->
((
get1
a
p
)
<=
(
get1
a
q
))
%
Z
.
Definition
i_invariant
(
m
:
Z
)
(
n
:
Z
)
(
i
:
Z
)
(
r
:
Z
)
(
a
:
(
array
Z
))
:
Prop
:=
(
m
<=
i
)
%
Z
/
\
((
forall
(
p
:
Z
),
((
1
%
Z
<=
p
)
%
Z
/
\
(
p
<
i
)
%
Z
)
->
((
get1
a
p
)
<=
r
)
%
Z
)
/
\
((
i
<=
n
)
%
Z
->
exists
p
:
Z
,
((
i
<=
p
)
%
Z
/
\
(
p
<=
n
)
%
Z
)
/
\
(
r
<=
(
get1
a
p
))
%
Z
)).
Definition
j_invariant
(
m
:
Z
)
(
n
:
Z
)
(
j
:
Z
)
(
r
:
Z
)
(
a
:
(
array
Z
))
:
Prop
:=
(
j
<=
n
)
%
Z
/
\
((
forall
(
q
:
Z
),
((
j
<
q
)
%
Z
/
\
(
q
<=
(
usN
))
%
Z
)
->
(
r
<=
(
get1
a
q
))
%
Z
)
/
\
((
m
<=
j
)
%
Z
->
exists
q
:
Z
,
((
m
<=
q
)
%
Z
/
\
(
q
<=
j
)
%
Z
)
/
\
((
get1
a
q
)
<=
r
)
%
Z
)).
Definition
termination
(
i
:
Z
)
(
j
:
Z
)
(
i0
:
Z
)
(
j0
:
Z
)
(
r
:
Z
)
(
a
:
(
array
Z
))
:
Prop
:=
((
i0
<
i
)
%
Z
/
\
(
j
<
j0
)
%
Z
)
\
/
(((
i
<=
(
f
))
%
Z
/
\
((
f
)
<=
j
)
%
Z
)
/
\
((
get1
a
(
f
))
=
r
)).
Theorem
WP_parameter_find
:
forall
(
a
:
Z
),
forall
(
a1
:
(
map
Z
Z
)),
let
a2
:=
(
mk_array
a
a1
)
in
((
a
=
((
usN
)
+
1
%
Z
)
%
Z
)
->
forall
(
n
:
Z
),
forall
(
m
:
Z
),
forall
(
a3
:
(
map
Z
Z
)),
let
a4
:=
(
mk_array
a
a3
)
in
(((
m_invariant
m
a4
)
/
\
((
n_invariant
n
a4
)
/
\
((
permut
a4
a2
)
/
\
((
1
%
Z
<=
m
)
%
Z
/
\
(
n
<=
(
usN
))
%
Z
))))
->
((
m
<
n
)
%
Z
->
(((
0
%
Z
<=
(
f
))
%
Z
/
\
((
f
)
<
a
)
%
Z
)
->
let
result
:=
(
get
a3
(
f
))
in
forall
(
j
:
Z
),
forall
(
i
:
Z
),
forall
(
a5
:
(
map
Z
Z
)),
let
a6
:=
(
mk_array
a
a5
)
in
(((
i_invariant
m
n
i
result
a6
)
/
\
((
j_invariant
m
n
j
result
a6
)
/
\
((
m_invariant
m
a6
)
/
\
((
n_invariant
n
a6
)
/
\
((
0
%
Z
<=
j
)
%
Z
/
\
((
i
<=
((
usN
)
+
1
%
Z
)
%
Z
)
%
Z
/
\
((
termination
i
j
m
n
result
a6
)
/
\
(
permut
a6
a2
))))))))
->
((
i
<=
j
)
%
Z
->
forall
(
i1
:
Z
),
((
i_invariant
m
n
i1
result
a6
)
/
\
(((
i
<=
i1
)
%
Z
/
\
(
i1
<=
n
)
%
Z
)
/
\
(
termination
i1
j
m
n
result
a6
)))
->
(((
0
%
Z
<=
i1
)
%
Z
/
\
(
i1
<
a
)
%
Z
)
->
((
~
((
get
a5
i1
)
<
result
)
%
Z
)
->
forall
(
j1
:
Z
),
((
j_invariant
m
n
j1
result
a6
)
/
\
((
j1
<=
j
)
%
Z
/
\
((
m
<=
j1
)
%
Z
/
\
(
termination
i1
j1
m
n
result
a6
))))
->
(((
0
%
Z
<=
j1
)
%
Z
/
\
(
j1
<
a
)
%
Z
)
->
((
~
(
result
<
(
get
a5
j1
))
%
Z
)
->
((((
get
a5
j1
)
<=
result
)
%
Z
/
\
(
result
<=
(
get
a5
i1
))
%
Z
)
->
((
i1
<=
j1
)
%
Z
->
(((
0
%
Z
<=
i1
)
%
Z
/
\
(
i1
<
a
)
%
Z
)
->
(((
0
%
Z
<=
j1
)
%
Z
/
\
(
j1
<
a
)
%
Z
)
->
(((
0
%
Z
<=
i1
)
%
Z
/
\
(
i1
<
a
)
%
Z
)
->
forall
(
a7
:
(
map
Z
Z
)),
(
a7
=
(
set
a5
i1
(
get
a5
j1
)))
->
(((
0
%
Z
<=
j1
)
%
Z
/
\
(
j1
<
a
)
%
Z
)
->
forall
(
a8
:
(
map
Z
Z
)),
(
a8
=
(
set
a7
j1
(
get
a5
i1
)))
->
((
exchange
a8
a5
i1
j1
)
->
(((
get
a8
i1
)
<=
result
)
%
Z
->
((
result
<=
(
get
a8
j1
))
%
Z
->
forall
(
i2
:
Z
),
(
i2
=
(
i1
+
1
%
Z
)
%
Z
)
->
forall
(
j2
:
Z
),
(
j2
=
(
j1
-
1
%
Z
)
%
Z
)
->
(
permut
(
mk_array
a
a8
)
a2
)))))))))))))))))))).
(
*
YOU
MAY
EDIT
THE
PROOF
BELOW
*
)
intuition
.
intuition
.
unfold
permut
;
simpl
.
intuition
.
apply
permut_trans
with
a5
.
apply
permut_exchange
with
i1
j1
;
intuition
.
red
in
H17
.
simpl
in
H17
.
intuition
.
Qed
.
(
*
DO
NOT
EDIT
BELOW
*
)
examples/programs/find/find_WP_FIND_WP_parameter_find_2.v
deleted
100644 → 0
View file @
0481a32c
(
*
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
mark
:
Type
.
Parameter
at1
:
forall
(
a
:
Type
),
a
->
mark
->
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
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
).
Parameter
usN
:
Z
.
Parameter
f
:
Z
.
Axiom
f_N_range
:
(
1
%
Z
<=
(
f
))
%
Z
/
\
((
f
)
<=
(
usN
))
%
Z
.
Definition
found
(
a
:
(
array
Z
))
:
Prop
:=
forall
(
p
:
Z
)
(
q
:
Z
),
((((
1
%
Z
<=
p
)
%
Z
/
\
(
p
<=
(
f
))
%
Z
)
/
\
((
f
)
<=
q
)
%
Z
)
/
\
(
q
<=
(
usN
))
%
Z
)
->
(((
get1
a
p
)
<=
(
get1
a
(
f
)))
%
Z
/
\
((
get1
a
(
f
))
<=
(
get1
a
q
))
%
Z
).
Definition
m_invariant
(
m
:
Z
)
(
a
:
(
array
Z
))
:
Prop
:=
(
m
<=
(
f
))
%
Z
/
\
forall
(
p
:
Z
)
(
q
:
Z
),
((((
1
%
Z
<=
p
)
%
Z
/
\
(
p
<
m
)
%
Z
)
/
\
(
m
<=
q
)
%
Z
)
/
\
(
q
<=
(
usN
))
%
Z
)
->
((
get1
a
p
)
<=
(
get1
a
q
))
%
Z
.
Definition
n_invariant
(
n
:
Z
)
(
a
:
(
array
Z
))
:
Prop
:=
((
f
)
<=
n
)
%
Z
/
\
forall
(
p
:
Z
)
(
q
:
Z
),
((((
1
%
Z
<=
p
)
%
Z
/
\
(
p
<=
n
)
%
Z
)
/
\
(
n
<
q
)
%
Z
)
/
\
(
q
<=
(
usN
))
%
Z
)
->
((
get1
a
p
)
<=
(
get1
a
q
))
%
Z
.
Definition
i_invariant
(
m
:
Z
)
(
n
:
Z
)
(
i
:
Z
)
(
r
:
Z
)
(
a
:
(
array
Z
))
:
Prop
:=
(
m
<=
i
)
%
Z
/
\
((
forall
(
p
:
Z
),
((
1
%
Z
<=
p
)
%
Z
/
\
(
p
<
i
)
%
Z
)
->
((
get1
a
p
)
<=
r
)
%
Z
)
/
\
((
i
<=
n
)
%
Z
->
exists
p
:
Z
,
((
i
<=
p
)
%
Z
/
\
(
p
<=
n
)
%
Z
)
/
\
(
r
<=
(
get1
a
p
))
%
Z
)).
Definition
j_invariant
(
m
:
Z
)
(
n
:
Z
)
(
j
:
Z
)
(
r
:
Z
)
(
a
:
(
array
Z
))
:
Prop
:=
(
j
<=
n
)
%
Z
/
\
((
forall
(
q
:
Z
),
((
j
<
q
)
%
Z
/
\
(
q
<=
(
usN
))
%
Z
)
->
(
r
<=
(
get1
a
q
))
%
Z
)
/
\
((
m
<=
j
)
%
Z
->
exists
q
:
Z
,
((
m
<=
q
)
%
Z
/
\
(
q
<=
j
)
%
Z
)
/
\
((
get1
a
q
)
<=
r
)
%
Z
)).
Definition
termination
(
i
:
Z
)
(
j
:
Z
)
(
i0
:
Z
)
(
j0
:
Z
)
(
r
:
Z
)
(
a
:
(
array
Z
))
:
Prop
:=
((
i0
<
i
)
%
Z
/
\
(
j
<
j0
)
%
Z
)
\
/
(((
i
<=
(
f
))
%
Z
/
\
((
f
)
<=
j
)
%
Z
)
/
\
((
get1
a
(
f
))
=
r
)).
Theorem
WP_parameter_find
:
forall
(
a
:
Z
),
forall
(
a1
:
(
map
Z
Z
)),
let
a2
:=
(
mk_array
a
a1
)
in
((
a
=
((
usN
)
+
1
%
Z
)
%
Z
)
->
forall
(
n
:
Z
),
forall
(
m
:
Z
),
forall
(
a3
:
(
map
Z
Z
)),
let
a4
:=
(
mk_array
a
a3
)
in
((((
m
<=
(
f
))
%
Z
/
\
forall
(
p
:
Z
)
(
q
:
Z
),
((((
1
%
Z
<=
p
)
%
Z
/
\
(
p
<
m
)
%
Z
)
/
\
(
m
<=
q
)
%
Z
)
/
\
(
q
<=
(
usN
))
%
Z
)
->
((
get1
a4
p
)
<=
(
get1
a4
q
))
%
Z
)
/
\
((((
f
)
<=
n
)
%
Z
/
\
forall
(
p
:
Z
)
(
q
:
Z
),
((((
1
%
Z
<=
p
)
%
Z
/
\
(
p
<=
n
)
%
Z
)
/
\
(
n
<
q
)
%
Z
)
/
\
(
q
<=
(
usN
))
%
Z
)
->
((
get1
a4
p
)
<=
(
get1
a4
q
))
%
Z
)
/
\
((((
length
a4
)
=
(
length
a2
))
/
\
(
permut_sub
(
elts
a4
)
(
elts
a2
)
0
%
Z
(
length
a4
)))
/
\
(((
1
%
Z
<
m
)
%
Z
\
/
(
1
%
Z
=
m
))
/
\
((
n
<
(
usN
))
%
Z
\
/
(
n
=
(
usN
)))))))
->
((
m
<
n
)
%
Z
->
((((
0
%
Z
<
(
f
))
%
Z
\
/
(
0
%
Z
=
(
f
)))
/
\
((
f
)
<
a
)
%
Z
)
->
let
result
:=
(
get
a3
(
f
))
in
forall
(
j
:
Z
),
forall
(
i
:
Z
),
forall
(
a5
:
(
map
Z
Z
)),
let
a6
:=
(
mk_array
a
a5
)
in
((((
m
<=
i
)
%
Z
/
\
((
forall
(
p
:
Z
),
((
1
%
Z
<=
p
)
%
Z
/
\
(
p
<
i
)
%
Z
)
->
((
get1
a6
p
)
<=
result
)
%
Z
)
/
\
((
i
<=
n
)
%
Z
->
exists
p
:
Z
,
((
i
<=
p
)
%
Z
/
\
(
p
<=
n
)
%
Z
)
/
\
(
result
<=
(
get1
a6
p
))
%
Z
)))
/
\
(((
j
<=
n
)
%
Z
/
\
((
forall
(
q
:
Z
),
((
j
<
q
)
%
Z
/
\
(
q
<=
(
usN
))
%
Z
)
->
(
result
<=
(
get1
a6
q
))
%
Z
)
/
\
((
m
<=
j
)
%
Z
->
exists
q
:
Z
,
((
m
<=
q
)
%
Z
/
\
(
q
<=
j
)
%
Z
)
/
\
((
get1
a6
q
)
<=
result
)
%
Z
)))
/
\
(((
m
<=
(
f
))
%
Z
/
\
forall
(
p
:
Z
)
(
q
:
Z
),
((((
1
%
Z
<=
p
)
%
Z
/
\
(
p
<
m
)
%
Z
)
/
\
(
m
<=
q
)
%
Z
)
/
\
(
q
<=
(
usN
))
%
Z
)
->
((
get1
a6
p
)
<=
(
get1
a6
q
))
%
Z
)
/
\
((((
f
)
<=
n
)
%
Z
/
\
forall
(
p
:
Z
)
(
q
:
Z
),
((((
1
%
Z
<=
p
)
%
Z
/
\
(
p
<=
n
)
%
Z
)
/
\
(
n
<
q
)
%
Z
)
/
\
(
q
<=
(
usN
))
%
Z
)
->
((
get1
a6
p
)
<=
(
get1
a6
q
))
%
Z
)
/
\
(((
0
%
Z
<
j
)
%
Z
\
/
(
0
%
Z
=
j
))
/
\
(((
i
<
((
usN
)
+
1
%
Z
)
%
Z
)
%
Z
\
/
(
i
=
((
usN
)
+
1
%
Z
)
%
Z
))
/
\
((((
m
<
i
)
%
Z
/
\
(
j
<
n
)
%
Z
)
\
/
(((
i
<=
(
f
))
%
Z
/
\
((
f
)
<=
j
)
%
Z
)
/
\
((
get1
a6
(
f
))
=
result
)))
/
\
(((
length
a6
)
=
(
length
a2
))
/
\
(
permut_sub
(
elts
a6
)
(
elts
a2
)
0
%
Z
(
length
a6
))))))))))
->
(((
i
<
j
)
%
Z
\
/
(
i
=
j
))
->
forall
(
i1
:
Z
),
(((
m
<=
i1
)
%
Z
/
\
((
forall
(
p
:
Z
),
((
1
%
Z
<=
p
)
%
Z
/
\
(
p
<
i1
)
%
Z
)
->
((
get1
a6
p
)
<=
result
)
%
Z
)
/
\
((
i1
<=
n
)
%
Z
->
exists
p
:
Z
,
((
i1
<=
p
)
%
Z
/
\
(
p
<=
n
)
%
Z
)
/
\
(
result
<=
(
get1
a6
p
))
%
Z
)))
/
\
((((
i
<
i1
)
%
Z
\
/
(
i
=
i1
))
/
\
((
i1
<
n
)
%
Z
\
/
(
i1
=
n
)))
/
\
(((
m
<
i1
)
%
Z
/
\
(
j
<
n
)
%
Z
)
\
/
(((
i1
<=
(
f
))
%
Z
/
\
((
f
)
<=
j
)
%
Z
)
/
\
((
get1
a6
(
f
))
=
result
)))))
->
((((
0
%
Z
<
i1
)
%
Z
\
/
(
0
%
Z
=
i1
))
/
\
(
i1
<
a
)
%
Z
)
->
((
~
((
get
a5
i1
)
<
result
)
%
Z
)
->
forall
(
j1
:
Z
),
(((
j1
<=
n
)
%
Z
/
\
((
forall
(
q
:
Z
),
((
j1
<
q
)
%
Z
/
\
(
q
<=
(
usN
))
%
Z
)
->
(
result
<=
(
get1
a6
q
))
%
Z
)
/
\
((
m
<=
j1
)
%
Z
->
exists
q
:
Z
,
((
m
<=
q
)
%
Z
/
\
(
q
<=
j1
)
%
Z
)
/
\
((
get1
a6
q
)
<=
result
)
%
Z
)))
/
\
(((
j1
<
j
)
%
Z
\
/
(
j1
=
j
))
/
\
(((
m
<
j1
)
%
Z
\
/
(
m
=
j1
))
/
\
(((
m
<
i1
)
%
Z
/
\
(
j1
<
n
)
%
Z
)
\
/
(((
i1
<=
(
f
))
%
Z
/
\
((
f
)
<=
j1
)
%
Z
)
/
\
((
get1
a6
(
f
))
=
result
))))))
->
((((
0
%
Z
<
j1
)
%
Z
\
/
(
0
%
Z
=
j1
))
/
\
(
j1
<
a
)
%
Z
)
->
((
~
(
result
<
(
get
a5
j1
))
%
Z
)
->
(((((
get
a5
j1
)
<
result
)
%
Z
\
/
((
get
a5
j1
)
=
result
))
/
\
((
result
<
(
get
a5
i1
))
%
Z
\
/
(
result
=
(
get
a5
i1
))))
->
(((
i1
<
j1
)
%
Z
\
/
(
i1
=
j1
))
->
((((
0
%
Z
<
i1
)
%
Z
\
/
(
0
%
Z
=
i1
))
/
\
(
i1
<
a
)
%
Z
)
->
((((
0
%
Z
<
j1
)
%
Z
\
/
(
0
%
Z
=
j1
))
/
\
(
j1
<
a
)
%
Z
)
->
((((
0
%
Z
<
i1
)
%
Z
\
/
(
0
%
Z
=
i1
))
/
\
(
i1
<
a
)
%
Z
)
->
forall
(
a7
:
(
map
Z
Z
)),
(
a7
=
(
set
a5
i1
(
get
a5
j1
)))
->
((((
0
%
Z
<
j1
)
%
Z
\
/
(
0
%
Z
=
j1
))
/
\
(
j1
<
a
)
%
Z
)
->
forall
(
a8
:
(
map
Z
Z
)),
(
a8
=
(
set
a7
j1
(
get
a5
i1
)))
->
((((
get
a8
i1
)
=
(
get
a5
j1
))
/
\
(((
get
a5
i1
)
=
(
get
a8
j1
))
/
\
forall
(
k
:
Z
),
((
~
(
k
=
i1
))
/
\
~
(
k
=
j1
))
->
((
get
a8
k
)
=
(
get
a5
k
))))
->
((((
get
a8
i1
)
<
result
)
%
Z
\
/
((
get
a8
i1
)
=
result
))
->
(((
result
<
(
get
a8
j1
))
%
Z
\
/
(
result
=
(
get
a8
j1
)))
->
forall
(
i2
:
Z
),
(
i2
=
(
i1
+
1
%
Z
)
%
Z
)
->
forall
(
j2
:
Z
),
(
j2
=
(
j1
+
(
-
1
%
Z
)
%
Z
)
%
Z
)
->
forall
(
p
:
Z
),
((
1
%
Z
<=
p
)
%
Z
/
\
(
p
<
i2
)
%
Z
)
->
((
get1
(
mk_array
a
a8
)
p
)
<=
result
)
%
Z
))))))))))))))))))).
(
*
YOU
MAY
EDIT
THE
PROOF
BELOW
*
)
unfold
get1
;
simpl
;
intros
.
destruct
H19
.
rewrite
H19
in
*
;
clear
H19
.
destruct
H25
.
rewrite
<-
H19
in
*
;
clear
H19
.
Qed
.
(
*
DO
NOT
EDIT
BELOW
*
)
examples/programs/find/find_WP_FIND_WP_parameter_find_
3
.v
→
examples/programs/find/find_WP_FIND_WP_parameter_find_
4
.v
View file @
c053d61f
...
...
@@ -6,11 +6,11 @@ Definition unit := unit.
Parameter
mark
:
Type
.
Parameter
at1
:
forall
(
a
:
Type
),
a
->
mark
->
a
.
Parameter
at1
:
forall
(
a
:
Type
),
a
->
mark
->
a
.
Implicit
Arguments
at1
.
Parameter
old
:
forall
(
a
:
Type
),
a
->
a
.
Parameter
old
:
forall
(
a
:
Type
),
a
->
a
.
Implicit
Arguments
old
.
...
...
@@ -26,11 +26,11 @@ Implicit Arguments contents.
Parameter
map
:
forall
(
a
:
Type
)
(
b
:
Type
),
Type
.
Parameter
get
:
forall
(
a
:
Type
)
(
b
:
Type
),
(
map
a
b
)
->
a
->
b
.
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
).
Parameter
set
:
forall
(
a
:
Type
)
(
b
:
Type
),
(
map
a
b
)
->
a
->
b
->
(
map
a
b
).
Implicit
Arguments
set
.
...
...
@@ -42,7 +42,7 @@ 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
).
Parameter
const
:
forall
(
b
:
Type
)
(
a
:
Type
),
b
->
(
map
a
b
).
Set
Contextual
Implicit
.
Implicit
Arguments
const
.
...
...
@@ -107,8 +107,8 @@ Axiom permut_weakening : forall (a:Type), forall (a1:(map Z a)) (a2:(map 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
))
)
.