Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
why3
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
126
Issues
126
List
Boards
Labels
Service Desk
Milestones
Merge Requests
16
Merge Requests
16
Operations
Operations
Incidents
Packages & Registries
Packages & Registries
Container Registry
Analytics
Analytics
Repository
Value Stream
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Commits
Issue Boards
Open sidebar
Why3
why3
Commits
98920324
Commit
98920324
authored
Feb 23, 2016
by
MARCHE Claude
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
sessions: more updates for Coq 8.5
parent
5a24300d
Changes
17
Expand all
Hide whitespace changes
Inline
Side-by-side
Showing
17 changed files
with
1064 additions
and
1109 deletions
+1064
-1109
examples/bellman_ford/bellman_ford_Graph_long_path_decomposition_1.v
...llman_ford/bellman_ford_Graph_long_path_decomposition_1.v
+4
-4
examples/bellman_ford/bellman_ford_Graph_long_path_decomposition_pigeon1_1.v
...rd/bellman_ford_Graph_long_path_decomposition_pigeon1_1.v
+146
-175
examples/bellman_ford/bellman_ford_Graph_long_path_decomposition_pigeon3_1.v
...rd/bellman_ford_Graph_long_path_decomposition_pigeon3_1.v
+117
-108
examples/bellman_ford/bf_Graph_key_lemma_1_1.v
examples/bellman_ford/bf_Graph_key_lemma_1_1.v
+3
-2
examples/bellman_ford/bf_Graph_simple_path_1.v
examples/bellman_ford/bf_Graph_simple_path_1.v
+3
-2
examples/bellman_ford/bf_WP_BellmanFord_WP_parameter_bellman_ford_15.v
...man_ford/bf_WP_BellmanFord_WP_parameter_bellman_ford_15.v
+142
-134
examples/bellman_ford/bf_WP_BellmanFord_WP_parameter_bellman_ford_17.v
...man_ford/bf_WP_BellmanFord_WP_parameter_bellman_ford_17.v
+8
-4
examples/bellman_ford/bf_WP_BellmanFord_WP_parameter_bellman_ford_18.v
...man_ford/bf_WP_BellmanFord_WP_parameter_bellman_ford_18.v
+2
-2
examples/bellman_ford/bf_WP_BellmanFord_WP_parameter_bellman_ford_19.v
...man_ford/bf_WP_BellmanFord_WP_parameter_bellman_ford_19.v
+8
-6
examples/bellman_ford/bf_WP_BellmanFord_WP_parameter_bellman_ford_20.v
...man_ford/bf_WP_BellmanFord_WP_parameter_bellman_ford_20.v
+10
-6
examples/bellman_ford/bf_WP_BellmanFord_WP_parameter_relax_7.v
...les/bellman_ford/bf_WP_BellmanFord_WP_parameter_relax_7.v
+3
-3
examples/bellman_ford/bf_WP_BellmanFord_key_lemma_2_1.v
examples/bellman_ford/bf_WP_BellmanFord_key_lemma_2_1.v
+3
-3
examples/bellman_ford/why3session.xml
examples/bellman_ford/why3session.xml
+541
-543
examples/euler002.mlw
examples/euler002.mlw
+6
-3
examples/euler002/euler002_FibOnlyEven_fib_even_1.v
examples/euler002/euler002_FibOnlyEven_fib_even_1.v
+0
-29
examples/euler002/why3session.xml
examples/euler002/why3session.xml
+68
-85
examples/euler002/why3shapes.gz
examples/euler002/why3shapes.gz
+0
-0
No files found.
examples/bellman_ford/bellman_ford_Graph_long_path_decomposition_1.v
View file @
98920324
...
...
@@ -241,6 +241,9 @@ Axiom long_path_decomposition_pigeon3 : forall (l:(list vertex)) (v:vertex),
exists
l3
:
(
list
vertex
),
(
l
=
(
Init
.
Datatypes
.
app
l1
(
Init
.
Datatypes
.
cons
n
(
Init
.
Datatypes
.
app
l2
(
Init
.
Datatypes
.
cons
n
l3
)))))).
Require
Import
Why3
.
Ltac
ae
:=
why3
"Alt-Ergo,0.99.1,"
timelimit
5
;
admit
.
(
*
Why3
goal
*
)
Theorem
long_path_decomposition
:
forall
(
l
:
(
list
vertex
))
(
v
:
vertex
),
(
path
s
l
v
)
->
(((
cardinal
vertices
)
<=
(
list
.
Length
.
length
l
))
%
Z
->
...
...
@@ -252,11 +255,8 @@ Theorem long_path_decomposition : forall (l:(list vertex)) (v:vertex), (path
(
*
Why3
intros
l
v
h1
h2
.
*
)
intuition
.
Require
Why3
.
Ltac
ae
:=
why3
"alt-ergo"
.
apply
long_path_decomposition_pigeon3
.
apply
long_path_decomposition_pigeon2
;
ae
.
Q
ed
.
Admitt
ed
.
examples/bellman_ford/bellman_ford_Graph_long_path_decomposition_pigeon1_1.v
View file @
98920324
(
*
This
file
is
generated
by
Why3
'
s
Coq
driver
*
)
(
*
Beware
!
Only
edit
allowed
sections
below
*
)
Require
Import
ZArith
.
Require
Import
Rbase
.
Require
Import
BuiltIn
.
Require
BuiltIn
.
Require
list
.
List
.
Require
list
.
Length
.
Require
int
.
Int
.
Require
list
.
Mem
.
Require
list
.
Append
.
(
*
Why3
assumption
*
)
Inductive
list
(
a
:
Type
)
:=
|
Nil
:
list
a
|
Cons
:
a
->
(
list
a
)
->
list
a
.
Set
Contextual
Implicit
.
Implicit
Arguments
Nil
.
Unset
Contextual
Implicit
.
Implicit
Arguments
Cons
.
(
*
Why3
assumption
*
)
Set
Implicit
Arguments
.
Fixpoint
length
(
a
:
Type
)(
l
:
(
list
a
))
{
struct
l
}:
Z
:=
match
l
with
|
Nil
=>
0
%
Z
|
(
Cons
_
r
)
=>
(
1
%
Z
+
(
length
r
))
%
Z
end
.
Unset
Implicit
Arguments
.
Axiom
set
:
forall
(
a
:
Type
),
Type
.
Parameter
set_WhyType
:
forall
(
a
:
Type
)
{
a_WT
:
WhyType
a
}
,
WhyType
(
set
a
).
Existing
Instance
set_WhyType
.
Axiom
Length_nonnegative
:
forall
(
a
:
Type
),
forall
(
l
:
(
list
a
)),
(
0
%
Z
<=
(
length
l
))
%
Z
.
Axiom
Length_nil
:
forall
(
a
:
Type
),
forall
(
l
:
(
list
a
)),
((
length
l
)
=
0
%
Z
)
<->
(
l
=
(
Nil
:
(
list
a
))).
Parameter
set
:
forall
(
a
:
Type
),
Type
.
Parameter
mem
:
forall
(
a
:
Type
),
a
->
(
set
a
)
->
Prop
.
Implicit
Arguments
mem
.
Parameter
mem
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
a
->
(
set
a
)
->
Prop
.
(
*
Why3
assumption
*
)
Definition
infix_eqeq
(
a
:
Type
)(
s1
:
(
set
a
))
(
s2
:
(
set
a
))
:
Prop
:=
forall
(
x
:
a
),
(
mem
x
s1
)
<->
(
mem
x
s2
).
Implicit
Arguments
infix_eqeq
.
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
),
forall
(
s1
:
(
set
a
))
(
s2
:
(
set
a
)),
(
infix_eqeq
s1
s2
)
->
(
s1
=
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
)(
s1
:
(
set
a
))
(
s2
:
(
set
a
))
:
Prop
:=
forall
(
x
:
a
),
(
mem
x
s1
)
->
(
mem
x
s2
).
Implicit
Arguments
subset
.
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_
trans
:
forall
(
a
:
Type
),
forall
(
s1
:
(
set
a
))
(
s2
:
(
set
a
))
(
s
3
:
(
set
a
)),
(
subset
s1
s2
)
->
((
subset
s2
s3
)
->
(
subset
s1
s3
)
).
Axiom
subset_
refl
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
s
:
(
set
a
)),
(
s
ubset
s
s
).
Parameter
empty
:
forall
(
a
:
Type
),
(
set
a
).
Set
Contextual
Implicit
.
Implicit
Arguments
empty
.
Unset
Contextual
Implicit
.
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
)(
s
:
(
set
a
))
:
Prop
:=
forall
(
x
:
a
),
~
(
mem
x
s
).
Implicit
Arguments
is_empty
.
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
empty_def1
:
forall
(
a
:
Type
),
(
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
->
(
set
a
)
->
(
set
a
).
Implicit
Arguments
add
.
Parameter
add
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
a
->
(
set
a
)
->
(
set
a
).
Axiom
add_def1
:
forall
(
a
:
Type
),
forall
(
x
:
a
)
(
y
:
a
),
forall
(
s
:
(
set
a
)
),
(
mem
x
(
add
y
s
))
<->
((
x
=
y
)
\
/
(
mem
x
s
)).
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
->
(
set
a
)
->
(
set
a
).
Implicit
Arguments
remove
.
Parameter
remove
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
a
->
(
set
a
)
->
(
set
a
).
Axiom
remove_def1
:
forall
(
a
:
Type
),
forall
(
x
:
a
)
(
y
:
a
)
(
s
:
(
set
a
)),
(
mem
x
(
remove
y
s
))
<->
((
~
(
x
=
y
))
/
\
(
mem
x
s
)).
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
),
forall
(
x
:
a
)
(
s
:
(
set
a
)),
(
subset
(
remove
x
s
)
s
).
Axiom
add_remove
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
x
:
a
)
(
s
:
(
set
a
)),
(
mem
x
s
)
->
((
add
x
(
remove
x
s
))
=
s
).
Parameter
union
:
forall
(
a
:
Type
),
(
set
a
)
->
(
set
a
)
->
(
set
a
).
Implicit
Arguments
union
.
Axiom
remove_add
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
x
:
a
)
(
s
:
(
set
a
)),
((
remove
x
(
add
x
s
))
=
(
remove
x
s
))
.
Axiom
union_def1
:
forall
(
a
:
Type
),
forall
(
s1
:
(
set
a
))
(
s2
:
(
set
a
))
(
x
:
a
),
(
mem
x
(
union
s1
s2
))
<->
((
mem
x
s1
)
\
/
(
mem
x
s2
)
).
Axiom
subset_remove
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
x
:
a
)
(
s
:
(
set
a
)),
(
subset
(
remove
x
s
)
s
).
Parameter
inter
:
forall
(
a
:
Type
),
(
set
a
)
->
(
set
a
)
->
(
set
a
).
Implicit
Arguments
inter
.
Parameter
union
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
(
set
a
)
->
(
set
a
)
->
(
set
a
)
.
Axiom
inter_def1
:
forall
(
a
:
Type
),
forall
(
s1
:
(
set
a
))
(
s2
:
(
set
a
))
(
x
:
a
),
(
mem
x
(
inter
s1
s2
))
<->
((
mem
x
s1
)
/
\
(
mem
x
s2
)).
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
diff
:
forall
(
a
:
Type
),
(
set
a
)
->
(
set
a
)
->
(
set
a
).
Implicit
Arguments
diff
.
Parameter
inter
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
(
set
a
)
->
(
set
a
)
->
(
set
a
)
.
Axiom
diff_def1
:
forall
(
a
:
Type
),
forall
(
s1
:
(
set
a
))
(
s2
:
(
set
a
))
(
x
:
a
),
(
mem
x
(
diff
s1
s2
))
<->
((
mem
x
s1
)
/
\
~
(
mem
x
s2
)).
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
)).
Axiom
subset_diff
:
forall
(
a
:
Type
),
forall
(
s1
:
(
set
a
))
(
s2
:
(
set
a
)),
(
subset
(
diff
s1
s2
)
s1
).
Parameter
diff
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
(
set
a
)
->
(
set
a
)
->
(
set
a
).
Parameter
choose
:
forall
(
a
:
Type
),
(
set
a
)
->
a
.
Implicit
Arguments
choose
.
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
choose_def
:
forall
(
a
:
Type
),
forall
(
s
:
(
set
a
)),
(
~
(
is_empty
s
))
->
(
mem
(
choose
s
)
s
).
Axiom
subset_diff
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
s1
:
(
set
a
))
(
s2
:
(
set
a
)),
(
subset
(
diff
s1
s2
)
s1
).
Parameter
all
:
forall
(
a
:
Type
),
(
set
a
).
Set
Contextual
Implicit
.
Implicit
Arguments
all
.
Unset
Contextual
Implicit
.
Parameter
choose
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
(
set
a
)
->
a
.
Axiom
all_def
:
forall
(
a
:
Type
),
forall
(
x
:
a
),
(
mem
x
(
all
:
(
set
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
),
(
set
a
)
->
Z
.
Implicit
Arguments
cardinal
.
Parameter
cardinal
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
(
set
a
)
->
Z
.
Axiom
cardinal_nonneg
:
forall
(
a
:
Type
)
,
forall
(
s
:
(
set
a
)),
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
)
,
forall
(
s
:
(
set
a
)),
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
),
forall
(
x
:
a
),
forall
(
s
:
(
set
a
)),
(
~
(
mem
x
s
))
->
((
cardinal
(
add
x
s
))
=
(
1
%
Z
+
(
cardinal
s
))
%
Z
).
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
),
forall
(
x
:
a
),
forall
(
s
:
(
set
a
)),
(
mem
x
s
)
->
((
cardinal
s
)
=
(
1
%
Z
+
(
cardinal
(
remove
x
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
),
forall
(
s1
:
(
set
a
))
(
s2
:
(
set
a
)),
(
subset
s1
s2
)
->
((
cardinal
s1
)
<=
(
cardinal
s2
))
%
Z
.
Axiom
cardinal_subset
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
s1
:
(
set
a
))
(
s
2
:
(
set
a
)),
(
s
ubset
s1
s2
)
->
((
cardinal
s1
)
<=
(
cardinal
s2
))
%
Z
.
Axiom
cardinal1
:
forall
(
a
:
Type
),
forall
(
s
:
(
set
a
)),
((
cardinal
s
)
=
1
%
Z
)
->
forall
(
x
:
a
),
(
mem
x
s
)
->
(
x
=
(
choose
s
)).
Parameter
nth
:
forall
(
a
:
Type
),
Z
->
(
set
a
)
->
a
.
Implicit
Arguments
nth
.
Axiom
nth_injective
:
forall
(
a
:
Type
),
forall
(
s
:
(
set
a
))
(
i
:
Z
)
(
j
:
Z
),
((
0
%
Z
<=
i
)
%
Z
/
\
(
i
<
(
cardinal
s
))
%
Z
)
->
(((
0
%
Z
<=
j
)
%
Z
/
\
(
j
<
(
cardinal
s
))
%
Z
)
->
(((
nth
i
s
)
=
(
nth
j
s
))
->
(
i
=
j
))).
Axiom
subset_eq
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
s1
:
(
set
a
))
(
s2
:
(
set
a
)),
(
subset
s1
s2
)
->
(((
cardinal
s1
)
=
(
cardinal
s2
))
->
(
infix_eqeq
s1
s2
)).
Axiom
nth_surjective
:
forall
(
a
:
Type
),
forall
(
s
:
(
set
a
))
(
x
:
a
),
(
mem
x
s
)
->
exists
i
:
Z
,
((
0
%
Z
<=
i
)
%
Z
/
\
(
i
<
(
cardinal
s
))
%
Z
)
->
(
x
=
(
nth
i
s
)).
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
)).
Parameter
vertex
:
Type
.
Axiom
vertex
:
Type
.
Parameter
vertex_WhyType
:
WhyType
vertex
.
Existing
Instance
vertex_WhyType
.
Parameter
vertices
:
(
set
vertex
).
Parameter
edges
:
(
set
(
vertex
*
vertex
)
%
type
).
(
*
Why3
assumption
*
)
Definition
edge
(
x
:
vertex
)
(
y
:
vertex
)
:
Prop
:=
(
mem
(
x
,
y
)
edges
).
Definition
edge
(
x
:
vertex
)
(
y
:
vertex
)
:
Prop
:=
(
mem
(
x
,
y
)
edges
).
Axiom
edges_def
:
forall
(
x
:
vertex
)
(
y
:
vertex
),
(
mem
(
x
,
y
)
edges
)
->
((
mem
x
vertices
)
/
\
(
mem
y
vertices
)).
...
...
@@ -160,103 +136,99 @@ Axiom s_in_graph : (mem s vertices).
Axiom
vertices_cardinal_pos
:
(
0
%
Z
<
(
cardinal
vertices
))
%
Z
.
(
*
Why3
assumption
*
)
Set
Implicit
Arguments
.
Fixpoint
infix_plpl
(
a
:
Type
)(
l1
:
(
list
a
))
(
l2
:
(
list
a
))
{
struct
l1
}:
(
list
a
)
:=
match
l1
with
|
Nil
=>
l2
|
(
Cons
x1
r1
)
=>
(
Cons
x1
(
infix_plpl
r1
l2
))
end
.
Unset
Implicit
Arguments
.
Axiom
Append_assoc
:
forall
(
a
:
Type
),
forall
(
l1
:
(
list
a
))
(
l2
:
(
list
a
))
(
l3
:
(
list
a
)),
((
infix_plpl
l1
(
infix_plpl
l2
l3
))
=
(
infix_plpl
(
infix_plpl
l1
l2
)
l3
)).
Axiom
Append_l_nil
:
forall
(
a
:
Type
),
forall
(
l
:
(
list
a
)),
((
infix_plpl
l
(
Nil
:
(
list
a
)))
=
l
).
Axiom
Append_length
:
forall
(
a
:
Type
),
forall
(
l1
:
(
list
a
))
(
l2
:
(
list
a
)),
((
length
(
infix_plpl
l1
l2
))
=
((
length
l1
)
+
(
length
l2
))
%
Z
).
(
*
Why3
assumption
*
)
Set
Implicit
Arguments
.
Fixpoint
mem1
(
a
:
Type
)(
x
:
a
)
(
l
:
(
list
a
))
{
struct
l
}:
Prop
:=
match
l
with
|
Nil
=>
False
|
(
Cons
y
r
)
=>
(
x
=
y
)
\
/
(
mem1
x
r
)
end
.
Unset
Implicit
Arguments
.
Axiom
mem_append
:
forall
(
a
:
Type
),
forall
(
x
:
a
)
(
l1
:
(
list
a
))
(
l2
:
(
list
a
)),
(
mem1
x
(
infix_plpl
l1
l2
))
<->
((
mem1
x
l1
)
\
/
(
mem1
x
l2
)).
Axiom
mem_decomp
:
forall
(
a
:
Type
),
forall
(
x
:
a
)
(
l
:
(
list
a
)),
(
mem1
x
l
)
->
exists
l1
:
(
list
a
),
exists
l2
:
(
list
a
),
(
l
=
(
infix_plpl
l1
(
Cons
x
l2
))).
(
*
Why3
assumption
*
)
Inductive
path
:
vertex
->
(
list
vertex
)
->
vertex
->
Prop
:=
|
Path_empty
:
forall
(
x
:
vertex
),
(
path
x
(
Nil
:
(
list
vertex
))
x
)
Inductive
path
:
vertex
->
(
list
vertex
)
->
vertex
->
Prop
:=
|
Path_empty
:
forall
(
x
:
vertex
),
(
path
x
Init
.
Datatypes
.
nil
x
)
|
Path_cons
:
forall
(
x
:
vertex
)
(
y
:
vertex
)
(
z
:
vertex
)
(
l
:
(
list
vertex
)),
(
edge
x
y
)
->
((
path
y
l
z
)
->
(
path
x
(
C
ons
x
l
)
z
)).
(
edge
x
y
)
->
((
path
y
l
z
)
->
(
path
x
(
Init
.
Datatypes
.
c
ons
x
l
)
z
)).
Axiom
path_right_extension
:
forall
(
x
:
vertex
)
(
y
:
vertex
)
(
z
:
vertex
)
(
l
:
(
list
vertex
)),
(
path
x
l
y
)
->
((
edge
y
z
)
->
(
path
x
(
infix_plpl
l
(
Cons
y
(
Nil
:
(
list
vertex
))
))
z
)).
Axiom
path_right_extension
:
forall
(
x
:
vertex
)
(
y
:
vertex
)
(
z
:
vertex
)
(
l
:
(
list
vertex
)),
(
path
x
l
y
)
->
((
edge
y
z
)
->
(
path
x
(
Init
.
Datatypes
.
app
l
(
Init
.
Datatypes
.
cons
y
Init
.
Datatypes
.
nil
))
z
)).
Axiom
path_right_inversion
:
forall
(
x
:
vertex
)
(
z
:
vertex
)
(
l
:
(
list
vertex
)),
(
path
x
l
z
)
->
(((
x
=
z
)
/
\
(
l
=
(
Nil
:
(
list
vertex
))))
\
/
exists
y
:
vertex
,
exists
lqt
:
(
list
vertex
),
(
path
x
lqt
y
)
/
\
((
edge
y
z
)
/
\
(
l
=
(
infix_plpl
lqt
(
Cons
y
(
Nil
:
(
list
vertex
))
))))).
(
path
x
l
z
)
->
(((
x
=
z
)
/
\
(
l
=
Init
.
Datatypes
.
nil
))
\
/
exists
y
:
vertex
,
exists
l
'
:
(
list
vertex
),
(
path
x
l
'
y
)
/
\
((
edge
y
z
)
/
\
(
l
=
(
Init
.
Datatypes
.
app
l
'
(
Init
.
Datatypes
.
cons
y
Init
.
Datatypes
.
nil
))))).
Axiom
path_trans
:
forall
(
x
:
vertex
)
(
y
:
vertex
)
(
z
:
vertex
)
(
l1
:
(
list
vertex
))
(
l2
:
(
list
vertex
)),
(
path
x
l1
y
)
->
((
path
y
l2
z
)
->
(
path
x
(
infix_plpl
l1
l2
)
z
)).
(
Init
.
Datatypes
.
app
l1
l2
)
z
)).
Axiom
empty_path
:
forall
(
x
:
vertex
)
(
y
:
vertex
),
(
path
x
(
Nil
:
(
list
vertex
))
Axiom
empty_path
:
forall
(
x
:
vertex
)
(
y
:
vertex
),
(
path
x
Init
.
Datatypes
.
nil
y
)
->
(
x
=
y
).
Axiom
path_decomposition
:
forall
(
x
:
vertex
)
(
y
:
vertex
)
(
z
:
vertex
)
(
l1
:
(
list
vertex
))
(
l2
:
(
list
vertex
)),
(
path
x
(
infix_plpl
l1
(
Cons
y
l2
))
z
)
->
((
path
x
l1
y
)
/
\
(
path
y
(
Cons
y
l2
)
z
)).
Axiom
path_decomposition
:
forall
(
x
:
vertex
)
(
y
:
vertex
)
(
z
:
vertex
)
(
l1
:
(
list
vertex
))
(
l2
:
(
list
vertex
)),
(
path
x
(
Init
.
Datatypes
.
app
l1
(
Init
.
Datatypes
.
cons
y
l2
))
z
)
->
((
path
x
l1
y
)
/
\
(
path
y
(
Init
.
Datatypes
.
cons
y
l2
)
z
)).
Parameter
weight
:
vertex
->
vertex
->
Z
.
(
*
Why3
assumption
*
)
Set
Implicit
Arguments
.
Fixpoint
path_weight
(
l
:
(
list
vertex
))
(
dst
:
vertex
)
{
struct
l
}:
Z
:=
Fixpoint
path_weight
(
l
:
(
list
vertex
))
(
dst
:
vertex
)
{
struct
l
}:
Z
:=
match
l
with
|
Nil
=>
0
%
Z
|
(
Cons
x
Nil
)
=>
(
weight
x
dst
)
|
(
Cons
x
((
Cons
y
_
)
as
r
))
=>
((
weight
x
y
)
+
(
path_weight
r
dst
))
%
Z
|
Init
.
Datatypes
.
nil
=>
0
%
Z
|
(
Init
.
Datatypes
.
cons
x
Init
.
Datatypes
.
nil
)
=>
(
weight
x
dst
)
|
(
Init
.
Datatypes
.
cons
x
((
Init
.
Datatypes
.
cons
y
_
)
as
r
))
=>
((
weight
x
y
)
+
(
path_weight
r
dst
))
%
Z
end
.
Unset
Implicit
Arguments
.
Axiom
path_weight_right_extension
:
forall
(
x
:
vertex
)
(
y
:
vertex
)
(
l
:
(
list
vertex
)),
((
path_weight
(
infix_plpl
l
(
Cons
x
(
Nil
:
(
list
vertex
))))
Axiom
path_weight_right_extension
:
forall
(
x
:
vertex
)
(
y
:
vertex
)
(
l
:
(
list
vertex
)),
((
path_weight
(
Init
.
Datatypes
.
app
l
(
Init
.
Datatypes
.
cons
x
Init
.
Datatypes
.
nil
))
y
)
=
((
path_weight
l
x
)
+
(
weight
x
y
))
%
Z
).
Axiom
path_weight_decomposition
:
forall
(
y
:
vertex
)
(
z
:
vertex
)
(
l1
:
(
list
vertex
))
(
l2
:
(
list
vertex
)),
((
path_weight
(
infix_plpl
l1
(
Cons
y
l2
))
z
)
=
((
path_weight
l1
y
)
+
(
path_weight
(
Cons
y
l2
)
z
))
%
Z
).
Axiom
path_weight_decomposition
:
forall
(
y
:
vertex
)
(
z
:
vertex
)
(
l1
:
(
list
vertex
))
(
l2
:
(
list
vertex
)),
((
path_weight
(
Init
.
Datatypes
.
app
l1
(
Init
.
Datatypes
.
cons
y
l2
))
z
)
=
((
path_weight
l1
y
)
+
(
path_weight
(
Init
.
Datatypes
.
cons
y
l2
)
z
))
%
Z
).
Axiom
path_in_vertices
:
forall
(
v1
:
vertex
)
(
v2
:
vertex
)
(
l
:
(
list
vertex
)),
(
mem
v1
vertices
)
->
((
path
v1
l
v2
)
->
(
mem
v2
vertices
)).
(
*
Why3
assumption
*
)
Definition
pigeon_set
(
s1
:
(
set
vertex
))
:
Prop
:=
forall
(
l
:
(
list
vertex
)),
(
forall
(
e
:
vertex
),
(
list
.
Mem
.
mem
e
l
)
->
(
mem
e
s1
))
->
(((
cardinal
s1
)
<
(
list
.
Length
.
length
l
))
%
Z
->
exists
e
:
vertex
,
exists
l1
:
(
list
vertex
),
exists
l2
:
(
list
vertex
),
exists
l3
:
(
list
vertex
),
(
l
=
(
Init
.
Datatypes
.
app
l1
(
Init
.
Datatypes
.
cons
e
(
Init
.
Datatypes
.
app
l2
(
Init
.
Datatypes
.
cons
e
l3
)))))).
Axiom
Induction
:
(
forall
(
s1
:
(
set
vertex
)),
(
is_empty
s1
)
->
(
pigeon_set
s1
))
->
((
forall
(
s1
:
(
set
vertex
)),
(
pigeon_set
s1
)
->
forall
(
t
:
vertex
),
(
~
(
mem
t
s1
))
->
(
pigeon_set
(
add
t
s1
)))
->
forall
(
s1
:
(
set
vertex
)),
(
pigeon_set
s1
)).
Axiom
corner
:
forall
(
s1
:
(
set
vertex
))
(
l
:
(
list
vertex
)),
((
list
.
Length
.
length
l
)
=
(
cardinal
s1
))
->
((
forall
(
e
:
vertex
),
(
list
.
Mem
.
mem
e
l
)
->
(
mem
e
s1
))
->
((
exists
e
:
vertex
,
(
exists
l1
:
(
list
vertex
),
(
exists
l2
:
(
list
vertex
),
(
exists
l3
:
(
list
vertex
),
(
l
=
(
Init
.
Datatypes
.
app
l1
(
Init
.
Datatypes
.
cons
e
(
Init
.
Datatypes
.
app
l2
(
Init
.
Datatypes
.
cons
e
l3
)))))))))
\
/
forall
(
e
:
vertex
),
(
mem
e
s1
)
->
(
list
.
Mem
.
mem
e
l
))).
Axiom
pigeon_0
:
(
pigeon_set
(
empty
:
(
set
vertex
))).
Axiom
pigeon_1
:
forall
(
s1
:
(
set
vertex
)),
(
pigeon_set
s1
)
->
forall
(
t
:
vertex
),
(
pigeon_set
(
add
t
s1
)).
Axiom
pigeon_2
:
forall
(
s1
:
(
set
vertex
)),
(
pigeon_set
s1
).
Axiom
pigeonhole
:
forall
(
s1
:
(
set
vertex
))
(
l
:
(
list
vertex
)),
(
forall
(
e
:
vertex
),
(
mem1
e
l
)
->
(
mem
e
s1
))
->
(((
cardinal
s1
)
<
(
length
l
))
%
Z
->
exists
e
:
vertex
,
exists
l1
:
(
list
vertex
),
exists
l2
:
(
list
vertex
),
exists
l3
:
(
list
vertex
),
(
l
=
(
infix_plpl
l1
(
Cons
e
(
infix_plpl
l2
(
Cons
e
l3
)))))).
(
forall
(
e
:
vertex
),
(
list
.
Mem
.
mem
e
l
)
->
(
mem
e
s1
))
->
(((
cardinal
s1
)
<
(
list
.
Length
.
length
l
))
%
Z
->
exists
e
:
vertex
,
exists
l1
:
(
list
vertex
),
exists
l2
:
(
list
vertex
),
exists
l3
:
(
list
vertex
),
(
l
=
(
Init
.
Datatypes
.
app
l1
(
Init
.
Datatypes
.
cons
e
(
Init
.
Datatypes
.
app
l2
(
Init
.
Datatypes
.
cons
e
l3
)))))).
Require
Import
Why3
.
Ltac
ae
:=
why3
"Alt-Ergo,0.99.1,"
;
admit
.
(
*
Why3
goal
*
)
Theorem
long_path_decomposition_pigeon1
:
forall
(
l
:
(
list
vertex
))
(
v
:
vertex
),
(
path
s
l
v
)
->
((
~
(
l
=
(
Nil
:
(
list
vertex
))))
->
forall
(
v1
:
vertex
),
(
mem1
v1
(
Cons
v
l
))
->
(
mem
v1
vertices
)).
Require
Why3
.
Ltac
ae
:=
why3
"alt-ergo"
.
Ltac
cvc
:=
why3
"cvc3"
.
(
v
:
vertex
),
(
path
s
l
v
)
->
((
~
(
l
=
Init
.
Datatypes
.
nil
))
->
forall
(
v1
:
vertex
),
(
list
.
Mem
.
mem
v1
(
Init
.
Datatypes
.
cons
v
l
))
->
(
mem
v1
vertices
)).
(
*
Why3
intros
l
v
h1
h2
v1
h3
.
*
)
intros
l
v
H0
.
induction
H0
.
...
...
@@ -265,6 +237,5 @@ tauto.
apply
edges_def
in
H
.
ae
.
Qed
.
Admitted
.
examples/bellman_ford/bellman_ford_Graph_long_path_decomposition_pigeon3_1.v
View file @
98920324
...
...
@@ -8,116 +8,120 @@ Require int.Int.
Require
list
.
Mem
.
Require
list
.
Append
.
Axiom
set
:
forall
(
a
:
Type
)
{
a_WT
:
WhyType
a
}
,
Type
.
Axiom
set
:
forall
(
a
:
Type
),
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
a_WT
)
->
Prop
.
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
a_WT
))
(
s2
:
(
@
set
a
a_WT
))
:
Prop
:=
forall
(
x
:
a
),
(
mem
x
s1
)
<->
(
mem
x
s2
).
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
a_WT
))
(
s2
:
(
@
set
a
a_WT
)),
(
infix_eqeq
s1
s2
)
->
(
s1
=
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
a_WT
))
(
s2
:
(
@
set
a
a_WT
))
:
Prop
:=
forall
(
x
:
a
),
(
mem
x
s1
)
->
(
mem
x
s2
).
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
a_WT
)),
(
subset
s
s
).
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
a_WT
))
(
s2
:
(
@
set
a
a_WT
))
(
s3
:
(
@
set
a
a_WT
)),
(
subset
s1
s2
)
->
((
subset
s
2
s3
)
->
(
subset
s1
s
3
)).
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
a_WT
).
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
a_WT
))
:
Prop
:=
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
a_WT
))).
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
a_WT
))).
(
empty
:
(
set
a
))).
Parameter
add
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
a
->
(
@
set
a
a_WT
)
->
(
@
set
a
a_WT
).
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
a_WT
)),
(
mem
x
(
add
y
s
))
<->
((
x
=
y
)
\
/
(
mem
x
s
)).
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
a_WT
)
->
(
@
set
a
a_WT
).