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
124
Issues
124
List
Boards
Labels
Service Desk
Milestones
Merge Requests
18
Merge Requests
18
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
58d81b49
Commit
58d81b49
authored
Feb 15, 2013
by
MARCHE Claude
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
treedel example: a few renamings
type point -> loc predicate tree -> istree post-condition: t -> t'
parent
6847fe50
Changes
4
Expand all
Hide whitespace changes
Inline
Side-by-side
Showing
4 changed files
with
235 additions
and
220 deletions
+235
-220
examples/verifythis_fm2012_treedel.mlw
examples/verifythis_fm2012_treedel.mlw
+29
-29
examples/verifythis_fm2012_treedel/verifythis_fm2012_treedel_Treedel_WP_parameter_search_tree_delete_min_2.v
...2_treedel_Treedel_WP_parameter_search_tree_delete_min_2.v
+31
-31
examples/verifythis_fm2012_treedel/verifythis_fm2012_treedel_Treedel_main_lemma_1.v
..._treedel/verifythis_fm2012_treedel_Treedel_main_lemma_1.v
+80
-65
examples/verifythis_fm2012_treedel/why3session.xml
examples/verifythis_fm2012_treedel/why3session.xml
+95
-95
No files found.
examples/verifythis_fm2012_treedel.mlw
View file @
58d81b49
...
...
@@ -12,7 +12,7 @@ Iterative deletion in a binary search tree - 90 minutes
VERIFICATION TASK
-----------------
Given: a
pointer
t to the root of a non-empty binary search tree (not
Given: a
loc
t to the root of a non-empty binary search tree (not
necessarily balanced). Verify that the following procedure removes the
node with the minimal key from the tree. After removal, the data
structure should again be a binary search tree.
...
...
@@ -38,30 +38,30 @@ Note: When implementing in a garbage-collected language, the call to
dispose() is superfluous.
*)
(* Why3 has no
pointer
data structures, so we model the heap *)
(* Why3 has no
loc
data structures, so we model the heap *)
module Memory
use export map.Map
use export ref.Ref
type
pointer
constant null:
pointer
type node = { left:
pointer; right: pointer
; data: int; }
type memory = map
pointer
node
type
loc
constant null:
loc
type node = { left:
loc; right: loc
; data: int; }
type memory = map
loc
node
(* the global variable mem contains the current state of the memory *)
val mem: ref memory
(* accessor functions to ensure safety i.e. no null
pointer
dereference *)
let get_left (p:
pointer) : pointer
=
(* accessor functions to ensure safety i.e. no null
loc
dereference *)
let get_left (p:
loc) : loc
=
requires { p <> null }
ensures { result = !mem[p].left }
!mem[p].left
let get_right (p:
pointer) : pointer
=
let get_right (p:
loc) : loc
=
requires { p <> null }
ensures { result = !mem[p].right }
!mem[p].right
let get_data (p:
pointer
) : int =
let get_data (p:
loc
) : int =
requires { p <> null }
ensures { result = !mem[p].data }
!mem[p].data
...
...
@@ -76,14 +76,14 @@ module Treedel
use import list.Distinct
(* there is a binary tree t rooted at p in memory m *)
inductive
tree (m: memory) (p: pointer) (t: tree pointer
) =
inductive
istree (m: memory) (p: loc) (t: tree loc
) =
| leaf: forall m: memory.
tree m null Empty
| node: forall m: memory, p:
pointer, l r: tree pointer
.
is
tree m null Empty
| node: forall m: memory, p:
loc, l r: tree loc
.
p <> null ->
tree m m[p].left l ->
tree m m[p].right r ->
tree m p (Node l p r)
is
tree m m[p].left l ->
is
tree m m[p].right r ->
is
tree m p (Node l p r)
(* degenerated zipper for a left descent (= list of pairs) *)
type zipper 'a =
...
...
@@ -99,32 +99,32 @@ module Treedel
forall z "induction": zipper 'a, x: 'a, l r: tree 'a.
inorder (zip (Node l x r) z) = inorder l ++ Cons x (inorder (zip r z))
let ghost left (t: tree
pointer
) =
let ghost left (t: tree
loc
) =
requires { t <> Empty }
ensures { match t with Empty -> false | Node l _ _ -> result = l end }
match t with Empty -> absurd | Node l _ _ -> l end
let ghost right (t: tree
pointer
) =
let ghost right (t: tree
loc
) =
requires { t <> Empty }
ensures { match t with Empty -> false | Node _ _ r -> result = r end }
match t with Empty -> absurd | Node _ _ r -> r end
lemma main_lemma:
forall m: memory, t pp p:
pointer, ppr pr: tree pointer, z: zipper pointer
.
forall m: memory, t pp p:
loc, ppr pr: tree loc, z: zipper loc
.
let it = zip (Node (Node Empty p pr) pp ppr) z in
tree m t it -> distinct (inorder it) ->
is
tree m t it -> distinct (inorder it) ->
let m' = m[pp <- { m[pp] with left = m[p].right }] in
tree m' t (zip (Node pr pp ppr) z)
is
tree m' t (zip (Node pr pp ppr) z)
(* specification is as follows: if t is a tree and its list of
pointer
s
(* specification is as follows: if t is a tree and its list of
loc
s
is x::l then, at the end of execution, its list is l and m = x.data *)
let search_tree_delete_min
(t:
pointer) (ghost it: tree pointer) (ghost ot: ref (tree pointer
))
: (
pointer
, int)
(t:
loc) (ghost it: tree loc) (ghost ot: ref (tree loc
))
: (
loc
, int)
requires { t <> null }
requires { tree !mem t it }
requires {
is
tree !mem t it }
requires { distinct (inorder it) }
ensures { let (t
, m) = result in tree !mem t
!ot /\
ensures { let (t
', m) = result in istree !mem t'
!ot /\
match inorder it with
| Nil -> false
| Cons p l -> m = !mem[p].data /\ inorder !ot = l end }
...
...
@@ -146,8 +146,8 @@ module Treedel
invariant { !pp <> null /\ !mem[!pp].left = !p }
invariant { !p <> null /\ !mem[!p].left = !tt }
invariant { let pt = Node !subtree !pp !ppr in
tree !mem !pp pt /\ zip pt !zipper = it }
assert { tree !mem !p !subtree };
is
tree !mem !pp pt /\ zip pt !zipper = it }
assert {
is
tree !mem !p !subtree };
ghost zipper := Left !zipper !pp !ppr;
ghost ppr := right !subtree;
ghost subtree := left !subtree;
...
...
@@ -155,7 +155,7 @@ module Treedel
p := !tt;
tt := get_left !p
done;
assert { tree !mem !p !subtree };
assert {
is
tree !mem !p !subtree };
assert { !pp <> !p };
let m = get_data !p in
tt := get_right !p;
...
...
examples/verifythis_fm2012_treedel/verifythis_fm2012_treedel_Treedel_WP_parameter_search_tree_delete_min_2.v
View file @
58d81b49
...
...
@@ -21,15 +21,15 @@ Definition contents {a:Type} {a_WT:WhyType a} (v:(ref a)): a :=
|
(
mk_ref
x
)
=>
x
end
.
Axiom
pointer
:
Type
.
Parameter
pointer_WhyType
:
WhyType
pointer
.
Existing
Instance
pointer
_WhyType
.
Axiom
loc
:
Type
.
Parameter
loc_WhyType
:
WhyType
loc
.
Existing
Instance
loc
_WhyType
.
Parameter
null
:
pointer
.
Parameter
null
:
loc
.
(
*
Why3
assumption
*
)
Inductive
node
:=
|
mk_node
:
pointer
->
pointer
->
Z
->
node
.
|
mk_node
:
loc
->
loc
->
Z
->
node
.
Axiom
node_WhyType
:
WhyType
node
.
Existing
Instance
node_WhyType
.
...
...
@@ -39,19 +39,19 @@ Definition data (v:node): Z := match v with
end
.
(
*
Why3
assumption
*
)
Definition
right1
(
v
:
node
)
:
pointer
:=
Definition
right1
(
v
:
node
)
:
loc
:=
match
v
with
|
(
mk_node
x
x1
x2
)
=>
x1
end
.
(
*
Why3
assumption
*
)
Definition
left1
(
v
:
node
)
:
pointer
:=
Definition
left1
(
v
:
node
)
:
loc
:=
match
v
with
|
(
mk_node
x
x1
x2
)
=>
x
end
.
(
*
Why3
assumption
*
)
Definition
memory
:=
(
map
.
Map
.
map
pointer
node
).
Definition
memory
:=
(
map
.
Map
.
map
loc
node
).
(
*
Why3
assumption
*
)
Inductive
tree
...
...
@@ -140,12 +140,12 @@ Axiom distinct_append : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list
x
l1
)
->
~
(
mem
x
l2
))
->
(
distinct
(
infix_plpl
l1
l2
)))).
(
*
Why3
assumption
*
)
Inductive
tree1
:
(
map
.
Map
.
map
pointer
node
)
->
pointer
->
(
tree
pointer
)
->
Prop
:=
|
leaf
:
forall
(
m
:
(
map
.
Map
.
map
pointer
node
)),
(
tree1
m
null
(
Empty
:
(
tree
pointer
)))
|
node1
:
forall
(
m
:
(
map
.
Map
.
map
pointer
node
))
(
p
:
pointer
)
(
l
:
(
tree
pointer
))
(
r
:
(
tree
pointer
)),
(
~
(
p
=
null
))
->
((
tree1
m
Inductive
tree1
:
(
map
.
Map
.
map
loc
node
)
->
loc
->
(
tree
loc
)
->
Prop
:=
|
leaf
:
forall
(
m
:
(
map
.
Map
.
map
loc
node
)),
(
tree1
m
null
(
Empty
:
(
tree
loc
)))
|
node1
:
forall
(
m
:
(
map
.
Map
.
map
loc
node
))
(
p
:
loc
)
(
l
:
(
tree
loc
))
(
r
:
(
tree
loc
)),
(
~
(
p
=
null
))
->
((
tree1
m
(
left1
(
map
.
Map
.
get
m
p
))
l
)
->
((
tree1
m
(
right1
(
map
.
Map
.
get
m
p
))
r
)
->
(
tree1
m
p
(
Node
l
p
r
)))).
...
...
@@ -171,9 +171,9 @@ Axiom inorder_zip : forall {a:Type} {a_WT:WhyType a}, forall (z:(zipper a))
(
x
:
a
)
(
l
:
(
tree
a
))
(
r
:
(
tree
a
)),
((
inorder
(
zip
(
Node
l
x
r
)
z
))
=
(
infix_plpl
(
inorder
l
)
(
Cons
x
(
inorder
(
zip
r
z
))))).
Axiom
main_lemma
:
forall
(
m
:
(
map
.
Map
.
map
pointer
node
))
(
t
:
pointer
)
(
pp
:
pointer
)
(
p
:
pointer
)
(
ppr
:
(
tree
pointer
))
(
pr
:
(
tree
pointer
))
(
z
:
(
zipper
pointer
)),
let
it
:=
(
zip
(
Node
(
Node
(
Empty
:
(
tree
pointer
))
p
Axiom
main_lemma
:
forall
(
m
:
(
map
.
Map
.
map
loc
node
))
(
t
:
loc
)
(
pp
:
loc
)
(
p
:
loc
)
(
ppr
:
(
tree
loc
))
(
pr
:
(
tree
loc
))
(
z
:
(
zipper
loc
)),
let
it
:=
(
zip
(
Node
(
Node
(
Empty
:
(
tree
loc
))
p
pr
)
pp
ppr
)
z
)
in
((
tree1
m
t
it
)
->
((
distinct
(
inorder
it
))
->
(
tree1
(
map
.
Map
.
set
m
pp
(
mk_node
(
right1
(
map
.
Map
.
get
m
p
))
(
right1
(
map
.
Map
.
get
m
pp
))
(
data
(
map
.
Map
.
get
m
pp
))))
t
(
zip
(
Node
pr
pp
...
...
@@ -182,39 +182,39 @@ Axiom main_lemma : forall (m:(map.Map.map pointer node)) (t:pointer)
Require
Import
Why3
.
Ltac
ae
:=
why3
"alt-ergo"
timelimit
3.
(
*
Why3
goal
*
)
Theorem
WP_parameter_search_tree_delete_min
:
forall
(
t
:
pointer
)
(
it
:
(
tree
pointer
)),
forall
(
mem1
:
(
map
.
Map
.
map
pointer
node
)),
(((
~
(
t
=
null
))
/
\
Theorem
WP_parameter_search_tree_delete_min
:
forall
(
t
:
loc
)
(
it
:
(
tree
loc
)),
forall
(
mem1
:
(
map
.
Map
.
map
loc
node
)),
(((
~
(
t
=
null
))
/
\
(
tree1
mem1
t
it
))
/
\
(
distinct
(
inorder
it
)))
->
((
~
(
t
=
null
))
->
((
~
((
left1
(
map
.
Map
.
get
mem1
t
))
=
null
))
->
((
~
((
left1
(
map
.
Map
.
get
mem1
t
))
=
null
))
->
((
~
(
it
=
(
Empty
:
(
tree
pointer
))))
->
forall
(
o
:
(
tree
pointer
)),
match
it
with
t
))
=
null
))
->
((
~
(
it
=
(
Empty
:
(
tree
loc
))))
->
forall
(
o
:
(
tree
loc
)),
match
it
with
|
Empty
=>
False
|
(
Node
_
_
r
)
=>
(
o
=
r
)
end
->
((
~
(
it
=
(
Empty
:
(
tree
pointer
))))
->
forall
(
o1
:
(
tree
pointer
)),
end
->
((
~
(
it
=
(
Empty
:
(
tree
loc
))))
->
forall
(
o1
:
(
tree
loc
)),
match
it
with
|
Empty
=>
False
|
(
Node
l
_
_
)
=>
(
o1
=
l
)
end
->
forall
(
subtree
:
(
tree
pointer
))
(
ppr
:
(
tree
pointer
))
(
zipper1
:
(
zipper
pointer
))
(
tt
:
pointer
)
(
pp
:
pointer
)
(
p
:
pointer
),
end
->
forall
(
subtree
:
(
tree
loc
))
(
ppr
:
(
tree
loc
))
(
zipper1
:
(
zipper
loc
))
(
tt
:
loc
)
(
pp
:
loc
)
(
p
:
loc
),
((((
~
(
pp
=
null
))
/
\
((
left1
(
map
.
Map
.
get
mem1
pp
))
=
p
))
/
\
((
~
(
p
=
null
))
/
\
((
left1
(
map
.
Map
.
get
mem1
p
))
=
tt
)))
/
\
let
pt
:=
(
Node
subtree
pp
ppr
)
in
((
tree1
mem1
pp
pt
)
/
\
((
zip
pt
zipper1
)
=
it
)))
->
((
tt
=
null
)
->
((
tree1
mem1
p
subtree
)
->
((
~
(
pp
=
p
))
->
((
~
(
p
=
null
))
->
((
~
(
p
=
null
))
->
forall
(
tt1
:
pointer
),
(
tt1
=
(
right1
(
map
.
Map
.
get
mem1
p
)))
->
forall
(
mem2
:
(
map
.
Map
.
map
pointer
node
)),
(
mem2
=
(
map
.
Map
.
set
mem1
pp
forall
(
tt1
:
loc
),
(
tt1
=
(
right1
(
map
.
Map
.
get
mem1
p
)))
->
forall
(
mem2
:
(
map
.
Map
.
map
loc
node
)),
(
mem2
=
(
map
.
Map
.
set
mem1
pp
(
mk_node
tt1
(
right1
(
map
.
Map
.
get
mem1
pp
))
(
data
(
map
.
Map
.
get
mem1
pp
)))))
->
((
~
(
subtree
=
(
Empty
:
(
tree
pointer
))))
->
forall
(
pl
:
(
tree
pointer
)),
pp
)))))
->
((
~
(
subtree
=
(
Empty
:
(
tree
loc
))))
->
forall
(
pl
:
(
tree
loc
)),
match
subtree
with
|
Empty
=>
False
|
(
Node
l
_
_
)
=>
(
pl
=
l
)
end
->
((
pl
=
(
Empty
:
(
tree
pointer
)))
->
((
~
(
subtree
=
(
Empty
:
(
tree
pointer
))))
->
forall
(
o2
:
(
tree
pointer
)),
end
->
((
pl
=
(
Empty
:
(
tree
loc
)))
->
((
~
(
subtree
=
(
Empty
:
(
tree
loc
))))
->
forall
(
o2
:
(
tree
loc
)),
match
subtree
with
|
Empty
=>
False
|
(
Node
_
_
r
)
=>
(
o2
=
r
)
end
->
forall
(
ot
:
(
tree
pointer
)),
(
ot
=
(
zip
o2
(
Left
zipper1
pp
ppr
)))
->
end
->
forall
(
ot
:
(
tree
loc
)),
(
ot
=
(
zip
o2
(
Left
zipper1
pp
ppr
)))
->
match
(
inorder
it
)
with
|
Nil
=>
True
|
(
Cons
p1
l
)
=>
((
inorder
ot
)
=
l
)
...
...
examples/verifythis_fm2012_treedel/verifythis_fm2012_treedel_Treedel_main_lemma_1.v
View file @
58d81b49
...
...
@@ -2,11 +2,35 @@
(
*
Beware
!
Only
edit
allowed
sections
below
*
)
Require
Import
BuiltIn
.
Require
BuiltIn
.
Require
map
.
Map
.
Require
int
.
Int
.
(
*
Why3
assumption
*
)
Definition
unit
:=
unit
.
Definition
unit
:=
unit
.
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
set
:
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
(
set
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
(
set
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
).
(
*
Why3
assumption
*
)
Inductive
ref
(
a
:
Type
)
{
a_WT
:
WhyType
a
}
:=
...
...
@@ -16,46 +40,43 @@ 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
:=
Definition
contents
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
(
v
:
(
ref
a
))
:
a
:=
match
v
with
|
(
mk_ref
x
)
=>
x
end
.
Axiom
pointer
:
Type
.
Parameter
pointer_WhyType
:
WhyType
pointer
.
Existing
Instance
pointer
_WhyType
.
Axiom
loc
:
Type
.
Parameter
loc_WhyType
:
WhyType
loc
.
Existing
Instance
loc
_WhyType
.
Parameter
null
:
pointer
.
Parameter
null
:
loc
.
(
*
Why3
assumption
*
)
Inductive
node
:=
|
mk_node
:
pointer
->
pointer
->
Z
->
node
.
Inductive
node
:=
|
mk_node
:
loc
->
loc
->
Z
->
node
.
Axiom
node_WhyType
:
WhyType
node
.
Existing
Instance
node_WhyType
.
(
*
Why3
assumption
*
)
Definition
data
(
v
:
node
)
:
Z
:=
match
v
with
Definition
data
(
v
:
node
)
:
Z
:=
match
v
with
|
(
mk_node
x
x1
x2
)
=>
x2
end
.
(
*
Why3
assumption
*
)
Definition
right1
(
v
:
node
)
:
pointer
:=
match
v
with
Definition
right1
(
v
:
node
)
:
loc
:=
match
v
with
|
(
mk_node
x
x1
x2
)
=>
x1
end
.
(
*
Why3
assumption
*
)
Definition
left1
(
v
:
node
)
:
pointer
:=
match
v
with
Definition
left1
(
v
:
node
)
:
loc
:=
match
v
with
|
(
mk_node
x
x1
x2
)
=>
x
end
.
(
*
Why3
assumption
*
)
Definition
memory
:=
(
map
.
Map
.
map
pointer
node
).
Definition
memory
:=
(
map
loc
node
).
(
*
Why3
assumption
*
)
Inductive
tree
(
a
:
Type
)
{
a_WT
:
WhyType
a
}
:=
Inductive
tree
(
a
:
Type
)
{
a_WT
:
WhyType
a
}
:=
|
Empty
:
tree
a
|
Node
:
(
tree
a
)
->
a
->
(
tree
a
)
->
tree
a
.
Axiom
tree_WhyType
:
forall
(
a
:
Type
)
{
a_WT
:
WhyType
a
}
,
WhyType
(
tree
a
).
...
...
@@ -64,8 +85,7 @@ Implicit Arguments Empty [[a] [a_WT]].
Implicit
Arguments
Node
[[
a
]
[
a_WT
]].
(
*
Why3
assumption
*
)
Inductive
list
(
a
:
Type
)
{
a_WT
:
WhyType
a
}
:=
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
).
...
...
@@ -74,7 +94,7 @@ 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
Fixpoint
infix_plpl
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
(
l1
:
(
list
a
))
(
l2
:
(
list
a
))
{
struct
l1
}:
(
list
a
)
:=
match
l1
with
|
Nil
=>
l2
...
...
@@ -89,7 +109,7 @@ 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
}:
Z
:=
Fixpoint
length
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
(
l
:
(
list
a
))
{
struct
l
}:
Z
:=
match
l
with
|
Nil
=>
0
%
Z
|
(
Cons
_
r
)
=>
(
1
%
Z
+
(
length
r
))
%
Z
...
...
@@ -106,7 +126,7 @@ Axiom Append_length : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
l2
))
=
((
length
l1
)
+
(
length
l2
))
%
Z
).
(
*
Why3
assumption
*
)
Fixpoint
mem
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
(
x
:
a
)
(
l
:
(
list
a
))
{
struct
l
}:
Prop
:=
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
)
...
...
@@ -121,7 +141,7 @@ Axiom mem_decomp : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l:(list
(
l
=
(
infix_plpl
l1
(
Cons
x
l2
))).
(
*
Why3
assumption
*
)
Fixpoint
inorder
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
(
t
:
(
tree
a
))
{
struct
t
}:
(
list
Fixpoint
inorder
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
(
t
:
(
tree
a
))
{
struct
t
}:
(
list
a
)
:=
match
t
with
|
Empty
=>
(
Nil
:
(
list
a
))
...
...
@@ -132,26 +152,22 @@ Fixpoint inorder {a:Type} {a_WT:WhyType a} (t:(tree a)) {struct t}: (list
Inductive
distinct
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
:
(
list
a
)
->
Prop
:=
|
distinct_zero
:
(
distinct
(
Nil
:
(
list
a
)))
|
distinct_one
:
forall
(
x
:
a
),
(
distinct
(
Cons
x
(
Nil
:
(
list
a
))))
|
distinct_many
:
forall
(
x
:
a
)
(
l
:
(
list
a
)),
(
~
(
mem
x
l
))
->
((
distinct
l
)
->
(
distinct
(
Cons
x
l
))).
|
distinct_many
:
forall
(
x
:
a
)
(
l
:
(
list
a
)),
(
~
(
mem
x
l
))
->
((
distinct
l
)
->
(
distinct
(
Cons
x
l
))).
Axiom
distinct_append
:
forall
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
,
forall
(
l1
:
(
list
a
))
(
l2
:
(
list
a
)),
(
distinct
l1
)
->
((
distinct
l2
)
->
((
forall
(
x
:
a
),
(
mem
x
l1
)
->
~
(
mem
x
l2
))
->
(
distinct
(
infix_plpl
l1
l2
)))).
a
))
(
l2
:
(
list
a
)),
(
distinct
l1
)
->
((
distinct
l2
)
->
((
forall
(
x
:
a
),
(
mem
x
l1
)
->
~
(
mem
x
l2
))
->
(
distinct
(
infix_plpl
l1
l2
)))).
(
*
Why3
assumption
*
)
Inductive
tree1
:
(
map
.
Map
.
map
pointer
node
)
->
pointer
->
(
tree
pointer
)
->
Prop
:=
|
leaf
:
forall
(
m
:
(
map
.
Map
.
map
pointer
node
)),
(
tree1
m
null
(
Empty
:
(
tree
pointer
)))
|
node1
:
forall
(
m
:
(
map
.
Map
.
map
pointer
node
))
(
p
:
pointer
)
(
l
:
(
tree
pointer
))
(
r
:
(
tree
pointer
)),
(
~
(
p
=
null
))
->
((
tree1
m
(
left1
(
map
.
Map
.
get
m
p
))
l
)
->
((
tree1
m
(
right1
(
map
.
Map
.
get
m
p
))
r
)
->
(
tree1
m
p
(
Node
l
p
r
)))).
Inductive
istree
:
(
map
loc
node
)
->
loc
->
(
tree
loc
)
->
Prop
:=
|
leaf
:
forall
(
m
:
(
map
loc
node
)),
(
istree
m
null
(
Empty
:
(
tree
loc
)))
|
node1
:
forall
(
m
:
(
map
loc
node
))
(
p
:
loc
)
(
l
:
(
tree
loc
))
(
r
:
(
tree
loc
)),
(
~
(
p
=
null
))
->
((
istree
m
(
left1
(
get
m
p
))
l
)
->
((
istree
m
(
right1
(
get
m
p
))
r
)
->
(
istree
m
p
(
Node
l
p
r
)))).
(
*
Why3
assumption
*
)
Inductive
zipper
(
a
:
Type
)
{
a_WT
:
WhyType
a
}
:=
Inductive
zipper
(
a
:
Type
)
{
a_WT
:
WhyType
a
}
:=
|
Top
:
zipper
a
|
Left
:
(
zipper
a
)
->
a
->
(
tree
a
)
->
zipper
a
.
Axiom
zipper_WhyType
:
forall
(
a
:
Type
)
{
a_WT
:
WhyType
a
}
,
WhyType
(
zipper
a
).
...
...
@@ -160,7 +176,7 @@ Implicit Arguments Top [[a] [a_WT]].
Implicit
Arguments
Left
[[
a
]
[
a_WT
]].
(
*
Why3
assumption
*
)
Fixpoint
zip
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
(
t
:
(
tree
a
))
(
z
:
(
zipper
Fixpoint
zip
{
a
:
Type
}
{
a_WT
:
WhyType
a
}
(
t
:
(
tree
a
))
(
z
:
(
zipper
a
))
{
struct
z
}:
(
tree
a
)
:=
match
z
with
|
Top
=>
t
...
...
@@ -177,7 +193,7 @@ Require Import Why3.
Ltac
ae
:=
why3
"Alt-Ergo,0.95,"
timelimit
3.
Lemma
distinct1
:
forall
(
p
pp
:
pointer
)
(
pr
ppr
:
tree
pointer
),
forall
(
p
pp
:
loc
)
(
pr
ppr
:
tree
loc
),
distinct
(
Cons
p
(
infix_plpl
(
inorder
pr
)
(
Cons
pp
(
inorder
ppr
))))
->
p
<>
pp
.
Proof
.
...
...
@@ -187,7 +203,7 @@ Lemma distinct1:
Lemma
distinct2
:
forall
m
p
p
'
n
t
,
let
m
'
:=
Map
.
set
m
p
'
n
in
tree1
m
p
t
->
~
(
mem
p
'
(
inorder
t
))
->
tree1
m
'
p
t
.
istree
m
p
t
->
~
(
mem
p
'
(
inorder
t
))
->
istree
m
'
p
t
.
Proof
.
induction
1
;
simpl
.
ae
.
...
...
@@ -202,27 +218,27 @@ Lemma distinct2:
Qed
.
Lemma
distinct3
:
forall
(
pp
:
pointer
)
(
l1
l2
:
list
pointer
),
forall
(
pp
:
loc
)
(
l1
l2
:
list
loc
),
distinct
(
infix_plpl
l1
(
Cons
pp
l2
))
->
~
(
mem
pp
l1
).
Proof
.
induction
l1
;
simpl
;
ae
.
Qed
.
Lemma
distinct4
:
forall
(
pp
:
pointer
)
(
l1
l2
:
list
pointer
),
forall
(
pp
:
loc
)
(
l1
l2
:
list
loc
),
distinct
(
infix_plpl
l1
(
Cons
pp
l2
))
->
~
(
mem
pp
l2
).
Proof
.
induction
l1
;
simpl
;
ae
.
Qed
.
Lemma
distinct_append1
:
forall
(
l1
l2
:
list
pointer
),
distinct
(
infix_plpl
l1
l2
)
->
distinct
l1
.
forall
(
l1
l2
:
list
loc
),
distinct
(
infix_plpl
l1
l2
)
->
distinct
l1
.
Proof
.
induction
l1
;
simpl
;
ae
.
Qed
.
Lemma
distinct5
:
forall
z
(
p
:
pointer
)
(
l
r
:
tree
pointer
),
forall
z
(
p
:
loc
)
(
l
r
:
tree
loc
),
distinct
(
inorder
(
zip
(
Node
l
p
r
)
z
))
->
distinct
(
inorder
(
Node
l
p
r
)).
Proof
.
induction
z
.
...
...
@@ -233,9 +249,9 @@ generalize (IHz a (Node l p r) t); clear IHz.
ae
.
Qed
.
Lemma
tree1
_zip
:
Lemma
istree
_zip
:
forall
m
t
z
l
r
pp
,
tree1
m
t
(
zip
(
Node
l
pp
r
)
z
)
->
tree1
m
pp
(
Node
l
pp
r
).
istree
m
t
(
zip
(
Node
l
pp
r
)
z
)
->
istree
m
pp
(
Node
l
pp
r
).
Proof
.
induction
z
;
simpl
.
ae
.
...
...
@@ -245,13 +261,13 @@ generalize (IHz (Node l pp r) t0 a).
ae
.
Qed
.
Lemma
tree1
_zip_2
:
Lemma
istree
_zip_2
:
forall
m
n
a
z
t
pp
l
r
tr
'
,
tree1
m
t
(
zip
(
Node
l
pp
r
)
z
)
->
istree
m
t
(
zip
(
Node
l
pp
r
)
z
)
->
distinct
(
inorder
(
zip
(
Node
l
pp
r
)
z
))
->
mem
a
(
inorder
(
Node
l
pp
r
))
->
let
m
'
:=
Map
.
set
m
a
n
in
tree1
m
'
pp
tr
'
->
tree1
m
'
t
(
zip
tr
'
z
).
istree
m
'
pp
tr
'
->
istree
m
'
t
(
zip
tr
'
z
).
Proof
.
induction
z
;
simpl
.
ae
.
...
...
@@ -265,20 +281,20 @@ apply node1.
why3
"cvc3"
.
assert
(
left1
(
Map
.
get
(
Map
.
set
m
a
n
)
a0
)
=
pp
).
rewrite
Map
.
Select_neq
.
generalize
(
tree1
_zip
_
_
_
_
_
_
H
).
generalize
(
istree
_zip
_
_
_
_
_
_
H
).
inversion
1.
inversion
H11
;
auto
.
assumption
.
ae
.
assert
(
right1
(
Map
.
get
(
Map
.
set
m
a
n
)
a0
)
=
right1
(
Map
.
get
m
a0
)).
rewrite
Map
.
Select_neq
.
generalize
(
tree1
_zip
_
_
_
_
_
_
H
).
generalize
(
istree
_zip
_
_
_
_
_
_
H
).
inversion
1.
inversion
H11
;
auto
.
assumption
.
rewrite
H5
;
clear
H5
.
apply
distinct2
.
generalize
(
tree1
_zip
_
_
_
_
_
_
H
).
generalize
(
istree
_zip
_
_
_
_
_
_
H
).
inversion
1.
ae
.
clear
H4
H2
H
H3
.
...
...
@@ -297,20 +313,19 @@ ae.
Qed
.
(
*
Why3
goal
*
)
Theorem
main_lemma
:
forall
(
m
:
(
map
.
Map
.
map
pointer
node
))
(
t
:
pointer
)
(
pp
:
pointer
)
(
p
:
pointer
)
(
ppr
:
(
tree
pointer
))
(
pr
:
(
tree
pointer
))
(
z
:
(
zipper
pointer
)),
let
it
:=
(
zip
(
Node
(
Node
(
Empty
:
(
tree
pointer
))
p
pr
)
pp
ppr
)
z
)
in
((
tree1
m
t
it
)
->
((
distinct
(
inorder
it
))
->
(
tree1
(
map
.
Map
.
set
m
pp
(
mk_node
(
right1
(
map
.
Map
.
get
m
p
))
(
right1
(
map
.
Map
.
get
m
pp
))
(
data
(
map
.
Map
.
get
m
pp
))))
t
(
zip
(
Node
pr
pp
ppr
)
z
)))).
Theorem
main_lemma
:
forall
(
m
:
(
map
loc
node
))
(
t
:
loc
)
(
pp
:
loc
)
(
p
:
loc
)
(
ppr
:
(
tree
loc
))
(
pr
:
(
tree
loc
))
(
z
:
(
zipper
loc
)),
let
it
:=
(
zip
(
Node
(
Node
(
Empty
:
(
tree
loc
))
p
pr
)
pp
ppr
)
z
)
in
((
istree
m
t
it
)
->
((
distinct
(
inorder
it
))
->
(
istree
(
set
m
pp
(
mk_node
(
right1
(
get
m
p
))
(
right1
(
get
m
pp
))
(
data
(
get
m
pp
))))
t
(
zip
(
Node
pr
pp
ppr
)
z
)))).
intros
m
t
pp
p
ppr
pr
z
it
h1
h2
.
pose
(
m
'
:=
(
Map
.
set
m
pp
(
mk_node
(
right1
(
Map
.
get
m
p
))
(
right1
(
Map
.
get
m
pp
))
<