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
8ac305a7
Commit
8ac305a7
authored
Jul 08, 2014
by
Guillaume Melquiond
Browse files
Remove useless Coq proofs.
parent
d93d8a61
Changes
166
Expand all
Hide whitespace changes
Inline
Side-by-side
examples/algo63/algo63_Algo63_WP_parameter_partition_1.v
deleted
100644 → 0
View file @
d93d8a61
(
*
This
file
is
generated
by
Why3
'
s
Coq
8.4
driver
*
)
(
*
Beware
!
Only
edit
allowed
sections
below
*
)
Require
Import
BuiltIn
.
Require
BuiltIn
.
Require
int
.
Int
.
Require
map
.
Map
.
Require
map
.
MapPermut
.
(
*
Why3
assumption
*
)
Definition
unit
:=
unit
.
(
*
Why3
assumption
*
)
Inductive
ref
(
a
:
Type
)
{
a_WT
:
WhyType
a
}
:=
|
mk_ref
:
a
->
ref
a
.
Axiom
ref_WhyType
:
forall
(
a
:
Type
)
{
a_WT
:
WhyType
a
}
,
WhyType
(
ref
a
).
Existing
Instance
ref_WhyType
.
Implicit
Arguments
mk_ref
[[
a
]
[
a_WT
]].
(
*
Why3
assumption
*
)
Definition
contents
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
(
v
:
(
@
ref
a
a_WT
))
:
a
:=
match
v
with
|
(
mk_ref
x
)
=>
x
end
.
(
*
Why3
assumption
*
)
Inductive
array
(
a
:
Type
)
{
a_WT
:
WhyType
a
}
:=
|
mk_array
:
Z
->
(
@
map
.
Map
.
map
Z
_
a
a_WT
)
->
array
a
.
Axiom
array_WhyType
:
forall
(
a
:
Type
)
{
a_WT
:
WhyType
a
}
,
WhyType
(
array
a
).
Existing
Instance
array_WhyType
.
Implicit
Arguments
mk_array
[[
a
]
[
a_WT
]].
(
*
Why3
assumption
*
)
Definition
elts
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
(
v
:
(
@
array
a
a_WT
))
:
(
@
map
.
Map
.
map
Z
_
a
a_WT
)
:=
match
v
with
|
(
mk_array
x
x1
)
=>
x1
end
.
(
*
Why3
assumption
*
)
Definition
length
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
(
v
:
(
@
array
a
a_WT
))
:
Z
:=
match
v
with
|
(
mk_array
x
x1
)
=>
x
end
.
(
*
Why3
assumption
*
)
Definition
get
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
(
a1
:
(
@
array
a
a_WT
))
(
i
:
Z
)
:
a
:=
(
map
.
Map
.
get
(
elts
a1
)
i
).
(
*
Why3
assumption
*
)
Definition
set
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
(
a1
:
(
@
array
a
a_WT
))
(
i
:
Z
)
(
v
:
a
)
:
(
@
array
a
a_WT
)
:=
(
mk_array
(
length
a1
)
(
map
.
Map
.
set
(
elts
a1
)
i
v
)).
(
*
Why3
assumption
*
)
Definition
make
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
(
n
:
Z
)
(
v
:
a
)
:
(
@
array
a
a_WT
)
:=
(
mk_array
n
(
map
.
Map
.
const
v
:
(
@
map
.
Map
.
map
Z
_
a
a_WT
))).
(
*
Why3
assumption
*
)
Definition
map_eq_sub
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
(
a1
:
(
@
map
.
Map
.
map
Z
_
a
a_WT
))
(
a2
:
(
@
map
.
Map
.
map
Z
_
a
a_WT
))
(
l
:
Z
)
(
u
:
Z
)
:
Prop
:=
forall
(
i
:
Z
),
((
l
<=
i
)
%
Z
/
\
(
i
<
u
)
%
Z
)
->
((
map
.
Map
.
get
a1
i
)
=
(
map
.
Map
.
get
a2
i
)).
(
*
Why3
assumption
*
)
Definition
array_eq_sub
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
(
a1
:
(
@
array
a
a_WT
))
(
a2
:
(
@
array
a
a_WT
))
(
l
:
Z
)
(
u
:
Z
)
:
Prop
:=
((
length
a1
)
=
(
length
a2
))
/
\
(((
0
%
Z
<=
l
)
%
Z
/
\
(
l
<=
(
length
a1
))
%
Z
)
/
\
(((
0
%
Z
<=
u
)
%
Z
/
\
(
u
<=
(
length
a1
))
%
Z
)
/
\
(
map_eq_sub
(
elts
a1
)
(
elts
a2
)
l
u
))).
(
*
Why3
assumption
*
)
Definition
array_eq
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
(
a1
:
(
@
array
a
a_WT
))
(
a2
:
(
@
array
a
a_WT
))
:
Prop
:=
((
length
a1
)
=
(
length
a2
))
/
\
(
map_eq_sub
(
elts
a1
)
(
elts
a2
)
0
%
Z
(
length
a1
)).
(
*
Why3
assumption
*
)
Definition
exchange
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
(
a1
:
(
@
array
a
a_WT
))
(
a2
:
(
@
array
a
a_WT
))
(
i
:
Z
)
(
j
:
Z
)
:
Prop
:=
((
length
a1
)
=
(
length
a2
))
/
\
(((
0
%
Z
<=
i
)
%
Z
/
\
(
i
<
(
length
a1
))
%
Z
)
/
\
(((
0
%
Z
<=
j
)
%
Z
/
\
(
j
<
(
length
a1
))
%
Z
)
/
\
(((
get
a1
i
)
=
(
get
a2
j
))
/
\
(((
get
a1
j
)
=
(
get
a2
i
))
/
\
forall
(
k
:
Z
),
((
0
%
Z
<=
k
)
%
Z
/
\
(
k
<
(
length
a1
))
%
Z
)
->
((
~
(
k
=
i
))
->
((
~
(
k
=
j
))
->
((
get
a1
k
)
=
(
get
a2
k
)))))))).
(
*
Why3
assumption
*
)
Definition
map_permut_sub
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
(
a1
:
(
@
array
a
a_WT
))
(
a2
:
(
@
array
a
a_WT
))
(
l
:
Z
)
(
u
:
Z
)
:
Prop
:=
((
length
a1
)
=
(
length
a2
))
/
\
(((
0
%
Z
<=
l
)
%
Z
/
\
(
l
<=
(
length
a1
))
%
Z
)
/
\
(((
0
%
Z
<=
u
)
%
Z
/
\
(
u
<=
(
length
a1
))
%
Z
)
/
\
(
map
.
MapPermut
.
permut_sub
(
elts
a1
)
(
elts
a2
)
l
u
))).
(
*
Why3
assumption
*
)
Definition
permut_sub
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
(
a1
:
(
@
array
a
a_WT
))
(
a2
:
(
@
array
a
a_WT
))
(
l
:
Z
)
(
u
:
Z
)
:
Prop
:=
(
array_eq_sub
a1
a2
0
%
Z
l
)
/
\
((
map_permut_sub
a1
a2
l
u
)
/
\
(
array_eq_sub
a2
a2
u
(
length
a1
))).
(
*
Why3
assumption
*
)
Definition
permut
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
(
a1
:
(
@
array
a
a_WT
))
(
a2
:
(
@
array
a
a_WT
))
:
Prop
:=
((
length
a1
)
=
(
length
a2
))
/
\
(
map
.
MapPermut
.
permut_sub
(
elts
a1
)
(
elts
a2
)
0
%
Z
(
length
a1
)).
Axiom
permut_refl
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
a1
:
(
@
array
a
a_WT
)),
(
permut
a1
a1
).
Axiom
exchange_permut
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
a1
:
(
@
array
a
a_WT
))
(
a2
:
(
@
array
a
a_WT
))
(
i
:
Z
)
(
j
:
Z
),
(
exchange
a1
a2
i
j
)
->
(
permut
a1
a2
).
Axiom
permut_sym
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
a1
:
(
@
array
a
a_WT
))
(
a2
:
(
@
array
a
a_WT
)),
(
permut
a1
a2
)
->
(
permut
a2
a1
).
Axiom
permut_trans
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
a1
:
(
@
array
a
a_WT
))
(
a2
:
(
@
array
a
a_WT
))
(
a3
:
(
@
array
a
a_WT
)),
(
permut
a1
a2
)
->
((
permut
a2
a3
)
->
(
permut
a1
a3
)).
Axiom
array_eq_permut
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
a1
:
(
@
array
a
a_WT
))
(
a2
:
(
@
array
a
a_WT
)),
(
array_eq
a1
a2
)
->
(
permut
a1
a2
).
Axiom
permut_sub_weakening
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
a1
:
(
@
array
a
a_WT
))
(
a2
:
(
@
array
a
a_WT
))
(
l1
:
Z
)
(
u1
:
Z
)
(
l2
:
Z
)
(
u2
:
Z
),
(
permut_sub
a1
a2
l1
u1
)
->
(((
0
%
Z
<=
l2
)
%
Z
/
\
(
l2
<=
l1
)
%
Z
)
->
(((
u1
<=
u2
)
%
Z
/
\
(
u2
<=
(
length
a1
))
%
Z
)
->
(
permut_sub
a1
a2
l2
u2
))).
Axiom
permut_sub_permut
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
a1
:
(
@
array
a
a_WT
))
(
a2
:
(
@
array
a
a_WT
))
(
l
:
Z
)
(
u
:
Z
),
(
permut_sub
a1
a2
l
u
)
->
(
permut
a1
a2
).
(
*
Why3
goal
*
)
Theorem
WP_parameter_partition
:
forall
(
a
:
Z
)
(
a1
:
(
@
map
.
Map
.
map
Z
_
Z
_
))
(
m
:
Z
)
(
n
:
Z
),
((
0
%
Z
<=
a
)
%
Z
/
\
((
0
%
Z
<=
m
)
%
Z
/
\
((
m
<
n
)
%
Z
/
\
(
n
<
a
)
%
Z
)))
->
(((
0
%
Z
<=
m
)
%
Z
/
\
((
m
<
n
)
%
Z
/
\
(
n
<
a
)
%
Z
))
->
forall
(
o
:
Z
)
(
j
:
Z
)
(
i
:
Z
)
(
a2
:
(
@
map
.
Map
.
map
Z
_
Z
_
)),
((
0
%
Z
<=
a
)
%
Z
/
\
(((
m
<=
j
)
%
Z
/
\
((
j
<
i
)
%
Z
/
\
(
i
<=
n
)
%
Z
))
/
\
((
permut_sub
(
mk_array
a
a1
)
(
mk_array
a
a2
)
m
(
n
+
1
%
Z
)
%
Z
)
/
\
((
forall
(
r
:
Z
),
((
m
<=
r
)
%
Z
/
\
(
r
<=
j
)
%
Z
)
->
((
map
.
Map
.
get
a2
r
)
<=
o
)
%
Z
)
/
\
((
forall
(
r
:
Z
),
((
j
<
r
)
%
Z
/
\
(
r
<
i
)
%
Z
)
->
((
map
.
Map
.
get
a2
r
)
=
o
))
/
\
forall
(
r
:
Z
),
((
i
<=
r
)
%
Z
/
\
(
r
<=
n
)
%
Z
)
->
(
o
<=
(
map
.
Map
.
get
a2
r
))
%
Z
)))))
->
exists
x
:
Z
,
(
forall
(
r
:
Z
),
((
m
<=
r
)
%
Z
/
\
(
r
<=
j
)
%
Z
)
->
((
map
.
Map
.
get
a2
r
)
<=
x
)
%
Z
)
/
\
((
forall
(
r
:
Z
),
((
j
<
r
)
%
Z
/
\
(
r
<
i
)
%
Z
)
->
((
map
.
Map
.
get
a2
r
)
=
x
))
/
\
forall
(
r
:
Z
),
((
i
<=
r
)
%
Z
/
\
(
r
<=
n
)
%
Z
)
->
(
x
<=
(
map
.
Map
.
get
a2
r
))
%
Z
)).
intros
a
a1
m
n
(
h1
,(
h2
,(
h3
,
h4
)))
(
h5
,(
h6
,
h7
))
o
j
i
a2
(
h8
,((
h9
,(
h10
,
h11
)),(
h12
,(
h13
,(
h14
,
h15
))))).
exists
o
;
auto
.
Qed
.
examples/bitvectors/double_of_int/double_of_int_DoubleOfInt_from_int2c_to_nat_sub_gen_1.v
deleted
100644 → 0
View file @
d93d8a61
This diff is collapsed.
Click to expand it.
examples/bts/13849/13849_T_x_1.v
deleted
100644 → 0
View file @
d93d8a61
(
*
This
file
is
generated
by
Why3
'
s
Coq
driver
*
)
(
*
Beware
!
Only
edit
allowed
sections
below
*
)
Require
Import
ZArith
.
Require
Import
Rbase
.
Inductive
t
:=
|
T
:
t
.
Inductive
x
(
a
:
Type
)
(
b
:
Type
)
:=
|
X
:
t
->
a
->
x
a
b
|
Y
:
t
->
b
->
x
a
b
.
Set
Contextual
Implicit
.
Implicit
Arguments
X
.
Unset
Contextual
Implicit
.
Set
Contextual
Implicit
.
Implicit
Arguments
Y
.
Unset
Contextual
Implicit
.
Inductive
a
:=
|
A0
:
a
|
A1
:
a
.
Inductive
b
:=
|
B
:
b
.
(
*
YOU
MAY
EDIT
THE
CONTEXT
BELOW
*
)
(
*
DO
NOT
EDIT
BELOW
*
)
Theorem
x1
:
((
X
T
A0
:
(
x
a
b
))
=
(
X
T
A1
:
(
x
a
b
))).
(
*
YOU
MAY
EDIT
THE
PROOF
BELOW
*
)
intuition
.
Qed
.
(
*
DO
NOT
EDIT
BELOW
*
)
examples/dijkstra/dijkstra_DijkstraShortestPath_WP_parameter_shortest_path_code_1.v
deleted
100644 → 0
View file @
d93d8a61
(
*
This
file
is
generated
by
Why3
'
s
Coq
driver
*
)
(
*
Beware
!
Only
edit
allowed
sections
below
*
)
Require
Import
BuiltIn
.
Require
BuiltIn
.
Require
int
.
Int
.
(
*
Why3
assumption
*
)
Definition
unit
:=
unit
.
(
*
Why3
assumption
*
)
Inductive
ref
(
a
:
Type
)
{
a_WT
:
WhyType
a
}
:=
|
mk_ref
:
a
->
ref
a
.
Axiom
ref_WhyType
:
forall
(
a
:
Type
)
{
a_WT
:
WhyType
a
}
,
WhyType
(
ref
a
).
Existing
Instance
ref_WhyType
.
Implicit
Arguments
mk_ref
[[
a
]
[
a_WT
]].
(
*
Why3
assumption
*
)
Definition
contents
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
(
v
:
(
ref
a
))
:
a
:=
match
v
with
|
(
mk_ref
x
)
=>
x
end
.
Axiom
set
:
forall
(
a
:
Type
)
{
a_WT
:
WhyType
a
}
,
Type
.
Parameter
set_WhyType
:
forall
(
a
:
Type
)
{
a_WT
:
WhyType
a
}
,
WhyType
(
set
a
).
Existing
Instance
set_WhyType
.
Parameter
mem
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
a
->
(
set
a
)
->
Prop
.
(
*
Why3
assumption
*
)
Definition
infix_eqeq
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
(
s1
:
(
set
a
))
(
s2
:
(
set
a
))
:
Prop
:=
forall
(
x
:
a
),
(
mem
x
s1
)
<->
(
mem
x
s2
).
Axiom
extensionality
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
s1
:
(
set
a
))
(
s2
:
(
set
a
)),
(
infix_eqeq
s1
s2
)
->
(
s1
=
s2
).
(
*
Why3
assumption
*
)
Definition
subset
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
(
s1
:
(
set
a
))
(
s2
:
(
set
a
))
:
Prop
:=
forall
(
x
:
a
),
(
mem
x
s1
)
->
(
mem
x
s2
).
Axiom
subset_refl
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
s
:
(
set
a
)),
(
subset
s
s
).
Axiom
subset_trans
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
s1
:
(
set
a
))
(
s2
:
(
set
a
))
(
s3
:
(
set
a
)),
(
subset
s1
s2
)
->
((
subset
s2
s3
)
->
(
subset
s1
s3
)).
Parameter
empty
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
(
set
a
).
(
*
Why3
assumption
*
)
Definition
is_empty
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
(
s
:
(
set
a
))
:
Prop
:=
forall
(
x
:
a
),
~
(
mem
x
s
).
Axiom
empty_def1
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
(
is_empty
(
empty
:
(
set
a
))).
Axiom
mem_empty
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
x
:
a
),
~
(
mem
x
(
empty
:
(
set
a
))).
Parameter
add
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
a
->
(
set
a
)
->
(
set
a
).
Axiom
add_def1
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
x
:
a
)
(
y
:
a
),
forall
(
s
:
(
set
a
)),
(
mem
x
(
add
y
s
))
<->
((
x
=
y
)
\
/
(
mem
x
s
)).
Parameter
remove
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
a
->
(
set
a
)
->
(
set
a
).
Axiom
remove_def1
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
x
:
a
)
(
y
:
a
)
(
s
:
(
set
a
)),
(
mem
x
(
remove
y
s
))
<->
((
~
(
x
=
y
))
/
\
(
mem
x
s
)).
Axiom
subset_remove
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
x
:
a
)
(
s
:
(
set
a
)),
(
subset
(
remove
x
s
)
s
).
Parameter
union
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
(
set
a
)
->
(
set
a
)
->
(
set
a
).
Axiom
union_def1
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
s1
:
(
set
a
))
(
s2
:
(
set
a
))
(
x
:
a
),
(
mem
x
(
union
s1
s2
))
<->
((
mem
x
s1
)
\
/
(
mem
x
s2
)).
Parameter
inter
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
(
set
a
)
->
(
set
a
)
->
(
set
a
).
Axiom
inter_def1
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
s1
:
(
set
a
))
(
s2
:
(
set
a
))
(
x
:
a
),
(
mem
x
(
inter
s1
s2
))
<->
((
mem
x
s1
)
/
\
(
mem
x
s2
)).
Parameter
diff
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
(
set
a
)
->
(
set
a
)
->
(
set
a
).
Axiom
diff_def1
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
s1
:
(
set
a
))
(
s2
:
(
set
a
))
(
x
:
a
),
(
mem
x
(
diff
s1
s2
))
<->
((
mem
x
s1
)
/
\
~
(
mem
x
s2
)).
Axiom
subset_diff
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
s1
:
(
set
a
))
(
s2
:
(
set
a
)),
(
subset
(
diff
s1
s2
)
s1
).
Parameter
choose
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
(
set
a
)
->
a
.
Axiom
choose_def
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
s
:
(
set
a
)),
(
~
(
is_empty
s
))
->
(
mem
(
choose
s
)
s
).
Parameter
cardinal
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
(
set
a
)
->
Z
.
Axiom
cardinal_nonneg
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
s
:
(
set
a
)),
(
0
%
Z
<=
(
cardinal
s
))
%
Z
.
Axiom
cardinal_empty
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
s
:
(
set
a
)),
((
cardinal
s
)
=
0
%
Z
)
<->
(
is_empty
s
).
Axiom
cardinal_add
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
x
:
a
),
forall
(
s
:
(
set
a
)),
(
~
(
mem
x
s
))
->
((
cardinal
(
add
x
s
))
=
(
1
%
Z
+
(
cardinal
s
))
%
Z
).
Axiom
cardinal_remove
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
x
:
a
),
forall
(
s
:
(
set
a
)),
(
mem
x
s
)
->
((
cardinal
s
)
=
(
1
%
Z
+
(
cardinal
(
remove
x
s
)))
%
Z
).
Axiom
cardinal_subset
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
s1
:
(
set
a
))
(
s2
:
(
set
a
)),
(
subset
s1
s2
)
->
((
cardinal
s1
)
<=
(
cardinal
s2
))
%
Z
.
Axiom
cardinal1
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
s
:
(
set
a
)),
((
cardinal
s
)
=
1
%
Z
)
->
forall
(
x
:
a
),
(
mem
x
s
)
->
(
x
=
(
choose
s
)).
Axiom
map
:
forall
(
a
:
Type
)
{
a_WT
:
WhyType
a
}
(
b
:
Type
)
{
b_WT
:
WhyType
b
}
,
Type
.
Parameter
map_WhyType
:
forall
(
a
:
Type
)
{
a_WT
:
WhyType
a
}
(
b
:
Type
)
{
b_WT
:
WhyType
b
}
,
WhyType
(
map
a
b
).
Existing
Instance
map_WhyType
.
Parameter
get
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
{
b
:
Type
}
{
b_WT
:
WhyType
b
}
,
(
map
a
b
)
->
a
->
b
.
Parameter
set1
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
{
b
:
Type
}
{
b_WT
:
WhyType
b
}
,
(
map
a
b
)
->
a
->
b
->
(
map
a
b
).
Axiom
Select_eq
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
{
b
:
Type
}
{
b_WT
:
WhyType
b
}
,
forall
(
m
:
(
map
a
b
)),
forall
(
a1
:
a
)
(
a2
:
a
),
forall
(
b1
:
b
),
(
a1
=
a2
)
->
((
get
(
set1
m
a1
b1
)
a2
)
=
b1
).
Axiom
Select_neq
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
{
b
:
Type
}
{
b_WT
:
WhyType
b
}
,
forall
(
m
:
(
map
a
b
)),
forall
(
a1
:
a
)
(
a2
:
a
),
forall
(
b1
:
b
),
(
~
(
a1
=
a2
))
->
((
get
(
set1
m
a1
b1
)
a2
)
=
(
get
m
a2
)).
Parameter
const
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
{
b
:
Type
}
{
b_WT
:
WhyType
b
}
,
b
->
(
map
a
b
).
Axiom
Const
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
{
b
:
Type
}
{
b_WT
:
WhyType
b
}
,
forall
(
b1
:
b
)
(
a1
:
a
),
((
get
(
const
b1
:
(
map
a
b
))
a1
)
=
b1
).
Axiom
vertex
:
Type
.
Parameter
vertex_WhyType
:
WhyType
vertex
.
Existing
Instance
vertex_WhyType
.
Parameter
v
:
(
set
vertex
).
Parameter
g_succ
:
vertex
->
(
set
vertex
).
Axiom
G_succ_sound
:
forall
(
x
:
vertex
),
(
subset
(
g_succ
x
)
v
).
Parameter
weight
:
vertex
->
vertex
->
Z
.
Axiom
Weight_nonneg
:
forall
(
x
:
vertex
)
(
y
:
vertex
),
(
0
%
Z
<=
(
weight
x
y
))
%
Z
.
(
*
Why3
assumption
*
)
Definition
min
(
m
:
vertex
)
(
q
:
(
set
vertex
))
(
d
:
(
map
vertex
Z
))
:
Prop
:=
(
mem
m
q
)
/
\
forall
(
x
:
vertex
),
(
mem
x
q
)
->
((
get
d
m
)
<=
(
get
d
x
))
%
Z
.
(
*
Why3
assumption
*
)
Inductive
path
:
vertex
->
vertex
->
Z
->
Prop
:=
|
Path_nil
:
forall
(
x
:
vertex
),
(
path
x
x
0
%
Z
)
|
Path_cons
:
forall
(
x
:
vertex
)
(
y
:
vertex
)
(
z
:
vertex
),
forall
(
d
:
Z
),
(
path
x
y
d
)
->
((
mem
z
(
g_succ
y
))
->
(
path
x
z
(
d
+
(
weight
y
z
))
%
Z
)).
Axiom
Length_nonneg
:
forall
(
x
:
vertex
)
(
y
:
vertex
),
forall
(
d
:
Z
),
(
path
x
y
d
)
->
(
0
%
Z
<=
d
)
%
Z
.
(
*
Why3
assumption
*
)
Definition
shortest_path
(
x
:
vertex
)
(
y
:
vertex
)
(
d
:
Z
)
:
Prop
:=
(
path
x
y
d
)
/
\
forall
(
d
'
:
Z
),
(
path
x
y
d
'
)
->
(
d
<=
d
'
)
%
Z
.
Axiom
Path_inversion
:
forall
(
src
:
vertex
)
(
v1
:
vertex
),
forall
(
d
:
Z
),
(
path
src
v1
d
)
->
(((
v1
=
src
)
/
\
(
d
=
0
%
Z
))
\
/
exists
v
'
:
vertex
,
(
path
src
v
'
(
d
-
(
weight
v
'
v1
))
%
Z
)
/
\
(
mem
v1
(
g_succ
v
'
))).
Axiom
Path_shortest_path
:
forall
(
src
:
vertex
)
(
v1
:
vertex
),
forall
(
d
:
Z
),
(
path
src
v1
d
)
->
exists
d
'
:
Z
,
(
shortest_path
src
v1
d
'
)
/
\
(
d
'
<=
d
)
%
Z
.
Axiom
Main_lemma
:
forall
(
src
:
vertex
)
(
v1
:
vertex
),
forall
(
d
:
Z
),
(
path
src
v1
d
)
->
((
~
(
shortest_path
src
v1
d
))
->
(((
v1
=
src
)
/
\
(
0
%
Z
<
d
)
%
Z
)
\
/
exists
v
'
:
vertex
,
exists
d
'
:
Z
,
(
shortest_path
src
v
'
d
'
)
/
\
((
mem
v1
(
g_succ
v
'
))
/
\
((
d
'
+
(
weight
v
'
v1
))
%
Z
<
d
)
%
Z
))).
Axiom
Completeness_lemma
:
forall
(
s
:
(
set
vertex
)),
(
forall
(
v1
:
vertex
),
(
mem
v1
s
)
->
forall
(
w
:
vertex
),
(
mem
w
(
g_succ
v1
))
->
(
mem
w
s
))
->
forall
(
src
:
vertex
),
(
mem
src
s
)
->
forall
(
dst
:
vertex
),
forall
(
d
:
Z
),
(
path
src
dst
d
)
->
(
mem
dst
s
).
(
*
Why3
assumption
*
)
Definition
inv_src
(
src
:
vertex
)
(
s
:
(
set
vertex
))
(
q
:
(
set
vertex
))
:
Prop
:=
(
mem
src
s
)
\
/
(
mem
src
q
).
(
*
Why3
assumption
*
)
Definition
inv
(
src
:
vertex
)
(
s
:
(
set
vertex
))
(
q
:
(
set
vertex
))
(
d
:
(
map
vertex
Z
))
:
Prop
:=
(
inv_src
src
s
q
)
/
\
(((
get
d
src
)
=
0
%
Z
)
/
\
((
subset
s
v
)
/
\
((
subset
q
v
)
/
\
((
forall
(
v1
:
vertex
),
(
mem
v1
q
)
->
~
(
mem
v1
s
))
/
\
((
forall
(
v1
:
vertex
),
(
mem
v1
s
)
->
(
shortest_path
src
v1
(
get
d
v1
)))
/
\
((
forall
(
v1
:
vertex
),
(
mem
v1
q
)
->
(
path
src
v1
(
get
d
v1
)))
/
\
forall
(
m
:
vertex
),
(
min
m
q
d
)
->
forall
(
x
:
vertex
),
forall
(
dx
:
Z
),
(
path
src
x
dx
)
->
((
dx
<
(
get
d
m
))
%
Z
->
(
mem
x
s
)))))))).
(
*
Why3
assumption
*
)
Definition
inv_succ
(
src
:
vertex
)
(
s
:
(
set
vertex
))
(
q
:
(
set
vertex
))
:
Prop
:=
forall
(
x
:
vertex
),
(
mem
x
s
)
->
forall
(
y
:
vertex
),
(
mem
y
(
g_succ
x
))
->
((
mem
y
s
)
\
/
(
mem
y
q
)).
(
*
Why3
assumption
*
)
Definition
inv_succ2
(
src
:
vertex
)
(
s
:
(
set
vertex
))
(
q
:
(
set
vertex
))
(
u
:
vertex
)
(
su
:
(
set
vertex
))
:
Prop
:=
forall
(
x
:
vertex
),
(
mem
x
s
)
->
forall
(
y
:
vertex
),
(
mem
y
(
g_succ
x
))
->
(((
~
(
x
=
u
))
\
/
((
x
=
u
)
/
\
~
(
mem
y
su
)))
->
((
mem
y
s
)
\
/
(
mem
y
q
))).
Require
Import
Why3
.
Ltac
ae
:=
why3
"alt-ergo"
.
(
*
Why3
goal
*
)
Theorem
WP_parameter_shortest_path_code
:
forall
(
src
:
vertex
)
(
dst
:
vertex
),
forall
(
d
:
(
map
vertex
Z
)),
((
mem
src
v
)
/
\
(
mem
dst
v
))
->
forall
(
q
:
(
set
vertex
))
(
d1
:
(
map
vertex
Z
))
(
visited
:
(
set
vertex
)),
(((
forall
(
x
:
vertex
),
~
(
mem
x
visited
))
/
\
(
q
=
(
add
src
(
empty
:
(
set
vertex
)))))
/
\
(
d1
=
(
set1
d
src
0
%
Z
)))
->
forall
(
q1
:
(
set
vertex
))
(
d2
:
(
map
vertex
Z
))
(
visited1
:
(
set
vertex
)),
(((
inv_src
src
visited1
q1
)
/
\
(((
get
d2
src
)
=
0
%
Z
)
/
\
((
subset
visited1
v
)
/
\
((
subset
q1
v
)
/
\
((
forall
(
v1
:
vertex
),
(
mem
v1
q1
)
->
~
(
mem
v1
visited1
))
/
\
((
forall
(
v1
:
vertex
),
(
mem
v1
visited1
)
->
(
shortest_path
src
v1
(
get
d2
v1
)))
/
\
((
forall
(
v1
:
vertex
),
(
mem
v1
q1
)
->
(
path
src
v1
(
get
d2
v1
)))
/
\
forall
(
m
:
vertex
),
(
min
m
q1
d2
)
->
forall
(
x
:
vertex
),
forall
(
dx
:
Z
),
(
path
src
x
dx
)
->
((
dx
<
(
get
d2
m
))
%
Z
->
(
mem
x
visited1
)))))))))
/
\
forall
(
x
:
vertex
),
(
mem
x
visited1
)
->
forall
(
y
:
vertex
),
(
mem
y
(
g_succ
x
))
->
((
mem
y
visited1
)
\
/
(
mem
y
q1
)))
->
forall
(
o
:
bool
),
((
o
=
true
)
<->
forall
(
x
:
vertex
),
~
(
mem
x
q1
))
->
((
~
(
o
=
true
))
->
((
~
forall
(
x
:
vertex
),
~
(
mem
x
q1
))
->
forall
(
q2
:
(
set
vertex
)),
forall
(
u
:
vertex
),
(((
mem
u
q1
)
/
\
forall
(
x
:
vertex
),
(
mem
x
q1
)
->
((
get
d2
u
)
<=
(
get
d2
x
))
%
Z
)
/
\
(
q2
=
(
remove
u
q1
)))
->
(((
path
src
u
(
get
d2
u
))
/
\
forall
(
d
'
:
Z
),
(
path
src
u
d
'
)
->
((
get
d2
u
)
<=
d
'
)
%
Z
)
->
forall
(
visited2
:
(
set
vertex
)),
(
visited2
=
(
add
u
visited1
))
->
forall
(
m
:
vertex
),
(
min
m
q2
d2
)
->
forall
(
x
:
vertex
),
forall
(
dx
:
Z
),
(
path
src
x
dx
)
->
((
dx
<
(
get
d2
m
))
%
Z
->
(
mem
x
visited2
))))).
intros
src
dst
d
(
h1
,
h2
)
q
d1
visited
((
h3
,
h4
),
h5
)
q1
d2
visited1
((
h6
,(
h7
,(
h8
,(
h9
,(
h10
,(
h11
,
h12
)))))),
h13
)
o
h14
h15
h16
q2
u
((
h17
,
h18
),
h19
)
(
h20
,
h21
)
visited2
h22
m
h23
x
dx
pathx
.
generalize
x
pathx
.
pattern
dx
.
apply
Z_lt_induction
.
2
:
ae
.
clear
x
dx
pathx
.
intros
dx
IH
x
pathx
hdx
.
destruct
(
Path_inversion
_
_
_
pathx
).
ae
.
Qed
.
examples/dijkstra/dijkstra_DijkstraShortestPath_WP_parameter_shortest_path_code_4.v
deleted
100644 → 0
View file @
d93d8a61
(
*
This
file
is
generated
by
Why3
'
s
Coq
driver
*
)
(
*
Beware
!
Only
edit
allowed
sections
below
*
)
Require
Import
BuiltIn
.
Require
BuiltIn
.
Require
int
.
Int
.
(
*
Why3
assumption
*
)
Definition
unit
:=
unit
.
(
*
Why3
assumption
*
)
Inductive
ref
(
a
:
Type
)
{
a_WT
:
WhyType
a
}
:=
|
mk_ref
:
a
->
ref
a
.
Axiom
ref_WhyType
:
forall
(
a
:
Type
)
{
a_WT
:
WhyType
a
}
,
WhyType
(
ref
a
).
Existing
Instance
ref_WhyType
.
Implicit
Arguments
mk_ref
[[
a
]
[
a_WT
]].
(
*
Why3
assumption
*
)
Definition
contents
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
(
v
:
(
ref
a
))
:
a
:=
match
v
with
|
(
mk_ref
x
)
=>
x
end
.
Axiom
set
:
forall
(
a
:
Type
)
{
a_WT
:
WhyType
a
}
,
Type
.
Parameter
set_WhyType
:
forall
(
a
:
Type
)
{
a_WT
:
WhyType
a
}
,
WhyType
(
set
a
).
Existing
Instance
set_WhyType
.
Parameter
mem
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
a
->
(
set
a
)
->
Prop
.
(
*
Why3
assumption
*
)
Definition
infix_eqeq
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
(
s1
:
(
set
a
))
(
s2
:
(
set
a
))
:
Prop
:=
forall
(
x
:
a
),
(
mem
x
s1
)
<->
(
mem
x
s2
).
Axiom
extensionality
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
s1
:
(
set
a
))
(
s2
:
(
set
a
)),
(
infix_eqeq
s1
s2
)
->
(
s1
=
s2
).
(
*
Why3
assumption
*
)
Definition
subset
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
(
s1
:
(
set
a
))
(
s2
:
(
set
a
))
:
Prop
:=
forall
(
x
:
a
),
(
mem
x
s1
)
->
(
mem
x
s2
).
Axiom
subset_refl
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
s
:
(
set
a
)),
(
subset
s
s
).
Axiom
subset_trans
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
s1
:
(
set
a
))
(
s2
:
(
set
a
))
(
s3
:
(
set
a
)),
(
subset
s1
s2
)
->
((
subset
s2
s3
)
->
(
subset
s1
s3
)).
Parameter
empty
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
(
set
a
).
(
*
Why3
assumption
*
)
Definition
is_empty
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
(
s
:
(
set
a
))
:
Prop
:=
forall
(
x
:
a
),
~
(
mem
x
s
).
Axiom
empty_def1
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
(
is_empty
(
empty
:
(
set
a
))).
Axiom
mem_empty
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
x
:
a
),
~
(
mem
x
(
empty
:
(
set
a
))).
Parameter
add
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
a
->
(
set
a
)
->
(
set
a
).
Axiom
add_def1
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
x
:
a
)
(
y
:
a
),
forall
(
s
:
(
set
a
)),
(
mem
x
(
add
y
s
))
<->
((
x
=
y
)
\
/
(
mem
x
s
)).
Parameter
remove
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
a
->
(
set
a
)
->
(
set
a
).
Axiom
remove_def1
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
x
:
a
)
(
y
:
a
)
(
s
:
(
set
a
)),
(
mem
x
(
remove
y
s
))
<->
((
~
(
x
=
y
))
/
\
(
mem
x
s
)).
Axiom
subset_remove
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
x
:
a
)
(
s
:
(
set
a
)),
(
subset
(
remove
x
s
)
s
).
