Intervals as a Compact Set.
We want to make an efficent implementation of intervals as compact sets. We want to minimize the number of sample points in the approximations of a compact interval.
UniformPartition produces a set of n points uniformly distributed
inside the interval [l, r].
Definition UniformPartition (n:nat) :=
map (f n) (iterateN Zsucc 0%Z n).
Lemma UniformPartitionZ : forall n z, In z (iterateN Zsucc 0%Z n) <-> (0 <= z < n)%Z.
Lemma UniformPartition_inside : forall n x, In x (UniformPartition n) -> l <= x <= r.
map (f n) (iterateN Zsucc 0%Z n).
Lemma UniformPartitionZ : forall n z, In z (iterateN Zsucc 0%Z n) <-> (0 <= z < n)%Z.
Lemma UniformPartition_inside : forall n x, In x (UniformPartition n) -> l <= x <= r.
Given a point x in the interval [l, r], one can find a
nearby point in our UniformPartition.
Definition rasterize1 n (x:Q) := Qfloor ((Z_of_nat n)*(x-l)/(r-l)).
Lemma rasterize1_close : l < r -> forall n (x:Q), Qabs (x - f (S n) (rasterize1 (S n) x)) <= ((r-l)/(2*(S n))).
Definition rasterize1_boundL : forall n (x:Q), l <= x -> (0 <= rasterize1 n x)%Z.
Qed.
Definition rasterize1_boundR : forall n (x:Q), x < r -> (rasterize1 (S n) x < (S n))%Z.
Qed.
Lemma UniformPartition_fine : forall n x,
l <= x <= r -> {y | In y (UniformPartition (S n)) /\ Qabs (x - y) <= ((r-l)/(2*(S n)))}.
Lemma rasterize1_close : l < r -> forall n (x:Q), Qabs (x - f (S n) (rasterize1 (S n) x)) <= ((r-l)/(2*(S n))).
Definition rasterize1_boundL : forall n (x:Q), l <= x -> (0 <= rasterize1 n x)%Z.
Qed.
Definition rasterize1_boundR : forall n (x:Q), x < r -> (rasterize1 (S n) x < (S n))%Z.
Qed.
Lemma UniformPartition_fine : forall n x,
l <= x <= r -> {y | In y (UniformPartition (S n)) /\ Qabs (x - y) <= ((r-l)/(2*(S n)))}.
Construct the compact set.
Lemma CompactIntervalQ_nat : forall (e:Qpos), (0 <= Qceiling ((r-l)/(2*e)))%Z.
Definition CompactIntervalQ_raw (e:QposInf) : FinEnum stableQ :=
match e with
| ∞ => nil
| Qpos2QposInf e' =>
UniformPartition (max 1 (Z_to_nat (CompactIntervalQ_nat e')))
end.
Lemma CompactIntervalQ_prf : is_RegularFunction CompactIntervalQ_raw.
Definition CompactIntervalQ : Compact stableQ :=
Build_RegularFunction CompactIntervalQ_prf.
Definition CompactIntervalQ_raw (e:QposInf) : FinEnum stableQ :=
match e with
| ∞ => nil
| Qpos2QposInf e' =>
UniformPartition (max 1 (Z_to_nat (CompactIntervalQ_nat e')))
end.
Lemma CompactIntervalQ_prf : is_RegularFunction CompactIntervalQ_raw.
Definition CompactIntervalQ : Compact stableQ :=
Build_RegularFunction CompactIntervalQ_prf.
The compact set indeed represents the interval [l, r].
Lemma CompactIntervalQ_correct1 : forall (x:CR),
inCompact x CompactIntervalQ -> ('l <= x /\ x <= 'r).
Lemma CompactIntervalQ_correct2 : forall (x:CR),
('l <= x /\ x <= 'r) -> inCompact x CompactIntervalQ.
Lemma CompactIntervalQ_bonus_correct : forall e x,
In x (approximate CompactIntervalQ e) -> (l <= x <= r).
End Interval.
inCompact x CompactIntervalQ -> ('l <= x /\ x <= 'r).
Lemma CompactIntervalQ_correct2 : forall (x:CR),
('l <= x /\ x <= 'r) -> inCompact x CompactIntervalQ.
Lemma CompactIntervalQ_bonus_correct : forall e x,
In x (approximate CompactIntervalQ e) -> (l <= x <= r).
End Interval.