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
31a17623
Commit
31a17623
authored
Jun 13, 2013
by
Guillaume Melquiond
Browse files
Fix Coq scripts for examples/vstte12_tree_reconstruction.mlw.
parent
5aaa72aa
Changes
13
Hide whitespace changes
Inline
Side-by-side
examples/vstte12_tree_reconstruction/vstte12_tree_reconstruction_Tree_depths_subtree_1.v
View file @
31a17623
(
*
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
int
.
Int
.
Require
list
.
List
.
Require
list
.
Length
.
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
.
Inductive
tree
:=
|
Leaf
:
tree
|
Node
:
tree
->
tree
->
tree
.
Axiom
tree_WhyType
:
WhyType
tree
.
Existing
Instance
tree_WhyType
.
(
*
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
).
(
*
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
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
))).
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
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
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
))).
(
*
Why3
assumption
*
)
Inductive
tree
:=
|
Leaf
:
tree
|
Node
:
tree
->
tree
->
tree
.
(
*
Why3
assumption
*
)
Set
Implicit
Arguments
.
Fixpoint
depths
(
d
:
Z
)
(
t
:
tree
)
{
struct
t
}:
(
list
Z
)
:=
Fixpoint
depths
(
d
:
Z
)
(
t
:
tree
)
{
struct
t
}:
(
list
Z
)
:=
match
t
with
|
Leaf
=>
(
C
ons
d
(
Nil
:
(
list
Z
))
)
|
(
Node
l
r
)
=>
(
infix_plpl
(
depths
(
d
+
1
%
Z
)
%
Z
l
)
(
depths
(
d
+
1
%
Z
)
%
Z
r
))
|
Leaf
=>
(
c
ons
d
nil
)
|
(
Node
l
r
)
=>
(
List
.
app
(
depths
(
d
+
1
%
Z
)
%
Z
l
)
(
depths
(
d
+
1
%
Z
)
%
Z
r
))
end
.
Unset
Implicit
Arguments
.
Axiom
depths_head
:
forall
(
t
:
tree
)
(
d
:
Z
),
match
(
depths
d
t
)
with
|
(
C
ons
x
_
)
=>
(
d
<=
x
)
%
Z
|
N
il
=>
False
|
(
c
ons
x
_
)
=>
(
d
<=
x
)
%
Z
|
n
il
=>
False
end
.
Axiom
depths_unique
:
forall
(
t1
:
tree
)
(
t2
:
tree
)
(
d
:
Z
)
(
s1
:
(
list
Z
))
(
s2
:
(
list
Z
)),
((
infix_plpl
(
depths
d
t1
)
s1
)
=
(
infix_plpl
(
depths
d
t2
)
s2
))
->
((
t1
=
t2
)
/
\
(
s1
=
s2
)).
Axiom
depths_unique2
:
forall
(
t1
:
tree
)
(
t2
:
tree
)
(
d1
:
Z
)
(
d2
:
Z
),
((
depths
d1
t1
)
=
(
depths
d2
t2
))
->
((
d1
=
d2
)
/
\
(
t1
=
t2
)).
(
s2
:
(
list
Z
)),
((
List
.
app
(
depths
d
t1
)
s1
)
=
(
List
.
app
(
depths
d
t2
)
s2
))
->
((
t1
=
t2
)
/
\
(
s1
=
s2
)).
Axiom
depths_prefix
:
forall
(
t
:
tree
)
(
d1
:
Z
)
(
d2
:
Z
)
(
s1
:
(
list
Z
))
(
s2
:
(
list
Z
)),
((
infix_plpl
(
depths
d1
t
)
s1
)
=
(
infix_plpl
(
depths
d2
t
)
s2
))
->
(
d1
=
d2
).
Axiom
depths_prefix
:
forall
(
t
:
tree
)
(
d1
:
Z
)
(
d2
:
Z
)
(
s1
:
(
list
Z
))
(
s2
:
(
list
Z
)),
((
List
.
app
(
depths
d1
t
)
s1
)
=
(
List
.
app
(
depths
d2
t
)
s2
))
->
(
d1
=
d2
).
Axiom
depths_prefix_simple
:
forall
(
t
:
tree
)
(
d1
:
Z
)
(
d2
:
Z
),
((
depths
d1
t
)
=
(
depths
d2
t
))
->
(
d1
=
d2
).
...
...
@@ -100,18 +42,20 @@ Axiom depths_prefix_simple : forall (t:tree) (d1:Z) (d2:Z), ((depths d1
Require
Import
Why3
.
Ltac
z
:=
why3
"z3"
timelimit
5.
(
*
Why3
goal
*
)
Theorem
depths_subtree
:
forall
(
t1
:
tree
)
(
t2
:
tree
)
(
d1
:
Z
)
(
d2
:
Z
)
(
s1
:
(
list
Z
)),
((
infix_plpl
(
depths
d1
t1
)
s1
)
=
(
depths
d2
t2
))
->
(
d2
<=
d1
)
%
Z
.
Theorem
depths_subtree
:
forall
(
t1
:
tree
)
(
t2
:
tree
)
(
d1
:
Z
)
(
d2
:
Z
)
(
s1
:
(
list
Z
)),
((
List
.
app
(
depths
d1
t1
)
s1
)
=
(
depths
d2
t2
))
->
(
d2
<=
d1
)
%
Z
.
(
*
Why3
intros
t1
t2
d1
d2
s1
h1
.
*
)
induction
t1
;
simpl
.
z
.
intros
t2
d1
d2
s1
.
rewrite
<-
Append_assoc
.
rewrite
<-
Append
.
Append_assoc
.
intro
h
.
assert
(
d2
<=
d1
+
1
)
%
Z
by
z
.
assert
(
d2
=
d1
+
1
\
/
d2
<
d1
+
1
)
%
Z
by
omega
.
destruct
H0
.
subst
d2
.
replace
(
depths
(
d1
+
1
)
t2
)
%
Z
with
(
infix_plpl
(
depths
(
d1
+
1
)
t2
)
N
il
)
%
Z
in
h
.
replace
(
depths
(
d1
+
1
)
t2
)
%
Z
with
(
app
(
depths
(
d1
+
1
)
t2
)
n
il
)
%
Z
in
h
.
assert
(
t1_1
=
t2
)
by
z
.
z
.
z
.
...
...
examples/vstte12_tree_reconstruction/vstte12_tree_reconstruction_Tree_depths_unique2_1.v
View file @
31a17623
(
*
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
int
.
Int
.
Require
list
.
List
.
Require
list
.
Length
.
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
.
Inductive
tree
:=
|
Leaf
:
tree
|
Node
:
tree
->
tree
->
tree
.
Axiom
tree_WhyType
:
WhyType
tree
.
Existing
Instance
tree_WhyType
.
(
*
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
).
(
*
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
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
))).
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
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
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
))).
(
*
Why3
assumption
*
)
Inductive
tree
:=
|
Leaf
:
tree
|
Node
:
tree
->
tree
->
tree
.
(
*
Why3
assumption
*
)
Set
Implicit
Arguments
.
Fixpoint
depths
(
d
:
Z
)
(
t
:
tree
)
{
struct
t
}:
(
list
Z
)
:=
Fixpoint
depths
(
d
:
Z
)
(
t
:
tree
)
{
struct
t
}:
(
list
Z
)
:=
match
t
with
|
Leaf
=>
(
C
ons
d
(
Nil
:
(
list
Z
))
)
|
(
Node
l
r
)
=>
(
infix_plpl
(
depths
(
d
+
1
%
Z
)
%
Z
l
)
(
depths
(
d
+
1
%
Z
)
%
Z
r
))
|
Leaf
=>
(
c
ons
d
nil
)
|
(
Node
l
r
)
=>
(
List
.
app
(
depths
(
d
+
1
%
Z
)
%
Z
l
)
(
depths
(
d
+
1
%
Z
)
%
Z
r
))
end
.
Unset
Implicit
Arguments
.
Axiom
depths_head
:
forall
(
t
:
tree
)
(
d
:
Z
),
match
(
depths
d
t
)
with
|
(
C
ons
x
_
)
=>
(
d
<=
x
)
%
Z
|
N
il
=>
False
|
(
c
ons
x
_
)
=>
(
d
<=
x
)
%
Z
|
n
il
=>
False
end
.
Axiom
depths_unique
:
forall
(
t1
:
tree
)
(
t2
:
tree
)
(
d
:
Z
)
(
s1
:
(
list
Z
))
(
s2
:
(
list
Z
)),
((
infix_plpl
(
depths
d
t1
)
s1
)
=
(
infix_plpl
(
depths
d
t2
)
s2
))
->
((
t1
=
t2
)
/
\
(
s1
=
s2
)).
(
s2
:
(
list
Z
)),
((
List
.
app
(
depths
d
t1
)
s1
)
=
(
List
.
app
(
depths
d
t2
)
s2
))
->
((
t1
=
t2
)
/
\
(
s1
=
s2
)).
Axiom
depths_prefix
:
forall
(
t
:
tree
)
(
d1
:
Z
)
(
d2
:
Z
)
(
s1
:
(
list
Z
))
(
s2
:
(
list
Z
)),
((
infix_plpl
(
depths
d1
t
)
s1
)
=
(
infix_plpl
(
depths
d2
t
)
s2
))
->
(
d1
=
d2
).
Axiom
depths_prefix
:
forall
(
t
:
tree
)
(
d1
:
Z
)
(
d2
:
Z
)
(
s1
:
(
list
Z
))
(
s2
:
(
list
Z
)),
((
List
.
app
(
depths
d1
t
)
s1
)
=
(
List
.
app
(
depths
d2
t
)
s2
))
->
(
d1
=
d2
).
Axiom
depths_prefix_simple
:
forall
(
t
:
tree
)
(
d1
:
Z
)
(
d2
:
Z
),
((
depths
d1
t
)
=
(
depths
d2
t
))
->
(
d1
=
d2
).
Axiom
depths_subtree
:
forall
(
t1
:
tree
)
(
t2
:
tree
)
(
d1
:
Z
)
(
d2
:
Z
)
(
s1
:
(
list
Z
)),
((
infix_plpl
(
depths
d1
t1
)
s1
)
=
(
depths
d2
t2
))
->
(
d2
<=
d1
)
%
Z
.
Axiom
depths_subtree
:
forall
(
t1
:
tree
)
(
t2
:
tree
)
(
d1
:
Z
)
(
d2
:
Z
)
(
s1
:
(
list
Z
)),
((
List
.
app
(
depths
d1
t1
)
s1
)
=
(
depths
d2
t2
))
->
(
d2
<=
d1
)
%
Z
.
Require
Import
Why3
.
Ltac
z
:=
why3
"z3"
timelimit
5.
(
*
Why3
goal
*
)
Theorem
depths_unique2
:
forall
(
t1
:
tree
)
(
t2
:
tree
)
(
d1
:
Z
)
(
d2
:
Z
),
((
depths
d1
t1
)
=
(
depths
d2
t2
))
->
((
d1
=
d2
)
/
\
(
t1
=
t2
)).
(
*
Why3
intros
t1
t2
d1
d2
h1
.
*
)
intros
t1
t2
d1
d2
h
.
assert
(
depths
d1
t1
=
infix_plpl
(
depths
d1
t1
)
N
il
)
by
z
.
assert
(
depths
d1
t1
=
app
(
depths
d1
t1
)
n
il
)
by
z
.
assert
(
d1
>=
d2
)
%
Z
by
z
.
assert
(
depths
d2
t2
=
infix_plpl
(
depths
d2
t2
)
N
il
)
by
z
.
assert
(
depths
d2
t2
=
app
(
depths
d2
t2
)
n
il
)
by
z
.
assert
(
d1
=
d2
)
by
z
.
z
.
Qed
.
...
...
examples/vstte12_tree_reconstruction/vstte12_tree_reconstruction_Tree_depths_unique_1.v
View file @
31a17623
(
*
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
int
.
Int
.
Require
list
.
List
.
Require
list
.
Length
.
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
.
Inductive
tree
:=
|
Leaf
:
tree
|
Node
:
tree
->
tree
->
tree
.
Axiom
tree_WhyType
:
WhyType
tree
.
Existing
Instance
tree_WhyType
.
(
*
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
).
(
*
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
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
))).
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
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
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
))).
(
*
Why3
assumption
*
)
Inductive
tree
:=
|
Leaf
:
tree
|
Node
:
tree
->
tree
->
tree
.
(
*
Why3
assumption
*
)
Set
Implicit
Arguments
.
Fixpoint
depths
(
d
:
Z
)
(
t
:
tree
)
{
struct
t
}:
(
list
Z
)
:=
Fixpoint
depths
(
d
:
Z
)
(
t
:
tree
)
{
struct
t
}:
(
list
Z
)
:=
match
t
with
|
Leaf
=>
(
C
ons
d
(
Nil
:
(
list
Z
))
)
|
(
Node
l
r
)
=>
(
infix_plpl
(
depths
(
d
+
1
%
Z
)
%
Z
l
)
(
depths
(
d
+
1
%
Z
)
%
Z
r
))
|
Leaf
=>
(
c
ons
d
nil
)
|
(
Node
l
r
)
=>
(
List
.
app
(
depths
(
d
+
1
%
Z
)
%
Z
l
)
(
depths
(
d
+
1
%
Z
)
%
Z
r
))
end
.
Unset
Implicit
Arguments
.
Axiom
depths_head
:
forall
(
t
:
tree
)
(
d
:
Z
),
match
(
depths
d
t
)
with
|
(
C
ons
x
_
)
=>
(
d
<=
x
)
%
Z
|
N
il
=>
False
|
(
c
ons
x
_
)
=>
(
d
<=
x
)
%
Z
|
n
il
=>
False
end
.
(
*
Why3
goal
*
)
Theorem
depths_unique
:
forall
(
t1
:
tree
)
(
t2
:
tree
)
(
d
:
Z
)
(
s1
:
(
list
Z
))
(
s2
:
(
list
Z
)),
((
infix_plpl
(
depths
d
t1
)
s1
)
=
(
infix_plpl
(
depths
d
t2
)
s2
))
->
((
t1
=
t2
)
/
\
(
s1
=
s2
)).
(
*
YOU
MAY
EDIT
THE
PROOF
BELOW
*
)
(
s2
:
(
list
Z
)),
((
List
.
app
(
depths
d
t1
)
s1
)
=
(
List
.
app
(
depths
d
t2
)
s2
))
->
((
t1
=
t2
)
/
\
(
s1
=
s2
)).
(
*
Why3
intros
t1
t2
d
s1
s2
h1
.
*
)
induction
t1
.
simpl
;
intros
.
induction
t2
.
...
...
@@ -112,7 +57,7 @@ intros h; injection h.
intros
;
apply
False_ind
;
omega
.
(
*
t2
=
Node
*
)
intros
.
do
2
(
rewrite
<-
Append_assoc
in
H
).
do
2
(
rewrite
<-
Append
.
Append_assoc
in
H
).
generalize
(
IHt1_1
t2_1
(
d
+
1
)
_
_
H
)
%
Z
.
clear
IHt1_1
.
intros
(
eq1
,
H1
).
generalize
(
IHt1_2
t2_2
(
d
+
1
)
_
_
H1
)
%
Z
.
clear
IHt1_2
.
...
...
examples/vstte12_tree_reconstruction/vstte12_tree_reconstruction_WP_Harness_WP_parameter_harness2_2.v
View file @
31a17623
...
...
@@ -3,116 +3,61 @@
Require
Import
BuiltIn
.
Require
BuiltIn
.
Require
int
.
Int
.
Require
list
.
List
.
Require
list
.
Length
.
Require
list
.
Mem
.
Require
list
.
Append
.
(
*
Why3
assumption
*
)
Definition
unit
:=
unit
.
Definition
unit
:=
unit
.
(
*
Why3
assumption
*
)
Inductive
list
(
a
:
Type
)
{
a_WT
:
WhyType
a
}
:=
|
Nil
:
list
a
|
Cons
:
a
->
(
list
a
)
->
list
a
.
Axiom
list_WhyType
:
forall
(
a
:
Type
)
{
a_WT
:
WhyType
a
}
,
WhyType
(
list
a
).
Existing
Instance
list_WhyType
.
Implicit
Arguments
Nil
[[
a
]
[
a_WT
]].
Implicit
Arguments
Cons
[[
a
]
[
a_WT
]].
(
*
Why3
assumption
*
)
Fixpoint
infix_plpl
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
(
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
.
Axiom
Append_assoc
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
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
}
{
a_WT
:
WhyType
a
}
,
forall
(
l
:
(
list
a
)),
((
infix_plpl
l
(
Nil
:
(
list
a
)))
=
l
).
(
*
Why3
assumption
*
)
Fixpoint
length
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
(
l
:
(
list
a
))
{
struct
l
}:
BuiltIn
.
int
:=
match
l
with
|
Nil
=>
0
%
Z
|
(
Cons
_
r
)
=>
(
1
%
Z
+
(
length
r
))
%
Z
end
.
Axiom
Length_nonnegative
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
l
:
(
list
a
)),
(
0
%
Z
<=
(
length
l
))
%
Z
.
Axiom
Length_nil
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
l
:
(
list
a
)),
((
length
l
)
=
0
%
Z
)
<->
(
l
=
(
Nil
:
(
list
a
))).
Axiom
Append_length
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
l1
:
(
list
a
))
(
l2
:
(
list
a
)),
((
length
(
infix_plpl
l1
l2
))
=
((
length
l1
)
+
(
length
l2
))
%
Z
).
(
*
Why3
assumption
*
)
Fixpoint
mem
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
(
x
:
a
)
(
l
:
(
list
a
))
{
struct
l
}:
Prop
:=
match
l
with
|
Nil
=>
False
|
(
Cons
y
r
)
=>
(
x
=
y
)
\
/
(
mem
x
r
)
end
.
Axiom
mem_append
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
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
}
{
a_WT
:
WhyType
a
}
,
forall
(
x
:
a
)
(
l
:
(
list
a
)),
(
mem
x
l
)
->
exists
l1
:
(
list
a
),
exists
l2
:
(
list
a
),
(
l
=
(
infix_plpl
l1
(
Cons
x
l2
))).
(
*
Why3
assumption
*
)
Inductive
tree
:=
|
Leaf
:
tree
|
Node
:
tree
->
tree
->
tree
.
Inductive
tree
:=
|
Leaf
:
tree
|
Node
:
tree
->
tree
->
tree
.
Axiom
tree_WhyType
:
WhyType
tree
.
Existing
Instance
tree_WhyType
.
(
*
Why3
assumption
*
)
Fixpoint
depths
(
d
:
BuiltIn
.
int
)
(
t
:
tree
)
{
struct
t
}:
(
list
BuiltIn
.
int
)
:=
Fixpoint
depths
(
d
:
Z
)
(
t
:
tree
)
{
struct
t
}:
(
list
Z
)
:=
match
t
with
|
Leaf
=>
(
C
ons
d
(
Nil
:
(
list
BuiltIn
.
int
))
)
|
(
Node
l
r
)
=>
(
infix_plpl
(
depths
(
d
+
1
%
Z
)
%
Z
l
)
(
depths
(
d
+
1
%
Z
)
%
Z
r
))
|
Leaf
=>
(
c
ons
d
nil
)
|
(
Node
l
r
)
=>
(
List
.
app
(
depths
(
d
+
1
%
Z
)
%
Z
l
)
(
depths
(
d
+
1
%
Z
)
%
Z
r
))
end
.
Axiom
depths_head
:
forall
(
t
:
tree
)
(
d
:
BuiltIn
.
int
),
match
(
depths
d
Axiom
depths_head
:
forall
(
t
:
tree
)
(
d
:
Z
),
match
(
depths
d
t
)
with
|
(
C
ons
x
_
)
=>
(
d
<=
x
)
%
Z
|
N
il
=>
False
|
(
c
ons
x
_
)
=>
(
d
<=
x
)
%
Z
|
n
il
=>
False
end
.
Axiom
depths_unique
:
forall
(
t1
:
tree
)
(
t2
:
tree
)
(
d
:
BuiltIn
.
int
)
(
s1
:
(
list
BuiltIn
.
int
))
(
s2
:
(
list
BuiltIn
.
int
)),
((
infix_plpl
(
depths
d
t1
)
s1
)
=
(
infix_plpl
(
depths
d
t2
)
s2
))
->
((
t1
=
t2
)
/
\
(
s1
=
s2
)).
Axiom
depths_unique
:
forall
(
t1
:
tree
)
(
t2
:
tree
)
(
d
:
Z
)
(
s1
:
(
list
Z
))
(
s2
:
(
list
Z
)),
((
List
.
app
(
depths
d
t1
)
s1
)
=
(
List
.
app
(
depths
d
t2
)
s2
))
->
((
t1
=
t2
)
/
\
(
s1
=
s2
)).
Axiom
depths_prefix
:
forall
(
t
:
tree
)
(
d1
:
BuiltIn
.
int
)
(
d2
:
BuiltIn
.
int
)
(
s
1
:
(
list
BuiltIn
.
int
))
(
s2
:
(
list
BuiltIn
.
int
)),
((
infix_plpl
(
depths
d
1
t
)
s1
)
=
(
infix_plpl
(
depths
d2
t
)
s2
))
->
(
d1
=
d2
).
Axiom
depths_prefix
:
forall
(
t
:
tree
)
(
d1
:
Z
)
(
d2
:
Z
)
(
s1
:
(
list
Z
)
)
(
s
2
:
(
list
Z
))
,
(
(
List
.
app
(
depths
d1
t
)
s1
)
=
(
List
.
app
(
depths
d
2
t
)
s2
))
->
(
d1
=
d2
).