Hey @SpiceGuid, I was hoping to post sooner once I had proven all the theorems you listed, but have been caught up with research so haven’t had the chance to work on this recently.
Seeing as you’re close to finishing the book, lest my work be for naught, I thought I might as well share what I have had the chance to do so far (see below):
I’ve proven the key properties for interval, union, filter and intersection. A couple of the theorems were too weak in their assumptions (in particular they made no assumptions about the ordering of the tree), so I had to strengthen them.
If I have some free time in the following weeks, I think I’ll try finishing the remaining properties (for disjoint, difference and remove).
(* un arbre est soit vide soit une séparation en deux *)
Inductive tree : Set :=
| Empty: tree
| Fork: tree -> nat -> tree -> tree.
Require Import Arith.Arith_base.
(* nombre de strahler *)
Fixpoint strahler t :=
match t with
| Empty => 0
| Fork l n r =>
let sl := strahler l in
let sr := strahler r in
if beq_nat sl sr then S sl else max sl sr
end.
(* recherche d'un entier n dans un arbre t *)
Fixpoint member_of n t :=
match t with
| Empty => false (* absent *)
| Fork l m r =>
match n ?= m with
| Eq => true (* on l'a trouvé *)
| Lt => member_of n l (* on cherche à gauche *)
| Gt => member_of n r (* on cherche à droite *)
end
end.
(* insertion d'un entier n dans un arbre t *)
Fixpoint add n t :=
match t with
| Empty => Fork Empty n Empty (* on crée un singleton *)
| Fork l m r =>
match n ?= m with
| Eq => t (* déjà présent *)
| Lt => Fork (add n l) m r (* on insère à gauche *)
| Gt => Fork l m (add n r) (* on insère à droite *)
end
end.
(* extraction de l'intervalle [low,high] de l'arbre t *)
Fixpoint interval low high t :=
match t with
| Empty => Empty
| Fork l n r =>
match high ?= n with
| Lt => interval low high l
| Gt | Eq =>
match low ?= n with
| Gt => interval low high r
| Lt | Eq => Fork (interval low high l) n (interval low high r)
end
end
end.
(* c'est là qu'est défini le type list *)
Require Import Lists.List.
(* conversion de l'arbre t en une liste triée *)
Fixpoint to_list acc t :=
match t with
| Empty => acc
| Fork l n r => to_list (n::to_list acc r) l
end.
(* trouve le plus petit élément de l'arbre t *)
Fixpoint minimum acc t :=
match t with
| Empty => acc
| Fork l n r => minimum n l
end.
(* supprime le plus petit élément de l'arbre t *)
Fixpoint remove_minimum la na ra :=
match la with
| Empty => ra
| Fork lb nb rb => Fork (remove_minimum lb nb rb) na ra
end.
(* agglomère les arbres ta et tb *)
(* les éléments de ta doivent être strictement inférieurs aux éléments de tb *)
Fixpoint concat ta tb :=
match ta,tb with
| _,Empty => ta
| Empty,_ => tb
| _,Fork lb nb rb =>
Fork ta (minimum nb lb) (remove_minimum lb nb rb)
end.
(* supprime l'élément n de l'arbre t *)
Fixpoint remove n t :=
match t with
| Empty => Empty
| Fork l m r =>
match n ?= m with
| Lt => Fork (remove n l) m r
| Gt => Fork l m (remove n r)
| Eq => concat l r
end
end.
(* filtre l'arbre t suivant le prédicat cond *)
Fixpoint filter (cond : nat -> bool) t :=
match t with
| Empty => Empty
| Fork l n r =>
if cond n then Fork (filter cond l) n (filter cond r)
else concat (filter cond l) (filter cond r)
end.
(* nombres d'éléments de l'arbre t *)
Fixpoint cardinal t :=
match t with
| Empty => 0
| Fork l _ r => cardinal l + 1 + cardinal r
end.
(* c'est là qu'est défini l'opérateur && *)
Require Import Bool.Bool.
Require Import Coq.Program.Wf.
Require Import Lia.
(* l'arbre ta est-il un sous-ensemble de l'arbre tb ? *)
Program Fixpoint subset (ta : tree) (tb : tree) {measure (cardinal ta + cardinal tb)} : bool :=
match ta,tb with
| Empty,_ => true
| _,Empty => false
| Fork la na ra,Fork lb nb rb =>
match na ?= nb with
| Lt => subset (Fork la na Empty) lb && subset ra tb
| Gt => subset (Fork Empty na ra) rb && subset la tb
| Eq => subset la lb && subset ra rb
end
end.
Next Obligation. Proof. simpl; lia. Qed.
Next Obligation. Proof. simpl; lia. Qed.
Next Obligation. Proof. simpl; lia. Qed.
Next Obligation. Proof. simpl; lia. Qed.
Next Obligation. Proof. simpl; lia. Qed.
Next Obligation. Proof. simpl; lia. Qed.
(* inclusion réciproque *)
Definition equal ta tb :=
subset ta tb && subset tb ta.
(* découpe t en deux parties inférieures et supérieures à n *)
Fixpoint split n t :=
match t with
| Empty => (Empty,false,Empty)
| Fork l m r =>
match n ?= m with
| Lt => let '(la,present,ra) := split n l in (la,present,Fork ra m r)
| Gt => let '(lb,present,rb) := split n r in (Fork l m lb,present,rb)
| Eq => (l,true,r)
end
end.
(* fusionne les arbres ta et tb *)
Fixpoint union ta tb :=
match ta,tb with
| _,Empty => ta
| Empty,_ => tb
| Fork la na ra,_ =>
let '(lb,_,rb) := split na tb
in Fork (union la lb) na (union ra rb)
end.
Fixpoint intersection ta tb :=
match ta,tb with
| _,Empty | Empty,_ => Empty
| Fork la na ra,_ =>
let '(lb,present,rb) := split na tb in
if present then Fork (intersection la lb) na (intersection ra rb)
else concat (intersection la lb) (intersection ra rb)
end.
Fixpoint disjoint ta tb :=
match ta,tb with
| _,Empty | Empty,_ => true
| Fork la na ra,_ =>
let '(lb,present,rb) := split na tb in
if present then false
else disjoint la lb && disjoint ra rb
end.
Fixpoint difference ta tb :=
match ta,tb with
| _,Empty => ta
| Empty,_ => Empty
| Fork la na ra,_ =>
let '(lb,present,rb) := split na tb in
if present then concat (difference la lb) (difference ra rb)
else Fork (difference la lb) na (difference ra rb)
end.
Inductive member : nat -> tree -> Prop :=
| root_member :
forall l n r,
member n (Fork l n r)
| left_member :
forall m n l r,
member n l ->
member n (Fork l m r)
| right_member :
forall m n l r,
member n r ->
member n (Fork l m r).
Lemma member_compose:
forall l m r n,
member n l \/ member n r \/ (n =? m = true) ->
member n (Fork l m r).
Proof.
intros l m r n H.
destruct H as [H | [H | ]].
- apply left_member; auto.
- apply right_member; auto.
- destruct (Nat.eqb_spec n m) as [H | H].
rewrite <- H; apply root_member.
inversion H0.
Qed.
Lemma member_decompose:
forall l m r n,
member n (Fork l m r) ->
member n l \/ member n r \/ (n =? m = true).
Proof.
intros l m r n H.
remember (Fork l m r) as node eqn:H_eq.
destruct H as [ l' n r' | |]; inversion H_eq as [[H1 H2 H3]].
- right; right; rewrite <- H2; apply Nat.eqb_refl.
- left; rewrite H1 in *; auto.
- right;left; rewrite H3 in *; auto.
Qed.
Lemma member_property_split:
forall l m r n,
member n (Fork l m r) <->
member n l \/ member n r \/ (n =? m = true).
Proof.
intros l m r n; split.
- apply member_decompose.
- apply member_compose.
Qed.
Theorem add_main_property :
forall n t, member n (add n t).
Proof.
intros n t. induction t.
(* Empty *)
unfold add.
apply root_member.
(* Fork *)
unfold add. remember (n ?= n0) as cmp.
destruct cmp.
(* Eq *)
symmetry in Heqcmp.
apply (nat_compare_eq n n0) in Heqcmp.
subst n0. apply root_member.
(* Lt *)
apply left_member. exact IHt1.
(* Gt *)
apply right_member. exact IHt2.
Qed.
Theorem add_is_conservative :
forall m n t, member m t -> member m (add n t).
Proof.
intros m n t H. induction t.
(* Empty *)
unfold add.
apply left_member. exact H.
(* Fork *)
remember (Fork t1 n0 t2) as node.
destruct H.
(* root_member *)
unfold add. destruct (n ?= n1).
apply root_member.
apply root_member.
apply root_member.
(* left_member *)
inversion Heqnode. rewrite H1 in H.
unfold add. destruct (n ?= n0).
apply left_member. exact H.
apply IHt1 in H. apply left_member. exact H.
apply left_member. exact H.
(* right_member *)
inversion Heqnode. rewrite H3 in H.
unfold add. destruct (n ?= n0).
apply right_member. exact H.
apply right_member. exact H.
apply IHt2 in H. apply right_member. exact H.
Qed.
Inductive tree_less : tree -> nat -> Prop :=
| empty_tree_less :
forall b, tree_less Empty b
| fork_tree_less :
forall l m r b,
tree_less l b -> tree_less r b -> m < b ->
tree_less (Fork l m r) b.
Inductive tree_more : tree -> nat -> Prop :=
| empty_tree_more :
forall a, tree_more Empty a
| fork_tree_more :
forall l m r a,
tree_more l a -> tree_more r a -> m > a ->
tree_more (Fork l m r) a.
Inductive tree_ordered : tree -> Prop :=
| empty_tree_ordered :
tree_ordered Empty
| fork_tree_ordered :
forall l m r,
tree_ordered l -> tree_ordered r ->
tree_less l m -> tree_more r m ->
tree_ordered (Fork l m r).
Lemma tree_ordered_compose:
forall l m r,
tree_ordered l /\ tree_ordered r /\ tree_less l m /\ tree_more r m ->
tree_ordered (Fork l m r).
Proof.
intros l m r [H1 [H2 [H3 H4]]].
apply fork_tree_ordered; auto.
Qed.
Lemma tree_ordered_decompose:
forall l m r,
tree_ordered (Fork l m r) ->
tree_ordered l /\ tree_ordered r /\ tree_less l m /\ tree_more r m.
Proof.
intros l m r H; inversion H; subst.
split; auto.
Qed.
Lemma tree_ordered_property_split:
forall l m r,
tree_ordered (Fork l m r) <->
tree_ordered l /\ tree_ordered r /\ tree_less l m /\ tree_more r m.
Proof.
intros l m r; split.
- apply tree_ordered_decompose.
- apply tree_ordered_compose.
Qed.
Fact tree_less_upper_bound:
forall t n, tree_less t n <-> forall m, member m t -> m < n.
Proof.
split.
(* -> *)
intros Hless m Hm. induction t.
inversion Hm.
inversion Hm; inversion Hless; subst; auto.
(* <- *)
intros H. induction t.
constructor.
constructor.
apply IHt1. intros m Hm. apply H. apply left_member. assumption.
apply IHt2. intros m Hm. apply H. apply right_member. assumption.
apply H. apply root_member.
Qed.
Fact tree_more_lower_bound:
forall t n, tree_more t n <-> forall m, member m t -> m > n.
Proof.
split.
(* -> *)
intros Hmore m Hm. induction t.
inversion Hm.
inversion Hm; inversion Hmore; subst; auto.
(* <- *)
intros H. induction t.
constructor.
constructor.
apply IHt1. intros m Hm. apply H. apply left_member. assumption.
apply IHt2. intros m Hm. apply H. apply right_member. assumption.
apply H. apply root_member.
Qed.
(* Require Import Arith.Lt Arith.Gt. *)
Lemma member_left:
forall l m r n, tree_ordered (Fork l m r) -> member n (Fork l m r) -> n < m -> member n l.
Proof.
intros l m r n Hord Hmem Hlt.
inversion Hord; subst; clear Hord.
inversion Hmem; subst; clear Hmem.
contradict Hlt. apply lt_irrefl.
assumption.
apply tree_more_lower_bound with (m:=n) in H5.
contradict H5. apply gt_asym. assumption.
assumption.
Qed.
Lemma member_right:
forall l m r n, tree_ordered (Fork l m r) -> member n (Fork l m r) -> n > m -> member n r.
Proof.
intros l m r n Hord Hmem Hlt.
inversion Hord; subst; clear Hord.
inversion Hmem; subst; clear Hmem.
contradict Hlt. apply lt_irrefl.
apply tree_less_upper_bound with (m:=n) in H4.
contradict H4. apply lt_asym. assumption. assumption.
assumption.
Qed.
Lemma add_preserves_less:
forall t n m, tree_less t n -> m < n -> tree_less (add m t) n.
Proof.
induction t; intros; inversion H; subst; clear H.
repeat constructor. assumption.
simpl. destruct (m ?= n); constructor; auto.
Qed.
Lemma add_preserves_more:
forall t n m, tree_more t n -> m > n -> tree_more (add m t) n.
Proof.
induction t; intros; inversion H; subst; clear H.
repeat constructor. assumption.
simpl. destruct (m ?= n); constructor; auto.
Qed.
Theorem add_preserves_order :
forall t, tree_ordered t ->
forall n, tree_ordered (add n t).
Proof.
induction t; intros.
(* Empty *)
simpl. repeat constructor.
(* Fork *)
simpl. remember (n0 ?= n) as cmp. symmetry in Heqcmp.
destruct cmp.
assumption.
inversion H; subst; clear H. constructor; auto.
apply nat_compare_lt in Heqcmp. apply add_preserves_less; assumption.
inversion H; subst; clear H. constructor; auto.
apply nat_compare_gt in Heqcmp. apply add_preserves_more; assumption.
Qed.
Theorem interval_membership_sound_property :
forall low high n t, member n (interval low high t) -> member n t /\ low <= n <= high.
Proof.
intros low high n t.
induction t; simpl.
* intro H; inversion H.
* case_eq (Nat.compare high n0); intros H_high.
case_eq (Nat.compare low n0); intros H_low.
+ rewrite member_property_split; intros H.
case H as [H|[H|H]].
++ pose proof (IHt1 H) as H_t1; case H_t1 as [H_mem H_rng].
split; auto; apply left_member; assumption.
++ pose proof (IHt2 H) as H_t2; case H_t2 as [H_mem H_rng].
split; auto; apply right_member; assumption.
++ rewrite (Nat.compare_eq _ _ H_high).
rewrite (Nat.compare_eq _ _ H_low).
rewrite (beq_nat_true _ _ H); split; auto.
apply root_member.
+ rewrite member_property_split; intros H.
case H as [H|[H|H]].
++ pose proof (IHt1 H) as H_t1; case H_t1 as [H_mem H_rng].
split; auto; apply left_member; assumption.
++ pose proof (IHt2 H) as H_t2; case H_t2 as [H_mem H_rng].
split; auto; apply right_member; assumption.
++ rewrite (Nat.compare_eq _ _ H_high).
pose proof (nat_compare_Lt_lt _ _ H_low) as H_lt.
rewrite (beq_nat_true _ _ H); split; auto.
apply root_member.
split; auto.
apply Nat.lt_le_incl; assumption.
+ intro H; pose proof (IHt2 H) as [H1 H2]; split; auto.
apply right_member; assumption.
+ intro H; pose proof (IHt1 H) as [H1 H2]; split; auto.
apply left_member; assumption.
+ case_eq (Nat.compare low n0); intros H_low.
++ rewrite member_property_split; intros H.
case H as [H|[H|H]].
pose proof (IHt1 H) as [H1 H2]; split; auto.
apply left_member; assumption.
pose proof (IHt2 H) as [H1 H2]; split; auto.
apply right_member; assumption.
rewrite (Nat.compare_eq _ _ H_low).
rewrite (beq_nat_true _ _ H); split; auto.
apply root_member.
split; auto.
apply Nat.lt_le_incl; apply Nat.compare_gt_iff; assumption.
++ rewrite member_property_split; intros H.
case H as [H|[H|H]].
pose proof (IHt1 H) as [H1 H2]; split; auto.
apply left_member; assumption.
pose proof (IHt2 H) as [H1 H2]; split; auto.
apply right_member; assumption.
rewrite (beq_nat_true _ _ H); split; auto.
apply root_member.
split; auto.
apply Nat.lt_le_incl; apply Nat.compare_lt_iff; assumption.
apply Nat.lt_le_incl; apply Nat.compare_gt_iff; assumption.
++ intro H; pose proof (IHt2 H) as [H1 H2]; split; auto.
apply right_member; assumption.
Qed.
Theorem interval_membership_complete_property :
forall low high n t, member n t /\ low <= n <= high /\ tree_ordered t -> member n (interval low high t).
Proof.
intros low high n t.
generalize low high n; clear low high n; induction t as [| l IHl n0 r IHr].
- intros low high n H; case H as []; simpl; auto.
- intros low high n; simpl.
case_eq (Nat.compare high n0); intros H_high.
case_eq (Nat.compare low n0); intros H_low.
++ rewrite member_property_split; intros H.
case H as [[H0 | [H0 | H0]] [H1 H2]].
inversion H2; subst; apply left_member; apply IHl; split; auto.
inversion H2; subst; apply right_member; apply IHr; split; auto.
rewrite (beq_nat_true _ _ H0); apply root_member.
++ rewrite member_property_split; intros H.
case H as [[H0 | [H0 | H0]] [H1 H2]].
inversion H2; subst; apply left_member; apply IHl; split; auto.
inversion H2; subst; apply right_member; apply IHr; split; auto.
rewrite (beq_nat_true _ _ H0); apply root_member.
++ rewrite (Nat.compare_eq _ _ H_high); intros H.
case H as [H0 [H1 H2]]; inversion H2; subst.
pose proof (nat_compare_Gt_gt _ _ H_low).
lia.
++ pose proof (nat_compare_Lt_lt _ _ H_high) as H_high'; intros H.
case H as [H0 [H1 H2]]; inversion H2; subst.
apply IHl; split; auto.
apply (member_left l n0 r n); auto.
lia.
++ case_eq (Nat.compare low n0); intros H_low.
** rewrite member_property_split; intros H.
case H as [[H0 | [H0 | H0]] [H1 H2]].
inversion H2; subst; apply left_member; apply IHl; split; auto.
inversion H2; subst; apply right_member; apply IHr; split; auto.
rewrite (beq_nat_true _ _ H0); apply root_member.
** rewrite member_property_split; intros H.
case H as [[H0 | [H0 | H0]] [H1 H2]].
inversion H2; subst; apply left_member; apply IHl; split; auto.
inversion H2; subst; apply right_member; apply IHr; split; auto.
rewrite (beq_nat_true _ _ H0); apply root_member.
** pose proof (nat_compare_Gt_gt _ _ H_high) as H_high' .
pose proof (nat_compare_Gt_gt _ _ H_low) as H_low' .
intros H.
case H as [H0 [H1 H2]]; inversion H2; subst.
apply IHr; split; auto.
apply (member_right l n0 r n); auto.
lia.
Qed.
(* specification des opérations ensemblistes *)
Theorem interval_main_property :
forall low high n t, tree_ordered t -> member n (interval low high t) <-> member n t /\ low <= n <= high.
Proof.
intros low high n t Hord; split.
apply interval_membership_sound_property.
intro H; case H as [H1 H2]; apply interval_membership_complete_property; split; auto.
Qed.
Theorem remove_minimum_preserves_membership :
forall n m l r, tree_ordered (Fork l n r) -> member m (Fork l n r) ->
minimum m (Fork l n r) <> m -> member m (remove_minimum l n r).
Proof.
intros n m l r.
generalize n m r; clear n m r.
induction l as [|ll IHll ln lr IHlr]; intros n m r; simpl.
- rewrite tree_ordered_property_split; intros [Hord1 [Hord2 [Hord3 Hord4]]].
rewrite member_property_split; intros Hmem.
case Hmem as [Hmem| [Hmem|Hmem]]; auto.
* inversion Hmem.
* apply beq_nat_true in Hmem; rewrite Hmem; intros Hneq; contradict Hneq; auto.
- rewrite tree_ordered_property_split; intros [Hord1 [Hord2 [Hord3 Hord4]]].
rewrite member_property_split; intros Hmem.
case Hmem as [Hmem| [Hmem|Hmem]]; auto.
* intros Hmin; apply left_member; apply IHll; auto.
* intros Hmin; apply right_member; auto.
* apply beq_nat_true in Hmem; rewrite Hmem; intros Hmin; apply root_member.
Qed.
Theorem remove_minimum_preserves_membership_strong :
forall n m l r, member m (Fork l n r) ->
minimum m (Fork l n r) <> m -> member m (remove_minimum l n r).
Proof.
intros n m l r.
generalize n m r; clear n m r.
induction l as [|ll IHll ln lr IHlr]; intros n m r; simpl.
- rewrite member_property_split; intros Hmem.
case Hmem as [Hmem| [Hmem|Hmem]]; auto.
* inversion Hmem.
* apply beq_nat_true in Hmem; rewrite Hmem; intros Hneq; contradict Hneq; auto.
- rewrite member_property_split; intros Hmem.
case Hmem as [Hmem| [Hmem|Hmem]]; auto.
* intros Hmin; apply left_member; apply IHll; auto.
* intros Hmin; apply right_member; auto.
* apply beq_nat_true in Hmem; rewrite Hmem; intros Hmin; apply root_member.
Qed.
Theorem concat_preserves_membership_left :
forall m l r, member m l -> member m (concat l r).
Proof.
intros m l r; case l; simpl.
- intros H; inversion H.
- intros H; case r; auto.
intros; apply left_member; auto.
Qed.
Theorem concat_preserves_membership_internal_strong : forall m l n r ta,
member m (Fork l n r) ->
member m (Fork ta (minimum n l) (remove_minimum l n r)).
Proof.
intros m l n r ta.
intros Hmem.
pose proof (remove_minimum_preserves_membership_strong n m l r Hmem) as Hmin; simpl in Hmin.
case_eq ((minimum n l) =? m).
- intros Hminl; apply beq_nat_true in Hminl; rewrite Hminl; apply root_member.
- intros Hminl; apply beq_nat_false in Hminl; apply right_member; apply Hmin; auto.
Qed.
Theorem concat_preserves_membership_right_strong :
forall m l r, member m r -> member m (concat l r).
Proof.
intros m l r; generalize m l; clear m l; induction r as [| rl IHrl rn rr IHrr]; simpl; intros m l.
- intros H; inversion H.
- rewrite member_property_split; intros [Hmem | [ Hmem | Hmem]]; simpl.
* case l; simpl; try apply left_member; auto.
intros ll ln lr. apply concat_preserves_membership_internal_strong; auto; apply left_member; auto.
* case l; simpl; try apply right_member; auto.
intros ll ln lr; apply concat_preserves_membership_internal_strong; auto; apply right_member; auto.
* apply beq_nat_true in Hmem; rewrite Hmem; clear Hmem.
case l; simpl; try apply root_member; auto.
intros ll ln lr; apply concat_preserves_membership_internal_strong; auto; apply root_member; auto.
Qed.
Theorem member_property_remove_minimum_split :
forall m l n r, member m (remove_minimum l n r) -> member m l \/ member m r \/ (m =? n) = true.
Proof.
intros m l n r; generalize m r n; clear m r n; induction l as [| ll IHll ln lr IHlr]; simpl; intros m r n; auto.
rewrite member_property_split; intros [Hmem|[Hmem|Hmem]]; auto; left;
pose proof (IHll m lr ln Hmem) as [H1 | [H1 | H1]]; auto.
apply left_member; auto.
apply right_member; auto.
apply beq_nat_true in H1; rewrite H1 in *; apply root_member.
Qed.
Theorem member_property_concat_split :
forall m l r, member m (concat l r) -> member m l \/ member m r.
Proof.
intros m l r; generalize m r; clear m r; induction l as [| ll IHll ln lr IHlr]; simpl; intros m r.
* case r; auto.
* case r as [| rl rn rr]; auto.
rewrite member_property_split; intros [Hmem|[Hmem|Hmem]].
** left; auto.
** apply member_property_remove_minimum_split in Hmem.
case Hmem as [Hmem|[Hmem|Hmem]].
*** right; apply left_member; auto.
*** right; apply right_member; auto.
*** apply beq_nat_true in Hmem; rewrite Hmem in *; right; apply root_member.
** apply beq_nat_true in Hmem; rewrite Hmem in *; right.
clear.
generalize rl rn rr; clear rl rn rr; intros l.
induction l as [|ll IHll ln lr IHlr]; simpl; try apply root_member.
intros n r; apply left_member; apply IHll.
Qed.
Theorem remove_is_conservative :
forall m n t, member m t /\ m <> n -> member m (remove n t).
Proof.
intros m n t; generalize m n; clear m n; induction t as [| l IHl n0 r IHr]; simpl; auto; intros m n.
- intros H; inversion H; auto.
- rewrite member_property_split; intros [[H | [H | H]] Hneq].
* case_eq (Nat.compare n n0); intros H_n0.
** apply concat_preserves_membership_left; auto.
** apply left_member; apply IHl; auto.
** apply left_member; auto.
* case_eq (Nat.compare n n0); intros H_n0.
** apply concat_preserves_membership_right_strong; auto.
** apply right_member; auto.
** apply right_member; apply IHr; auto.
* apply beq_nat_true in H; rewrite H in *; clear H.
case_eq (Nat.compare n n0); intros H_n0.
** apply nat_compare_eq in H_n0; rewrite H_n0 in Hneq; contradict Hneq; auto.
** apply root_member; auto.
** apply root_member; auto.
Qed.
Theorem filter_main_property :
forall n t cond, member n (filter cond t) <-> member n t /\ cond n = true.
Proof.
intros n t cond; split.
- generalize n cond; clear n cond; induction t as [| l IHl n r IHr]; intros m cond; simpl.
* intros H; inversion H.
* case_eq (cond n); intros Hcond; simpl.
** rewrite member_property_split; intros [Hmem|[Hmem|Hmem]].
*** pose proof (IHl m cond Hmem) as [H1 H2].
split; auto; apply left_member; auto.
*** pose proof (IHr m cond Hmem) as [H1 H2].
split; auto; apply right_member; auto.
*** apply beq_nat_true in Hmem; rewrite Hmem in *; split; auto; apply root_member.
** simpl; intros H; apply member_property_concat_split in H.
case H as [H|H].
*** pose proof (IHl m cond H) as [H1 H2].
split; auto; apply left_member; auto.
*** pose proof (IHr m cond H) as [H1 H2].
split; auto; apply right_member; auto.
- intros [Hl Hr]; generalize Hr Hl; clear Hl Hr.
generalize n cond; clear n cond; induction t as [| l IHl n r IHr]; intros m cond; simpl; auto.
* intros Hcondm; case_eq (cond n); intros Hcond; simpl.
** rewrite member_property_split; intros [Hmem|[Hmem|Hmem]].
*** apply left_member; apply IHl; auto.
*** apply right_member; apply IHr; auto.
*** apply beq_nat_true in Hmem; rewrite Hmem in *; apply root_member.
** rewrite member_property_split; intros [Hmem|[Hmem|Hmem]].
*** apply concat_preserves_membership_left; apply IHl; auto.
*** apply concat_preserves_membership_right_strong; apply IHr; auto.
*** apply beq_nat_true in Hmem; rewrite Hmem in *.
rewrite Hcond in Hcondm.
contradict Hcondm; auto.
Qed.
Theorem split_preserves_membership: forall m k t,
member m t ->
let '(l, _, _) := split k t in member m l \/
let '(_, _, r) := split k t in member m r \/
(m =? k) = true.
Proof.
intros m k t; generalize m k; clear m k; induction t as [|l IHl n r IHr]; intros m k.
- intros H; inversion H.
- rewrite member_property_split; intros [Hmem|[Hmem|Hmem]]; simpl.
* case_eq (Nat.compare k n); intros Heq.
** left; auto.
** pose proof (IHl m k Hmem); generalize H; clear H.
case (split k l) as [[Hl Hn] Hr]; intros [H|[H|H]]; auto;
right;left; apply left_member; auto.
** case (split k r) as [[Hl Hn] Hr]; left; apply left_member; auto.
* case_eq (Nat.compare k n); intros Heq; auto.
** case (split k l) as [[Hl Hn] Hr]; right;left; apply right_member; auto.
** pose proof (IHr m k Hmem); generalize H; clear H.
case (split k r) as [[Hl Hn] Hr]; intros [H|[H|H]]; auto;
left; apply right_member; auto.
* case_eq (Nat.compare k n); intros Heq; auto.
** right; right; apply nat_compare_eq in Heq; rewrite Heq; auto.
** apply beq_nat_true in Hmem; case (split k l) as [[Hl Hn] Hr].
rewrite Hmem in *; right; left; apply root_member.
** apply beq_nat_true in Hmem; case (split k r) as [[Hl Hn] Hr].
rewrite Hmem in *; left; apply root_member.
Qed.
Theorem split_is_conservative_left: forall m k t,
let '(l, _, _) := split k t in member m l -> member m t.
Proof.
intros m k t; generalize m k; clear m k; induction t as [|l IHl n r IHr]; intros m k; simpl; auto.
case_eq (Nat.compare k n); intros Heq.
- intros Hmem; apply left_member; auto.
- pose proof (IHl m k) as Hspl; generalize Hspl; clear Hspl.
case (split k l) as [[Hl Hn] Hr]; intros Hmem Hv.
apply left_member; apply Hmem; auto.
- pose proof (IHr m k) as Hspl; generalize Hspl; clear Hspl.
case (split k r) as [[Hl Hn] Hr]; intros Hfnl.
rewrite member_property_split; intros [Hmem|[Hmem|Hmem]]; simpl.
* apply left_member; auto.
* apply right_member; apply Hfnl; auto.
* apply beq_nat_true in Hmem; rewrite Hmem in *; apply root_member.
Qed.
Theorem split_is_conservative_right: forall m k t,
let '(_, _, r) := split k t in member m r -> member m t.
Proof.
intros m k t; generalize m k; clear m k; induction t as [|l IHl n r IHr]; intros m k; simpl; auto.
case_eq (Nat.compare k n); intros Heq.
- intros Hmem; apply right_member; auto.
- pose proof (IHl m k) as Hspl; generalize Hspl; clear Hspl.
case (split k l) as [[Hl Hn] Hr]; intros Hfnl.
rewrite member_property_split; intros [Hmem|[Hmem|Hmem]]; simpl.
* apply left_member; apply Hfnl; auto.
* apply right_member; auto.
* apply beq_nat_true in Hmem; rewrite Hmem in *; apply root_member.
- pose proof (IHr m k) as Hspl; generalize Hspl; clear Hspl.
case (split k r) as [[Hl Hn] Hr]; intros Hmem Hv.
apply right_member; apply Hmem; auto.
Qed.
Theorem split_is_conservative_present: forall m t,
let '(_, present, _) := split m t in present = true -> member m t.
Proof.
intros m t; generalize m; clear m; induction t as [|l IHl n r IHr]; intros m; simpl; auto.
- intros H; inversion H.
- case_eq (Nat.compare m n); intros Heq.
* intros _. apply nat_compare_eq in Heq; rewrite Heq; apply root_member.
* pose proof (IHl m) as H; generalize H; clear H.
case (split m l) as [[Hl Hn] Hr]; intros Hfnl Htr.
apply left_member; apply Hfnl; auto.
* pose proof (IHr m) as H; generalize H; clear H.
case (split m r) as [[Hl Hn] Hr]; intros Hfnl Htr.
apply right_member; apply Hfnl; auto.
Qed.
Theorem split_is_sound_present: forall m t,
let '(_, present, _) := split m t in tree_ordered t -> present = false -> ~ member m t.
Proof.
intros m t; generalize m; clear m; induction t as [|l IHl n r IHr]; intros m; simpl; auto.
- intros _ _ H; inversion H.
- case_eq (Nat.compare m n); intros Heq.
* intros _ Hf; inversion Hf.
* pose proof (IHl m) as H; generalize H; clear H.
case (split m l) as [[Hl Hn] Hr]; intros Hfnl Htr.
pose proof (tree_ordered_decompose l n r Htr) as [Hlord [Hrord [Hltl Hltr]]].
intros Hfl; pose proof (Hfnl Hlord Hfl) as Hneg; clear Hfnl Hfl.
apply nat_compare_lt in Heq.
rewrite member_property_split; intros [H|[H|H]].
++ apply Hneg; auto.
++ rewrite tree_more_lower_bound in Hltr; pose proof (Hltr m H); lia.
++ apply beq_nat_true in H; lia.
* pose proof (IHr m) as H; generalize H; clear H.
case (split m r) as [[Hl Hn] Hr]; intros Hfnl Htr.
pose proof (tree_ordered_decompose l n r Htr) as [Hlord [Hrord [Hltl Hltr]]].
intros Hfl; pose proof (Hfnl Hrord Hfl) as Hneg; clear Hfnl Hfl.
apply nat_compare_gt in Heq.
rewrite member_property_split; intros [H|[H|H]].
++ rewrite tree_less_upper_bound in Hltl; pose proof (Hltl m H); lia.
++ apply Hneg; auto.
++ apply beq_nat_true in H; lia.
Qed.
Theorem union_main_property :
forall n ta tb, member n ta \/ member n tb <-> member n (union ta tb).
Proof.
intros n ta tb; split.
- generalize n tb; clear n tb; induction ta as [| tl IHtl tn tr IHtr]; intros n tb; simpl.
* case tb as [|tbl tbn tbr]; intros [H|H]; auto; inversion H.
* case tb as [|tbl tbn tbr]; intros [H|H]; auto.
** inversion H.
** case (split tn (Fork tbl tbn tbr)) as [[lb _] lr].
apply member_property_split in H; case H as [Hmem|[Hmem|Hmem]].
*** apply left_member; apply IHtl; left; auto.
*** apply right_member; apply IHtr; left; auto.
*** apply beq_nat_true in Hmem; rewrite Hmem in *; apply root_member.
** pose proof (split_preserves_membership n tn (Fork tbl tbn tbr) H) as Hspl.
generalize Hspl; clear Hspl.
case_eq (split tn (Fork tbl tbn tbr)); intros [lb unused] lr Heq [Hm|[Hm|Hm]].
*** apply left_member; apply IHtl; auto.
*** apply right_member; apply IHtr; auto.
*** apply beq_nat_true in Hm; rewrite Hm in *; apply root_member.
- generalize n tb; clear n tb; induction ta as [| tl IHtl tn tr IHtr]; intros n tb; simpl.
* case tb as [| tbl tbn tbr]; auto.
* case tb as [| tbl tbn tbr]; auto.
pose proof (split_is_conservative_left n tn (Fork tbl tbn tbr)) as Hspl; generalize Hspl; clear Hspl.
pose proof (split_is_conservative_right n tn (Fork tbl tbn tbr)) as Hspl; generalize Hspl; clear Hspl.
case (split tn (Fork tbl tbn tbr)) as [[lb unused] lr] eqn:Hspl; intros Hfnr Hfnl.
rewrite member_property_split; intros [H|[H|H]].
** pose proof (IHtl n lb H) as [H1|H1].
*** left; apply left_member; auto.
*** right; apply Hfnl; auto.
** pose proof (IHtr n lr H) as [H1|H1].
*** left; apply right_member; auto.
*** right; apply Hfnr; auto.
** apply beq_nat_true in H; rewrite H in *; left; apply root_member.
Qed.
Theorem split_tree_ordered_left : forall n t,
tree_ordered t ->
tree_less (let '(l, _, _) := split n t in l) n.
Proof.
intros n t; generalize n; clear n.
induction t as [| l IHl n r IHr ]; intros m Hord; simpl.
- apply empty_tree_less.
- case_eq (Nat.compare m n); intros Heq.
* pose proof (tree_ordered_decompose l n r Hord) as [Hl [Hr [Hltl Hltr]]].
apply nat_compare_eq in Heq; rewrite Heq; auto.
* pose proof (IHl m) as H; generalize H; clear H.
case (split m l) as [[Hll Hnl] Hrl]; intros Heqn; apply Heqn.
pose proof (tree_ordered_decompose l n r Hord) as [Hl [Hr [Hltl Hltr]]].
auto.
* pose proof (IHr m) as H; generalize H; clear H.
case (split m r) as [[Hll Hnl] Hrl]; intros Heqn.
pose proof (tree_ordered_decompose l n r Hord) as [Hl [Hr [Hltl Hltr]]].
apply fork_tree_less; try apply tree_less_upper_bound; try intros m' Hm'.
** rewrite tree_less_upper_bound in Hltl.
pose proof (Hltl m' Hm').
rewrite Nat.compare_gt_iff in Heq.
eapply lt_trans; auto.
** pose proof (Heqn Hr) as Hltlm'.
rewrite tree_less_upper_bound in Hltlm'.
exact (Hltlm' m' Hm').
** apply Nat.compare_gt_iff; auto.
Qed.
Theorem split_tree_ordered_right : forall n t,
tree_ordered t ->
tree_more (let '(_, _, r) := split n t in r) n.
Proof.
intros n t; generalize n; clear n.
induction t as [| l IHl n r IHr ]; intros m Hord; simpl.
- apply empty_tree_more.
- case_eq (Nat.compare m n); intros Heq.
* pose proof (tree_ordered_decompose l n r Hord) as [Hl [Hr [Hltl Hltr]]].
apply nat_compare_eq in Heq; rewrite Heq; auto.
* pose proof (IHl m) as H; generalize H; clear H.
case (split m l) as [[Hll Hnl] Hrl]; intros Heqn.
pose proof (tree_ordered_decompose l n r Hord) as [Hl [Hr [Hltl Hltr]]].
apply fork_tree_more; try apply tree_more_lower_bound; try intros m' Hm'.
** pose proof (Heqn Hl) as Hltlm'.
rewrite tree_more_lower_bound in Hltlm'.
exact (Hltlm' m' Hm').
** rewrite tree_more_lower_bound in Hltr.
pose proof (Hltr m' Hm').
apply nat_compare_lt in Heq.
eapply gt_trans; auto.
** apply Nat.compare_lt_iff; auto.
* pose proof (IHr m) as H; generalize H; clear H.
case (split m r) as [[Hll Hnl] Hrl]; intros Heqn; apply Heqn.
pose proof (tree_ordered_decompose l n r Hord) as [Hl [Hr [Hltl Hltr]]].
auto.
Qed.
Theorem split_tree_ordered_preserves_left : forall n t,
tree_ordered t ->
tree_ordered (let '(l, _, _) := split n t in l).
Proof.
intros m t; induction t as [|l IHl n r IHr].
- intros H; simpl; auto.
- intros Hord; pose proof (tree_ordered_decompose l n r Hord) as [Hl [Hr [Hltl Hltr]]].
simpl; case_eq (Nat.compare m n); intro Hcmp; auto.
* pose proof (IHl Hl) as H; generalize H; clear H.
case_eq (split m l); intros [ll lp] lr; simpl; auto.
* pose proof (IHr Hr) as H; generalize H; clear H.
case_eq (split m r); intros [ll lp] lr; simpl; intros Heq Hord'.
apply tree_ordered_compose; repeat split; auto.
apply tree_more_lower_bound; intros m' Hm'.
rewrite tree_more_lower_bound in Hltr.
apply Hltr.
pose proof (split_is_conservative_left m' m r) as Himpl.
rewrite Heq in Himpl; apply Himpl; auto.
Qed.
Theorem split_tree_ordered_preserves_right : forall n t,
tree_ordered t ->
tree_ordered (let '(_, _, r) := split n t in r).
Proof.
intros m t; induction t as [|l IHl n r IHr].
- intros H; simpl; auto.
- intros Hord; pose proof (tree_ordered_decompose l n r Hord) as [Hl [Hr [Hltl Hltr]]].
simpl; case_eq (Nat.compare m n); intro Hcmp; auto.
* pose proof (IHl Hl) as H; generalize H; clear H.
case_eq (split m l); intros [ll lp] lr; simpl; intros Heq Hord'.
apply tree_ordered_compose; repeat split; auto.
apply tree_less_upper_bound; intros m' Hm'.
rewrite tree_less_upper_bound in Hltl.
apply Hltl.
pose proof (split_is_conservative_right m' m l) as Himpl.
rewrite Heq in Himpl; apply Himpl; auto.
* pose proof (IHr Hr) as H; generalize H; clear H.
case_eq (split m r); intros [ll lp] lr; simpl; auto.
Qed.
Theorem intersection_conservative :
forall n ta tb,
tree_ordered ta -> tree_ordered tb ->
member n (intersection ta tb) -> member n ta /\ member n tb.
Proof.
intros n ta tb Hta Htb Htmem;
generalize n Hta tb Htb Htmem;
clear n tb Htb Hta Htmem.
induction ta as [|tal IHtal tan tar IHtar].
- simpl; intros n tord [|] _ H; inversion H.
- intros n Hord.
pose proof (tree_ordered_decompose tal tan tar Hord) as [Hl [Hr [Hltl Hltr]]].
pose proof (IHtal n Hl) as IHl; clear IHtal.
pose proof (IHtar n Hr) as IHr; clear IHtar.
intros tb Hbord; simpl.
pose proof (IHl tb Hbord) as IHlb.
pose proof (IHr tb Hbord) as IHrb.
generalize Hbord IHlb IHrb; clear Hbord IHlb IHrb.
case tb as [|tbl tbn tbr]; simpl.
* intros _ _ _ H; inversion H.
* intros Hordb Hmeml Hmemr.
pose proof (tree_ordered_decompose _ _ _ Hordb) as [Hl' [Hr' [Hltl' Hltr']]].
case_eq (Nat.compare tan tbn); intros Heq.
** rewrite member_property_split.
intros [Hmem'|[Hmem'|Hmem']].
pose proof (IHl tbl Hl' Hmem') as [H1 H2]; split; apply left_member; auto.
pose proof (IHr tbr Hr' Hmem') as [H1 H2]; split; apply right_member; auto.
apply beq_nat_true in Hmem'; rewrite Hmem' in *.
apply nat_compare_eq in Heq; rewrite Heq in *; split; apply root_member.
** case_eq (split tan tbl); intros [Htbl [|]] Htbr Heq'.
rewrite member_property_split; intros [Hmem'|[Hmem'|Hmem']].
*** pose proof (split_tree_ordered_preserves_left tan tbl Hl') as Htl.
rewrite Heq' in Htl; pose proof (IHl Htbl Htl Hmem') as [H1 H2].
split; first [apply left_member]; auto.
pose proof (split_is_conservative_left n tan tbl) as H3.
rewrite Heq' in H3; apply H3; auto.
*** assert (tree_ordered (Fork Htbr tbn tbr)). {
apply tree_ordered_compose; repeat split; auto.
pose proof (split_tree_ordered_preserves_right tan tbl Hl') as Htl;
rewrite Heq' in Htl; auto.
apply tree_less_upper_bound; intros m Hmem.
rewrite tree_less_upper_bound in Hltl'.
apply Hltl'.
pose proof (split_is_conservative_right m tan tbl) as H1; rewrite Heq' in H1.
apply H1; auto.
}
pose proof (IHr _ H Hmem') as [H1 H2]; split.
**** apply right_member; auto.
**** rewrite member_property_split in H2; case H2 as [H2|[H2|H2]].
***** pose proof (split_is_conservative_right n tan tbl) as H'; rewrite Heq' in H'; apply left_member; apply H'; auto.
***** apply right_member; auto.
***** apply beq_nat_true in H2; rewrite H2 in *; apply root_member.
*** apply beq_nat_true in Hmem'; rewrite Hmem' in *; split.
**** apply root_member.
**** pose proof (split_is_conservative_present tan tbl) as H.
rewrite Heq' in H; apply left_member; apply H; auto.
*** intros Hmem; apply (member_property_concat_split) in Hmem.
case Hmem as [Hmem|Hmem].
**** assert (tree_ordered Htbl) as Htblord. {
pose proof (split_tree_ordered_preserves_left tan tbl Hl') as H'; rewrite Heq' in H'.
auto.
}
pose proof (IHl Htbl Htblord Hmem) as [H1 H2]; split.
apply left_member; auto.
pose proof (split_is_conservative_left n tan tbl) as H; rewrite Heq' in H.
apply left_member; apply H; auto.
**** assert (tree_ordered (Fork Htbr tbn tbr)) as Htblord. {
apply tree_ordered_compose; repeat split; auto.
pose proof (split_tree_ordered_preserves_right tan tbl Hl') as H'; rewrite Heq' in H'; auto.
apply tree_less_upper_bound; intros m' Hmemm'.
rewrite tree_less_upper_bound in Hltl'; apply Hltl'.
pose proof (split_is_conservative_right m' tan tbl) as H; rewrite Heq' in H.
apply H; auto.
}
pose proof (IHr _ Htblord Hmem) as [H1 H2]; split.
apply right_member; auto.
rewrite member_property_split in H2; case H2 as [H|[H|H]].
***** pose proof (split_is_conservative_right n tan tbl) as H'; rewrite Heq' in H'; apply left_member; apply H'; auto.
***** apply right_member; auto.
***** apply beq_nat_true in H; rewrite H in *; apply root_member.
** case_eq (split tan tbr); intros [Htbl [|]] Htbr Heq'.
rewrite member_property_split; intros [Hmem'|[Hmem'|Hmem']].
*** assert (tree_ordered (Fork tbl tbn Htbl)). {
apply tree_ordered_compose; repeat split; auto.
pose proof (split_tree_ordered_preserves_left tan tbr Hr') as Htl;
rewrite Heq' in Htl; auto.
apply tree_more_lower_bound; intros m Hmem.
rewrite tree_more_lower_bound in Hltr'; apply Hltr'.
pose proof (split_is_conservative_left m tan tbr) as H1; rewrite Heq' in H1.
apply H1; auto.
}
pose proof (IHl _ H Hmem') as [H1 H2]; split.
**** apply left_member; auto.
**** rewrite member_property_split in H2; case H2 as [H2|[H2|H2]].
***** apply left_member; auto.
***** pose proof (split_is_conservative_left n tan tbr) as H'; rewrite Heq' in H'; apply right_member; apply H'; auto.
***** apply beq_nat_true in H2; rewrite H2 in *; apply root_member.
*** pose proof (split_tree_ordered_preserves_right tan tbr Hr') as Htl.
rewrite Heq' in Htl; pose proof (IHr Htbr Htl Hmem') as [H1 H2].
split; first [apply right_member]; auto.
pose proof (split_is_conservative_right n tan tbr) as H3.
rewrite Heq' in H3; apply H3; auto.
*** apply beq_nat_true in Hmem'; rewrite Hmem' in *; split.
**** apply root_member.
**** pose proof (split_is_conservative_present tan tbr) as H.
rewrite Heq' in H; apply right_member; apply H; auto.
*** intros Hmem; apply (member_property_concat_split) in Hmem.
case Hmem as [Hmem|Hmem].
**** assert (tree_ordered (Fork tbl tbn Htbl)) as Htblord. {
apply tree_ordered_compose; repeat split; auto.
pose proof (split_tree_ordered_preserves_left tan tbr Hr') as H'; rewrite Heq' in H'; auto.
apply tree_more_lower_bound; intros m' Hmemm'.
rewrite tree_more_lower_bound in Hltr'; apply Hltr'.
pose proof (split_is_conservative_left m' tan tbr) as H; rewrite Heq' in H.
apply H; auto.
}
pose proof (IHl _ Htblord Hmem) as [H1 H2]; split.
apply left_member; auto.
rewrite member_property_split in H2; case H2 as [H|[H|H]].
***** apply left_member; auto.
***** pose proof (split_is_conservative_left n tan tbr) as H'; rewrite Heq' in H'; apply right_member; apply H'; auto.
***** apply beq_nat_true in H; rewrite H in *; apply root_member.
**** assert (tree_ordered Htbr) as Htblord. {
pose proof (split_tree_ordered_preserves_right tan tbr Hr') as H'; rewrite Heq' in H'.
auto.
}
pose proof (IHr Htbr Htblord Hmem) as [H1 H2]; split.
apply right_member; auto.
pose proof (split_is_conservative_right n tan tbr) as H; rewrite Heq' in H.
apply right_member; apply H; auto.
Qed.
Theorem intersection_sound :
forall n ta tb,
tree_ordered ta -> tree_ordered tb ->
member n ta /\ member n tb -> member n (intersection ta tb).
Proof.
intros n ta tb Hta Htb [Htmem1 Htmem2];
generalize n Hta tb Htb Htmem2 Htmem1;
clear n tb Htb Hta Htmem1 Htmem2.
induction ta as [|tal IHtal tan tar IHtar].
- intros n _ tb _ _ H; inversion H.
- intros n Hordf tb Hordtb Htb; rewrite member_property_split.
pose proof (tree_ordered_decompose _ _ _ Hordf) as [Hfl [Hfr [Hfltl Hfltr]]].
pose proof (IHtal n Hfl) as IHl; clear IHtal.
pose proof (IHtar n Hfr) as IHr; clear IHtar.
intros [Htal|[Htal|Htal]].
* (* pose proof (IHl tb Hordtb Hmemtb Hmem) as H; generalize H; clear H; simpl. *)
(* intros Hmemi; pose proof (intersection_conservative _ _ _ Hfl Hordtb Hmemi) as [Htal Htb]. *)
destruct tb as[| tbl tbn tbr]; simpl; auto.
case_eq (Nat.compare tan tbn); intros Hcomp.
** rewrite member_property_split in Htb; case Htb as [Htb|[Htb|Htb]].
*** pose proof (tree_ordered_decompose _ _ _ Hordtb) as [Htbl [Htbr [Htbltl Htbltr]]].
pose proof (IHl tbl Htbl Htb Htal); apply left_member; auto.
*** pose proof (tree_ordered_decompose _ _ _ Hordtb) as [Htbl [Htbr [Htbltl Htbltr]]].
rewrite tree_less_upper_bound in Hfltl.
rewrite tree_more_lower_bound in Htbltr.
pose proof (Hfltl n Htal) as H; generalize H; clear H.
pose proof (Htbltr n Htb) as H; generalize H; clear H.
apply nat_compare_eq in Hcomp; rewrite Hcomp in *; lia.
*** apply nat_compare_eq in Hcomp; rewrite Hcomp in *.
apply beq_nat_true in Htb; rewrite Htb in *; apply root_member.
** rewrite member_property_split in Htb; case Htb as [Htb|[Htb|Htb]].
*** pose proof (split_preserves_membership n tan tbl Htb) as H; generalize H; clear H.
case_eq (split tan tbl); intros [xl xp] xr Hspl.
intros [Hmem'|[Hmem'|Hmem']].
**** assert (tree_ordered xl) as Hord'. {
pose proof (tree_ordered_decompose _ _ _ Hordtb) as [Htbl [Htbr [Htbltl Htbltr]]].
pose proof (split_tree_ordered_preserves_left tan tbl Htbl) as H'; rewrite Hspl in H'; auto.
}
pose proof (IHl xl Hord' Hmem' Htal).
destruct xp.
apply left_member; auto.
apply concat_preserves_membership_left; auto.
****
pose proof (tree_ordered_decompose _ _ _ Hordtb) as [Htbl [Htbr [Htbltl Htbltr]]].
pose proof (split_tree_ordered_right tan tbl Htbl) as H; rewrite Hspl in H.
apply nat_compare_lt in Hcomp.
rewrite tree_less_upper_bound in Hfltl; pose proof (Hfltl n Htal).
rewrite tree_more_lower_bound in H; pose proof (H n Hmem'); lia.
**** apply beq_nat_true in Hmem'; rewrite <- Hmem' in *; clear Hmem' tan.
destruct xp; try apply root_member.
pose proof (tree_ordered_decompose _ _ _ Hordtb) as [Htbl [Htbr [Htbltl Htbltr]]].
pose proof (split_is_sound_present n tbl) as Htmp; rewrite Hspl in Htmp.
pose proof (Htmp Htbl eq_refl Htb) as [].
*** pose proof (tree_ordered_decompose _ _ _ Hordtb) as [Htbl [Htbr [Htbltl Htbltr]]].
apply nat_compare_lt in Hcomp.
rewrite tree_less_upper_bound in Hfltl; pose proof (Hfltl n Htal).
rewrite tree_more_lower_bound in Htbltr; pose proof (Htbltr n Htb).
lia.
*** apply nat_compare_lt in Hcomp.
pose proof (tree_ordered_decompose _ _ _ Hordtb) as [Htbl [Htbr [Htbltl Htbltr]]].
rewrite tree_less_upper_bound in Hfltl; pose proof (Hfltl n Htal).
apply beq_nat_true in Htb.
lia.
** rewrite member_property_split in Htb; case Htb as [Htb|[Htb|Htb]].
*** case_eq (split tan tbr); intros [xl xp] xr Hspl.
assert (tree_ordered (Fork tbl tbn xl)) as Hordfk. {
pose proof (tree_ordered_decompose _ _ _ Hordtb) as [Htbl [Htbr [Htbltl Htbltr]]].
apply tree_ordered_compose; repeat split; auto.
pose proof (split_tree_ordered_preserves_left tan tbr Htbr) as H; rewrite Hspl in H; auto.
pose proof (split_tree_ordered_right tan tbr Htbr) .
apply tree_more_lower_bound; intros m Hm.
pose proof (split_is_conservative_left m tan tbr) as H0; rewrite Hspl in H0.
pose proof (H0 Hm) as H'; clear H0.
rewrite tree_more_lower_bound in Htbltr; pose proof (Htbltr m H').
auto.
}
pose proof (IHl (Fork tbl tbn xl) Hordfk (left_member _ _ _ _ Htb) Htal).
destruct xp.
apply left_member; auto.
apply concat_preserves_membership_left; auto.
*** pose proof (tree_ordered_decompose _ _ _ Hordtb) as [Htbl [Htbr [Htbltl Htbltr]]].
pose proof (split_preserves_membership n tan tbr) as H; generalize H; clear H.
case_eq (split tan tbr); intros [l n'] r Hspl Htmp.
pose proof (Htmp Htb) as [H|[H|H]]; clear Htmp.
**** assert (tree_ordered (Fork tbl tbn l)) as Hmemfk. {
apply tree_ordered_compose; repeat split; auto.
pose proof (split_tree_ordered_preserves_left tan tbr Htbr) as Htmp;
rewrite Hspl in Htmp; auto.
apply tree_more_lower_bound; intros m Hm.
rewrite tree_more_lower_bound in Htbltr; apply Htbltr.
pose proof (split_is_conservative_left m tan tbr) as H'; rewrite Hspl in H'; apply H'; auto.
}
pose proof (IHl (Fork tbl tbn l) Hmemfk (right_member _ _ _ _ H) Htal).
destruct n'; try (apply left_member); try (apply concat_preserves_membership_left); auto.
**** pose proof (split_tree_ordered_right tan tbr Htbr) as H1; rewrite Hspl in H1.
rewrite tree_more_lower_bound in H1; pose proof (H1 n H).
rewrite tree_less_upper_bound in Hfltl; pose proof (Hfltl n Htal).
lia.
**** apply beq_nat_true in H; rewrite <- H in *.
rewrite tree_less_upper_bound in Hfltl; pose proof (Hfltl n Htal).
lia.
*** apply beq_nat_true in Htb; rewrite <- Htb in *; clear Htb.
apply nat_compare_gt in Hcomp.
(* pose proof (split_preserves_membership n tan tbr) as H; generalize H; clear H. *)
case_eq (split tan tbr); intros [l present] r Hspl.
assert (tree_ordered (Fork tbl n l)) as H. {
pose proof (tree_ordered_decompose _ _ _ Hordtb) as [Htbl [Htbr [Htbltl Htbltr]]].
apply tree_ordered_compose; repeat split; auto.
pose proof (split_tree_ordered_preserves_left tan tbr Htbr) as Htmp;
rewrite Hspl in Htmp; auto.
apply tree_more_lower_bound; intros m Hm.
rewrite tree_more_lower_bound in Htbltr; apply Htbltr.
pose proof (split_is_conservative_left m tan tbr) as H; rewrite Hspl in H; apply H; auto.
}
pose proof (IHl (Fork tbl n l) H (root_member _ _ _) Htal) as Hcon.
destruct present; try (apply left_member); try (apply concat_preserves_membership_left); auto.
* destruct tb as[| tbl tbn tbr]; simpl; auto.
case_eq (Nat.compare tan tbn); intros Hcomp.
** apply nat_compare_eq in Hcomp; rewrite Hcomp in *; clear Hcomp tan.
pose proof (tree_ordered_decompose _ _ _ Hordtb) as [Htbl [Htbr [Htbltl Htbltr]]]; auto.
rewrite member_property_split in Htb; case Htb as [Htb|[Htb|Htb]].
*** rewrite tree_more_lower_bound in Hfltr; pose proof (Hfltr n Htal).
rewrite tree_less_upper_bound in Htbltl; pose proof (Htbltl n Htb); lia.
*** apply right_member; apply IHr; auto.
*** apply beq_nat_true in Htb; rewrite Htb in *; apply root_member.
** apply nat_compare_lt in Hcomp.
case_eq (split tan tbl); intros [l present] r Heq.
pose proof (tree_ordered_decompose _ _ _ Hordtb) as [Htbl [Htbr [Htbltl Htbltr]]]; clear Hordtb; auto.
rewrite member_property_split in Htb; case Htb as [Htb|[Htb|Htb]].
*** assert (tree_ordered (Fork r tbn tbr)) as Hfkr. {
apply tree_ordered_compose; repeat split; auto.
pose proof (split_tree_ordered_preserves_right tan tbl Htbl) as Htmp; rewrite Heq in Htmp; auto.
apply tree_less_upper_bound; intros m Hmemm.
rewrite tree_less_upper_bound in Htbltl; apply Htbltl.
pose proof (split_is_conservative_right m tan tbl) as H; rewrite Heq in H; apply H; auto.
}
assert (member n (Fork r tbn tbr)) as Hmemfk. {
pose proof (split_preserves_membership n tan tbl Htb) as H; rewrite Heq in H.
case H as [H|[H|H]].
* pose proof (split_tree_ordered_left tan tbl Htbl) as H'; rewrite Heq in H'.
rewrite tree_more_lower_bound in Hfltr; pose proof (Hfltr n Htal).
rewrite tree_less_upper_bound in H'; pose proof (H' n H).
lia.
* apply left_member; auto.
* apply beq_nat_true in H; rewrite <- H in *; clear H tan.
rewrite tree_more_lower_bound in Hfltr; pose proof (Hfltr n Htal).
lia.
}
pose proof (IHr _ Hfkr Hmemfk Htal).
destruct present; try (apply right_member); try (apply concat_preserves_membership_right_strong); auto.
*** generalize Htbltr; intros H1; rewrite tree_more_lower_bound in H1; pose proof (H1 n Htb) as Htbn; clear H1.
generalize Hfltr; intros H1; rewrite tree_more_lower_bound in H1; pose proof (H1 n Htal) as Htan; clear H1.
assert (tree_ordered (Fork r tbn tbr)) as Hfkr. {
apply tree_ordered_compose; repeat split; auto.
pose proof (split_tree_ordered_preserves_right tan tbl Htbl) as Htmp; rewrite Heq in Htmp; auto.
apply tree_less_upper_bound; intros m Hmemm.
rewrite tree_less_upper_bound in Htbltl; apply Htbltl.
pose proof (split_is_conservative_right m tan tbl) as H; rewrite Heq in H; apply H; auto.
}
assert (member n (Fork r tbn tbr)) as Hmemfk. { apply right_member; auto. }
pose proof (IHr _ Hfkr Hmemfk Htal).
destruct present; try (apply right_member); try (apply concat_preserves_membership_right_strong); auto.
*** apply beq_nat_true in Htb; rewrite <- Htb in *; clear Htb tbn.
assert (tree_ordered (Fork r n tbr)) as Hfkr. {
apply tree_ordered_compose; repeat split; auto.
pose proof (split_tree_ordered_preserves_right tan tbl Htbl) as Htmp; rewrite Heq in Htmp; auto.
apply tree_less_upper_bound; intros m Hmemm.
rewrite tree_less_upper_bound in Htbltl; apply Htbltl.
pose proof (split_is_conservative_right m tan tbl) as H; rewrite Heq in H; apply H; auto.
}
assert (member n (Fork r n tbr)) as Hmemfk. { apply root_member; auto. }
pose proof (IHr _ Hfkr Hmemfk Htal).
destruct present; try (apply right_member); try (apply concat_preserves_membership_right_strong); auto.
** apply nat_compare_gt in Hcomp.
case_eq (split tan tbr); intros [l present] r Heq.
pose proof (tree_ordered_decompose _ _ _ Hordtb) as [Htbl [Htbr [Htbltl Htbltr]]]; clear Hordtb; auto.
generalize Hfltr; intros H1; rewrite tree_more_lower_bound in H1; pose proof (H1 n Htal) as Htan; clear H1.
rewrite member_property_split in Htb; case Htb as [Htb|[Htb|Htb]].
*** generalize Htbltl; intros H1; rewrite tree_less_upper_bound in H1; pose proof (H1 n Htb) as Htbn; clear H1.
lia.
*** generalize Htbltr; intros H1; rewrite tree_more_lower_bound in H1; pose proof (H1 n Htb) as Htbn; clear H1.
assert (tree_ordered r) as Hrord. {
pose proof (split_tree_ordered_preserves_right tan tbr Htbr) as H; rewrite Heq in H; auto.
}
assert (member n r) as Hmem. {
pose proof (split_preserves_membership n tan tbr Htb) as H; rewrite Heq in H.
case H as [H|[H|H]]; auto.
* pose proof (split_tree_ordered_left tan tbr Htbr) as H'; rewrite Heq in H'.
rewrite tree_less_upper_bound in H'; pose proof (H' n H).
lia.
* apply beq_nat_true in H; rewrite <- H in *; clear H tan.
rewrite tree_more_lower_bound in Hfltr; pose proof (Hfltr n Htal).
lia.
}
pose proof (IHr _ Hrord Hmem Htal).
destruct present; try (apply right_member); try (apply concat_preserves_membership_right_strong); auto.
*** apply beq_nat_true in Htb; rewrite <- Htb in *; clear Htb tbn. lia.
* apply beq_nat_true in Htal; rewrite <- Htal in *; clear Htal tan; simpl.
destruct tb as[| tbl tbn tbr]; simpl; auto.
case_eq (Nat.compare n tbn); intros Hcomp.
** apply root_member.
** case_eq (split n tbl); intros [l present] r Heq.
destruct present; try (apply root_member).
pose proof (tree_ordered_decompose _ _ _ Hordtb) as [Htbl [Htbr [Htbltl Htbltr]]]; clear Hordtb; auto.
apply nat_compare_lt in Hcomp.
rewrite member_property_split in Htb; case Htb as [Htb|[Htb|Htb]].
*** pose proof (split_is_sound_present n tbl) as H0; rewrite Heq in H0.
pose proof (H0 Htbl eq_refl Htb) as [].
*** rewrite tree_more_lower_bound in Htbltr; pose proof (Htbltr n Htb); lia.
*** apply beq_nat_true in Htb; rewrite <- Htb in *; clear Htb tbn; lia.
** case_eq (split n tbr); intros [l present] r Heq.
destruct present; try (apply root_member).
pose proof (tree_ordered_decompose _ _ _ Hordtb) as [Htbl [Htbr [Htbltl Htbltr]]]; clear Hordtb; auto.
apply nat_compare_gt in Hcomp.
rewrite member_property_split in Htb; case Htb as [Htb|[Htb|Htb]].
*** rewrite tree_less_upper_bound in Htbltl; pose proof (Htbltl n Htb); lia.
*** pose proof (split_is_sound_present n tbr) as H0; rewrite Heq in H0.
pose proof (H0 Htbr eq_refl Htb) as [].
*** apply beq_nat_true in Htb; rewrite <- Htb in *; clear Htb tbn; lia.
Qed.
Theorem intersection_main_property :
forall n ta tb,
tree_ordered ta -> tree_ordered tb ->
member n ta /\ member n tb <-> member n (intersection ta tb).
Proof.
intros n ta tb; split.
apply intersection_sound; auto.
apply intersection_conservative; auto.
Qed.