Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
R
rtproofs
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
0
Issues
0
List
Boards
Labels
Milestones
Merge Requests
0
Merge Requests
0
CI / CD
CI / CD
Pipelines
Jobs
Schedules
Analytics
Analytics
CI / CD
Repository
Value Stream
Wiki
Wiki
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Jobs
Commits
Issue Boards
Open sidebar
Sophie Quinton
rtproofs
Commits
3a2bf991
Commit
3a2bf991
authored
Mar 29, 2017
by
Felipe Cerqueira
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Add pickany, pickmin, pickmax
parent
e4012a4d
Changes
2
Hide whitespace changes
Inline
Sidebyside
Showing
2 changed files
with
163 additions
and
0 deletions
+163
0
util/all.v
util/all.v
+1
0
util/pick.v
util/pick.v
+162
0
No files found.
util/all.v
View file @
3a2bf991
...
@@ 16,3 +16,4 @@ Require Export rt.util.sum.
...
@@ 16,3 +16,4 @@ Require Export rt.util.sum.
Require
Export
rt
.
util
.
minmax
.
Require
Export
rt
.
util
.
minmax
.
Require
Export
rt
.
util
.
seqset
.
Require
Export
rt
.
util
.
seqset
.
Require
Export
rt
.
util
.
step_function
.
Require
Export
rt
.
util
.
step_function
.
Require
Export
rt
.
util
.
pick
.
\ No newline at end of file
util/pick.v
0 → 100644
View file @
3a2bf991
From
mathcomp
Require
Import
ssreflect
ssrbool
ssrfun
eqtype
ssrnat
seq
fintype
.
(* In this file, we define functions for picking numbers in an interval [0, n). *)
(** Auxiliary Functions *)
Definition
default0
{
n
}
(
x
:
option
'
I_n
)
:
nat
:
=
if
x
is
Some
y
then
y
else
0
.
Definition
arg_pred_nat
n
(
P
:
pred
'
I_n
)
ord
:
=
[
pred
i

P
i
&
[
forall
j
:
'
I_n
,
P
j
==>
ord
i
j
]].
Definition
pred_min_nat
n
(
P
:
pred
'
I_n
)
:
=
arg_pred_nat
n
P
leq
.
Definition
pred_max_nat
n
(
P
:
pred
'
I_n
)
:
=
arg_pred_nat
n
P
(
fun
x
y
=>
geq
x
y
).
(** Defining Pick functions *)
(* (pick_any n P) returns some number < n that satisfies P, or 0 if it cannot be found. *)
Definition
pick_any
n
(
P
:
pred
'
I_n
)
:
=
default0
(
pick
P
).
(* (pick_min n P) returns the smallest number < n that satisfies P, or 0 if it cannot be found. *)
Definition
pick_min
n
(
P
:
pred
'
I_n
)
:
=
default0
(
pick
(
pred_min_nat
n
P
)).
(* (pick_max n P) returns the largest number < n that satisfies P, or 0 if it cannot be found. *)
Definition
pick_max
n
(
P
:
pred
'
I_n
)
:
=
default0
(
pick
(
pred_max_nat
n
P
)).
(** Improved notation *)
(* Next we provide the following notation for the variations of pick:
[pickany x <= N  P], [pickany x < N  P]
[pickmin x <= N  P], [pickmin x < N  P]
[pickmax x <= N  P], [pickmax x < N  P]. *)
Notation
"[ 'pickany' x <= N  P ]"
:
=
(
pick_any
N
.+
1
(
fun
x
:
'
I_N
.+
1
=>
P
%
B
))
(
at
level
0
,
x
ident
,
only
parsing
)
:
form_scope
.
Notation
"[ 'pickany' x < N  P ]"
:
=
(
pick_any
N
(
fun
x
:
'
I_N
=>
P
%
B
))
(
at
level
0
,
x
ident
,
only
parsing
)
:
form_scope
.
Notation
"[ 'pickmin' x <= N  P ]"
:
=
(
pick_min
N
.+
1
(
fun
x
:
'
I_N
.+
1
=>
P
%
B
))
(
at
level
0
,
x
ident
,
only
parsing
)
:
form_scope
.
Notation
"[ 'pickmin' x < N  P ]"
:
=
(
pick_min
N
(
fun
x
:
'
I_N
=>
P
%
B
))
(
at
level
0
,
x
ident
,
only
parsing
)
:
form_scope
.
Notation
"[ 'pickmax' x <= N  P ]"
:
=
(
pick_max
N
.+
1
(
fun
x
:
'
I_N
.+
1
=>
P
%
B
))
(
at
level
0
,
x
ident
,
only
parsing
)
:
form_scope
.
Notation
"[ 'pickmax' x < N  P ]"
:
=
(
pick_max
N
(
fun
x
:
'
I_N
=>
P
%
B
))
(
at
level
0
,
x
ident
,
only
parsing
)
:
form_scope
.
(** Lemmas *)
(* First, we show that any property P of (pick_any n p) can be proven by showing that
P holds for any number < n that satisfies p. *)
Section
PickAny
.
Variable
n
:
nat
.
Variable
p
:
pred
'
I_n
.
Variable
P
:
nat
>
Prop
.
Hypothesis
EX
:
exists
x
:
'
I_n
,
p
x
.
Hypothesis
HOLDS
:
forall
x
,
p
x
>
P
x
.
Lemma
pick_any_holds
:
P
(
pick_any
n
p
).
Proof
.
rewrite
/
pick_any
/
default0
.
case
:
pickP
;
first
by
intros
x
PRED
;
apply
HOLDS
.
intros
NONE
;
red
in
NONE
;
exfalso
.
move
:
EX
=>
[
x
PRED
].
by
specialize
(
NONE
x
)
;
rewrite
PRED
in
NONE
.
Qed
.
End
PickAny
.
(* Next, we show that any property P of (pick_min n p) can be proven by showing that
P holds for the smallest number < n that satisfies p. *)
Section
PickMin
.
Variable
n
:
nat
.
Variable
p
:
pred
'
I_n
.
Variable
P
:
nat
>
Prop
.
Hypothesis
EX
:
exists
x
:
'
I_n
,
p
x
.
Hypothesis
MIN
:
forall
x
,
p
x
>
(
forall
y
,
p
y
>
x
<=
y
)
>
P
x
.
Lemma
pick_min_holds
:
P
(
pick_min
n
p
).
Proof
.
rewrite
/
pick_min
/
odflt
/
oapp
.
case
:
pickP
.
{
move
=>
x
/
andP
[
PRED
/
forallP
ALL
].
apply
MIN
;
first
by
done
.
by
intros
y
Py
;
specialize
(
ALL
y
)
;
move
:
ALL
=>
/
implyP
ALL
;
apply
ALL
.
}
{
intros
NONE
;
red
in
NONE
;
exfalso
.
move
:
EX
=>
[
x
PRED
]
;
clear
EX
.
set
argmin
:
=
arg_min
x
p
id
.
specialize
(
NONE
argmin
).
suff
ARGMIN
:
(
pred_min_nat
n
p
)
argmin
by
rewrite
ARGMIN
in
NONE
.
rewrite
/
argmin
;
case
:
arg_minP
;
first
by
done
.
intros
y
Py
MINy
.
apply
/
andP
;
split
;
first
by
done
.
by
apply
/
forallP
;
intros
y0
;
apply
/
implyP
;
intros
Py0
;
apply
MINy
.
}
Qed
.
End
PickMin
.
(* Next, we show that any property P of (pick_max n p) can be proven by showing that
P holds for the largest number < n that satisfies p. *)
Section
PickMax
.
Variable
n
:
nat
.
Variable
p
:
pred
'
I_n
.
Variable
P
:
nat
>
Prop
.
Hypothesis
EX
:
exists
x
:
'
I_n
,
p
x
.
Hypothesis
MAX
:
forall
x
,
p
x
>
(
forall
y
,
p
y
>
x
>=
y
)
>
P
x
.
Lemma
pick_max_holds
:
P
(
pick_max
n
p
).
Proof
.
rewrite
/
pick_max
/
odflt
/
oapp
.
case
:
pickP
.
{
move
=>
x
/
andP
[
PRED
/
forallP
ALL
].
apply
MAX
;
first
by
done
.
by
intros
y
Py
;
specialize
(
ALL
y
)
;
move
:
ALL
=>
/
implyP
ALL
;
apply
ALL
.
}
{
intros
NONE
;
red
in
NONE
;
exfalso
.
move
:
EX
=>
[
x
PRED
]
;
clear
EX
.
set
argmax
:
=
arg_max
x
p
id
.
specialize
(
NONE
argmax
).
suff
ARGMAX
:
(
pred_max_nat
n
p
)
argmax
by
rewrite
ARGMAX
in
NONE
.
rewrite
/
argmax
;
case
:
arg_maxP
;
first
by
done
.
intros
y
Py
MAXy
.
apply
/
andP
;
split
;
first
by
done
.
by
apply
/
forallP
;
intros
y0
;
apply
/
implyP
;
intros
Py0
;
apply
MAXy
.
}
Qed
.
End
PickMax
.
\ No newline at end of file
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment