Definitions and theorems about semi-open integer intervals
From Coq Require Import Zwf Program.Wf.
Require Import Coqlib Iteration.
Definition interv :
Type := (
Z *
Z)%
type.
Membership
Definition In (
x:
Z) (
i:
interv) :
Prop :=
fst i <=
x <
snd i.
Lemma In_dec:
forall x i, {
In x i} + {~
In x i}.
Proof.
unfold In;
intros.
case (
zle (
fst i)
x);
intros.
case (
zlt x (
snd i));
intros.
left;
auto.
right;
intuition.
right;
intuition.
Qed.
Lemma notin_range:
forall x i,
x <
fst i \/
x >=
snd i -> ~
In x i.
Proof.
unfold In;
intros;
lia.
Qed.
Lemma range_notin:
forall x i,
~
In x i ->
fst i <
snd i ->
x <
fst i \/
x >=
snd i.
Proof.
unfold In;
intros;
lia.
Qed.
Emptyness
Definition empty (
i:
interv) :
Prop :=
fst i >=
snd i.
Lemma empty_dec:
forall i, {
empty i} + {~
empty i}.
Proof.
unfold empty;
intros.
case (
zle (
snd i) (
fst i));
intros.
left;
lia.
right;
lia.
Qed.
Lemma is_notempty:
forall i,
fst i <
snd i -> ~
empty i.
Proof.
unfold empty;
intros;
lia.
Qed.
Lemma empty_notin:
forall x i,
empty i -> ~
In x i.
Proof.
unfold empty,
In;
intros.
lia.
Qed.
Lemma in_notempty:
forall x i,
In x i -> ~
empty i.
Proof.
unfold empty,
In;
intros.
lia.
Qed.
Disjointness
Definition disjoint (
i j:
interv) :
Prop :=
forall x,
In x i -> ~
In x j.
Lemma disjoint_sym:
forall i j,
disjoint i j ->
disjoint j i.
Proof.
unfold disjoint;
intros;
red;
intros.
elim (
H x);
auto.
Qed.
Lemma empty_disjoint_r:
forall i j,
empty j ->
disjoint i j.
Proof.
Lemma empty_disjoint_l:
forall i j,
empty i ->
disjoint i j.
Proof.
Lemma disjoint_range:
forall i j,
snd i <=
fst j \/
snd j <=
fst i ->
disjoint i j.
Proof.
Lemma range_disjoint:
forall i j,
disjoint i j ->
empty i \/
empty j \/
snd i <=
fst j \/
snd j <=
fst i.
Proof.
Lemma range_disjoint':
forall i j,
disjoint i j ->
fst i <
snd i ->
fst j <
snd j ->
snd i <=
fst j \/
snd j <=
fst i.
Proof.
Lemma disjoint_dec:
forall i j, {
disjoint i j} + {~
disjoint i j}.
Proof.
Shifting an interval by some amount
Definition shift (
i:
interv) (
delta:
Z) :
interv := (
fst i +
delta,
snd i +
delta).
Lemma in_shift:
forall x i delta,
In x i ->
In (
x +
delta) (
shift i delta).
Proof.
unfold shift,
In;
intros.
simpl.
lia.
Qed.
Lemma in_shift_inv:
forall x i delta,
In x (
shift i delta) ->
In (
x -
delta)
i.
Proof.
unfold shift,
In;
simpl;
intros.
lia.
Qed.
Enumerating the elements of an interval
Definition elements (
i:
interv) :
list Z :=
CountedLoop.up List.cons (
fst i) (
snd i)
List.nil.
Lemma in_elements:
forall x i,
In x i ->
List.In x (
elements i).
Proof.
Lemma elements_in:
forall x i,
List.In x (
elements i) ->
In x i.
Proof.
Checking properties on all elements of an interval
Section FORALL.
Variables P Q:
Z ->
Prop.
Variable f:
forall (
x:
Z), {
P x} + {
Q x}.
Variable lo:
Z.
Program Fixpoint forall_rec (
hi:
Z) {
wf (
Zwf lo)
hi}:
{
forall x,
lo <=
x <
hi ->
P x}
+ {
exists x,
lo <=
x <
hi /\
Q x} :=
if zlt lo hi then
match f (
hi - 1)
with
|
left _ =>
match forall_rec (
hi - 1)
with
|
left _ =>
left _ _
|
right _ =>
right _ _
end
|
right _ =>
right _ _
end
else
left _ _
.
Next Obligation.
red. lia.
Qed.
Next Obligation.
assert (EITHER: x = hi - 1 \/ x < hi - 1) by lia.
destruct EITHER. congruence. auto.
Qed.
Next Obligation.
exists wildcard'; split; auto. lia.
Qed.
Next Obligation.
exists (hi - 1); split; auto. lia.
Qed.
Next Obligation.
extlia.
Defined.
End FORALL.
Definition forall_dec
(
P Q:
Z ->
Prop) (
f:
forall (
x:
Z), {
P x} + {
Q x}) (
i:
interv) :
{
forall x,
In x i ->
P x} + {
exists x,
In x i /\
Q x} :=
forall_rec P Q f (
fst i) (
snd i).
Folding a function over all elements of an interval
Definition fold {
A:
Type} (
f:
Z ->
A ->
A) (
a:
A) (
i:
interv) :
A :=
CountedLoop.up f (
fst i) (
snd i)
a.
Lemma fold_elements:
forall (
A:
Type) (
f:
Z ->
A ->
A)
a i,
fold f a i =
List.fold_right f a (
elements i).
Proof.
Hints
Create HintDb intv.
Global Hint Resolve
notin_range range_notin
is_notempty empty_notin in_notempty
disjoint_sym empty_disjoint_r empty_disjoint_l
disjoint_range
in_shift in_shift_inv
in_elements elements_in :
intv.