Skip to content

Instantly share code, notes, and snippets.

@CharlieQiu2017

CharlieQiu2017/RBTSet.v

Last active March 7, 2025 15:30
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save CharlieQiu2017/53db86b79b98c29481acc5a971ab4f36 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save CharlieQiu2017/53db86b79b98c29481acc5a971ab4f36 to your computer and use it in GitHub Desktop.
Download ZIP
Red-black tree with insertion and deletion in Coq
Raw
_CoqProject
-Q . RBTree
Raw
RBTree.v
From Coq Require Import
List
Equalities.
Import Notations ListNotations.
Module MRBTree (T : Typ).
Inductive rb_color :=
| black
| red.
Definition val_t := T.t.
Inductive rb_tree :=
| nil
| node (x : val_t) (l : rb_tree) (r : rb_tree) (c : rb_color).
Definition rb_tree_color (tree : rb_tree) :=
match tree with
| nil => black
| node _ _ _ c => c
end.
Fixpoint rb_tree_bh (tree : rb_tree) :=
match tree with
| nil => 1
| node _ l r black => S (rb_tree_bh l)
| node _ l r red => rb_tree_bh l
end.
Lemma rb_tree_bh_pos : forall tree, rb_tree_bh tree <> 0.
Proof. intros tree.
induction tree.
- cbn; auto.
- destruct c; cbn; auto.
Qed.
#[export] Hint Resolve rb_tree_bh_pos : rbtree.
Inductive rb_tree_valid : rb_tree -> Prop :=
| rb_tree_valid_nil : rb_tree_valid nil
| rb_tree_valid_black :
forall x l r,
rb_tree_valid l ->
rb_tree_valid r ->
rb_tree_bh l = rb_tree_bh r ->
rb_tree_valid (node x l r black)
| rb_tree_valid_red :
forall x l r,
rb_tree_valid l ->
rb_tree_valid r ->
rb_tree_color l = black ->
rb_tree_color r = black ->
rb_tree_bh l = rb_tree_bh r ->
rb_tree_valid (node x l r red).
#[export] Hint Resolve rb_tree_valid_nil : rbtree.
Ltac rb_tree_valid_ind Hval := induction Hval as [| x l r Hval_l IHl Hval_r IHr Hbh | x l r Hval_l IHl Hval_r IHr Hcl Hcr Hbh].
Lemma rb_tree_valid_left_subtree : forall x l r c,
rb_tree_valid (node x l r c) -> rb_tree_valid l.
Proof. intros x' l' r' c' Hval.
remember (node x' l' r' c') as tree.
revert Heqtree.
rb_tree_valid_ind Hval; intros Heqtree; try discriminate; inversion Heqtree; subst x' l' r' c'; auto.
Qed.
#[export] Hint Resolve rb_tree_valid_left_subtree : rbtree.
Lemma rb_tree_valid_right_subtree : forall x l r c,
rb_tree_valid (node x l r c) -> rb_tree_valid r.
Proof. intros x' l' r' c' Hval.
remember (node x' l' r' c') as tree.
revert Heqtree.
rb_tree_valid_ind Hval; intros Heqtree; try discriminate; inversion Heqtree; subst x' l' r' c'; auto.
Qed.
#[export] Hint Resolve rb_tree_valid_right_subtree : rbtree.
Lemma rb_tree_valid_bh_eq : forall x l r c,
rb_tree_valid (node x l r c) -> rb_tree_bh l = rb_tree_bh r.
Proof. intros x' l' r' c' Hval.
remember (node x' l' r' c') as tree.
revert Heqtree.
rb_tree_valid_ind Hval; intros Heqtree; try discriminate; inversion Heqtree; subst x' l' r' c'; auto.
Qed.
#[export] Hint Resolve rb_tree_valid_bh_eq : rbtree.
Lemma rb_tree_valid_red_child_black_l : forall x l r,
rb_tree_valid (node x l r red) ->
rb_tree_color l = black.
Proof. intros x' l' r' Hval.
remember (node x' l' r' red) as tree.
revert Heqtree.
rb_tree_valid_ind Hval; intros Heqtree; try discriminate; inversion Heqtree; subst x' l' r'; auto.
Qed.
#[export] Hint Resolve rb_tree_valid_red_child_black_l : rbtree.
Lemma rb_tree_valid_red_child_black_r : forall x l r,
rb_tree_valid (node x l r red) ->
rb_tree_color r = black.
Proof. intros x' l' r' Hval.
remember (node x' l' r' red) as tree.
revert Heqtree.
rb_tree_valid_ind Hval; intros Heqtree; try discriminate; inversion Heqtree; subst x' l' r'; auto.
Qed.
#[export] Hint Resolve rb_tree_valid_red_child_black_r : rbtree.
Lemma rb_tree_black_child_bh_l : forall x l r n,
rb_tree_valid (node x l r black) ->
rb_tree_bh (node x l r black) = S n ->
rb_tree_bh l = n.
Proof. intros x l r n Hval Hbh.
assert (rb_tree_bh l = rb_tree_bh r) by eauto with rbtree.
cbn in Hbh.
congruence.
Qed.
#[export] Hint Resolve rb_tree_black_child_bh_l : rbtree.
Lemma rb_tree_black_child_bh_r : forall x l r n,
rb_tree_valid (node x l r black) ->
rb_tree_bh (node x l r black) = S n ->
rb_tree_bh r = n.
Proof. intros x l r n Hval Hbh.
assert (rb_tree_bh l = rb_tree_bh r) by eauto with rbtree.
cbn in Hbh.
congruence.
Qed.
#[export] Hint Resolve rb_tree_black_child_bh_r : rbtree.
Lemma rb_tree_red_child_bh_l : forall x l r n,
rb_tree_valid (node x l r red) ->
rb_tree_bh (node x l r red) = n ->
rb_tree_bh l = n.
Proof. intros x l r n Hval Hbh.
assert (rb_tree_bh l = rb_tree_bh r) by eauto with rbtree.
cbn in Hbh.
congruence.
Qed.
#[export] Hint Resolve rb_tree_red_child_bh_l : rbtree.
Lemma rb_tree_red_child_bh_r : forall x l r n,
rb_tree_valid (node x l r red) ->
rb_tree_bh (node x l r red) = n ->
rb_tree_bh r = n.
Proof. intros x l r n Hval Hbh.
assert (rb_tree_bh l = rb_tree_bh r) by eauto with rbtree.
cbn in Hbh.
congruence.
Qed.
#[export] Hint Resolve rb_tree_red_child_bh_r : rbtree.
Lemma rb_tree_black_child_bh_l_inv : forall x l r n,
rb_tree_valid (node x l r black) ->
rb_tree_bh l = n ->
rb_tree_bh (node x l r black) = S n.
Proof. intros x l r n Hval Hbh.
assert (rb_tree_bh l = rb_tree_bh r) by eauto with rbtree.
cbn.
congruence.
Qed.
#[export] Hint Resolve rb_tree_black_child_bh_l_inv : rbtree.
Lemma rb_tree_black_child_bh_r_inv : forall x l r n,
rb_tree_valid (node x l r black) ->
rb_tree_bh r = n ->
rb_tree_bh (node x l r black) = S n.
Proof. intros x l r n Hval Hbh.
assert (rb_tree_bh l = rb_tree_bh r) by eauto with rbtree.
cbn.
congruence.
Qed.
#[export] Hint Resolve rb_tree_black_child_bh_r_inv : rbtree.
Lemma rb_tree_red_child_bh_l_inv : forall x l r n,
rb_tree_valid (node x l r red) ->
rb_tree_bh l = n ->
rb_tree_bh (node x l r red) = n.
Proof. intros x l r n Hval Hbh.
assert (rb_tree_bh l = rb_tree_bh r) by eauto with rbtree.
cbn.
congruence.
Qed.
#[export] Hint Resolve rb_tree_red_child_bh_l_inv : rbtree.
Lemma rb_tree_red_child_bh_r_inv : forall x l r n,
rb_tree_valid (node x l r red) ->
rb_tree_bh r = n ->
rb_tree_bh (node x l r red) = n.
Proof. intros x l r n Hval Hbh.
assert (rb_tree_bh l = rb_tree_bh r) by eauto with rbtree.
cbn.
congruence.
Qed.
#[export] Hint Resolve rb_tree_red_child_bh_r_inv : rbtree.
Lemma s_n_not_n n : ~ S n = n.
Proof. induction n; [ discriminate | intros Heq; inversion Heq; contradiction ]. Qed.
(* From a hypothesis rb_tree_valid tree, infer that subtrees are valid and have equal bh *)
Ltac rb_infer_valid H :=
match type of H with
| rb_tree_valid (node ?x ?l ?r black) =>
let new_H1 := fresh "H" in
let new_H2 := fresh "H" in
let new_H3 := fresh "H" in
let new_H4 := fresh "H" in
let new_H5 := fresh "H" in
assert (new_H1 : rb_tree_valid l) by eauto with rbtree;
assert (new_H2 : rb_tree_valid r) by eauto with rbtree;
assert (new_H3 : rb_tree_bh l = rb_tree_bh r) by eauto with rbtree;
assert (new_H4 : rb_tree_bh l <> 0) by eauto with rbtree;
assert (new_H5 : rb_tree_bh (node x l r black) = S (rb_tree_bh l)) by eauto with rbtree;
try rb_infer_valid new_H1; try rb_infer_valid new_H2
| rb_tree_valid (node ?x ?l ?r red) =>
let new_H1 := fresh "H" in
let new_H2 := fresh "H" in
let new_H3 := fresh "H" in
let new_H4 := fresh "H" in
let new_H5 := fresh "H" in
let new_H6 := fresh "H" in
let new_H7 := fresh "H" in
assert (new_H1 : rb_tree_valid l) by eauto with rbtree;
assert (new_H2 : rb_tree_valid r) by eauto with rbtree;
assert (new_H3 : rb_tree_bh l = rb_tree_bh r) by eauto with rbtree;
assert (new_H4 : rb_tree_bh l <> 0) by eauto with rbtree;
assert (new_H5 : rb_tree_bh (node x l r red) = rb_tree_bh l) by eauto with rbtree;
assert (new_H6 : rb_tree_color l = black) by eauto with rbtree;
assert (new_H7 : rb_tree_color r = black) by eauto with rbtree;
cbn in new_H6, new_H7;
match type of new_H6 with ?x = _ => try subst x end;
match type of new_H7 with ?x = _ => try subst x end;
try rb_infer_valid new_H1; try rb_infer_valid new_H2
| _ => idtac
end.
Ltac prove_tree_valid' tree :=
match tree with
| (node _ ?a ?b _) =>
match a with
| node ?ax ?al ?ar ?ac =>
prove_tree_valid' (node ax al ar ac)
| _ => idtac
end;
match b with
| node ?bx ?bl ?br ?bc =>
prove_tree_valid' (node bx bl br bc)
| _ => idtac
end;
let H := fresh "H" in
try assert (H : rb_tree_valid tree) by (constructor; eauto with rbtree; try congruence; cbn; congruence);
try rb_infer_valid H
| _ => idtac
end.
Ltac prove_tree_valid :=
match goal with
| |- rb_tree_valid nil => auto with rbtree
| |- rb_tree_valid ?t => prove_tree_valid' t; auto
end.
(* To define correctness of insertion and deletion,
we need to introduce the infix traversal of a tree.
*)
Fixpoint rb_tree_infix (tree : rb_tree) :=
match tree with
| nil => []
| node x l r _ => rb_tree_infix l ++ [x] ++ rb_tree_infix r
end.
Definition rb_insert_rel tree tree' :=
rb_tree_bh tree' = rb_tree_bh tree \/
rb_tree_bh tree' = S (rb_tree_bh tree) /\
rb_tree_color tree' = black /\
match tree' with
| node _ l r _ => rb_tree_color l = red -> rb_tree_color r = red -> rb_tree_color tree = red
| _ => True
end.
Lemma rb_insert_rel_base x :
rb_insert_rel nil (node x nil nil red).
Proof. left; cbn; auto. Qed.
#[export] Hint Resolve rb_insert_rel_base : rbtree.
Definition rb_insert_rebalance_left x l' r c (is_bh_equal : bool) : rb_tree * bool :=
match c with
| black =>
if is_bh_equal then
(node x l' r black, true)
else
match l' with
| nil => (* Impossible *) (nil, true)
| node l'_x l'_l l'_r _ => (* l'_c must be black *)
match rb_tree_color l'_l with
| black =>
match rb_tree_color l'_r with
| black =>
(node x (node l'_x l'_l l'_r red) r black, true)
| red =>
match l'_r with
| nil => (* Impossible *) (nil, true)
| node l'_r_x l'_r_l l'_r_r l'_r_c =>
(node l'_r_x (node l'_x l'_l l'_r_l black) (node x l'_r_r r black) red, true)
end
end
| red =>
match l'_l with
| nil => (* Impossible *) (nil, true)
| node l'_l_x l'_l_l l'_l_r l'_l_c =>
(node l'_x (node l'_l_x l'_l_l l'_l_r black) (node x l'_r r black) red, true)
end
end
end
| red =>
if is_bh_equal then
(node x l' r black, false)
else
match l' with
| nil => (* Impossible *) (nil, true)
| node l'_x l'_l l'_r l'_c => (* l'_c must be black *)
match rb_tree_color l'_l with
| black =>
match rb_tree_color l'_r with
| black =>
(node x (node l'_x l'_l l'_r red) r black, false)
| red =>
match l'_r with
| nil => (* Impossible *) (nil, true)
| node l'_r_x l'_r_l l'_r_r l'_r_c =>
(node l'_r_x (node l'_x l'_l l'_r_l red) (node x l'_r_r r red) black, false)
end
end
| red =>
match rb_tree_color l'_r with
| black =>
match l'_l with
| nil => (* Impossible *) (nil, true)
| node l'_l_x l'_l_l l'_l_r l'_l_c =>
(node l'_x (node l'_l_x l'_l_l l'_l_r red) (node x l'_r r red) black, false)
end
| red => (* Impossible *) (nil, true)
end
end
end
end.
Lemma rb_insert_rebalance_left_valid x l l' r c b :
rb_tree_valid (node x l r c) ->
rb_tree_valid l' ->
rb_insert_rel l l' ->
rb_tree_bh l' = rb_tree_bh l <-> b = true ->
let p := rb_insert_rebalance_left x l' r c b in
rb_tree_valid (fst p).
Proof. intros Hval Hval' Hrel Hbh.
destruct c; rb_infer_valid Hval.
all: destruct Hrel as [Hrel | Hrel].
1,3: pose proof Hrel as Hb; rewrite Hbh in Hb; subst b; clear Hbh.
3,4: destruct Hrel as (Hrel1 & Hrel2 & Hrel3);
assert (Hb : b = false) by (destruct b; auto; destruct Hbh as (_ & Hbh); specialize (Hbh ltac:(auto)); rewrite Hrel1 in Hbh; exfalso; eapply s_n_not_n; apply Hbh);
clear Hbh.
all: match goal with
|- context[rb_insert_rebalance_left ?x ?l' ?r ?c ?b] =>
remember (rb_insert_rebalance_left x l' r c b) as p
end; cbn.
all: unfold rb_insert_rebalance_left in Heqp.
all: repeat match type of Heqp with
| ?p = match ?t with _ => _ end =>
let H := fresh "H" in destruct t eqn:H
end; cbn in *; subst; cbn [fst];
rb_infer_valid Hval'; prove_tree_valid.
Qed.
Lemma rb_insert_rebalance_left_rel x l l' r c b :
rb_tree_valid (node x l r c) ->
rb_tree_valid l' ->
rb_insert_rel l l' ->
rb_tree_bh l' = rb_tree_bh l <-> b = true ->
let p := rb_insert_rebalance_left x l' r c b in
rb_insert_rel (node x l r c) (fst p).
Proof. intros Hval Hval' Hrel Hbh.
pose proof (rb_insert_rebalance_left_valid x l l' r c b ltac:(auto) ltac:(auto) ltac:(auto) ltac:(auto)) as Hval''.
hnf in Hval''.
destruct c; rb_infer_valid Hval.
all: destruct Hrel as [Hrel | Hrel].
1,3: pose proof Hrel as Hb; rewrite Hbh in Hb; subst b; clear Hbh.
3,4: destruct Hrel as (Hrel1 & Hrel2 & Hrel3);
assert (Hb : b = false) by (destruct b; auto; destruct Hbh as (_ & Hbh); specialize (Hbh ltac:(auto)); rewrite Hrel1 in Hbh; exfalso; eapply s_n_not_n; apply Hbh);
clear Hbh.
all: match goal with
|- context[rb_insert_rebalance_left ?x ?l' ?r ?c ?b] =>
remember (rb_insert_rebalance_left x l' r c b) as p
end; cbn.
all: unfold rb_insert_rebalance_left in Heqp.
all: repeat match type of Heqp with
| ?p = match ?t with _ => _ end =>
let H := fresh "H" in destruct t eqn:H
end; cbn in *; subst; cbn [fst]; cbn [fst] in Hval''.
all: match goal with H : red = red -> red = red -> _ |- _ => specialize (H ltac:(auto) ltac:(auto)) | _ => idtac end.
all: rb_infer_valid Hval; rb_infer_valid Hval'; rb_infer_valid Hval''.
all: unfold rb_insert_rel; try (left; cbn; congruence).
all: try (right; repeat split; congruence).
Qed.
Lemma rb_insert_rebalance_left_bh x l l' r c b :
rb_tree_valid (node x l r c) ->
rb_tree_valid l' ->
rb_insert_rel l l' ->
rb_tree_bh l' = rb_tree_bh l <-> b = true ->
let p := rb_insert_rebalance_left x l' r c b in
rb_tree_bh (fst p) = rb_tree_bh (node x l r c) <-> (snd p) = true.
Proof. intros Hval Hval' Hrel Hbh.
pose proof (rb_insert_rebalance_left_valid x l l' r c b ltac:(auto) ltac:(auto) ltac:(auto) ltac:(auto)) as Hval''.
hnf in Hval''.
destruct c; rb_infer_valid Hval.
all: destruct Hrel as [Hrel | Hrel].
1,3: pose proof Hrel as Hb; rewrite Hbh in Hb; subst b; clear Hbh.
3,4: destruct Hrel as (Hrel1 & Hrel2 & Hrel3);
assert (Hb : b = false) by (destruct b; auto; destruct Hbh as (_ & Hbh); specialize (Hbh ltac:(auto)); rewrite Hrel1 in Hbh; exfalso; eapply s_n_not_n; apply Hbh);
clear Hbh.
all: match goal with
|- context[rb_insert_rebalance_left ?x ?l' ?r ?c ?b] =>
remember (rb_insert_rebalance_left x l' r c b) as p
end; cbn.
all: unfold rb_insert_rebalance_left in Heqp.
all: repeat match type of Heqp with
| ?p = match ?t with _ => _ end =>
let H := fresh "H" in destruct t eqn:H
end; cbn in *; subst; cbn [fst snd]; cbn [fst] in Hval''.
all: match goal with H : red = red -> red = red -> _ |- _ => specialize (H ltac:(auto) ltac:(auto)) | _ => idtac end.
all: rb_infer_valid Hval; rb_infer_valid Hval'; rb_infer_valid Hval''.
all: split; try reflexivity.
all: try (intros; congruence).
all: match goal with H : rb_tree_bh ?t = S ?n |- context[rb_tree_bh ?t = _ -> _] => assert (rb_tree_bh t <> n) by (rewrite H; apply s_n_not_n) end.
all: intros; congruence.
Qed.
Lemma rb_insert_rebalance_left_not_nil x l l' r c b :
rb_tree_valid (node x l r c) ->
rb_tree_valid l' ->
rb_insert_rel l l' ->
rb_tree_bh l' = rb_tree_bh l <-> b = true ->
let p := rb_insert_rebalance_left x l' r c b in
fst p <> nil.
Proof. intros Hval Hval' Hrel Hbh.
pose proof (rb_insert_rebalance_left_valid x l l' r c b ltac:(auto) ltac:(auto) ltac:(auto) ltac:(auto)) as Hval''.
hnf in Hval''.
destruct c; rb_infer_valid Hval.
all: destruct Hrel as [Hrel | Hrel].
1,3: pose proof Hrel as Hb; rewrite Hbh in Hb; subst b; clear Hbh.
3,4: destruct Hrel as (Hrel1 & Hrel2 & Hrel3);
assert (Hb : b = false) by (destruct b; auto; destruct Hbh as (_ & Hbh); specialize (Hbh ltac:(auto)); rewrite Hrel1 in Hbh; exfalso; eapply s_n_not_n; apply Hbh);
clear Hbh.
all: match goal with
|- context[rb_insert_rebalance_left ?x ?l' ?r ?c ?b] =>
remember (rb_insert_rebalance_left x l' r c b) as p
end; cbn.
all: unfold rb_insert_rebalance_left in Heqp.
all: repeat match type of Heqp with
| ?p = match ?t with _ => _ end =>
let H := fresh "H" in destruct t eqn:H
end; cbn in *; subst; cbn [fst snd]; cbn [fst] in Hval''.
all: match goal with H : red = red -> red = red -> _ |- _ => specialize (H ltac:(auto) ltac:(auto)) | _ => idtac end.
all: rb_infer_valid Hval; rb_infer_valid Hval'; rb_infer_valid Hval''.
all: congruence.
Qed.
Lemma rb_insert_rebalance_left_infix x l l' r c b :
rb_tree_valid (node x l r c) ->
rb_tree_valid l' ->
rb_insert_rel l l' ->
rb_tree_bh l' = rb_tree_bh l <-> b = true ->
let p := rb_insert_rebalance_left x l' r c b in
rb_tree_infix (fst p) = rb_tree_infix l' ++ [x] ++ rb_tree_infix r.
Proof. intros Hval Hval' Hrel Hbh.
pose proof (rb_insert_rebalance_left_not_nil x l l' r c b ltac:(auto) ltac:(auto) ltac:(auto) ltac:(auto)) as Hnot_nil.
hnf in Hnot_nil.
destruct c.
all: destruct Hrel as [Hrel | Hrel].
1,3: pose proof Hrel as Hb; rewrite Hbh in Hb; subst b; clear Hbh.
3,4: destruct Hrel as (Hrel1 & Hrel2 & Hrel3);
assert (Hb : b = false) by (destruct b; auto; destruct Hbh as (_ & Hbh); specialize (Hbh ltac:(auto)); rewrite Hrel1 in Hbh; exfalso; eapply s_n_not_n; apply Hbh);
clear Hbh.
all: match goal with
|- context[rb_insert_rebalance_left ?x ?l' ?r ?c ?b] =>
remember (rb_insert_rebalance_left x l' r c b) as p
end; cbn.
all: unfold rb_insert_rebalance_left in Heqp.
all: repeat match type of Heqp with
| ?p = match ?t with _ => _ end =>
let H := fresh "H" in destruct t eqn:H
end; subst p; cbn [fst snd]; cbn [fst] in Hnot_nil.
all: try contradiction.
all: cbn [rb_tree_infix]; repeat rewrite <- app_assoc; auto.
Qed.
Lemma rb_insert_rebalance_left_correct x l l' r c b :
rb_tree_valid (node x l r c) ->
rb_tree_valid l' ->
rb_insert_rel l l' ->
rb_tree_bh l' = rb_tree_bh l <-> b = true ->
let p := rb_insert_rebalance_left x l' r c b in
rb_tree_valid (fst p) /\
rb_insert_rel (node x l r c) (fst p) /\
rb_tree_infix (fst p) = rb_tree_infix l' ++ [x] ++ rb_tree_infix r /\
(rb_tree_bh (fst p) = rb_tree_bh (node x l r c) <-> snd p = true).
Proof. cbn zeta.
intros; split; [|split]; [| |split];
[ eapply rb_insert_rebalance_left_valid
| eapply rb_insert_rebalance_left_rel
| eapply rb_insert_rebalance_left_infix
| eapply rb_insert_rebalance_left_bh ];
eauto.
Qed.
Definition rb_insert_rebalance_right x l r' c (is_bh_equal : bool) : rb_tree * bool :=
match c with
| black =>
if is_bh_equal then
(node x l r' black, true)
else
match r' with
| nil => (* Impossible *) (nil, true)
| node r'_x r'_l r'_r r'_c => (* r'_c must be black *)
match rb_tree_color r'_l with
| black =>
match rb_tree_color r'_r with
| black =>
(node x l (node r'_x r'_l r'_r red) black, true)
| red =>
match r'_r with
| nil => (* Impossible *) (nil, true)
| node r'_r_x r'_r_l r'_r_r r'_r_c =>
(node r'_x (node x l r'_l black) (node r'_r_x r'_r_l r'_r_r black) red, true)
end
end
| red =>
match r'_l with
| nil => (* Impossible *) (nil, true)
| node r'_l_x r'_l_l r'_l_r r'_l_c =>
(node r'_l_x (node x l r'_l_l black) (node r'_x r'_l_r r'_r black) red, true)
end
end
end
| red =>
if is_bh_equal then
(node x l r' black, false)
else
match r' with
| nil => (* Impossible *) (nil, true)
| node r'_x r'_l r'_r r'_c => (* r'_c must be black *)
match rb_tree_color r'_l with
| black =>
match rb_tree_color r'_r with
| black =>
(node x l (node r'_x r'_l r'_r red) black, false)
| red =>
match r'_r with
| nil => (* Impossible *) (nil, true)
| node r'_r_x r'_r_l r'_r_r r'_r_c =>
(node r'_x (node x l r'_l red) (node r'_r_x r'_r_l r'_r_r red) black, false)
end
end
| red =>
match rb_tree_color r'_r with
| black =>
match r'_l with
| nil => (* Impossible *) (nil, true)
| node r'_l_x r'_l_l r'_l_r r'_l_c =>
(node r'_l_x (node x l r'_l_l red) (node r'_x r'_l_r r'_r red) black, false)
end
| red => (* Impossible *) (nil, true)
end
end
end
end.
Lemma rb_insert_rebalance_right_valid x l r r' c b :
rb_tree_valid (node x l r c) ->
rb_tree_valid r' ->
rb_insert_rel r r' ->
rb_tree_bh r' = rb_tree_bh r <-> b = true ->
let p := rb_insert_rebalance_right x l r' c b in
rb_tree_valid (fst p).
Proof. intros Hval Hval' Hrel Hbh.
destruct c; rb_infer_valid Hval.
all: destruct Hrel as [Hrel | Hrel].
1,3: pose proof Hrel as Hb; rewrite Hbh in Hb; subst b; clear Hbh.
3,4: destruct Hrel as (Hrel1 & Hrel2 & Hrel3);
assert (Hb : b = false) by (destruct b; auto; destruct Hbh as (_ & Hbh); specialize (Hbh ltac:(auto)); rewrite Hrel1 in Hbh; exfalso; eapply s_n_not_n; apply Hbh);
clear Hbh.
all: match goal with
|- context[rb_insert_rebalance_right ?x ?l ?r' ?c ?b] =>
remember (rb_insert_rebalance_right x l r' c b) as p
end; cbn.
all: unfold rb_insert_rebalance_right in Heqp.
all: repeat match type of Heqp with
| ?p = match ?t with _ => _ end =>
let H := fresh "H" in destruct t eqn:H
end; cbn in *; subst; cbn [fst];
rb_infer_valid Hval'; prove_tree_valid.
Qed.
Lemma rb_insert_rebalance_right_rel x l r r' c b :
rb_tree_valid (node x l r c) ->
rb_tree_valid r' ->
rb_insert_rel r r' ->
rb_tree_bh r' = rb_tree_bh r <-> b = true ->
let p := rb_insert_rebalance_right x l r' c b in
rb_insert_rel (node x l r c) (fst p).
Proof. intros Hval Hval' Hrel Hbh.
pose proof (rb_insert_rebalance_right_valid x l r r' c b ltac:(auto) ltac:(auto) ltac:(auto) ltac:(auto)) as Hval''.
hnf in Hval''.
destruct c; rb_infer_valid Hval.
all: destruct Hrel as [Hrel | Hrel].
1,3: pose proof Hrel as Hb; rewrite Hbh in Hb; subst b; clear Hbh.
3,4: destruct Hrel as (Hrel1 & Hrel2 & Hrel3);
assert (Hb : b = false) by (destruct b; auto; destruct Hbh as (_ & Hbh); specialize (Hbh ltac:(auto)); rewrite Hrel1 in Hbh; exfalso; eapply s_n_not_n; apply Hbh);
clear Hbh.
all: match goal with
|- context[rb_insert_rebalance_right ?x ?l ?r' ?c ?b] =>
remember (rb_insert_rebalance_right x l r' c b) as p
end; cbn.
all: unfold rb_insert_rebalance_right in Heqp.
all: repeat match type of Heqp with
| ?p = match ?t with _ => _ end =>
let H := fresh "H" in destruct t eqn:H
end; cbn in *; subst; cbn [fst]; cbn [fst] in Hval''.
all: match goal with H : red = red -> red = red -> _ |- _ => specialize (H ltac:(auto) ltac:(auto)) | _ => idtac end.
all: rb_infer_valid Hval; rb_infer_valid Hval'; rb_infer_valid Hval''.
all: unfold rb_insert_rel; try (left; cbn; congruence).
all: try (right; repeat split; congruence).
Qed.
Lemma rb_insert_rebalance_right_bh x l r r' c b :
rb_tree_valid (node x l r c) ->
rb_tree_valid r' ->
rb_insert_rel r r' ->
rb_tree_bh r' = rb_tree_bh r <-> b = true ->
let p := rb_insert_rebalance_right x l r' c b in
rb_tree_bh (fst p) = rb_tree_bh (node x l r c) <-> (snd p) = true.
Proof. intros Hval Hval' Hrel Hbh.
pose proof (rb_insert_rebalance_right_valid x l r r' c b ltac:(auto) ltac:(auto) ltac:(auto) ltac:(auto)) as Hval''.
hnf in Hval''.
destruct c; rb_infer_valid Hval.
all: destruct Hrel as [Hrel | Hrel].
1,3: pose proof Hrel as Hb; rewrite Hbh in Hb; subst b; clear Hbh.
3,4: destruct Hrel as (Hrel1 & Hrel2 & Hrel3);
assert (Hb : b = false) by (destruct b; auto; destruct Hbh as (_ & Hbh); specialize (Hbh ltac:(auto)); rewrite Hrel1 in Hbh; exfalso; eapply s_n_not_n; apply Hbh);
clear Hbh.
all: match goal with
|- context[rb_insert_rebalance_right ?x ?l ?r' ?c ?b] =>
remember (rb_insert_rebalance_right x l r' c b) as p
end; cbn.
all: unfold rb_insert_rebalance_right in Heqp.
all: repeat match type of Heqp with
| ?p = match ?t with _ => _ end =>
let H := fresh "H" in destruct t eqn:H
end; cbn in *; subst; cbn [fst snd]; cbn [fst] in Hval''.
all: match goal with H : red = red -> red = red -> _ |- _ => specialize (H ltac:(auto) ltac:(auto)) | _ => idtac end.
all: rb_infer_valid Hval; rb_infer_valid Hval'; rb_infer_valid Hval''.
all: split; try reflexivity.
all: try (intros; congruence).
all: match goal with H : rb_tree_bh ?t = S ?n |- context[rb_tree_bh ?t = _ -> _] => assert (rb_tree_bh t <> n) by (rewrite H; apply s_n_not_n) end.
all: intros; congruence.
Qed.
Lemma rb_insert_rebalance_right_not_nil x l r r' c b :
rb_tree_valid (node x l r c) ->
rb_tree_valid r' ->
rb_insert_rel r r' ->
rb_tree_bh r' = rb_tree_bh r <-> b = true ->
let p := rb_insert_rebalance_right x l r' c b in
fst p <> nil.
Proof. intros Hval Hval' Hrel Hbh.
pose proof (rb_insert_rebalance_right_valid x l r r' c b ltac:(auto) ltac:(auto) ltac:(auto) ltac:(auto)) as Hval''.
hnf in Hval''.
destruct c; rb_infer_valid Hval.
all: destruct Hrel as [Hrel | Hrel].
1,3: pose proof Hrel as Hb; rewrite Hbh in Hb; subst b; clear Hbh.
3,4: destruct Hrel as (Hrel1 & Hrel2 & Hrel3);
assert (Hb : b = false) by (destruct b; auto; destruct Hbh as (_ & Hbh); specialize (Hbh ltac:(auto)); rewrite Hrel1 in Hbh; exfalso; eapply s_n_not_n; apply Hbh);
clear Hbh.
all: match goal with
|- context[rb_insert_rebalance_right ?x ?l ?r' ?c ?b] =>
remember (rb_insert_rebalance_right x l r' c b) as p
end; cbn.
all: unfold rb_insert_rebalance_right in Heqp.
all: repeat match type of Heqp with
| ?p = match ?t with _ => _ end =>
let H := fresh "H" in destruct t eqn:H
end; cbn in *; subst; cbn [fst snd]; cbn [fst] in Hval''.
all: match goal with H : red = red -> red = red -> _ |- _ => specialize (H ltac:(auto) ltac:(auto)) | _ => idtac end.
all: rb_infer_valid Hval; rb_infer_valid Hval'; rb_infer_valid Hval''.
all: congruence.
Qed.
Lemma rb_insert_rebalance_right_infix x l r r' c b :
rb_tree_valid (node x l r c) ->
rb_tree_valid r' ->
rb_insert_rel r r' ->
rb_tree_bh r' = rb_tree_bh r <-> b = true ->
let p := rb_insert_rebalance_right x l r' c b in
rb_tree_infix (fst p) = rb_tree_infix l ++ [x] ++ rb_tree_infix r'.
Proof. intros Hval Hval' Hrel Hbh.
pose proof (rb_insert_rebalance_right_not_nil x l r r' c b ltac:(auto) ltac:(auto) ltac:(auto) ltac:(auto)) as Hnot_nil.
hnf in Hnot_nil.
destruct c.
all: destruct Hrel as [Hrel | Hrel].
1,3: pose proof Hrel as Hb; rewrite Hbh in Hb; subst b; clear Hbh.
3,4: destruct Hrel as (Hrel1 & Hrel2 & Hrel3);
assert (Hb : b = false) by (destruct b; auto; destruct Hbh as (_ & Hbh); specialize (Hbh ltac:(auto)); rewrite Hrel1 in Hbh; exfalso; eapply s_n_not_n; apply Hbh);
clear Hbh.
all: match goal with
|- context[rb_insert_rebalance_right ?x ?l ?r' ?c ?b] =>
remember (rb_insert_rebalance_right x l r' c b) as p
end; cbn.
all: unfold rb_insert_rebalance_right in Heqp.
all: repeat match type of Heqp with
| ?p = match ?t with _ => _ end =>
let H := fresh "H" in destruct t eqn:H
end; subst p; cbn [fst snd]; cbn [fst] in Hnot_nil.
all: try contradiction.
all: cbn [rb_tree_infix]; repeat rewrite <- app_assoc; auto.
Qed.
Lemma rb_insert_rebalance_right_correct x l r r' c b :
rb_tree_valid (node x l r c) ->
rb_tree_valid r' ->
rb_insert_rel r r' ->
rb_tree_bh r' = rb_tree_bh r <-> b = true ->
let p := rb_insert_rebalance_right x l r' c b in
rb_tree_valid (fst p) /\
rb_insert_rel (node x l r c) (fst p) /\
rb_tree_infix (fst p) = rb_tree_infix l ++ [x] ++ rb_tree_infix r' /\
(rb_tree_bh (fst p) = rb_tree_bh (node x l r c) <-> snd p = true).
Proof. cbn zeta.
intros; split; [|split]; [| |split];
[ eapply rb_insert_rebalance_right_valid
| eapply rb_insert_rebalance_right_rel
| eapply rb_insert_rebalance_right_infix
| eapply rb_insert_rebalance_right_bh ];
eauto.
Qed.
Definition rb_delete_rel tree tree' :=
(rb_tree_bh tree' = rb_tree_bh tree \/ S (rb_tree_bh tree') = rb_tree_bh tree) /\
(rb_tree_color tree' = red -> rb_tree_bh tree' = rb_tree_bh tree -> rb_tree_color tree = red).
Lemma rb_delete_rel_base_left x l c :
rb_tree_valid (node x l nil c) ->
rb_delete_rel (node x l nil c) l.
Proof. intros Hval.
destruct c; rb_infer_valid Hval.
all: split; cbn; auto.
intros _ Heq; symmetry in Heq; exfalso; eapply s_n_not_n; apply Heq.
Qed.
#[export] Hint Resolve rb_delete_rel_base_left : rbtree.
Lemma rb_delete_rel_base_right x r c :
rb_tree_valid (node x nil r c) ->
rb_delete_rel (node x nil r c) r.
Proof. intros Hval.
destruct c; rb_infer_valid Hval.
all: split; cbn; auto.
cbn in *; intros; congruence.
Qed.
#[export] Hint Resolve rb_delete_rel_base_right : rbtree.
Definition rb_delete_rebalance_left x l' r c (is_bh_equal : bool) : rb_tree * bool :=
match c with
| black =>
if is_bh_equal then
(node x l' r black, true)
else
match rb_tree_color l' with
| black =>
match r with
| nil => (* Impossible *) (nil, true)
| node r_x r_l r_r r_c =>
match r_c with
| black =>
match r_l with
| nil =>
(node r_x (node x l' r_l red) r_r black, false)
| node r_l_x r_l_l r_l_r r_l_c =>
match r_l_c with
| black =>
(node r_x (node x l' r_l red) r_r black, false)
| red =>
(node r_l_x (node x l' r_l_l black) (node r_x r_l_r r_r black) red, false)
end
end
| red =>
match r_l with
| nil => (* Impossible *) (nil, true)
| node r_l_x r_l_l r_l_r r_l_c =>
match rb_tree_color r_l_l with
| black =>
(node r_x (node r_l_x (node x l' r_l_l red) r_l_r black) r_r red, false)
| red =>
match r_l_l with
| nil => (* Impossible *) (nil, true)
| node r_l_l_x r_l_l_l r_l_l_r r_l_l_c =>
(node r_x (node r_l_l_x (node x l' r_l_l_l black) (node r_l_x r_l_l_r r_l_r black) red) r_r black, true)
end
end
end
end
end
| red =>
match l' with
| nil => (* Impossible *) (nil, true)
| node l'_x l'_l l'_r l'_c =>
(node x (node l'_x l'_l l'_r black) r black, true)
end
end
| red =>
if is_bh_equal then
match rb_tree_color l' with
| black =>
(node x l' r red, true)
| red => (* Impossible *) (nil, true)
end
else
match rb_tree_color l' with
| black =>
match r with
| nil => (* Impossible *) (nil, true)
| node r_x r_l r_r r_c =>
match rb_tree_color r_l with
| black =>
(node r_x (node x l' r_l red) r_r black, true)
| red =>
match r_l with
| nil => (* Impossible *) (nil, true)
| node r_l_x r_l_l r_l_r r_l_c =>
(node r_l_x (node x l' r_l_l black) (node r_x r_l_r r_r black) red, true)
end
end
end
| red =>
match l' with
| nil => (* Impossible *) (nil, true)
| node l'_x l'_l l'_r l'_c =>
(node x (node l'_x l'_l l'_r black) r red, true)
end
end
end.
Lemma rb_delete_rebalance_left_valid x l l' r c b :
rb_tree_valid (node x l r c) ->
rb_tree_valid l' ->
rb_delete_rel l l' ->
rb_tree_bh l' = rb_tree_bh l <-> b = true ->
let p := rb_delete_rebalance_left x l' r c b in
rb_tree_valid (fst p).
Proof. intros Hval Hval' Hrel Hbh.
destruct c; rb_infer_valid Hval.
all: destruct Hrel as ([Hrel | Hrel] & Hred_root).
1,3: pose proof Hrel as Hb; rewrite Hbh in Hb; subst b; clear Hbh.
3,4: assert (Hb : b = false) by (destruct b; auto; destruct Hbh as (_ & Hbh); specialize (Hbh ltac:(auto)); rewrite <- Hrel in Hbh; symmetry in Hbh; exfalso; eapply s_n_not_n; apply Hbh);
clear Hbh.
all: match goal with
|- context[rb_delete_rebalance_left ?x ?l' ?r ?c ?b] =>
remember (rb_delete_rebalance_left x l' r c b) as p
end; cbn.
all: unfold rb_delete_rebalance_left in Heqp.
all: repeat match type of Heqp with
| ?p = match ?t with _ => _ end =>
let H := fresh "H" in destruct t eqn:H
end; cbn in *; subst; cbn [fst];
rb_infer_valid Hval; rb_infer_valid Hval'; prove_tree_valid.
Qed.
Lemma rb_delete_rebalance_left_rel x l l' r c b :
rb_tree_valid (node x l r c) ->
rb_tree_valid l' ->
rb_delete_rel l l' ->
rb_tree_bh l' = rb_tree_bh l <-> b = true ->
let p := rb_delete_rebalance_left x l' r c b in
rb_delete_rel (node x l r c) (fst p).
Proof. intros Hval Hval' Hrel Hbh.
pose proof (rb_delete_rebalance_left_valid x l l' r c b ltac:(auto) ltac:(auto) ltac:(auto) ltac:(auto)) as Hval''.
hnf in Hval''.
destruct c; rb_infer_valid Hval.
all: destruct Hrel as ([Hrel | Hrel] & Hred_root).
1,3: pose proof Hrel as Hb; rewrite Hbh in Hb; subst b; clear Hbh.
3,4: assert (Hb : b = false) by (destruct b; auto; destruct Hbh as (_ & Hbh); specialize (Hbh ltac:(auto)); rewrite <- Hrel in Hbh; symmetry in Hbh; exfalso; eapply s_n_not_n; apply Hbh);
clear Hbh.
all: match goal with
|- context[rb_delete_rebalance_left ?x ?l' ?r ?c ?b] =>
remember (rb_delete_rebalance_left x l' r c b) as p
end; cbn.
all: unfold rb_delete_rebalance_left in Heqp.
all: repeat match type of Heqp with
| ?p = match ?t with _ => _ end =>
let H := fresh "H" in destruct t eqn:H
end; cbn in *; subst; cbn [fst]; cbn [fst] in Hval''.
all: rb_infer_valid Hval; rb_infer_valid Hval'; rb_infer_valid Hval''.
all: match goal with H : red = red -> _ |- _ => specialize (H ltac:(auto) ltac:(congruence)) | _ => idtac end.
all: unfold rb_delete_rel; split; [|cbn; try congruence].
all: try (left; cbn; congruence).
all: try (right; cbn; congruence).
all: intros _ Heq; inversion Heq as [Heq']; rewrite Heq' in Hrel; exfalso; eapply s_n_not_n; apply Hrel.
Qed.
Lemma rb_delete_rebalance_left_bh x l l' r c b :
rb_tree_valid (node x l r c) ->
rb_tree_valid l' ->
rb_delete_rel l l' ->
rb_tree_bh l' = rb_tree_bh l <-> b = true ->
let p := rb_delete_rebalance_left x l' r c b in
rb_tree_bh (fst p) = rb_tree_bh (node x l r c) <-> (snd p) = true.
Proof. intros Hval Hval' Hrel Hbh.
pose proof (rb_delete_rebalance_left_valid x l l' r c b ltac:(auto) ltac:(auto) ltac:(auto) ltac:(auto)) as Hval''.
hnf in Hval''.
destruct c; rb_infer_valid Hval.
all: destruct Hrel as ([Hrel | Hrel] & Hred_root).
1,3: pose proof Hrel as Hb; rewrite Hbh in Hb; subst b; clear Hbh.
3,4: assert (Hb : b = false) by (destruct b; auto; destruct Hbh as (_ & Hbh); specialize (Hbh ltac:(auto)); rewrite <- Hrel in Hbh; symmetry in Hbh; exfalso; eapply s_n_not_n; apply Hbh);
clear Hbh.
all: match goal with
|- context[rb_delete_rebalance_left ?x ?l' ?r ?c ?b] =>
remember (rb_delete_rebalance_left x l' r c b) as p
end; cbn.
all: unfold rb_delete_rebalance_left in Heqp.
all: repeat match type of Heqp with
| ?p = match ?t with _ => _ end =>
let H := fresh "H" in destruct t eqn:H
end; cbn in *; subst; cbn [fst snd]; cbn [fst] in Hval''.
all: rb_infer_valid Hval; rb_infer_valid Hval'; rb_infer_valid Hval''.
all: match goal with H : red = red -> _ |- _ => specialize (H ltac:(auto) ltac:(congruence)) | _ => idtac end.
all: split; try reflexivity.
all: try (intros; congruence).
all: try (cbn; intros Heq; inversion Heq as [Heq']; rewrite Heq' in Hrel; exfalso; eapply s_n_not_n; apply Hrel).
all: assert (rb_tree_bh l' <> 0) by eauto with rbtree; congruence.
Qed.
Lemma rb_delete_rebalance_left_not_nil x l l' r c b :
rb_tree_valid (node x l r c) ->
rb_tree_valid l' ->
rb_delete_rel l l' ->
rb_tree_bh l' = rb_tree_bh l <-> b = true ->
let p := rb_delete_rebalance_left x l' r c b in
fst p <> nil.
Proof. intros Hval Hval' Hrel Hbh.
pose proof (rb_delete_rebalance_left_valid x l l' r c b ltac:(auto) ltac:(auto) ltac:(auto) ltac:(auto)) as Hval''.
hnf in Hval''.
destruct c; rb_infer_valid Hval.
all: destruct Hrel as ([Hrel | Hrel] & Hred_root).
1,3: pose proof Hrel as Hb; rewrite Hbh in Hb; subst b; clear Hbh.
3,4: assert (Hb : b = false) by (destruct b; auto; destruct Hbh as (_ & Hbh); specialize (Hbh ltac:(auto)); rewrite <- Hrel in Hbh; symmetry in Hbh; exfalso; eapply s_n_not_n; apply Hbh);
clear Hbh.
all: match goal with
|- context[rb_delete_rebalance_left ?x ?l' ?r ?c ?b] =>
remember (rb_delete_rebalance_left x l' r c b) as p
end; cbn.
all: unfold rb_delete_rebalance_left in Heqp.
all: repeat match type of Heqp with
| ?p = match ?t with _ => _ end =>
let H := fresh "H" in destruct t eqn:H
end; cbn in *; subst; cbn [fst snd]; cbn [fst] in Hval''.
all: rb_infer_valid Hval; rb_infer_valid Hval'; rb_infer_valid Hval''.
all: match goal with H : red = red -> _ |- _ => specialize (H ltac:(auto) ltac:(congruence)) | _ => idtac end.
all: try congruence.
all: assert (rb_tree_bh l' <> 0) by eauto with rbtree; congruence.
Qed.
Lemma rb_delete_rebalance_left_infix x l l' r c b :
rb_tree_valid (node x l r c) ->
rb_tree_valid l' ->
rb_delete_rel l l' ->
rb_tree_bh l' = rb_tree_bh l <-> b = true ->
let p := rb_delete_rebalance_left x l' r c b in
rb_tree_infix (fst p) = rb_tree_infix l' ++ [x] ++ rb_tree_infix r.
Proof. intros Hval Hval' Hrel Hbh.
pose proof (rb_delete_rebalance_left_not_nil x l l' r c b ltac:(auto) ltac:(auto) ltac:(auto) ltac:(auto)) as Hnot_nil.
hnf in Hnot_nil.
destruct c.
all: destruct Hrel as ([Hrel | Hrel] & Hred_root).
1,3: pose proof Hrel as Hb; rewrite Hbh in Hb; subst b; clear Hbh.
3,4: assert (Hb : b = false) by (destruct b; auto; destruct Hbh as (_ & Hbh); specialize (Hbh ltac:(auto)); rewrite <- Hrel in Hbh; symmetry in Hbh; exfalso; eapply s_n_not_n; apply Hbh);
clear Hbh.
all: match goal with
|- context[rb_delete_rebalance_left ?x ?l' ?r ?c ?b] =>
remember (rb_delete_rebalance_left x l' r c b) as p
end; cbn.
all: unfold rb_delete_rebalance_left in Heqp.
all: repeat match type of Heqp with
| ?p = match ?t with _ => _ end =>
let H := fresh "H" in destruct t eqn:H
end; subst p; cbn [fst snd]; cbn [fst] in Hnot_nil.
all: try contradiction.
all: cbn [rb_tree_infix]; repeat rewrite <- app_assoc; auto.
Qed.
Lemma rb_delete_rebalance_left_correct x l l' r c b :
rb_tree_valid (node x l r c) ->
rb_tree_valid l' ->
rb_delete_rel l l' ->
rb_tree_bh l' = rb_tree_bh l <-> b = true ->
let p := rb_delete_rebalance_left x l' r c b in
rb_tree_valid (fst p) /\
rb_delete_rel (node x l r c) (fst p) /\
rb_tree_infix (fst p) = rb_tree_infix l' ++ [x] ++ rb_tree_infix r /\
(rb_tree_bh (fst p) = rb_tree_bh (node x l r c) <-> snd p = true).
Proof. cbn zeta.
intros; split; [|split]; [| |split];
[ eapply rb_delete_rebalance_left_valid
| eapply rb_delete_rebalance_left_rel
| eapply rb_delete_rebalance_left_infix
| eapply rb_delete_rebalance_left_bh ];
eauto.
Qed.
Definition rb_delete_rebalance_right x l r' c (is_bh_equal : bool) : rb_tree * bool :=
match c with
| black =>
if is_bh_equal then
(node x l r' black, true)
else
match rb_tree_color r' with
| black =>
match l with
| nil => (* Impossible *) (nil, true)
| node l_x l_l l_r l_c =>
match l_c with
| black =>
match l_r with
| nil =>
(node l_x l_l (node x l_r r' red) black, false)
| node l_r_x l_r_l l_r_r l_r_c =>
match l_r_c with
| black =>
(node l_x l_l (node x l_r r' red) black, false)
| red =>
(node l_r_x (node l_x l_l l_r_l black) (node x l_r_r r' black) red, false)
end
end
| red =>
match l_r with
| nil => (* Impossible *) (nil, true)
| node l_r_x l_r_l l_r_r l_r_c =>
match rb_tree_color l_r_r with
| black =>
(node l_x l_l (node l_r_x l_r_l (node x l_r_r r' red) black) red, false)
| red =>
match l_r_r with
| nil => (* Impossible *) (nil, true)
| node l_r_r_x l_r_r_l l_r_r_r l_r_r_c =>
(node l_x l_l (node l_r_r_x (node l_r_x l_r_l l_r_r_l black) (node x l_r_r_r r' black) red) black, true)
end
end
end
end
end
| red =>
match r' with
| nil => (* Impossible *) (nil, true)
| node r'_x r'_l r'_r r'_c =>
(node x l (node r'_x r'_l r'_r black) black, true)
end
end
| red =>
if is_bh_equal then
match rb_tree_color r' with
| black =>
(node x l r' red, true)
| red => (* Impossible *) (nil, true)
end
else
match rb_tree_color r' with
| black =>
match l with
| nil => (* Impossible *) (nil, true)
| node l_x l_l l_r l_c =>
match rb_tree_color l_r with
| black =>
(node l_x l_l (node x l_r r' red) black, true)
| red =>
match l_r with
| nil => (* Impossible *) (nil, true)
| node l_r_x l_r_l l_r_r l_r_c =>
(node l_r_x (node l_x l_l l_r_l black) (node x l_r_r r' black) red, true)
end
end
end
| red =>
match r' with
| nil => (* Impossible *) (nil, true)
| node r'_x r'_l r'_r r'_c =>
(node x l (node r'_x r'_l r'_r black) red, true)
end
end
end.
Lemma rb_delete_rebalance_right_valid x l r r' c b :
rb_tree_valid (node x l r c) ->
rb_tree_valid r' ->
rb_delete_rel r r' ->
rb_tree_bh r' = rb_tree_bh r <-> b = true ->
let p := rb_delete_rebalance_right x l r' c b in
rb_tree_valid (fst p).
Proof. intros Hval Hval' Hrel Hbh.
destruct c; rb_infer_valid Hval.
all: destruct Hrel as ([Hrel | Hrel] & Hred_root).
1,3: pose proof Hrel as Hb; rewrite Hbh in Hb; subst b; clear Hbh.
3,4: assert (Hb : b = false) by (destruct b; auto; destruct Hbh as (_ & Hbh); specialize (Hbh ltac:(auto)); rewrite <- Hrel in Hbh; symmetry in Hbh; exfalso; eapply s_n_not_n; apply Hbh);
clear Hbh.
all: match goal with
|- context[rb_delete_rebalance_right ?x ?l ?r' ?c ?b] =>
remember (rb_delete_rebalance_right x l r' c b) as p
end; cbn.
all: unfold rb_delete_rebalance_right in Heqp.
all: repeat match type of Heqp with
| ?p = match ?t with _ => _ end =>
let H := fresh "H" in destruct t eqn:H
end; cbn in *; subst; cbn [fst];
rb_infer_valid Hval; rb_infer_valid Hval'; prove_tree_valid.
Qed.
Lemma rb_delete_rebalance_right_rel x l r r' c b :
rb_tree_valid (node x l r c) ->
rb_tree_valid r' ->
rb_delete_rel r r' ->
rb_tree_bh r' = rb_tree_bh r <-> b = true ->
let p := rb_delete_rebalance_right x l r' c b in
rb_delete_rel (node x l r c) (fst p).
Proof. intros Hval Hval' Hrel Hbh.
pose proof (rb_delete_rebalance_right_valid x l r r' c b ltac:(auto) ltac:(auto) ltac:(auto) ltac:(auto)) as Hval''.
hnf in Hval''.
destruct c; rb_infer_valid Hval.
all: destruct Hrel as ([Hrel | Hrel] & Hred_root).
1,3: pose proof Hrel as Hb; rewrite Hbh in Hb; subst b; clear Hbh.
3,4: assert (Hb : b = false) by (destruct b; auto; destruct Hbh as (_ & Hbh); specialize (Hbh ltac:(auto)); rewrite <- Hrel in Hbh; symmetry in Hbh; exfalso; eapply s_n_not_n; apply Hbh);
clear Hbh.
all: match goal with
|- context[rb_delete_rebalance_right ?x ?l ?r' ?c ?b] =>
remember (rb_delete_rebalance_right x l r' c b) as p
end; cbn.
all: unfold rb_delete_rebalance_right in Heqp.
all: repeat match type of Heqp with
| ?p = match ?t with _ => _ end =>
let H := fresh "H" in destruct t eqn:H
end; cbn in *; subst; cbn [fst]; cbn [fst] in Hval''.
all: rb_infer_valid Hval; rb_infer_valid Hval'; rb_infer_valid Hval''.
all: match goal with H : red = red -> _ |- _ => specialize (H ltac:(auto) ltac:(congruence)) | _ => idtac end.
all: unfold rb_delete_rel; split; [|cbn; try congruence].
all: try (left; cbn; congruence).
all: try (right; cbn; congruence).
1,3: intros _ Heq; inversion Heq as [Heq']; symmetry in Heq'; exfalso; eapply s_n_not_n; apply Heq'.
assert (rb_tree_bh r' <> 0) by eauto with rbtree.
cbn in *; congruence.
Qed.
Lemma rb_delete_rebalance_right_bh x l r r' c b :
rb_tree_valid (node x l r c) ->
rb_tree_valid r' ->
rb_delete_rel r r' ->
rb_tree_bh r' = rb_tree_bh r <-> b = true ->
let p := rb_delete_rebalance_right x l r' c b in
rb_tree_bh (fst p) = rb_tree_bh (node x l r c) <-> (snd p) = true.
Proof. intros Hval Hval' Hrel Hbh.
pose proof (rb_delete_rebalance_right_valid x l r r' c b ltac:(auto) ltac:(auto) ltac:(auto) ltac:(auto)) as Hval''.
hnf in Hval''.
destruct c; rb_infer_valid Hval.
all: destruct Hrel as ([Hrel | Hrel] & Hred_root).
1,3: pose proof Hrel as Hb; rewrite Hbh in Hb; subst b; clear Hbh.
3,4: assert (Hb : b = false) by (destruct b; auto; destruct Hbh as (_ & Hbh); specialize (Hbh ltac:(auto)); rewrite <- Hrel in Hbh; symmetry in Hbh; exfalso; eapply s_n_not_n; apply Hbh);
clear Hbh.
all: match goal with
|- context[rb_delete_rebalance_right ?x ?l ?r' ?c ?b] =>
remember (rb_delete_rebalance_right x l r' c b) as p
end; cbn.
all: unfold rb_delete_rebalance_right in Heqp.
all: repeat match type of Heqp with
| ?p = match ?t with _ => _ end =>
let H := fresh "H" in destruct t eqn:H
end; cbn in *; subst; cbn [fst snd]; cbn [fst] in Hval''.
all: rb_infer_valid Hval; rb_infer_valid Hval'; rb_infer_valid Hval''.
all: match goal with H : red = red -> _ |- _ => specialize (H ltac:(auto) ltac:(congruence)) | _ => idtac end.
all: split; try reflexivity.
all: try (intros; congruence).
all: try (cbn; intros Heq; inversion Heq as [Heq']; symmetry in Heq'; exfalso; eapply s_n_not_n; apply Heq').
all: assert (rb_tree_bh r' <> 0) by eauto with rbtree.
all: cbn in *; congruence.
Qed.
Lemma rb_delete_rebalance_right_not_nil x l r r' c b :
rb_tree_valid (node x l r c) ->
rb_tree_valid r' ->
rb_delete_rel r r' ->
rb_tree_bh r' = rb_tree_bh r <-> b = true ->
let p := rb_delete_rebalance_right x l r' c b in
fst p <> nil.
Proof. intros Hval Hval' Hrel Hbh.
pose proof (rb_delete_rebalance_right_valid x l r r' c b ltac:(auto) ltac:(auto) ltac:(auto) ltac:(auto)) as Hval''.
hnf in Hval''.
destruct c; rb_infer_valid Hval.
all: destruct Hrel as ([Hrel | Hrel] & Hred_root).
1,3: pose proof Hrel as Hb; rewrite Hbh in Hb; subst b; clear Hbh.
3,4: assert (Hb : b = false) by (destruct b; auto; destruct Hbh as (_ & Hbh); specialize (Hbh ltac:(auto)); rewrite <- Hrel in Hbh; symmetry in Hbh; exfalso; eapply s_n_not_n; apply Hbh);
clear Hbh.
all: match goal with
|- context[rb_delete_rebalance_right ?x ?l ?r' ?c ?b] =>
remember (rb_delete_rebalance_right x l r' c b) as p
end; cbn.
all: unfold rb_delete_rebalance_right in Heqp.
all: repeat match type of Heqp with
| ?p = match ?t with _ => _ end =>
let H := fresh "H" in destruct t eqn:H
end; cbn in *; subst; cbn [fst snd]; cbn [fst] in Hval''.
all: rb_infer_valid Hval; rb_infer_valid Hval'; rb_infer_valid Hval''.
all: match goal with H : red = red -> _ |- _ => specialize (H ltac:(auto) ltac:(congruence)) | _ => idtac end.
all: try congruence.
all: assert (rb_tree_bh r' <> 0) by eauto with rbtree; cbn in *; congruence.
Qed.
Lemma rb_delete_rebalance_right_infix x l r r' c b :
rb_tree_valid (node x l r c) ->
rb_tree_valid r' ->
rb_delete_rel r r' ->
rb_tree_bh r' = rb_tree_bh r <-> b = true ->
let p := rb_delete_rebalance_right x l r' c b in
rb_tree_infix (fst p) = rb_tree_infix l ++ [x] ++ rb_tree_infix r'.
Proof. intros Hval Hval' Hrel Hbh.
pose proof (rb_delete_rebalance_right_not_nil x l r r' c b ltac:(auto) ltac:(auto) ltac:(auto) ltac:(auto)) as Hnot_nil.
hnf in Hnot_nil.
destruct c.
all: destruct Hrel as ([Hrel | Hrel] & Hred_root).
1,3: pose proof Hrel as Hb; rewrite Hbh in Hb; subst b; clear Hbh.
3,4: assert (Hb : b = false) by (destruct b; auto; destruct Hbh as (_ & Hbh); specialize (Hbh ltac:(auto)); rewrite <- Hrel in Hbh; symmetry in Hbh; exfalso; eapply s_n_not_n; apply Hbh);
clear Hbh.
all: match goal with
|- context[rb_delete_rebalance_right ?x ?l ?r' ?c ?b] =>
remember (rb_delete_rebalance_right x l r' c b) as p
end; cbn.
all: unfold rb_delete_rebalance_right in Heqp.
all: repeat match type of Heqp with
| ?p = match ?t with _ => _ end =>
let H := fresh "H" in destruct t eqn:H
end; subst p; cbn [fst snd]; cbn [fst] in Hnot_nil.
all: try contradiction.
all: cbn [rb_tree_infix]; repeat rewrite <- app_assoc; auto.
Qed.
Lemma rb_delete_rebalance_right_correct x l r r' c b :
rb_tree_valid (node x l r c) ->
rb_tree_valid r' ->
rb_delete_rel r r' ->
rb_tree_bh r' = rb_tree_bh r <-> b = true ->
let p := rb_delete_rebalance_right x l r' c b in
rb_tree_valid (fst p) /\
rb_delete_rel (node x l r c) (fst p) /\
rb_tree_infix (fst p) = rb_tree_infix l ++ [x] ++ rb_tree_infix r' /\
(rb_tree_bh (fst p) = rb_tree_bh (node x l r c) <-> snd p = true).
Proof. cbn zeta.
intros; split; [|split]; [| |split];
[ eapply rb_delete_rebalance_right_valid
| eapply rb_delete_rebalance_right_rel
| eapply rb_delete_rebalance_right_infix
| eapply rb_delete_rebalance_right_bh ];
eauto.
Qed.
(* The following function deletes the left-most element of a tree and returns that element.
It is a sub-procedure for general deletion.
*)
Fixpoint delete_leftmost (tree : rb_tree) : option (rb_tree * bool * val_t) :=
match tree with
| nil => None
| node x nil r c =>
Some (r, match c with black => false | red => true end, x)
| node x l r c =>
let ret := delete_leftmost l in
match ret with
| None => None
| Some (l', b, v) =>
let (tree', b') := rb_delete_rebalance_left x l' r c b in
Some (tree', b', v)
end
end.
Lemma delete_leftmost_correct (tree : rb_tree) :
rb_tree_valid tree ->
tree <> nil ->
match delete_leftmost tree with
| None => False
| Some (tree', b, v) =>
rb_tree_valid tree' /\
rb_delete_rel tree tree' /\
(rb_tree_bh tree' = rb_tree_bh tree <-> b = true) /\
rb_tree_infix tree = v :: rb_tree_infix tree'
end.
Proof. induction tree.
- contradiction.
- intros Hval _.
destruct tree1 as [| tx tl tr tc] eqn:Etree1.
+ cbn [delete_leftmost].
split; [|split]; [| |split]; eauto with rbtree.
destruct c; rb_infer_valid Hval.
* cbn; split; cbn in *; congruence.
* split; congruence.
+ destruct c; rb_infer_valid Hval; specialize (IHtree1 ltac:(auto) ltac:(discriminate)); clear IHtree2; rewrite <- Etree1 in *.
all: cbn [delete_leftmost]; fold (delete_leftmost tree1);
rewrite Etree1; rewrite <- Etree1;
destruct (delete_leftmost tree1) as [p|]; try contradiction;
destruct p as [p' v];
destruct p' as [tree' b];
destruct IHtree1 as (Htree1 & Htree2 & Htree3 & Htree4);
pose proof (rb_delete_rebalance_left_correct x tree1 tree' tree2 _ b Hval Htree1 Htree2 Htree3) as Hrebal;
destruct (rb_delete_rebalance_left x tree' tree2 _ b) as (tree'' & b');
hnf in Hrebal;
cbn [fst snd] in Hrebal;
destruct Hrebal as (Hrebal1 & Hrebal2 & Hrebal3 & Hrebal4);
split; [|split]; [| |split]; auto;
cbn [rb_tree_infix];
rewrite Htree4, Hrebal3;
cbn [app]; auto.
Qed.
(* Delete the root of a tree.
Since every node is the root of a subtree,
this function can be used to delete any node in a tree.
*)
Definition delete_root (tree : rb_tree) : (rb_tree * bool) :=
match tree with
| nil => (nil, true)
| node x l nil c =>
(l, match c with black => false | red => true end)
| node x l r c =>
match delete_leftmost r with
| None => (nil, true)
| Some (r', b, v) =>
rb_delete_rebalance_right v l r' c b
end
end.
Lemma delete_root_correct (tree : rb_tree) :
rb_tree_valid tree ->
match tree with nil => True | node x l r c =>
let (tree', b) := delete_root tree in
rb_tree_valid tree' /\
rb_delete_rel tree tree' /\
(rb_tree_bh tree' = rb_tree_bh tree <-> b = true) /\
rb_tree_infix tree' = rb_tree_infix l ++ rb_tree_infix r
end.
Proof. intros Hval.
destruct tree; auto.
cbn [delete_root].
destruct tree2 as [| tx tl tr tc] eqn:Etree2.
- do 3 (split; eauto with rbtree).
+ destruct c; cbn; split; try congruence.
intros Heq; symmetry in Heq; exfalso; eapply s_n_not_n; apply Heq.
+ cbn; symmetry; apply app_nil_r.
- rewrite <- Etree2 in *.
assert (Hval' : rb_tree_valid tree2) by eauto with rbtree.
pose proof (delete_leftmost_correct _ Hval' ltac:(subst; discriminate)) as Hdel.
destruct (delete_leftmost tree2) as [p|]; try contradiction.
destruct p as (p & v).
destruct p as (tree' & b).
destruct Hdel as (Hdel1 & Hdel2 & Hdel3 & Hdel4).
assert (rb_tree_valid (node v tree1 tree2 c)) by (destruct c; constructor; eauto with rbtree).
pose proof (rb_delete_rebalance_right_correct v tree1 tree2 tree' c b ltac:(auto) ltac:(auto) ltac:(auto) ltac:(auto)) as Hrebal.
destruct (rb_delete_rebalance_right v tree1 tree' c b) as (tree'' & b').
hnf in Hrebal.
cbn [fst snd] in Hrebal.
destruct Hrebal as (Hrebal1 & Hrebal2 & Hrebal3 & Hrebal4).
do 3 (split; auto).
rewrite Hrebal3, Hdel4.
cbn; auto.
Qed.
End MRBTree.
Raw
RBTSet.v
From Coq Require Import
List
Equalities
Orders
OrdersFacts
OrdersLists.
From RBTree Require Import
RBTree.
Import Notations ListNotations.
Section Lemmas.
Lemma sorted_app_l {T : Type} {R : relation T} {l1 l2 : list T} :
Sorted R (l1 ++ l2) -> Sorted R l1.
Proof. induction l1.
- auto.
- cbn.
intros Hsort.
inversion Hsort as [| ? ? Hsort1 Hsort2]; subst.
specialize (IHl1 ltac:(auto)).
constructor; auto.
destruct l1; auto.
inversion Hsort2 as [| ? ? Hsort3]; subst.
constructor; auto.
Qed.
Lemma sorted_app_r {T : Type} {R : relation T} {l1 l2 : list T} :
Sorted R (l1 ++ l2) -> Sorted R l2.
Proof. induction l1.
- cbn; auto.
- cbn; intros Hsort.
inversion Hsort; subst.
auto.
Qed.
Lemma sorted_app_trans {T : Type} {R : relation T} {R_trans : Transitive R} {l1 l2 : list T} :
Sorted R (l1 ++ l2) ->
forall x y, In x l1 -> In y l2 -> R x y.
Proof. intros Hsort.
induction l1.
- contradiction.
- cbn in Hsort; inversion Hsort as [| ? ? Hsort1 Hsort2]; subst.
specialize (IHl1 Hsort1).
intros x y Hx Hy.
destruct Hx as [Hx | Hx]; [subst | auto].
destruct l1.
+ cbn in *; destruct l2; try contradiction.
inversion Hsort2; subst.
pose proof (Sorted_extends R_trans Hsort1) as Hext.
rewrite Forall_forall in Hext.
destruct Hy; try subst; auto.
transitivity t; auto.
+ inversion Hsort2; subst.
specialize (IHl1 _ _ ltac:(left; auto) Hy).
transitivity t; auto.
Qed.
Lemma in_reorder {T : Type} (x : T) a b c d :
In x (a :: b ++ c ++ d) <-> In x ((a :: d) ++ c ++ b).
Proof. split; intros Hin.
- destruct Hin as [Hin | Hin].
1: subst x; apply in_or_app; left; left; auto.
apply in_app_or in Hin; destruct Hin as [? | Hin].
1: do 2 (apply in_or_app; right); auto.
apply in_app_or in Hin; destruct Hin as [Hin | Hin].
1: apply in_or_app; right; apply in_or_app; left; auto.
apply in_or_app; left; right; auto.
- apply in_app_or in Hin.
destruct Hin as [[Hin | Hin] | Hin].
1: left; auto.
1: right; do 2 (apply in_or_app; right); auto.
right; rewrite app_assoc.
apply in_or_app; left.
apply in_app_or in Hin; apply in_or_app; destruct Hin; auto.
Qed.
Lemma NoDupA_eq_eq {T : Type} {eqA} {equiv : Equivalence eqA} (l : list T) x y :
NoDupA eqA l ->
In x l -> In y l -> eqA x y -> x = y.
Proof. intros Hnodup.
induction Hnodup.
- contradiction.
- intros Hx Hy.
destruct Hx as [Hx | Hx]; destruct Hy as [Hy | Hy].
1: subst; auto.
3: apply IHHnodup; auto.
all: subst; intros Heq.
+ rewrite Heq in H.
rewrite InA_altdef in H.
rewrite Exists_exists in H.
exfalso; apply H; exists y; split; auto.
apply equiv.
+ rewrite <- Heq in H.
rewrite InA_altdef in H.
rewrite Exists_exists in H.
exfalso; apply H; exists x; split; auto.
apply equiv.
Qed.
End Lemmas.
Module MRBTSet (T : OrderedType).
Module Import MRBTree := MRBTree T.
Inductive rb_tree_sorted : rb_tree -> Prop :=
| rb_tree_sorted_nil : rb_tree_sorted nil
| rb_tree_sorted_node : forall x l r c,
rb_tree_sorted l ->
rb_tree_sorted r ->
Forall (fun y => T.lt y x) (rb_tree_infix l) ->
Forall (fun y => T.lt x y) (rb_tree_infix r) ->
rb_tree_sorted (node x l r c).
#[export] Hint Resolve rb_tree_sorted_nil : rbtree.
Lemma rb_tree_sorted_infix_sorted (tree : rb_tree) :
rb_tree_sorted tree ->
sort T.lt (rb_tree_infix tree).
Proof. intros Hsort.
induction Hsort as [| x l r c Hsorted1 IH1 Hsorted2 IH2 Hlt1 Hlt2].
- cbn; auto.
- cbn.
apply (SortA_app T.eq_equiv); auto.
+ apply Sorted_cons; auto.
destruct (rb_tree_infix r); constructor.
inversion Hlt2; subst; auto.
+ intros xl xr Hin1 Hin2.
inversion Hin2 as [? ? Heq | ? ? Hin3]; subst.
* rewrite InA_altdef in Hin1.
rewrite Exists_exists in Hin1.
destruct Hin1 as (xl' & Hxl1 & Hxl2).
rewrite Forall_forall in Hlt1.
specialize (Hlt1 _ Hxl1).
rewrite Heq, Hxl2.
auto.
* rewrite InA_altdef in Hin1, Hin3.
rewrite Exists_exists in Hin1, Hin3.
destruct Hin1 as (xl' & Hxl1 & Hxl2).
destruct Hin3 as (xr' & Hxr1 & Hxr2).
rewrite Forall_forall in Hlt1, Hlt2.
specialize (Hlt1 _ Hxl1).
specialize (Hlt2 _ Hxr1).
rewrite Hxl2, Hxr2.
transitivity x; auto.
Qed.
Lemma infix_sorted_rb_tree_sorted (tree : rb_tree) :
sort T.lt (rb_tree_infix tree) ->
rb_tree_sorted tree.
Proof. induction tree.
- cbn; eauto with rbtree.
- cbn [rb_tree_infix].
intros Hsort.
pose proof (sorted_app_l Hsort) as Hsort1.
pose proof (sorted_app_r Hsort) as Hsort2.
pose proof (sorted_app_trans Hsort) as Hsort3.
pose proof (sorted_app_l Hsort2) as Hsort4.
pose proof (sorted_app_r Hsort2) as Hsort5.
pose proof (sorted_app_trans Hsort2) as Hsort6.
constructor.
+ apply IHtree1; auto.
+ apply IHtree2; auto.
+ rewrite Forall_forall.
intros xl Hxl.
apply (Hsort3 xl x Hxl ltac:(apply in_or_app; left; left; auto)).
+ rewrite Forall_forall.
intros xr Hxr.
apply (Hsort6 _ _ ltac:(left; auto) Hxr).
Qed.
Lemma rb_tree_sorted_eq_infix_sorted (tree : rb_tree) :
sort T.lt (rb_tree_infix tree) <-> rb_tree_sorted tree.
Proof. split.
- apply infix_sorted_rb_tree_sorted.
- apply rb_tree_sorted_infix_sorted.
Qed.
Fixpoint rb_tree_sorted_insert (z : val_t) (tree : rb_tree) : (rb_tree * bool * bool) :=
match tree with
| nil => (node z nil nil red, true, true)
| node x l r c =>
match T.compare z x with
| Eq => (node x l r c, true, false)
| Lt =>
let (p, inserted) := rb_tree_sorted_insert z l in
let (l', b) := p in
if inserted then (rb_insert_rebalance_left x l' r c b, true) else (tree, true, false)
| Gt =>
let (p, inserted) := rb_tree_sorted_insert z r in
let (r', b) := p in
if inserted then (rb_insert_rebalance_right x l r' c b, true) else (tree, true, false)
end
end.
Lemma rb_tree_sorted_insert_correct z tree :
rb_tree_valid tree ->
rb_tree_sorted tree ->
let (p, inserted) := rb_tree_sorted_insert z tree in
let (tree', b) := p in
(* Case 1: not inserted *)
InA T.eq z (rb_tree_infix tree) /\
tree' = tree /\
inserted = false \/
(* Case 2: inserted *)
~ InA T.eq z (rb_tree_infix tree) /\
rb_tree_valid tree' /\
rb_insert_rel tree tree' /\
rb_tree_sorted tree' /\
incl (z :: rb_tree_infix tree) (rb_tree_infix tree') /\
incl (rb_tree_infix tree') (z :: rb_tree_infix tree) /\
inserted = true /\
(rb_tree_bh tree' = rb_tree_bh tree <-> b = true).
Proof. induction tree.
- cbn; intros _ _; right.
repeat split; auto.
+ intros H; inversion H.
+ constructor; eauto with rbtree.
+ eauto with rbtree.
+ constructor; eauto with rbtree.
all: cbn; constructor.
+ apply incl_refl.
+ apply incl_refl.
- cbn [rb_tree_sorted_insert rb_tree_infix].
pose proof (T.compare_spec z x) as H; inversion H as [Heq | Hlt | Hgt].
+ intros Hval Hsort.
left.
repeat split; auto.
rewrite InA_app_iff; right; left; auto.
+ clear IHtree2.
intros Hval Hsort.
assert (Hval' : rb_tree_valid tree1) by eauto with rbtree.
pose proof Hsort as Hsort'; inversion Hsort' as [| ? ? ? ? Hsort1 Hsort2 Hsort3 Hsort4]; subst.
specialize (IHtree1 ltac:(auto) ltac:(auto)).
destruct (rb_tree_sorted_insert z tree1) as (p & inserted); destruct p as (l' & b).
destruct IHtree1 as [(Hins1 & Hins2 & Hins3) | (Hins1 & Hins2 & Hins3 & Hins4 & Hins5 & Hins6 & Hins7 & Hins8)].
* rewrite Hins3; left; repeat split.
rewrite InA_app_iff; left; auto.
* rewrite Hins7.
pose proof (rb_insert_rebalance_left_correct x tree1 l' tree2 c b ltac:(auto) ltac:(auto) ltac:(auto) ltac:(auto)) as Hrebal.
destruct (rb_insert_rebalance_left x l' tree2 c b) as (tree' & b').
hnf in Hrebal.
cbn [fst snd] in Hrebal.
destruct Hrebal as (Hrebal1 & Hrebal2 & Hrebal3 & Hrebal4).
right; repeat split; auto.
-- intros Hin.
do 2 rewrite InA_app_iff in Hin.
destruct Hin as [Hin | [Hin | Hin]]; auto.
++ inversion Hin as [? ? Hin' | ? ? Hin']; subst.
** rewrite Hin' in Hlt.
eapply StrictOrder_Irreflexive.
apply Hlt.
** inversion Hin'.
++ rewrite InA_altdef in Hin.
rewrite Exists_exists in Hin.
destruct Hin as (z' & Hz1 & Hz2).
rewrite Forall_forall in Hsort4.
specialize (Hsort4 _ Hz1).
rewrite <- Hz2 in Hsort4.
eapply (StrictOrder_Asymmetric T.lt_strorder).
1: apply Hsort4.
auto.
-- rewrite <- rb_tree_sorted_eq_infix_sorted.
rewrite Hrebal3.
apply (SortA_app T.eq_equiv).
2: apply (SortA_app T.eq_equiv).
++ rewrite rb_tree_sorted_eq_infix_sorted; auto.
++ constructor; constructor.
++ rewrite rb_tree_sorted_eq_infix_sorted; auto.
++ intros x' y Hin1 Hin2.
inversion Hin1 as [? ? Heq | ? ? Hin3]; subst.
2: inversion Hin3.
rewrite Heq.
rewrite InA_altdef in Hin2.
rewrite Exists_exists in Hin2.
destruct Hin2 as (y' & Hy1 & Hy2).
rewrite Forall_forall in Hsort4.
specialize (Hsort4 _ Hy1).
rewrite <- Hy2 in Hsort4.
auto.
++ intros xl y Hin1 Hin2.
rewrite InA_altdef in Hin1, Hin2.
rewrite Exists_exists in Hin1, Hin2.
destruct Hin1 as (xl' & Hxl1 & Hxl2).
destruct Hin2 as (y' & Hy1 & Hy2).
apply in_app_or in Hy1.
destruct Hy1 as [Hy1 | Hy1].
** destruct Hy1; try contradiction; subst y'.
rewrite Forall_forall in Hsort3.
apply Hins6 in Hxl1.
destruct Hxl1 as [Hxl1 | Hxl1].
--- subst xl'; rewrite Hxl2, Hy2; auto.
--- specialize (Hsort3 _ Hxl1).
rewrite Hy2, Hxl2.
auto.
** apply Hins6 in Hxl1.
rewrite Forall_forall in Hsort4.
destruct Hxl1 as [Hxl1 | Hxl1].
--- subst xl'.
specialize (Hsort4 _ Hy1).
rewrite Hxl2, Hy2.
transitivity x; auto.
--- rewrite Forall_forall in Hsort3.
specialize (Hsort3 _ Hxl1).
specialize (Hsort4 _ Hy1).
rewrite Hxl2, Hy2.
transitivity x; auto.
-- intros y Hin.
rewrite Hrebal3.
match type of Hin with context[?a :: ?b ++ ?c] => change (a :: b ++ c) with ((a :: b) ++ c) in Hin end.
apply in_app_or in Hin.
destruct Hin as [Hin | Hin].
1: apply Hins5 in Hin; apply in_or_app; left; auto.
apply in_or_app; right; auto.
-- rewrite Hrebal3.
intros y Hin.
apply in_app_or in Hin.
match goal with |- context[?a :: ?b ++ ?c] => change (a :: b ++ c) with ((a :: b) ++ c) end.
destruct Hin as [Hin | Hin].
++ apply in_or_app; left; auto.
++ apply in_or_app; right; auto.
-- apply Hrebal4.
-- apply Hrebal4.
+ clear IHtree1.
intros Hval Hsort.
assert (Hval' : rb_tree_valid tree2) by eauto with rbtree.
pose proof Hsort as Hsort'; inversion Hsort' as [| ? ? ? ? Hsort1 Hsort2 Hsort3 Hsort4]; subst.
specialize (IHtree2 ltac:(auto) ltac:(auto)).
destruct (rb_tree_sorted_insert z tree2) as (p & inserted); destruct p as (r' & b).
destruct IHtree2 as [(Hins1 & Hins2 & Hins3) | (Hins1 & Hins2 & Hins3 & Hins4 & Hins5 & Hins6 & Hins7 & Hins8)].
* rewrite Hins3; left; repeat split.
rewrite InA_app_iff; right; right; auto.
* rewrite Hins7.
pose proof (rb_insert_rebalance_right_correct x tree1 tree2 r' c b ltac:(auto) ltac:(auto) ltac:(auto) ltac:(auto)) as Hrebal.
destruct (rb_insert_rebalance_right x tree1 r' c b) as (tree' & b').
hnf in Hrebal.
cbn [fst snd] in Hrebal.
destruct Hrebal as (Hrebal1 & Hrebal2 & Hrebal3 & Hrebal4).
right; repeat split; auto.
-- intros Hin.
do 2 rewrite InA_app_iff in Hin.
destruct Hin as [Hin | [Hin | Hin]]; auto.
++ rewrite InA_altdef in Hin.
rewrite Exists_exists in Hin.
destruct Hin as (z' & Hz1 & Hz2).
rewrite Forall_forall in Hsort3.
specialize (Hsort3 _ Hz1).
rewrite <- Hz2 in Hsort3.
eapply (StrictOrder_Asymmetric T.lt_strorder).
1: apply Hsort3.
auto.
++ inversion Hin as [? ? Hin' | ? ? Hin']; subst.
** rewrite Hin' in Hgt.
eapply StrictOrder_Irreflexive.
apply Hgt.
** inversion Hin'.
-- rewrite <- rb_tree_sorted_eq_infix_sorted.
rewrite Hrebal3.
apply (SortA_app T.eq_equiv).
2: apply (SortA_app T.eq_equiv).
++ rewrite rb_tree_sorted_eq_infix_sorted; auto.
++ constructor; constructor.
++ rewrite rb_tree_sorted_eq_infix_sorted; auto.
++ intros x' y Hin1 Hin2.
inversion Hin1 as [? ? Heq | ? ? Hin3]; subst.
2: inversion Hin3.
rewrite Heq.
rewrite InA_altdef in Hin2.
rewrite Exists_exists in Hin2.
destruct Hin2 as (y' & Hy1 & Hy2).
rewrite Forall_forall in Hsort4.
apply Hins6 in Hy1.
destruct Hy1 as [Hy1 | Hy1].
** subst y'.
rewrite Hy2; auto.
** specialize (Hsort4 _ Hy1).
rewrite Hy2; auto.
++ intros xl y Hin1 Hin2.
rewrite InA_altdef in Hin1, Hin2.
rewrite Exists_exists in Hin1, Hin2.
destruct Hin1 as (xl' & Hxl1 & Hxl2).
destruct Hin2 as (y' & Hy1 & Hy2).
apply in_app_or in Hy1.
destruct Hy1 as [Hy1 | Hy1].
** destruct Hy1; try contradiction; subst y'.
rewrite Forall_forall in Hsort3.
specialize (Hsort3 _ Hxl1).
rewrite Hy2, Hxl2.
auto.
** rewrite Forall_forall in Hsort3.
apply Hins6 in Hy1.
destruct Hy1 as [Hy1 | Hy1].
--- subst y'.
specialize (Hsort3 _ Hxl1).
rewrite Hxl2, Hy2.
transitivity x; auto.
--- rewrite Forall_forall in Hsort4.
specialize (Hsort4 _ Hy1).
specialize (Hsort3 _ Hxl1).
rewrite Hxl2, Hy2.
transitivity x; auto.
-- intros y Hin.
rewrite Hrebal3.
rewrite in_reorder in Hin.
apply in_app_or in Hin.
destruct Hin as [Hin | Hin].
1: apply Hins5 in Hin; do 2 (apply in_or_app; right); auto.
rewrite app_assoc.
apply in_or_app; left.
apply in_app_or in Hin; apply in_or_app; destruct Hin; auto.
-- rewrite Hrebal3.
intros y Hin.
rewrite in_reorder.
apply in_app_or in Hin.
destruct Hin as [Hin | Hin].
1: do 2 (apply in_or_app; right); auto.
apply in_app_or in Hin.
destruct Hin as [Hin | Hin].
1: apply in_or_app; right; apply in_or_app; left; auto.
apply Hins6 in Hin.
apply in_or_app; left; auto.
-- apply Hrebal4.
-- apply Hrebal4.
Qed.
Fixpoint rb_tree_sorted_delete (z : val_t) (tree : rb_tree) : (rb_tree * bool * bool) :=
match tree with
| nil => (nil, true, false)
| node x l r c =>
match T.compare z x with
| Eq => (delete_root tree, true)
| Lt =>
let (p, deleted) := rb_tree_sorted_delete z l in
let (l', b) := p in
if deleted then (rb_delete_rebalance_left x l' r c b, true) else (tree, true, false)
| Gt =>
let (p, deleted) := rb_tree_sorted_delete z r in
let (r', b) := p in
if deleted then (rb_delete_rebalance_right x l r' c b, true) else (tree, true, false)
end
end.
Lemma rb_tree_sorted_delete_correct z tree :
rb_tree_valid tree ->
rb_tree_sorted tree ->
let (p, deleted) := rb_tree_sorted_delete z tree in
let (tree', b) := p in
(* Case 1: not deleted *)
~ InA T.eq z (rb_tree_infix tree) /\
tree' = tree /\
deleted = false \/
(* Case 2: deleted *)
rb_tree_valid tree' /\
rb_delete_rel tree tree' /\
rb_tree_sorted tree' /\
~ InA T.eq z (rb_tree_infix tree') /\
(exists z',
T.eq z z' /\
incl (rb_tree_infix tree) (z' :: rb_tree_infix tree') /\
incl (z' :: rb_tree_infix tree') (rb_tree_infix tree)) /\
deleted = true /\
(rb_tree_bh tree' = rb_tree_bh tree <-> b = true).
Proof. induction tree.
- intros _ _.
cbn.
left; repeat split; auto.
intros H; inversion H.
- intros Hval Hsort.
cbn [rb_tree_sorted_delete rb_tree_infix].
pose proof Hsort as Hsort'; inversion Hsort' as [| ? ? ? ? Hsort1 Hsort2 Hsort3 Hsort4]; subst.
pose proof (T.compare_spec z x) as H; inversion H as [Heq | Hlt | Hgt].
+ pose proof (delete_root_correct _ Hval) as Hdel.
cbn iota in Hdel.
destruct (delete_root (node x tree1 tree2 c)) as (tree' & b).
destruct Hdel as (Hdel1 & Hdel2 & Hdel3 & Hdel4).
right; repeat split; auto; try apply Hdel2.
3: exists x; repeat split; auto.
* rewrite <- rb_tree_sorted_eq_infix_sorted.
rewrite Hdel4.
apply (SortA_app T.eq_equiv).
1,2: rewrite rb_tree_sorted_eq_infix_sorted; auto.
intros xl xr Hin1 Hin2.
rewrite Forall_forall in Hsort3, Hsort4.
rewrite InA_altdef in Hin1, Hin2.
rewrite Exists_exists in Hin1, Hin2.
destruct Hin1 as (xl' & Hxl1 & Hxl2).
destruct Hin2 as (xr' & Hxr1 & Hxr2).
rewrite Hxl2, Hxr2.
transitivity x; auto.
* rewrite Hdel4.
intros Hin.
rewrite InA_altdef in Hin.
rewrite Exists_exists in Hin.
destruct Hin as (y & Hy1 & Hy2).
apply in_app_or in Hy1.
rewrite Forall_forall in Hsort3, Hsort4.
destruct Hy1 as [Hy1 | Hy1].
-- specialize (Hsort3 _ Hy1) as Hy3.
rewrite <- Hy2, <- Heq in Hy3.
eapply (StrictOrder_Irreflexive z); auto.
-- specialize (Hsort4 _ Hy1) as Hy3.
rewrite <- Hy2, <- Heq in Hy3.
eapply (StrictOrder_Irreflexive z); auto.
* rewrite Hdel4.
intros y Hy.
apply in_app_or in Hy; destruct Hy as [Hy | Hy].
2: apply in_app_or in Hy; destruct Hy as [Hy | Hy].
2: destruct Hy; try contradiction; subst; left; auto.
all: right; apply in_or_app; auto.
* rewrite Hdel4.
intros y Hy.
destruct Hy as [Hy | Hy].
1: subst y; apply in_or_app; right; apply in_or_app; left; left; auto.
apply in_app_or in Hy; destruct Hy.
1: apply in_or_app; left; auto.
do 2 (apply in_or_app; right); auto.
* apply Hdel3.
* apply Hdel3.
+ clear IHtree2.
specialize (IHtree1 ltac:(eauto with rbtree) ltac:(auto)).
rewrite Forall_forall in Hsort3, Hsort4.
destruct (rb_tree_sorted_delete z tree1) as (p & deleted).
destruct p as (tree' & b).
destruct IHtree1 as [(Hdel1 & Hdel2 & Hdel3) | (Hdel1 & Hdel2 & Hdel3 & Hdel4 & Hdel5 & Hdel6 & Hdel7)].
* rewrite Hdel3; left; repeat split; auto.
intros Hin.
apply InA_app in Hin.
destruct Hin as [Hin | Hin]; [contradiction|].
apply InA_app in Hin.
destruct Hin as [Hin | Hin].
1: inversion Hin as [? ? Heq | ? ? Hin']; [subst | inversion Hin'].
1: rewrite Heq in Hlt; eapply (StrictOrder_Irreflexive x); auto.
rewrite InA_altdef in Hin.
rewrite Exists_exists in Hin.
destruct Hin as (y & Hy1 & Hy2).
specialize (Hsort4 _ Hy1).
rewrite Hy2 in Hlt.
eapply (StrictOrder_Asymmetric T.lt_strorder); try apply Hlt; auto.
* rewrite Hdel6.
destruct Hdel5 as (z' & Hz1 & Hz2 & Hz3).
pose proof (rb_delete_rebalance_left_correct x tree1 tree' tree2 c b ltac:(auto) ltac:(auto) ltac:(auto) ltac:(auto)) as Hrebal.
destruct (rb_delete_rebalance_left x tree' tree2 c b) as (l' & b').
hnf in Hrebal.
cbn [fst snd] in Hrebal.
destruct Hrebal as (Hrebal1 & Hrebal2 & Hrebal3 & Hrebal4).
right; repeat split; auto; try apply Hrebal2.
3: exists z'; repeat split; auto.
-- rewrite <- rb_tree_sorted_eq_infix_sorted.
rewrite Hrebal3.
apply (SortA_app T.eq_equiv).
2: apply (SortA_app T.eq_equiv).
1,3: rewrite rb_tree_sorted_eq_infix_sorted; auto.
1: constructor; constructor.
++ intros x' y Hin1 Hin2.
inversion Hin1 as [? ? Hin1' | ? ? Hin1']; [subst | inversion Hin1'].
rewrite InA_altdef in Hin2.
rewrite Exists_exists in Hin2.
destruct Hin2 as (xr & Hxr1 & Hxr2).
specialize (Hsort4 _ Hxr1).
rewrite Hin1', Hxr2.
auto.
++ intros xl y Hin1 Hin2.
rewrite InA_altdef in Hin1.
rewrite Exists_exists in Hin1.
destruct Hin1 as (xl' & Hxl1 & Hxl2).
specialize (Hz3 _ ltac:(right; apply Hxl1)) as Hxl3.
specialize (Hsort3 _ Hxl3).
apply InA_app in Hin2.
destruct Hin2 as [Hin2 | Hin2].
1: inversion Hin2 as [? ? Hin2' | ? ? Hin2']; [subst | inversion Hin2'].
1: rewrite Hxl2, Hin2'; auto.
rewrite InA_altdef in Hin2.
rewrite Exists_exists in Hin2.
destruct Hin2 as (xr & Hxr1 & Hxr2).
specialize (Hsort4 _ Hxr1).
rewrite Hxl2, Hxr2.
transitivity x; auto.
-- rewrite Hrebal3.
intros Hin.
apply InA_app in Hin.
destruct Hin as [Hin | Hin].
1: contradiction.
apply InA_app in Hin.
destruct Hin as [Hin | Hin].
1: inversion Hin as [? ? Hin' | ? ? Hin']; [subst | inversion Hin']; rewrite Hin' in Hlt; eapply (StrictOrder_Irreflexive x); auto.
rewrite InA_altdef in Hin.
rewrite Exists_exists in Hin.
destruct Hin as (xr & Hxr1 & Hxr2).
specialize (Hsort4 _ Hxr1) as Hxr3.
rewrite <- Hxr2 in Hxr3.
eapply (StrictOrder_Asymmetric T.lt_strorder); try apply Hlt; auto.
-- rewrite Hrebal3.
intros y Hin.
match goal with |- context[?a :: ?b ++ ?c] => change (a :: b ++ c) with ((a :: b) ++ c) end.
apply in_app_or in Hin.
destruct Hin as [Hin | Hin].
1: apply Hz2 in Hin; apply in_or_app; left; auto.
apply in_or_app; right; auto.
-- rewrite Hrebal3.
intros y Hin.
match type of Hin with context[?a :: ?b ++ ?c] => change (a :: b ++ c) with ((a :: b) ++ c) in Hin end.
apply in_app_or in Hin.
destruct Hin as [Hin | Hin].
1: apply Hz3 in Hin; apply in_or_app; left; auto.
apply in_or_app; right; auto.
-- apply Hrebal4.
-- apply Hrebal4.
+ clear IHtree1.
specialize (IHtree2 ltac:(eauto with rbtree) ltac:(auto)).
rewrite Forall_forall in Hsort3, Hsort4.
destruct (rb_tree_sorted_delete z tree2) as (p & deleted).
destruct p as (tree' & b).
destruct IHtree2 as [(Hdel1 & Hdel2 & Hdel3) | (Hdel1 & Hdel2 & Hdel3 & Hdel4 & Hdel5 & Hdel6 & Hdel7)].
* rewrite Hdel3; left; repeat split; auto.
intros Hin.
apply InA_app in Hin.
destruct Hin as [Hin | Hin].
2: apply InA_app in Hin; destruct Hin as [Hin | Hin].
3: contradiction.
2: inversion Hin as [? ? Heq | ? ? Hin']; [subst | inversion Hin'].
2: rewrite Heq in Hgt; eapply (StrictOrder_Irreflexive x); auto.
rewrite InA_altdef in Hin.
rewrite Exists_exists in Hin.
destruct Hin as (y & Hy1 & Hy2).
specialize (Hsort3 _ Hy1).
rewrite Hy2 in Hgt.
eapply (StrictOrder_Asymmetric T.lt_strorder); try apply Hgt; auto.
* rewrite Hdel6.
destruct Hdel5 as (z' & Hz1 & Hz2 & Hz3).
pose proof (rb_delete_rebalance_right_correct x tree1 tree2 tree' c b ltac:(auto) ltac:(auto) ltac:(auto) ltac:(auto)) as Hrebal.
destruct (rb_delete_rebalance_right x tree1 tree' c b) as (l' & b').
hnf in Hrebal.
cbn [fst snd] in Hrebal.
destruct Hrebal as (Hrebal1 & Hrebal2 & Hrebal3 & Hrebal4).
right; repeat split; auto; try apply Hrebal2.
3: exists z'; repeat split; auto.
-- rewrite <- rb_tree_sorted_eq_infix_sorted.
rewrite Hrebal3.
apply (SortA_app T.eq_equiv).
2: apply (SortA_app T.eq_equiv).
1,3: rewrite rb_tree_sorted_eq_infix_sorted; auto.
1: constructor; constructor.
++ intros x' y Hin1 Hin2.
inversion Hin1 as [? ? Hin1' | ? ? Hin1']; [subst | inversion Hin1'].
rewrite InA_altdef in Hin2.
rewrite Exists_exists in Hin2.
destruct Hin2 as (xr & Hxr1 & Hxr2).
specialize (Hz3 _ ltac:(right; apply Hxr1)) as Hxr3.
specialize (Hsort4 _ Hxr3).
rewrite Hin1', Hxr2.
auto.
++ intros xl y Hin1 Hin2.
rewrite InA_altdef in Hin1.
rewrite Exists_exists in Hin1.
destruct Hin1 as (xl' & Hxl1 & Hxl2).
specialize (Hsort3 _ Hxl1).
apply InA_app in Hin2.
destruct Hin2 as [Hin2 | Hin2].
1: inversion Hin2 as [? ? Hin2' | ? ? Hin2']; [subst | inversion Hin2'].
1: rewrite Hxl2, Hin2'; auto.
rewrite InA_altdef in Hin2.
rewrite Exists_exists in Hin2.
destruct Hin2 as (xr & Hxr1 & Hxr2).
specialize (Hz3 _ ltac:(right; apply Hxr1)) as Hxr3.
specialize (Hsort4 _ Hxr3).
rewrite Hxl2, Hxr2.
transitivity x; auto.
-- rewrite Hrebal3.
intros Hin.
apply InA_app in Hin.
destruct Hin as [Hin | Hin].
2: apply InA_app in Hin; destruct Hin as [Hin | Hin].
3: contradiction.
2: inversion Hin as [? ? Hin' | ? ? Hin']; [subst | inversion Hin']; rewrite Hin' in Hgt; eapply (StrictOrder_Irreflexive x); auto.
rewrite InA_altdef in Hin.
rewrite Exists_exists in Hin.
destruct Hin as (xl & Hxl1 & Hxl2).
specialize (Hsort3 _ Hxl1) as Hxl3.
rewrite <- Hxl2 in Hxl3.
eapply (StrictOrder_Asymmetric T.lt_strorder); try apply Hgt; auto.
-- rewrite Hrebal3.
intros y Hin.
rewrite in_reorder.
apply in_app_or in Hin.
destruct Hin as [Hin | Hin].
1: do 2 (apply in_or_app; right); auto.
apply in_app_or in Hin.
destruct Hin as [Hin | Hin].
1: apply in_or_app; right; apply in_or_app; left; auto.
apply Hz2 in Hin; apply in_or_app; left; auto.
-- rewrite Hrebal3.
intros y Hin.
rewrite in_reorder in Hin.
apply in_app_or in Hin.
destruct Hin as [Hin | Hin].
1: apply Hz3 in Hin; do 2 (apply in_or_app; right); auto.
apply in_app_or in Hin.
destruct Hin as [Hin | Hin].
1: apply in_or_app; right; apply in_or_app; left; auto.
apply in_or_app; left; auto.
-- apply Hrebal4.
-- apply Hrebal4.
Qed.
Fixpoint rb_tree_sorted_lookup (z : val_t) (tree : rb_tree) : option val_t :=
match tree with
| nil => None
| node x l r c =>
match T.compare z x with
| Eq => Some x
| Lt => rb_tree_sorted_lookup z l
| Gt => rb_tree_sorted_lookup z r
end
end.
Lemma rb_tree_sorted_lookup_correct_some z x tree :
rb_tree_sorted_lookup z tree = Some x ->
In x (rb_tree_infix tree) /\ T.eq z x.
Proof. induction tree.
- cbn; discriminate.
- cbn.
pose proof (T.compare_spec z x0) as H; inversion H as [Heq | Hlt | Hgt].
+ intros Heq'; inversion Heq'; subst.
split; auto.
apply in_or_app; right; left; auto.
+ intros; specialize (IHtree1 ltac:(auto)); destruct IHtree1; split; auto.
apply in_or_app; left; auto.
+ intros; specialize (IHtree2 ltac:(auto)); destruct IHtree2; split; auto.
apply in_or_app; right; right; auto.
Qed.
Lemma rb_tree_sorted_lookup_correct_none z tree :
rb_tree_sorted tree ->
rb_tree_sorted_lookup z tree = None ->
~ InA T.eq z (rb_tree_infix tree).
Proof. intros Hsort.
induction Hsort as [| ? ? ? ? Hsort1 Hsort2 Hsort3 Hsort4 Hsort5 Hsort6].
- cbn; intros _ Hin; inversion Hin.
- cbn.
rewrite Forall_forall in Hsort5, Hsort6.
pose proof (T.compare_spec z x) as Hcmp; inversion Hcmp as [Heq | Hlt | Hgt].
+ discriminate.
+ intros Hnone; specialize (Hsort2 Hnone).
intros Hin.
apply InA_app in Hin.
destruct Hin as [Hin | Hin].
1: contradiction.
inversion Hin as [? ? Hin' | ? ? Hin']; subst.
* rewrite Hin' in Hlt.
eapply (StrictOrder_Irreflexive x); auto.
* rewrite InA_altdef in Hin'.
rewrite Exists_exists in Hin'.
destruct Hin' as (xr & Hxr1 & Hxr2).
specialize (Hsort6 _ Hxr1).
rewrite Hxr2 in Hlt.
eapply (StrictOrder_Asymmetric T.lt_strorder); try apply Hlt; auto.
+ intros Hnone; specialize (Hsort4 Hnone).
intros Hin.
apply InA_app in Hin.
destruct Hin as [Hin | Hin].
2: inversion Hin as [? ? Hin' | ? ? Hin']; subst.
3: contradiction.
* rewrite InA_altdef in Hin.
rewrite Exists_exists in Hin.
destruct Hin as (xl & Hxl1 & Hxl2).
specialize (Hsort5 _ Hxl1).
rewrite Hxl2 in Hgt.
eapply (StrictOrder_Asymmetric T.lt_strorder); try apply Hgt; auto.
* rewrite Hin' in Hgt.
eapply (StrictOrder_Irreflexive x); auto.
Qed.
Module Import OrderedTypeLists := OrderedTypeLists T.
Lemma rb_tree_sorted_infix_nodup (tree : rb_tree) :
rb_tree_sorted tree ->
NoDupA T.eq (rb_tree_infix tree).
Proof. intros Hsort.
rewrite <- rb_tree_sorted_eq_infix_sorted in Hsort.
apply Sort_NoDup; auto.
Qed.
Lemma rb_tree_sorted_lookup_correct_inv z x tree :
rb_tree_sorted tree ->
In x (rb_tree_infix tree) ->
T.eq z x ->
rb_tree_sorted_lookup z tree = Some x.
Proof. intros Hsort Hin Heq.
pose proof (rb_tree_sorted_infix_nodup _ Hsort) as Hnodup.
destruct (rb_tree_sorted_lookup z tree) eqn:Elookup.
- pose proof (rb_tree_sorted_lookup_correct_some _ _ _ Elookup) as (Hin' & Heq').
rewrite Heq in Heq'.
pose proof (NoDupA_eq_eq _ _ _ Hnodup Hin Hin' Heq').
subst; auto.
- pose proof (rb_tree_sorted_lookup_correct_none _ _ Hsort Elookup) as Hnone.
exfalso; apply Hnone.
rewrite InA_altdef.
rewrite Exists_exists.
exists x; split; auto.
Qed.
End MRBTSet.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment