Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
e0488669
Commit
e0488669
authored
Aug 02, 2011
by
Jean-Christophe Filliâtre
Browse files
mergesort_list: completed proof
parent
1567624e
Changes
7
Hide whitespace changes
Inline
Side-by-side
.gitignore
View file @
e0488669
...
...
@@ -154,7 +154,6 @@ why3.conf
/examples/programs/vacid_0_red_black_trees/
/examples/programs/vacid_0_red_black_trees_harness/
/examples/programs/next_digit_sum/
/examples/programs/mergesort_list/
/examples/programs/algo63/
/examples/programs/algo64/
/examples/programs/algo65/
...
...
examples/programs/mergesort_list.mlw
View file @
e0488669
...
...
@@ -9,14 +9,14 @@ module M
use import list.Append
use import list.Permut
lemma Permut_append:
forall l1 l2 k1 k2 : list 'a.
permut l1 k1 -> permut l2 k2 -> permut (l1 ++ l2) (k1 ++ k2)
lemma Permut_cons_append:
forall x : 'a, l1 l2 : list 'a.
permut (Cons x l1 ++ l2) (l1 ++ Cons x l2)
lemma Permut_append:
forall l1 l2 k1 k2 : list 'a.
permut l1 k1 -> permut l2 k2 -> permut (l1 ++ l2) (k1 ++ k2)
let split l0 =
{ length l0 >= 2 }
let rec split_aux (l1 : list 'a) l2 l variant { length l } =
...
...
examples/programs/mergesort_list/mergesort_list_WP_M_Permut_append_1.v
0 → 100644
View file @
e0488669
(
*
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
list
(
a
:
Type
)
:=
|
Nil
:
list
a
|
Cons
:
a
->
(
list
a
)
->
list
a
.
Set
Contextual
Implicit
.
Implicit
Arguments
Nil
.
Unset
Contextual
Implicit
.
Implicit
Arguments
Cons
.
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
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
))).
Inductive
sorted
:
(
list
Z
)
->
Prop
:=
|
Sorted_Nil
:
(
sorted
(
Nil
:
(
list
Z
)))
|
Sorted_One
:
forall
(
x
:
Z
),
(
sorted
(
Cons
x
(
Nil
:
(
list
Z
))))
|
Sorted_Two
:
forall
(
x
:
Z
)
(
y
:
Z
)
(
l
:
(
list
Z
)),
(
x
<=
y
)
%
Z
->
((
sorted
(
Cons
y
l
))
->
(
sorted
(
Cons
x
(
Cons
y
l
)))).
Set
Implicit
Arguments
.
Fixpoint
mem
(
a
:
Type
)(
x
:
a
)
(
l
:
(
list
a
))
{
struct
l
}:
Prop
:=
match
l
with
|
Nil
=>
False
|
Cons
y
r
=>
(
x
=
y
)
\
/
(
mem
x
r
)
end
.
Unset
Implicit
Arguments
.
Axiom
Sorted_mem
:
forall
(
x
:
Z
)
(
l
:
(
list
Z
)),
((
forall
(
y
:
Z
),
(
mem
y
l
)
->
(
x
<=
y
)
%
Z
)
/
\
(
sorted
l
))
<->
(
sorted
(
Cons
x
l
)).
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
).
Axiom
mem_append
:
forall
(
a
:
Type
),
forall
(
x
:
a
)
(
l1
:
(
list
a
))
(
l2
:
(
list
a
)),
(
mem
x
(
infix_plpl
l1
l2
))
<->
((
mem
x
l1
)
\
/
(
mem
x
l2
)).
Axiom
mem_decomp
:
forall
(
a
:
Type
),
forall
(
x
:
a
)
(
l
:
(
list
a
)),
(
mem
x
l
)
->
exists
l1
:
(
list
a
),
exists
l2
:
(
list
a
),
(
l
=
(
infix_plpl
l1
(
Cons
x
l2
))).
Parameter
num_occ
:
forall
(
a
:
Type
),
a
->
(
list
a
)
->
Z
.
Implicit
Arguments
num_occ
.
Axiom
num_occ_def
:
forall
(
a
:
Type
),
forall
(
x
:
a
)
(
l
:
(
list
a
)),
match
l
with
|
Nil
=>
((
num_occ
x
l
)
=
0
%
Z
)
|
Cons
y
r
=>
((
x
=
y
)
->
((
num_occ
x
l
)
=
(
1
%
Z
+
(
num_occ
x
r
))
%
Z
))
/
\
((
~
(
x
=
y
))
->
((
num_occ
x
l
)
=
(
0
%
Z
+
(
num_occ
x
r
))
%
Z
))
end
.
Axiom
Mem_Num_Occ
:
forall
(
a
:
Type
),
forall
(
x
:
a
)
(
l
:
(
list
a
)),
(
mem
x
l
)
<->
(
0
%
Z
<
(
num_occ
x
l
))
%
Z
.
Definition
permut
(
a
:
Type
)(
l1
:
(
list
a
))
(
l2
:
(
list
a
))
:
Prop
:=
forall
(
x
:
a
),
((
num_occ
x
l1
)
=
(
num_occ
x
l2
)).
Implicit
Arguments
permut
.
Axiom
Permut_refl
:
forall
(
a
:
Type
),
forall
(
l
:
(
list
a
)),
(
permut
l
l
).
Axiom
Permut_sym
:
forall
(
a
:
Type
),
forall
(
l1
:
(
list
a
))
(
l2
:
(
list
a
)),
(
permut
l1
l2
)
->
(
permut
l2
l1
).
Axiom
Permut_trans
:
forall
(
a
:
Type
),
forall
(
l1
:
(
list
a
))
(
l2
:
(
list
a
))
(
l3
:
(
list
a
)),
(
permut
l1
l2
)
->
((
permut
l2
l3
)
->
(
permut
l1
l3
)).
Axiom
Permut_cons
:
forall
(
a
:
Type
),
forall
(
x
:
a
)
(
l1
:
(
list
a
))
(
l2
:
(
list
a
)),
(
permut
l1
l2
)
->
(
permut
(
Cons
x
l1
)
(
Cons
x
l2
)).
Axiom
Permut_swap
:
forall
(
a
:
Type
),
forall
(
x
:
a
)
(
y
:
a
)
(
l
:
(
list
a
)),
(
permut
(
Cons
x
(
Cons
y
l
))
(
Cons
y
(
Cons
x
l
))).
Axiom
Permut_mem
:
forall
(
a
:
Type
),
forall
(
x
:
a
)
(
l1
:
(
list
a
))
(
l2
:
(
list
a
)),
(
permut
l1
l2
)
->
((
mem
x
l1
)
->
(
mem
x
l2
)).
Axiom
Permut_length
:
forall
(
a
:
Type
),
forall
(
l1
:
(
list
a
))
(
l2
:
(
list
a
)),
(
permut
l1
l2
)
->
((
length
l1
)
=
(
length
l2
)).
Axiom
Permut_cons_append
:
forall
(
a
:
Type
),
forall
(
x
:
a
)
(
l1
:
(
list
a
))
(
l2
:
(
list
a
)),
(
permut
(
infix_plpl
(
Cons
x
l1
)
l2
)
(
infix_plpl
l1
(
Cons
x
l2
))).
Theorem
Permut_append
:
forall
(
a
:
Type
),
forall
(
l1
:
(
list
a
))
(
l2
:
(
list
a
))
(
k1
:
(
list
a
))
(
k2
:
(
list
a
)),
(
permut
l1
k1
)
->
((
permut
l2
k2
)
->
(
permut
(
infix_plpl
l1
l2
)
(
infix_plpl
k1
k2
))).
(
*
YOU
MAY
EDIT
THE
PROOF
BELOW
*
)
intro
a
.
(
***
moved
to
list
.
why
assert
(
mem_decomp
:
forall
(
x
:
a
)
(
l
:
list
a
),
mem
x
l
->
exists
l1
:
list
a
,
exists
l2
:
list
a
,
l
=
infix_plpl
l1
(
Cons
x
l2
)).
induction
l
;
simpl
;
intros
.
elim
H
.
destruct
H
.
subst
a0
.
exists
Nil
.
exists
l
;
auto
.
destruct
(
IHl
H
)
as
(
e1
,
(
e2
,
h12
)).
exists
(
Cons
a0
e1
);
exists
e2
.
simpl
;
apply
f_equal
;
auto
.
***
)
induction
l1
;
simpl
.
intros
l2
k1
k2
hk1
.
assert
(
k1
=
Nil
).
assert
(
length
(
@
Nil
a
)
=
length
k1
)
%
Z
.
apply
Permut_length
;
auto
.
simpl
in
H
.
destruct
k1
;
auto
.
absurd
(
0
%
Z
=
length
(
Cons
a0
k1
));
auto
.
unfold
length
;
fold
length
.
generalize
(
Length_nonnegative
_
k1
).
omega
.
subst
k1
;
simpl
;
auto
.
intros
.
assert
(
mem
a0
k1
).
apply
Permut_mem
with
(
Cons
a0
l1
);
auto
.
red
;
auto
.
destruct
(
mem_decomp
_
a0
k1
H1
)
as
(
e1
,
(
e2
,
heq
)).
subst
k1
.
apply
Permut_trans
with
(
Cons
a0
(
infix_plpl
(
infix_plpl
e1
e2
)
k2
));
auto
.
apply
Permut_cons
.
apply
IHl1
;
auto
.
assert
(
permut
(
Cons
a0
l1
)
(
Cons
a0
(
infix_plpl
e1
e2
))).
apply
Permut_trans
with
(
infix_plpl
e1
(
Cons
a0
e2
));
auto
.
apply
Permut_sym
.
apply
Permut_cons_append
.
red
in
H2
;
simpl
in
H2
.
red
;
intros
.
generalize
(
H2
x
);
clear
H2
;
intro
.
generalize
(
num_occ_def
_
x
(
Cons
a0
l1
)).
generalize
(
num_occ_def
_
x
(
Cons
a0
(
infix_plpl
e1
e2
))).
assert
(
h
:
(
x
=
a0
\
/
x
<>
a0
)
%
Z
)
by
admit
(
*
excluded
middle
*
).
destruct
h
;
intuition
.
do
2
rewrite
<-
Append_assoc
.
simpl
.
apply
Permut_cons_append
.
Qed
.
(
*
DO
NOT
EDIT
BELOW
*
)
examples/programs/mergesort_list/mergesort_list_WP_M_Permut_cons_append_1.v
0 → 100644
View file @
e0488669
(
*
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
list
(
a
:
Type
)
:=
|
Nil
:
list
a
|
Cons
:
a
->
(
list
a
)
->
list
a
.
Set
Contextual
Implicit
.
Implicit
Arguments
Nil
.
Unset
Contextual
Implicit
.
Implicit
Arguments
Cons
.
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
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
))).
Inductive
sorted
:
(
list
Z
)
->
Prop
:=
|
Sorted_Nil
:
(
sorted
(
Nil
:
(
list
Z
)))
|
Sorted_One
:
forall
(
x
:
Z
),
(
sorted
(
Cons
x
(
Nil
:
(
list
Z
))))
|
Sorted_Two
:
forall
(
x
:
Z
)
(
y
:
Z
)
(
l
:
(
list
Z
)),
(
x
<=
y
)
%
Z
->
((
sorted
(
Cons
y
l
))
->
(
sorted
(
Cons
x
(
Cons
y
l
)))).
Set
Implicit
Arguments
.
Fixpoint
mem
(
a
:
Type
)(
x
:
a
)
(
l
:
(
list
a
))
{
struct
l
}:
Prop
:=
match
l
with
|
Nil
=>
False
|
Cons
y
r
=>
(
x
=
y
)
\
/
(
mem
x
r
)
end
.
Unset
Implicit
Arguments
.
Axiom
Sorted_mem
:
forall
(
x
:
Z
)
(
l
:
(
list
Z
)),
((
forall
(
y
:
Z
),
(
mem
y
l
)
->
(
x
<=
y
)
%
Z
)
/
\
(
sorted
l
))
<->
(
sorted
(
Cons
x
l
)).
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
).
Axiom
mem_append
:
forall
(
a
:
Type
),
forall
(
x
:
a
)
(
l1
:
(
list
a
))
(
l2
:
(
list
a
)),
(
mem
x
(
infix_plpl
l1
l2
))
<->
((
mem
x
l1
)
\
/
(
mem
x
l2
)).
Parameter
num_occ
:
forall
(
a
:
Type
),
a
->
(
list
a
)
->
Z
.
Implicit
Arguments
num_occ
.
Axiom
num_occ_def
:
forall
(
a
:
Type
),
forall
(
x
:
a
)
(
l
:
(
list
a
)),
match
l
with
|
Nil
=>
((
num_occ
x
l
)
=
0
%
Z
)
|
Cons
y
r
=>
((
x
=
y
)
->
((
num_occ
x
l
)
=
(
1
%
Z
+
(
num_occ
x
r
))
%
Z
))
/
\
((
~
(
x
=
y
))
->
((
num_occ
x
l
)
=
(
0
%
Z
+
(
num_occ
x
r
))
%
Z
))
end
.
Axiom
Mem_Num_Occ
:
forall
(
a
:
Type
),
forall
(
x
:
a
)
(
l
:
(
list
a
)),
(
mem
x
l
)
<->
(
0
%
Z
<
(
num_occ
x
l
))
%
Z
.
Definition
permut
(
a
:
Type
)(
l1
:
(
list
a
))
(
l2
:
(
list
a
))
:
Prop
:=
forall
(
x
:
a
),
((
num_occ
x
l1
)
=
(
num_occ
x
l2
)).
Implicit
Arguments
permut
.
Axiom
Permut_refl
:
forall
(
a
:
Type
),
forall
(
l
:
(
list
a
)),
(
permut
l
l
).
Axiom
Permut_sym
:
forall
(
a
:
Type
),
forall
(
l1
:
(
list
a
))
(
l2
:
(
list
a
)),
(
permut
l1
l2
)
->
(
permut
l2
l1
).
Axiom
Permut_trans
:
forall
(
a
:
Type
),
forall
(
l1
:
(
list
a
))
(
l2
:
(
list
a
))
(
l3
:
(
list
a
)),
(
permut
l1
l2
)
->
((
permut
l2
l3
)
->
(
permut
l1
l3
)).
Axiom
Permut_cons
:
forall
(
a
:
Type
),
forall
(
x
:
a
)
(
l1
:
(
list
a
))
(
l2
:
(
list
a
)),
(
permut
l1
l2
)
->
(
permut
(
Cons
x
l1
)
(
Cons
x
l2
)).
Axiom
Permut_swap
:
forall
(
a
:
Type
),
forall
(
x
:
a
)
(
y
:
a
)
(
l
:
(
list
a
)),
(
permut
(
Cons
x
(
Cons
y
l
))
(
Cons
y
(
Cons
x
l
))).
Axiom
Permut_mem
:
forall
(
a
:
Type
),
forall
(
x
:
a
)
(
l1
:
(
list
a
))
(
l2
:
(
list
a
)),
(
permut
l1
l2
)
->
((
mem
x
l1
)
->
(
mem
x
l2
)).
Axiom
Permut_length
:
forall
(
a
:
Type
),
forall
(
l1
:
(
list
a
))
(
l2
:
(
list
a
)),
(
permut
l1
l2
)
->
((
length
l1
)
=
(
length
l2
)).
Theorem
Permut_cons_append
:
forall
(
a
:
Type
),
forall
(
x
:
a
)
(
l1
:
(
list
a
))
(
l2
:
(
list
a
)),
(
permut
(
infix_plpl
(
Cons
x
l1
)
l2
)
(
infix_plpl
l1
(
Cons
x
l2
))).
(
*
YOU
MAY
EDIT
THE
PROOF
BELOW
*
)
induction
l1
;
simpl
;
intros
.
apply
Permut_cons
.
apply
Permut_refl
.
apply
Permut_trans
with
(
Cons
a0
(
Cons
x
(
infix_plpl
l1
l2
)));
auto
.
apply
Permut_swap
.
apply
Permut_cons
.
simpl
in
IHl1
.
auto
.
Qed
.
(
*
DO
NOT
EDIT
BELOW
*
)
examples/programs/mergesort_list/mergesort_list_WP_M_WP_parameter_mergesort_1.v
0 → 100644
View file @
e0488669
(
*
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
list
(
a
:
Type
)
:=
|
Nil
:
list
a
|
Cons
:
a
->
(
list
a
)
->
list
a
.
Set
Contextual
Implicit
.
Implicit
Arguments
Nil
.
Unset
Contextual
Implicit
.
Implicit
Arguments
Cons
.
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
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
))).
Inductive
sorted
:
(
list
Z
)
->
Prop
:=
|
Sorted_Nil
:
(
sorted
(
Nil
:
(
list
Z
)))
|
Sorted_One
:
forall
(
x
:
Z
),
(
sorted
(
Cons
x
(
Nil
:
(
list
Z
))))
|
Sorted_Two
:
forall
(
x
:
Z
)
(
y
:
Z
)
(
l
:
(
list
Z
)),
(
x
<=
y
)
%
Z
->
((
sorted
(
Cons
y
l
))
->
(
sorted
(
Cons
x
(
Cons
y
l
)))).
Set
Implicit
Arguments
.
Fixpoint
mem
(
a
:
Type
)(
x
:
a
)
(
l
:
(
list
a
))
{
struct
l
}:
Prop
:=
match
l
with
|
Nil
=>
False
|
Cons
y
r
=>
(
x
=
y
)
\
/
(
mem
x
r
)
end
.
Unset
Implicit
Arguments
.
Axiom
Sorted_mem
:
forall
(
x
:
Z
)
(
l
:
(
list
Z
)),
((
forall
(
y
:
Z
),
(
mem
y
l
)
->
(
x
<=
y
)
%
Z
)
/
\
(
sorted
l
))
<->
(
sorted
(
Cons
x
l
)).
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
).
Axiom
mem_append
:
forall
(
a
:
Type
),
forall
(
x
:
a
)
(
l1
:
(
list
a
))
(
l2
:
(
list
a
)),
(
mem
x
(
infix_plpl
l1
l2
))
<->
((
mem
x
l1
)
\
/
(
mem
x
l2
)).
Parameter
num_occ
:
forall
(
a
:
Type
),
a
->
(
list
a
)
->
Z
.
Implicit
Arguments
num_occ
.
Axiom
num_occ_def
:
forall
(
a
:
Type
),
forall
(
x
:
a
)
(
l
:
(
list
a
)),
match
l
with
|
Nil
=>
((
num_occ
x
l
)
=
0
%
Z
)
|
Cons
y
r
=>
((
x
=
y
)
->
((
num_occ
x
l
)
=
(
1
%
Z
+
(
num_occ
x
r
))
%
Z
))
/
\
((
~
(
x
=
y
))
->
((
num_occ
x
l
)
=
(
0
%
Z
+
(
num_occ
x
r
))
%
Z
))
end
.
Axiom
Mem_Num_Occ
:
forall
(
a
:
Type
),
forall
(
x
:
a
)
(
l
:
(
list
a
)),
(
mem
x
l
)
<->
(
0
%
Z
<
(
num_occ
x
l
))
%
Z
.
Definition
permut
(
a
:
Type
)(
l1
:
(
list
a
))
(
l2
:
(
list
a
))
:
Prop
:=
forall
(
x
:
a
),
((
num_occ
x
l1
)
=
(
num_occ
x
l2
)).
Implicit
Arguments
permut
.
Axiom
Permut_refl
:
forall
(
a
:
Type
),
forall
(
l
:
(
list
a
)),
(
permut
l
l
).
Axiom
Permut_sym
:
forall
(
a
:
Type
),
forall
(
l1
:
(
list
a
))
(
l2
:
(
list
a
)),
(
permut
l1
l2
)
->
(
permut
l2
l1
).
Axiom
Permut_trans
:
forall
(
a
:
Type
),
forall
(
l1
:
(
list
a
))
(
l2
:
(
list
a
))
(
l3
:
(
list
a
)),
(
permut
l1
l2
)
->
((
permut
l2
l3
)
->
(
permut
l1
l3
)).
Axiom
Permut_cons
:
forall
(
a
:
Type
),
forall
(
x
:
a
)
(
l1
:
(
list
a
))
(
l2
:
(
list
a
)),
(
permut
l1
l2
)
->
(
permut
(
Cons
x
l1
)
(
Cons
x
l2
)).
Axiom
Permut_swap
:
forall
(
a
:
Type
),
forall
(
x
:
a
)
(
y
:
a
)
(
l
:
(
list
a
)),
(
permut
(
Cons
x
(
Cons
y
l
))
(
Cons
y
(
Cons
x
l
))).
Axiom
Permut_mem
:
forall
(
a
:
Type
),
forall
(
x
:
a
)
(
l1
:
(
list
a
))
(
l2
:
(
list
a
)),
(
permut
l1
l2
)
->
((
mem
x
l1
)
->
(
mem
x
l2
)).
Axiom
Permut_length
:
forall
(
a
:
Type
),
forall
(
l1
:
(
list
a
))
(
l2
:
(
list
a
)),
(
permut
l1
l2
)
->
((
length
l1
)
=
(
length
l2
)).
Axiom
Permut_cons_append
:
forall
(
a
:
Type
),
forall
(
x
:
a
)
(
l1
:
(
list
a
))
(
l2
:
(
list
a
)),
(
permut
(
infix_plpl
(
Cons
x
l1
)
l2
)
(
infix_plpl
l1
(
Cons
x
l2
))).
Theorem
WP_parameter_mergesort
:
forall
(
l
:
(
list
Z
)),
match
l
with
|
(
Nil
|
Cons
_
Nil
)
=>
True
|
_
=>
(
2
%
Z
<=
(
length
l
))
%
Z
->
forall
(
result
:
(
list
Z
))
(
result1
:
(
list
Z
)),
((
1
%
Z
<=
(
length
result
))
%
Z
/
\
((
1
%
Z
<=
(
length
result1
))
%
Z
/
\
(
permut
l
(
infix_plpl
result
result1
))))
->
(((
0
%
Z
<=
(
length
l
))
%
Z
/
\
((
length
result
)
<
(
length
l
))
%
Z
)
->
forall
(
result2
:
(
list
Z
)),
((
sorted
result2
)
/
\
(
permut
result
result2
))
->
(((
0
%
Z
<=
(
length
l
))
%
Z
/
\
((
length
result1
)
<
(
length
l
))
%
Z
)
->
forall
(
result3
:
(
list
Z
)),
((
sorted
result3
)
/
\
(
permut
result1
result3
))
->
(((
sorted
result2
)
/
\
(
sorted
result3
))
->
forall
(
result4
:
(
list
Z
)),
((
sorted
result4
)
/
\
(
permut
result4
(
infix_plpl
result2
result3
)))
->
(
permut
l
result4
))))
end
.
(
*
YOU
MAY
EDIT
THE
PROOF
BELOW
*
)
destruct
l
;
try
trivial
.
destruct
l
;
try
trivial
.
intuition
.
apply
Permut_trans
with
(
infix_plpl
result2
result3
).
apply
Permut_trans
with
(
infix_plpl
result
result1
);
auto
.
apply
Permut_append
;
auto
.
apply
Permut_sym
;
auto
.
Qed
.
(
*
DO
NOT
EDIT
BELOW
*
)
examples/programs/mergesort_list/why3session.xml
0 → 100644
View file @
e0488669
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session
name=
"examples/programs/mergesort_list/why3session.xml"
>
<file
name=
"../mergesort_list.mlw"
verified=
"true"
expanded=
"true"
>
<theory
name=
"WP M"
verified=
"true"
expanded=
"true"
>
<goal
name=
"Permut_cons_append"
sum=
"0df043e8309df0e1689f1f7a88d0d180"
proved=
"true"
expanded=
"true"
>
<proof
prover=
"coq"
timelimit=
"10"
edited=
"mergesort_list_WP_M_Permut_cons_append_1.v"
obsolete=
"false"
>
<result
status=
"valid"
time=
"0.61"
/>
</proof>
</goal>
<goal
name=
"Permut_append"
sum=
"d4e21514e0240fc5a8bd445d2283b9bf"
proved=
"true"
expanded=
"true"
>
<proof
prover=
"coq"
timelimit=
"10"
edited=
"mergesort_list_WP_M_Permut_append_1.v"
obsolete=
"false"
>
<result
status=
"valid"
time=
"1.22"
/>
</proof>
</goal>
<goal
name=
"WP_parameter split"
expl=
"correctness of parameter split"
sum=
"9ff7c8dbe7d79e1015cb9368a03c1daf"
proved=
"true"
expanded=
"true"
>
<proof
prover=
"alt-ergo"
timelimit=
"10"
edited=
""
obsolete=
"false"
>
<result
status=
"valid"
time=
"6.84"
/>
</proof>
</goal>
<goal
name=
"WP_parameter merge"
expl=
"correctness of parameter merge"
sum=
"71611dbb934bd53af15c4a8a78858ad6"
proved=
"true"
expanded=
"true"
>
<transf
name=
"split_goal"
proved=
"true"
expanded=
"true"
>
<goal
name=
"WP_parameter merge.1"
expl=
"correctness of parameter merge"
sum=
"fe8bc9f9df8d9a6921a7196e1d60e387"
proved=
"true"
expanded=
"true"
>
<proof
prover=
"alt-ergo"
timelimit=
"10"
edited=
""
obsolete=
"false"
>
<result
status=
"valid"
time=
"0.05"
/>
</proof>
</goal>
<goal
name=
"WP_parameter merge.2"
expl=
"correctness of parameter merge"
sum=
"9fa15d85897c3aa78c4380dbaf90ebc6"
proved=
"true"
expanded=
"true"
>
<proof
prover=
"cvc3"
timelimit=
"10"
edited=
""
obsolete=
"false"
>
<result
status=
"valid"
time=
"1.57"
/>
</proof>
</goal>
<goal
name=
"WP_parameter merge.3"
expl=
"correctness of parameter merge"
sum=
"d16c4bd22b087a32b97aee68e2501bed"
proved=
"true"
expanded=
"true"
>
<proof
prover=
"cvc3"
timelimit=
"10"
edited=
""
obsolete=
"false"
>
<result
status=
"valid"
time=
"0.07"
/>
</proof>
<proof
prover=
"alt-ergo"
timelimit=
"10"
edited=
""
obsolete=
"false"
>
<result
status=
"valid"
time=
"0.04"
/>
</proof>
</goal>
<goal
name=
"WP_parameter merge.4"
expl=
"correctness of parameter merge"
sum=
"020cc4887c52566b6403bdfa06601ab1"
proved=
"true"
expanded=
"true"
>
<proof
prover=
"cvc3"
timelimit=
"10"
edited=
""
obsolete=
"false"
>
<result
status=
"valid"
time=
"7.53"
/>
</proof>
</goal>
<goal
name=
"WP_parameter merge.5"
expl=
"correctness of parameter merge"
sum=
"fd637999f4d66653db893dca4f5c92b2"
proved=
"true"
expanded=
"true"
>
<proof
prover=
"cvc3"
timelimit=
"10"
edited=
""
obsolete=
"false"
>
<result
status=
"valid"
time=
"0.03"
/>
</proof>
<proof
prover=
"alt-ergo"
timelimit=
"10"
edited=
""
obsolete=
"false"
>
<result
status=
"valid"
time=
"0.02"
/>
</proof>
</goal>
<goal
name=
"WP_parameter merge.6"
expl=
"correctness of parameter merge"
sum=
"75fd590235fcb4f15729660f43f7a752"
proved=
"true"
expanded=
"true"
>
<proof
prover=
"cvc3"
timelimit=
"10"
edited=
""
obsolete=
"false"
>
<result
status=
"valid"
time=
"0.02"
/>
</proof>
<proof
prover=
"alt-ergo"
timelimit=
"10"
edited=
""
obsolete=
"false"
>
<result
status=
"valid"
time=
"0.03"
/>