Module FSetAVLplus

An extension of FSetAVL (finite sets as balanced binary search trees) with extra interval-based operations, more efficient than standard operations.

Require Import FSetInterface.
Require FSetAVL.
Require Import Coqlib.

Module Make(X: OrderedType).

Include FSetAVL.Make(X).

Module Raw := MSet.Raw.

Section MEM_BETWEEN.

mem_between above below s is true iff there exists an element of s that belongs to the interval described by the predicates above and below. Using the monotonicity of above and below, the implementation of mem_between avoids traversing the subtrees of s that lie entirely outside the interval of interest.

Variable above_low_bound: elt -> bool.
Variable below_high_bound: elt -> bool.

Fixpoint raw_mem_between (m: Raw.tree) : bool :=
  match m with
  | Raw.Leaf => false
  | Raw.Node _ l x r =>
      if above_low_bound x
      then if below_high_bound x
           then true
           else raw_mem_between l
      else raw_mem_between r
  end.

Definition mem_between (m: t) : bool := raw_mem_between m.(MSet.this).

Hypothesis above_monotone:
  forall x1 x2, X.eq x1 x2 \/ X.lt x1 x2 -> above_low_bound x1 = true -> above_low_bound x2 = true.
Hypothesis below_monotone:
  forall x1 x2, X.eq x1 x2 \/ X.lt x2 x1 -> below_high_bound x1 = true -> below_high_bound x2 = true.

Lemma raw_mem_between_1:
  forall m,
  raw_mem_between m = true ->
  exists x, Raw.In x m /\ above_low_bound x = true /\ below_high_bound x = true.

Proof.

  induction m; simpl; intros.
