Commit 0d70f23e authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Include the math directory of the union find proof.

parent eca1d3c9
-Q theories iris_time
-arg -w -arg -notation-overridden
......@@ -13,3 +14,37 @@ theories/TimeCredits.v
This diff is collapsed.
From TLC Require Import LibTactics.
From TLC Require Import LibLogic. (* defines [pred_incl] *)
From TLC Require Import LibSet. (* defines [set] *)
(* ---------------------------------------------------------------------------- *)
(* Technically, a filter is a nonempty set of nonempty subsets of A, which is
closed under inclusion and intersection. *)
Definition filter A := set (set A).
(* Intuitively, a filter is a modality. Let us write [ultimately] for a filter.
If [P] is a predicate, then [ultimately P] is a proposition. Technically,
this proposition asserts that [P] is an element of the filter; intuitively,
it means that [P] holds ``in the limit''. *)
Class Filter {A : Type} (ultimately : filter A) := {
(* A filter must be nonempty. *)
exists P, ultimately P;
(* A filter does not have the empty set as a member. *)
forall P, ultimately P ->
exists a, P a;
(* A filter is closed by inclusion and by intersection. *)
forall P1 P2 P : set A,
ultimately P1 ->
ultimately P2 ->
(forall a, P1 a -> P2 a -> P a) ->
ultimately P
(* ---------------------------------------------------------------------------- *)
(* Basic properties of filters. *)
Section Properties.
Context {A : Type} {ultimately : filter A} `{@Filter A ultimately}.
(* A filter is closed by subset inclusion. In other words, if [ultimately]
is a filter, then it is covariant. *)
Lemma filter_closed_under_inclusion:
forall P1 P2 : set A,
ultimately P1 ->
(forall a, P1 a -> P2 a) ->
ultimately P2.
intros. eapply filter_closed_under_intersection; eauto.
(* A filter is compatible with extensional equality: if [P1] and [P2] are
extensionally equal, then [ultimately P1] is equivalent to [ultimately
P2]. *)
Lemma filter_extensional:
forall P1 P2 : set A,
(forall a, P1 a <-> P2 a) ->
(ultimately P1 <-> ultimately P2).
introv h. split; intros; eapply filter_closed_under_inclusion; eauto;
intros; eapply h; eauto.
(* A filter always contains the universe as a member. In other words, if
[P] holds everywhere, then [ultimately P] holds. *)
Lemma filter_universe:
forall P : set A,
(forall a, P a) ->
ultimately P.
(* A filter is nonempty, so it has one inhabitant. *)
destruct filter_nonempty.
(* A filter is closed by inclusion, so the universe is also
an inhabitant of the filter. *)
eauto using @filter_closed_under_inclusion.
(* If [P] holds ultimately and is independent of its argument, then [P]
holds, period. *)
Lemma filter_const:
forall P : Prop,
ultimately (fun _ => P) ->
forwards [ a ? ]: filter_member_nonempty. eauto.
End Properties.
(* ---------------------------------------------------------------------------- *)
(* Inclusion of filters. *)
Notation finer ultimately1 ultimately2 :=
(pred_incl ultimately2 ultimately1).
Notation coarser ultimately1 ultimately2 :=
(pred_incl ultimately1 ultimately2).
(* These relations are reflexive and transitive; see [pred_incl_refl] and
[pred_incl_trans] in [LibLogic]. *)
(* ---------------------------------------------------------------------------- *)
(* Applying a function [f] to a filter [ultimately] produces another filter,
known as the image of [ultimately] under [f]. *)
Definition image {A} (ultimately : filter A) {B} (f : A -> B) : set (set B) :=
fun P => ultimately (fun x => P (f x)).
(* Make this a definition, not an instance, because we do not wish it to be
used during the automated search for instances. *)
Definition filter_image {A} ultimately `{Filter A ultimately} {B} (f : A -> B) :
Filter (image ultimately f).
econstructor; unfold image.
(* There exists an element in this filter, namely the universe. *)
exists (fun (_ : B) => True). eauto using filter_universe.
(* No element of this filter is empty. *)
forwards [ a ? ]: filter_member_nonempty; eauto. simpl in *.
(* This filter is stable under intersection. *)
introv h1 h2 ?.
eapply (filter_closed_under_intersection _ _ _ h1 h2).
(* ---------------------------------------------------------------------------- *)
(* A notion of limit, or convergence. *)
(* The definition of [limit] does not really need proofs that [ultimatelyA]
and [ultimatelyB] are filters. Requesting these proofs anyway is useful,
as it helps the implicit argument inference system. *)
Definition limit
{A} ultimatelyA `{Filter A ultimatelyA}
{B} ultimatelyB `{Filter B ultimatelyB}
(f : A -> B)
coarser ultimatelyB (image ultimatelyA f).
Lemma limit_id:
forall A ultimately `{Filter A ultimately},
limit _ _ (fun a : A => a).
unfold limit, image. repeat intro. eapply filter_closed_under_inclusion; eauto.
(* ---------------------------------------------------------------------------- *)
(* The product of two filters. *)
Section FilterProduct.
Context {A1} ultimately1 `{Filter A1 ultimately1}.
Context {A2} ultimately2 `{Filter A2 ultimately2}.
Definition product : set (set (A1 * A2)) :=
fun P : set (A1 * A2) =>
exists P1 P2,
ultimately1 P1 /\ ultimately2 P2 /\
forall a1 a2, P1 a1 -> P2 a2 -> P (a1, a2).
Global Instance filter_product : Filter product.
econstructor; unfold product.
(* Existence of a member. *)
destruct (@filter_nonempty _ ultimately1) as [ P1 ? ]. eauto.
destruct (@filter_nonempty _ ultimately2) as [ P2 ? ]. eauto.
exists (fun a : A1 * A2 => let (a1, a2) := a in P1 a1 /\ P2 a2) P1 P2.
(* Nonemptiness of the members. *)
introv [ P1 [ P2 [ ? [ ? ? ]]]].
forwards [ a1 ? ]: (filter_member_nonempty P1). eauto.
forwards [ a2 ? ]: (filter_member_nonempty P2). eauto.
exists (a1, a2). eauto.
(* Closure under intersection and inclusion. *)
intros P Q R.
introv [ P1 [ P2 [ ? [ ? ? ]]]].
introv [ Q1 [ Q2 [ ? [ ? ? ]]]].
exists (fun a1 => P1 a1 /\ Q1 a1).
exists (fun a2 => P2 a2 /\ Q2 a2).
repeat split.
eapply filter_closed_under_intersection. 3: eauto. eauto. eauto.
eapply filter_closed_under_intersection. 3: eauto. eauto. eauto.
intuition eauto.
(* When the pair [a1, a2] goes to infinity, its components go to infinity. *)
Lemma limit_fst:
limit _ _ (@fst A1 A2).
unfold limit, image, product. simpl.
intros P1 ?.
exists P1 (fun _ : A2 => True).
repeat split.
eapply filter_universe. eauto.
Lemma limit_snd:
limit _ _ (@snd A1 A2).
unfold limit, image, product. simpl.
intros P2 ?.
exists (fun _ : A1 => True) P2.
repeat split.
eapply filter_universe. eauto.
(* When both components go to infinity, the pair goes to infinity. *)
(* The limit of a pair is a pair of the limits. *)
Lemma limit_pair :
forall A ultimately `{@Filter A ultimately},
forall (f1 : A -> A1) (f2 : A -> A2),
limit _ _ f1 ->
limit _ _ f2 ->
limit _ _ (fun a => (f1 a, f2 a)).
unfold limit, image.
introv ? h1 h2. intros P [ P1 [ P2 [ ? [ ? ? ]]]].
eapply filter_closed_under_intersection.
eapply h1. eauto.
eapply h2. eauto.
End FilterProduct.
Set Implicit Arguments.
Generalizable All Variables.
From TLC Require Import LibTactics.
From iris_time.union_find.math Require Import LibNatExtra Filter.
(* [le m] can be understood as the semi-open interval of the natural numbers
that are greater than or equal to [m]. The subsets [le m] form a filter
base; that is, if we close them under inclusion, then we obtain a filter,
which intuitively represents going to infinity. We call this modality
[towards_infinity]. *)
Definition towards_infinity (F : nat -> Prop) :=
exists m, forall n, m <= n -> F n.
Instance filter_towards_infinity : Filter towards_infinity.
unfold towards_infinity. econstructor.
(* There exists an element in this filter, namely the universe, [le 0]. *)
exists (fun n => 0 <= n). eauto.
(* Every set of the form [le m] is nonempty. *)
introv [ m ? ]. exists m. eauto.
(* Closure by intersection and subset. *)
introv [ m1 ? ] [ m2 ? ] ?. exists (max m1 m2). intros.
max_case; eauto with omega.
(* Every subset of the form [le m] is a member of this filter. *)
Lemma towards_infinity_le:
forall m,
towards_infinity (le m).
unfold towards_infinity. eauto.
Hint Resolve towards_infinity_le : filter.
(* The statement that [f x] tends towards infinity as [x] tends
towards infinity can be stated in its usual concrete form or
more abstractly using filters. *)
Lemma prove_tends_towards_infinity:
forall f : nat -> nat,
(forall y, exists x0, forall x, x0 <= x -> y <= f x) ->
limit towards_infinity towards_infinity f.
introv h. intros F [ m ? ].
generalize (h m); intros [ x0 ? ].
exists x0. eauto.
Lemma exploit_tends_towards_infinity:
forall f : nat -> nat,
limit towards_infinity towards_infinity f ->
(forall y, exists x0, forall x, x0 <= x -> y <= f x).
intros ? hlimit y.
forwards [ x0 ? ]: hlimit (le y).
eapply towards_infinity_le.
(* This module defines Tarjan's inverse of Ackermann's function. *)
From TLC Require Import LibTactics LibRelation LibMin.
From iris_time.union_find.math Require Import LibFunOrd LibIter LibNatExtra
Filter FilterTowardsInfinity Ackermann InverseNatNat.
(* -------------------------------------------------------------------------- *)
(* The function [fun k => A k 1] tends towards infinity. The function [alpha]
is defined as its upper inverse -- see [InverseNatNat]. *)
Notation alpha :=
(alphaf (fun k => A k 1)).
(* [alpha] is monotonic. *)
Lemma alpha_monotonic:
monotonic le le alpha.
Proof using.
eauto 8 with monotonic typeclass_instances.
Hint Resolve alpha_monotonic : monotonic typeclass_instances.
(* -------------------------------------------------------------------------- *)
(* The facts proven about [alphaf] in [InverseNatNat] can be applied to
[alpha]. The following tactic helps do this; it applies the theorem [th]
with an appropriate choice of [f], and uses [eauto with monotonic] to prove
that Ackermann's function is monotonic and tends towards infinity. *)
Ltac alpha th :=
eapply th with (f := fun k => A k 1);
eauto with monotonic.
(* Example. *)
forall y x,
alpha y <= x ->
y <= A x 1.
Proof using.
intros. alpha alphaf_spec_direct.
(* -------------------------------------------------------------------------- *)
(* It takes only [k = 0] to go from [x] to [x + 1]. *)
Lemma beta_x_succ_x:
forall x,
x > 0 ->
betaf (fun k => A k x) (x + 1) = 0.
Proof using.
cut (betaf (fun k => A k x) (x + 1) < 1). { omega. }
eapply betaf_spec_direct_contrapositive; eauto with monotonic.
{ rewrite Abase_eq. omega. }
{ rewrite A_1_eq. omega. }
(* -------------------------------------------------------------------------- *)
(* [alpha] grows very slowly. In particular, of course, it never grows by more
than one at a time. *)
(* We state this lemma directly in a generalized form that will be useful when
we later consider the function [alphar] introduced by Alstrup et al. *)
Lemma alpha_grows_one_by_one:
forall r,
1 <= r ->
forall n,
alphaf (fun k => A k r) (n + 1) <= alphaf (fun k => A k r) n + 1.
(* By definition of [alphaf]: *)
rewrite alphaf_spec by eauto with monotonic.
(* By definition of [A]: *)
rewrite (@plus_comm (alphaf (fun k : nat => A k r) n)).
rewrite Astep_eq. simpl.
(* Because [r] is at least 1, this iteration is taken at least once.
Because [A _] is inflationary, we have the following fact. *)
assert (fact:
let f := A (alphaf (fun k : nat => A k r) n) in
f r <= LibIter.iter r f r
{ simpl.
eapply iter_at_least_once with (okA := fun _ => True);
unfold preserves, within; eauto using le_trans, Ak_inflationary. }
(* Thus, we simplify: *)
rewrite <- fact. clear fact.
(* Furthermore, we have [n <= A (alphaf (fun k : nat => A k r) n) r]. *)
forwards fact: f_alphaf (fun k => A k r) n; eauto with monotonic.
(* Thus, we simplify: *)
rewrite <- fact. clear fact.
(* Because [n + 1] is [A 0 n], we can transform the goal to: *)
replace (n + 1) with (A 0 n) by (rewrite Abase_eq; omega).
(* The goal follows from the fact that [A] is monotonic. *)
eapply Akx_monotonic_in_k. omega.
(* Phew! *)
forall n,
alpha (n + 1) <= alpha n + 1.
eauto using alpha_grows_one_by_one.
(* -------------------------------------------------------------------------- *)
(* As soon as [n] is at least [4], [alpha n] is greater than one. *)
Lemma two_le_alpha:
forall n,
4 <= n ->
2 <= alpha n.
Proof using.
intros. alpha alphaf_spec_direct_contrapositive.
(* -------------------------------------------------------------------------- *)
(* [alpha n] is at most [1 + alpha (log2 n)]. This gives a weak sense of how
slowly the function [alpha] grows. In fact, the function [log*] would
satisfy the same property; yet [alpha] grows even more slowly than
[log*]. *)
(* This property also shows that [alpha n] and [alpha (log2 n)] are
asymptotically equivalent. This explains why Tarjan and Cormen et al. are
content with a bound of [alpha n] for the amortized complexity of union and
find, even though they could easily obtain [alpha (log2 n)]. See Exercise
21.4-6 in Cormen et al. *)
Lemma alpha_n_O_alpha_log2n:
forall n,
16 <= n ->
alpha n <= 1 + alpha (log2 n).
Proof using.
(* By definition of [alpha n], we have to prove this: *)
alpha alphaf_spec_reciprocal.
rewrite Astep_eq. simpl.
(* Now, the first occurrence of [alpha (log2 n)] in this goal
is at least [2]. *)
match goal with |- _ <= A _ ?x =>
transitivity (A 2 x); [ | eauto using two_le_alpha, prove_le_log2 with monotonic ]
(* And, by definition of [alpha], [A (alpha (log2 n)) 1] is at
least [log2 n]. *)
transitivity (A 2 (log2 n)); [ | eapply Akx_monotonic_in_x; alpha f_alphaf ].
(* There remains prove [n <= A 2 (log n)], which intuitively holds because
[A 2] is an exponential. *)
eapply A_2_log2_lower_bound.
This diff is collapsed.
(* This library defines some notions that involve functions and order,
such as the property of being monotonic. *)
Set Implicit Arguments.
Require Import Coq.Classes.Morphisms.
From TLC Require Import LibTactics.
Require Import Omega.
(* -------------------------------------------------------------------------- *)
(* Definitions. *)
(* [within okA okB f] holds iff [f] maps [okA] into [okB]. *)
Definition within A B (okA : A -> Prop) (okB : B -> Prop) (f : A -> B) :=
forall a,
okA a ->
okB (f a).
Definition preserves A (okA : A -> Prop) (f : A -> A) :=
within okA okA f.
(* [monotonic leA leB f] holds iff [f] is monotonic with respect to
the relations [leA] and [leB], i.e., [f] maps [leA] to [leB]. *)
Definition monotonic A B (leA : A -> A -> Prop) (leB : B -> B -> Prop) (f : A -> B) :=
forall a1 a2,
leA a1 a2 ->
leB (f a1) (f a2).
(* [inverse_monotonic leA leB f] holds iff [f^-1] maps [leB] to [leA]. *)
Definition inverse_monotonic A B (leA : A -> A -> Prop) (leB : B -> B -> Prop) (f : A -> B) :=
forall a1 a2,
leB (f a1) (f a2) ->
leA a1 a2.
(* [inflationary okA leA] holds iff [a] is less than [f a], with
respect to the relation [leA], and for every [a] in [okA]. *)
Definition inflationary A (okA : A -> Prop) (leA : A -> A -> Prop) (f : A -> A) :=
forall a,
okA a ->
leA a (f a).
(* If [leB] is a relation on [B], then [pointwise okA leB] is a relation
on [A -> B]. *)
Definition pointwise A B (okA : A -> Prop) (leB : B -> B -> Prop) (f g : A -> B) :=
forall a,
okA a ->
leB (f a) (g a).
(* -------------------------------------------------------------------------- *)
(* If [f] is monotonic, then rewriting in the argument of [f] is permitted. *)
(* Note: in order for [rewrite] to work properly, the lemmas that are able to
prove [monotonic] assertions should be added to [typeclass_instances]. *)
(* TEMPORARY maybe this should be the *definition* of [monotonic] *)
Program Instance monotonic_Proper
A B (leA : A -> A -> Prop) (leB : B -> B -> Prop) (f : A -> B) :
monotonic leA leB f -> Proper (leA ++> leB) f.
(* -------------------------------------------------------------------------- *)
(* Letting [eauto] exploit [monotonic] and [inverse_monotonic]. *)
Lemma use_monotonic:
forall B (leB : B -> B -> Prop) A (leA : A -> A -> Prop) (f : A -> B),
monotonic leA leB f ->
forall a1 a2,
leA a1 a2 ->
leB (f a1) (f a2).
Proof using.
unfold monotonic. eauto.
(* This variant is useful when the function has two arguments and one
wishes to exploit monotonicity in the first argument. *)
Lemma use_monotonic_2:
forall B (leB : B -> B -> Prop) A (leA : A -> A -> Prop) C (f : A -> C -> B) a1 a2 c,
monotonic leA leB (fun a => f a c) ->
leA a1 a2 ->
leB (f a1 c) (f a2 c).
Proof using.
unfold monotonic. eauto.
Lemma use_inverse_monotonic:
forall A (leA : A -> A -> Prop) B (leB : B -> B -> Prop) (f : A -> B),
inverse_monotonic leA leB f ->
forall a1 a2,
leB (f a1) (f a2) ->
leA a1 a2.
Proof using.
unfold inverse_monotonic. eauto.
(* It seems that these lemmas can be used as a hint only if we pick a
specific instance of the ordering relation that appears in the
conclusion. Furthermore, picking a specific instance of the
ordering relation that appears in the premise can help apply
[omega] to the premise. *)
Hint Resolve (@use_monotonic nat le nat le) (@use_monotonic nat lt nat lt)
: monotonic typeclass_instances.
Hint Resolve (@use_monotonic_2 nat le nat le) (@use_monotonic_2 nat lt nat lt)
: monotonic typeclass_instances.
Hint Resolve (@use_inverse_monotonic nat le nat le)
(@use_inverse_monotonic nat lt nat lt) : monotonic typeclass_instances.
(* -------------------------------------------------------------------------- *)
(* A little fact. If [f], viewed as a function of [A] into [B -> C], is
monotonic, then its specialized version [fun a => f a b], which is a
function of [A] to [C], is monotonic as well. And the converse holds. *)
Lemma monotonic_pointwise_specialize:
forall A B C leA okB leC (f : A -> B -> C),
monotonic leA (pointwise okB leC) f ->
forall b, okB b -> monotonic leA leC (fun a => f a b).
Proof using.
unfold monotonic, pointwise. auto.
Lemma monotonic_pointwise_generalize:
forall A B C leA (okB : B -> Prop) leC (f : A -> B -> C),
(forall b, okB b -> monotonic leA leC (fun a => f a b)) ->
monotonic leA (pointwise okB leC) f.
Proof using.
unfold monotonic, pointwise. auto.
(* -------------------------------------------------------------------------- *)
Require Import Coq.Arith.Arith.
(* The following tactics allow proving implications between inequalities
by contraposition, while exploiting the fact that the negation of a
strict inequality is a large inequality. *)