- discriminate.
- destruct (above_low_bound t1) eqn: LB; [destruct (below_high_bound t1) eqn: HB | idtac].
  + (* in interval *)
    exists t1; split; auto. apply Raw.IsRoot. auto.
  + (* above interval *)
    exploit IHm1; auto. intros [x' [A B]]. exists x'; split; auto. apply Raw.InLeft; auto.
  + (* below interval *)
    exploit IHm2; auto. intros [x' [A B]]. exists x'; split; auto. apply Raw.InRight; auto.
Qed.

Lemma raw_mem_between_2:
  forall x m,
  Raw.bst m ->
  Raw.In x m -> above_low_bound x = true -> below_high_bound x = true ->
  raw_mem_between m = true.

Proof.

  induction 1; simpl; intros.
- inv H.
- rewrite Raw.In_node_iff in H1.
  destruct (above_low_bound x0) eqn: LB; [destruct (below_high_bound x0) eqn: HB | idtac].
  + (* in interval *)
    auto.
  + (* above interval *)
    assert (X.eq x x0 \/ X.lt x0 x -> False).
    { intros. exploit below_monotone; eauto. congruence. }
    intuition.
  + assert (X.eq x x0 \/ X.lt x x0 -> False).
    { intros. exploit above_monotone; eauto. congruence. }
    intuition.
Qed.

Theorem mem_between_1:
  forall s,
  mem_between s = true ->
  exists x, In x s /\ above_low_bound x = true /\ below_high_bound x = true.

Proof.

intros. apply raw_mem_between_1. auto.
Qed.

Theorem mem_between_2:
  forall x s,
  In x s -> above_low_bound x = true -> below_high_bound x = true ->
  mem_between s = true.

Proof.

unfold mem_between; intros. apply raw_mem_between_2 with x; auto. apply MSet.is_ok.
Qed.

End MEM_BETWEEN.

Section ELEMENTS_BETWEEN.

elements_between above below s returns the set of elements of s that belong to the interval above,below.

Variable above_low_bound: elt -> bool.
Variable below_high_bound: elt -> bool.

Fixpoint raw_elements_between (m: Raw.tree) : Raw.tree :=
  match m with
  | Raw.Leaf => Raw.Leaf
  | Raw.Node _ l x r =>
      if above_low_bound x then
        if below_high_bound x then
          Raw.join (raw_elements_between l) x (raw_elements_between r)
        else
          raw_elements_between l
      else
        raw_elements_between r
  end.

Remark In_raw_elements_between_1:
  forall x m,
  Raw.In x (raw_elements_between m) -> Raw.In x m.

Proof.

  induction m; simpl; intros.
- inv H.
- rewrite Raw.In_node_iff.
  destruct (above_low_bound t1) eqn:LB; [destruct (below_high_bound t1) eqn: RB | idtac]; simpl in H.
  + rewrite Raw.join_spec in H. intuition.
  + left; apply IHm1; auto.
  + right; right; apply IHm2; auto.
Qed.

Lemma raw_elements_between_ok:
forall m, Raw.bst m -> Raw.bst (raw_elements_between m).

Proof.

  induction 1; simpl.
- constructor.
- destruct (above_low_bound x) eqn:LB; [destruct (below_high_bound x) eqn: RB | idtac]; simpl.
  + apply Raw.join_ok; auto.
    red; intros. apply l0. apply In_raw_elements_between_1; auto.
    red; intros. apply g. apply In_raw_elements_between_1; auto.
  + auto.
  + auto.
Qed.

Definition elements_between (s: t) : t :=
  @MSet.Mkt (raw_elements_between s.(MSet.this)) (raw_elements_between_ok s.(MSet.this) s.(MSet.is_ok)).

Hypothesis above_monotone:
  forall x1 x2, X.eq x1 x2 \/ X.lt x1 x2 -> above_low_bound x1 = true -> above_low_bound x2 = true.
Hypothesis below_monotone:
  forall x1 x2, X.eq x1 x2 \/ X.lt x2 x1 -> below_high_bound x1 = true -> below_high_bound x2 = true.

Remark In_raw_elements_between_2:
  forall x m,
  Raw.In x (raw_elements_between m) -> above_low_bound x = true /\ below_high_bound x = true.

Proof.

  induction m; simpl; intros.
- inv H.
- destruct (above_low_bound t1) eqn:LB; [destruct (below_high_bound t1) eqn: RB | idtac]; simpl in H.
  + rewrite Raw.join_spec in H. intuition.
    apply above_monotone with t1; auto.
    apply below_monotone with t1; auto.
  + auto.
  + auto.
Qed.

Remark In_raw_elements_between_3:
  forall x m,
  Raw.bst m ->
  Raw.In x m -> above_low_bound x = true -> below_high_bound x = true ->
  Raw.In x (raw_elements_between m).

Proof.

  induction 1; simpl; intros.
- auto.
- rewrite Raw.In_node_iff in H1.
  destruct (above_low_bound x0) eqn:LB; [destruct (below_high_bound x0) eqn: RB | idtac].
  + rewrite Raw.join_spec. intuition.
  + assert (X.eq x x0 \/ X.lt x0 x -> False).
    { intros. exploit below_monotone; eauto. congruence. }
    intuition. elim H7. apply g. auto.
  + assert (X.eq x x0 \/ X.lt x x0 -> False).
    { intros. exploit above_monotone; eauto. congruence. }
    intuition. elim H7. apply l0. auto.
Qed.

Theorem elements_between_iff:
forall x s,
In x (elements_between s) <-> In x s /\ above_low_bound x = true /\ below_high_bound x = true.

Proof.

  intros. unfold elements_between, In; simpl. split.
  intros. split. apply In_raw_elements_between_1; auto. eapply In_raw_elements_between_2; eauto.
  intros [A [B C]]. apply In_raw_elements_between_3; auto. apply MSet.is_ok.
Qed.

End ELEMENTS_BETWEEN.

Section FOR_ALL_BETWEEN.

for_all_between pred above below s is true iff all elements of s in a given variation interval satisfy predicate pred. The variation interval is given by two predicates above and below which must both hold if the element is part of the interval. Using the monotonicity of above and below, the implementation of for_all_between avoids traversing the subtrees of s that lie entirely outside the interval of interest.

Variable pred: elt -> bool.
Variable above_low_bound: elt -> bool.
Variable below_high_bound: elt -> bool.

Fixpoint raw_for_all_between (m: Raw.tree) : bool :=
  match m with
  | Raw.Leaf => true
  | Raw.Node _ l x r =>
      if above_low_bound x
      then if below_high_bound x
           then raw_for_all_between l && pred x && raw_for_all_between r
           else raw_for_all_between l
      else raw_for_all_between r
  end.

Definition for_all_between (m: t) : bool := raw_for_all_between m.(MSet.this).

Hypothesis pred_compat:
  forall x1 x2, X.eq x1 x2 -> pred x1 = pred x2.
Hypothesis above_monotone:
  forall x1 x2, X.eq x1 x2 \/ X.lt x1 x2 -> above_low_bound x1 = true -> above_low_bound x2 = true.
Hypothesis below_monotone:
  forall x1 x2, X.eq x1 x2 \/ X.lt x2 x1 -> below_high_bound x1 = true -> below_high_bound x2 = true.

Lemma raw_for_all_between_1:
  forall x m,
  Raw.bst m ->
  raw_for_all_between m = true ->
  Raw.In x m ->
  above_low_bound x = true ->
  below_high_bound x = true ->
  pred x = true.

Proof.

  induction 1; simpl; intros.
- inv H0.
- destruct (above_low_bound x0) eqn: LB; [destruct (below_high_bound x0) eqn: HB | idtac].
  + (* in interval *)
    destruct (andb_prop _ _ H1) as [P C]. destruct (andb_prop _ _ P) as [A B]. clear H1 P.
    inv H2.
    * erewrite pred_compat; eauto.
    * apply IHbst1; auto.
    * apply IHbst2; auto.
  + (* above interval *)
    inv H2.
    * assert (below_high_bound x0 = true) by (apply below_monotone with x; auto).
      congruence.
    * apply IHbst1; auto.
    * assert (below_high_bound x0 = true) by (apply below_monotone with x; auto).
      congruence.
  + (* below interval *)
    inv H2.
    * assert (above_low_bound x0 = true) by (apply above_monotone with x; auto).
      congruence.
    * assert (above_low_bound x0 = true) by (apply above_monotone with x; auto).
      congruence.
    * apply IHbst2; auto.
Qed.

Lemma raw_for_all_between_2:
  forall m,
  Raw.bst m ->
  (forall x, Raw.In x m -> above_low_bound x = true -> below_high_bound x = true -> pred x = true) ->
  raw_for_all_between m = true.

Proof.

  induction 1; intros; simpl.
- auto.
- destruct (above_low_bound x) eqn: LB; [destruct (below_high_bound x) eqn: HB | idtac].
  + (* in interval *)
    rewrite IHbst1. rewrite (H1 x). rewrite IHbst2. auto.
    intros. apply H1; auto. apply Raw.InRight; auto.
    apply Raw.IsRoot. reflexivity. auto. auto.
    intros. apply H1; auto. apply Raw.InLeft; auto.
  + (* above interval *)
    apply IHbst1. intros. apply H1; auto. apply Raw.InLeft; auto.
  + (* below interval *)
    apply IHbst2. intros. apply H1; auto. apply Raw.InRight; auto.
Qed.

Theorem for_all_between_iff:
forall s,
for_all_between s = true <-> (forall x, In x s -> above_low_bound x = true -> below_high_bound x = true -> pred x = true).

Proof.

unfold for_all_between; intros; split; intros.
- eapply raw_for_all_between_1; eauto. apply MSet.is_ok.
- apply raw_for_all_between_2; auto. apply MSet.is_ok.
Qed.

End FOR_ALL_BETWEEN.

Section PARTITION_BETWEEN.

Variable above_low_bound: elt -> bool.
Variable below_high_bound: elt -> bool.

Fixpoint raw_partition_between (m: Raw.tree) : Raw.tree * Raw.tree :=
  match m with
  | Raw.Leaf => (Raw.Leaf, Raw.Leaf)
  | Raw.Node _ l x r =>
      if above_low_bound x then
        if below_high_bound x then
          (let (l1, l2) := raw_partition_between l in
           let (r1, r2) := raw_partition_between r in
           (Raw.join l1 x r1, Raw.concat l2 r2))
        else
          (let (l1, l2) := raw_partition_between l in
           (l1, Raw.join l2 x r))
      else
        (let (r1, r2) := raw_partition_between r in
         (r1, Raw.join l x r2))
  end.

Remark In_raw_partition_between_1:
  forall x m,
  Raw.In x (fst (raw_partition_between m)) -> Raw.In x m.

Proof.

  induction m; simpl; intros.
- inv H.
- destruct (raw_partition_between m1) as [l1 l2] eqn:LEQ; simpl in *.
  destruct (raw_partition_between m2) as [r1 r2] eqn:REQ; simpl in *.
  destruct (above_low_bound t1) eqn:LB; [destruct (below_high_bound t1) eqn: RB | idtac]; simpl in H.
  + rewrite Raw.join_spec in H. rewrite Raw.In_node_iff. intuition.
  + rewrite Raw.In_node_iff. intuition.
  + rewrite Raw.In_node_iff. intuition.
Qed.

Remark In_raw_partition_between_2:
forall x m,
Raw.In x (snd (raw_partition_between m)) -> Raw.In x m.

Proof.

  induction m; simpl; intros.
- inv H.
- destruct (raw_partition_between m1) as [l1 l2] eqn:LEQ; simpl in *.
  destruct (raw_partition_between m2) as [r1 r2] eqn:REQ; simpl in *.
  destruct (above_low_bound t1) eqn:LB; [destruct (below_high_bound t1) eqn: RB | idtac]; simpl in H.
  + rewrite Raw.concat_spec in H. rewrite Raw.In_node_iff. intuition.
  + rewrite Raw.join_spec in H. rewrite Raw.In_node_iff. intuition.
  + rewrite Raw.join_spec in H. rewrite Raw.In_node_iff. intuition.
Qed.

Lemma raw_partition_between_ok:
forall m, Raw.bst m -> Raw.bst (fst (raw_partition_between m)) /\ Raw.bst (snd (raw_partition_between m)).

Proof.

  induction 1; simpl.
- split; constructor.
- destruct IHbst1 as [L1 L2]. destruct IHbst2 as [R1 R2].
  destruct (raw_partition_between l) as [l1 l2] eqn:LEQ; simpl in *.
  destruct (raw_partition_between r) as [r1 r2] eqn:REQ; simpl in *.
  destruct (above_low_bound x) eqn:LB; [destruct (below_high_bound x) eqn: RB | idtac]; simpl.
  + split.
    apply Raw.join_ok; auto.
    red; intros. apply l0. apply In_raw_partition_between_1. rewrite LEQ; auto.
    red; intros. apply g. apply In_raw_partition_between_1. rewrite REQ; auto.
    apply Raw.concat_ok; auto.
    intros. transitivity x.
    apply l0. apply In_raw_partition_between_2. rewrite LEQ; auto.
    apply g. apply In_raw_partition_between_2. rewrite REQ; auto.
  + split.
    auto.
    apply Raw.join_ok; auto.
    red; intros. apply l0. apply In_raw_partition_between_2. rewrite LEQ; auto.
  + split.
    auto.
    apply Raw.join_ok; auto.
    red; intros. apply g. apply In_raw_partition_between_2. rewrite REQ; auto.
Qed.

Hypothesis above_monotone:
  forall x1 x2, X.eq x1 x2 \/ X.lt x1 x2 -> above_low_bound x1 = true -> above_low_bound x2 = true.
Hypothesis below_monotone:
  forall x1 x2, X.eq x1 x2 \/ X.lt x2 x1 -> below_high_bound x1 = true -> below_high_bound x2 = true.

Remark In_raw_partition_between_3:
  forall x m,
  Raw.In x (fst (raw_partition_between m)) -> above_low_bound x = true /\ below_high_bound x = true.

Proof.

  induction m; simpl; intros.
- inv H.
- destruct (raw_partition_between m1) as [l1 l2] eqn:LEQ; simpl in *.
  destruct (raw_partition_between m2) as [r1 r2] eqn:REQ; simpl in *.
  destruct (above_low_bound t1) eqn:LB; [destruct (below_high_bound t1) eqn: RB | idtac]; simpl in H.
  + rewrite Raw.join_spec in H. intuition.
    apply above_monotone with t1; auto.
    apply below_monotone with t1; auto.
  + auto.
  + auto.
Qed.

Remark In_raw_partition_between_4:
  forall x m,
  Raw.bst m ->
  Raw.In x (snd (raw_partition_between m)) -> above_low_bound x = false \/ below_high_bound x = false.

Proof.

  induction 1; simpl; intros.
- inv H.
- destruct (raw_partition_between l) as [l1 l2] eqn:LEQ; simpl in *.
  destruct (raw_partition_between r) as [r1 r2] eqn:REQ; simpl in *.
  destruct (above_low_bound x0) eqn:LB; [destruct (below_high_bound x0) eqn: RB | idtac]; simpl in H.
  + simpl in H1. rewrite Raw.concat_spec in H1. intuition.
  + assert (forall y, X.eq y x0 \/ X.lt x0 y -> below_high_bound y = false).
    { intros. destruct (below_high_bound y) eqn:E; auto.
      assert (below_high_bound x0 = true) by (apply below_monotone with y; auto).
      congruence. }
    simpl in H1. rewrite Raw.join_spec in H1. intuition.
  + assert (forall y, X.eq y x0 \/ X.lt y x0 -> above_low_bound y = false).
    { intros. destruct (above_low_bound y) eqn:E; auto.
      assert (above_low_bound x0 = true) by (apply above_monotone with y; auto).
      congruence. }
    simpl in H1. rewrite Raw.join_spec in H1. intuition.
Qed.

Remark In_raw_partition_between_5:
  forall x m,
  Raw.bst m ->
  Raw.In x m -> above_low_bound x = true -> below_high_bound x = true ->
  Raw.In x (fst (raw_partition_between m)).

Proof.

  induction 1; simpl; intros.
- inv H.
- destruct (raw_partition_between l) as [l1 l2] eqn:LEQ; simpl in *.
  destruct (raw_partition_between r) as [r1 r2] eqn:REQ; simpl in *.
  destruct (above_low_bound x0) eqn:LB; [destruct (below_high_bound x0) eqn: RB | idtac]; simpl in H.
  + simpl. rewrite Raw.join_spec. inv H1.
    auto.
    right; left; apply IHbst1; auto.
    right; right; apply IHbst2; auto.
  + simpl. inv H1.
    assert (below_high_bound x0 = true) by (apply below_monotone with x; auto).
    congruence.
    auto.
    assert (below_high_bound x0 = true) by (apply below_monotone with x; auto).
    congruence.
  + simpl. inv H1.
    assert (above_low_bound x0 = true) by (apply above_monotone with x; auto).
    congruence.
    assert (above_low_bound x0 = true) by (apply above_monotone with x; auto).
    congruence.
    eauto.
Qed.

Remark In_raw_partition_between_6:
  forall x m,
  Raw.bst m ->
  Raw.In x m -> above_low_bound x = false \/ below_high_bound x = false ->
  Raw.In x (snd (raw_partition_between m)).

Proof.

  induction 1; simpl; intros.
- inv H.
- destruct (raw_partition_between l) as [l1 l2] eqn:LEQ; simpl in *.
  destruct (raw_partition_between r) as [r1 r2] eqn:REQ; simpl in *.
  destruct (above_low_bound x0) eqn:LB; [destruct (below_high_bound x0) eqn: RB | idtac]; simpl in H.
  + simpl. rewrite Raw.concat_spec. inv H1.
    assert (below_high_bound x = true) by (apply below_monotone with x0; auto; left; symmetry; auto).
    assert (above_low_bound x = true) by (apply above_monotone with x0; auto; left; symmetry; auto).
    destruct H2; congruence.
    left; apply IHbst1; auto.
    right; apply IHbst2; auto.
  + simpl. rewrite Raw.join_spec. inv H1.
    auto.
    right; left; apply IHbst1; auto.
    auto.
  + simpl. rewrite Raw.join_spec. inv H1.
    auto.
    auto.
    right; right; apply IHbst2; auto.
Qed.

Definition partition_between (s: t) : t * t :=
  let p := raw_partition_between s.(MSet.this) in
  (@MSet.Mkt (fst p) (proj1 (raw_partition_between_ok s.(MSet.this) s.(MSet.is_ok))),
   @MSet.Mkt (snd p) (proj2 (raw_partition_between_ok s.(MSet.this) s.(MSet.is_ok)))).

Theorem partition_between_iff_1:
  forall x s,
  In x (fst (partition_between s)) <->
  In x s /\ above_low_bound x = true /\ below_high_bound x = true.

Proof.

  intros. unfold partition_between, In; simpl. split.
  intros. split. apply In_raw_partition_between_1; auto. eapply In_raw_partition_between_3; eauto.
  intros [A [B C]]. apply In_raw_partition_between_5; auto. apply MSet.is_ok.
Qed.

Theorem partition_between_iff_2:
  forall x s,
  In x (snd (partition_between s)) <->
  In x s /\ (above_low_bound x = false \/ below_high_bound x = false).

Proof.

  intros. unfold partition_between, In; simpl. split.
  intros. split. apply In_raw_partition_between_2; auto. eapply In_raw_partition_between_4; eauto. apply MSet.is_ok.
  intros [A B]. apply In_raw_partition_between_6; auto. apply MSet.is_ok.
Qed.

End PARTITION_BETWEEN.

End Make.