From 4d542bc7eafadb16b845cf05d1eb4988eb55ed0f Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 20 Oct 2015 13:32:18 +0200 Subject: Updated PR by removing whitespaces. Bug 17450. --- lib/FSetAVLplus.v | 88 +++++++++++++++++++++++++++---------------------------- 1 file changed, 44 insertions(+), 44 deletions(-) (limited to 'lib/FSetAVLplus.v') diff --git a/lib/FSetAVLplus.v b/lib/FSetAVLplus.v index eab427be..f16805c6 100644 --- a/lib/FSetAVLplus.v +++ b/lib/FSetAVLplus.v @@ -65,7 +65,7 @@ Proof. - discriminate. - destruct (above_low_bound t1) eqn: LB; [destruct (below_high_bound t1) eqn: HB | idtac]. + (* in interval *) - exists t1; split; auto. apply Raw.IsRoot. auto. + exists t1; split; auto. apply Raw.IsRoot. auto. + (* above interval *) exploit IHm1; auto. intros [x' [A B]]. exists x'; split; auto. apply Raw.InLeft; auto. + (* below interval *) @@ -80,7 +80,7 @@ Lemma raw_mem_between_2: Proof. induction 1; simpl; intros. - inv H. -- rewrite Raw.In_node_iff in H1. +- rewrite Raw.In_node_iff in H1. destruct (above_low_bound x0) eqn: LB; [destruct (below_high_bound x0) eqn: HB | idtac]. + (* in interval *) auto. @@ -98,7 +98,7 @@ Theorem mem_between_1: mem_between s = true -> exists x, In x s /\ above_low_bound x = true /\ below_high_bound x = true. Proof. - intros. apply raw_mem_between_1. auto. + intros. apply raw_mem_between_1. auto. Qed. Theorem mem_between_2: @@ -138,9 +138,9 @@ Remark In_raw_elements_between_1: Proof. induction m; simpl; intros. - inv H. -- rewrite Raw.In_node_iff. +- rewrite Raw.In_node_iff. destruct (above_low_bound t1) eqn:LB; [destruct (below_high_bound t1) eqn: RB | idtac]; simpl in H. - + rewrite Raw.join_spec in H. intuition. + + rewrite Raw.join_spec in H. intuition. + left; apply IHm1; auto. + right; right; apply IHm2; auto. Qed. @@ -174,7 +174,7 @@ Proof. - inv H. - destruct (above_low_bound t1) eqn:LB; [destruct (below_high_bound t1) eqn: RB | idtac]; simpl in H. + rewrite Raw.join_spec in H. intuition. - apply above_monotone with t1; auto. + apply above_monotone with t1; auto. apply below_monotone with t1; auto. + auto. + auto. @@ -190,7 +190,7 @@ Proof. - auto. - rewrite Raw.In_node_iff in H1. destruct (above_low_bound x0) eqn:LB; [destruct (below_high_bound x0) eqn: RB | idtac]. - + rewrite Raw.join_spec. intuition. + + rewrite Raw.join_spec. intuition. + assert (X.eq x x0 \/ X.lt x0 x -> False). { intros. exploit below_monotone; eauto. congruence. } intuition. elim H7. apply g. auto. @@ -204,7 +204,7 @@ Theorem elements_between_iff: In x (elements_between s) <-> In x s /\ above_low_bound x = true /\ below_high_bound x = true. Proof. intros. unfold elements_between, In; simpl. split. - intros. split. apply In_raw_elements_between_1; auto. eapply In_raw_elements_between_2; eauto. + intros. split. apply In_raw_elements_between_1; auto. eapply In_raw_elements_between_2; eauto. intros [A [B C]]. apply In_raw_elements_between_3; auto. apply MSet.is_ok. Qed. @@ -254,24 +254,24 @@ Lemma raw_for_all_between_1: pred x = true. Proof. induction 1; simpl; intros. -- inv H0. +- inv H0. - destruct (above_low_bound x0) eqn: LB; [destruct (below_high_bound x0) eqn: HB | idtac]. + (* in interval *) destruct (andb_prop _ _ H1) as [P C]. destruct (andb_prop _ _ P) as [A B]. clear H1 P. inv H2. - * erewrite pred_compat; eauto. + * erewrite pred_compat; eauto. * apply IHbst1; auto. * apply IHbst2; auto. + (* above interval *) inv H2. - * assert (below_high_bound x0 = true) by (apply below_monotone with x; auto). + * assert (below_high_bound x0 = true) by (apply below_monotone with x; auto). congruence. * apply IHbst1; auto. * assert (below_high_bound x0 = true) by (apply below_monotone with x; auto). congruence. + (* below interval *) inv H2. - * assert (above_low_bound x0 = true) by (apply above_monotone with x; auto). + * assert (above_low_bound x0 = true) by (apply above_monotone with x; auto). congruence. * assert (above_low_bound x0 = true) by (apply above_monotone with x; auto). congruence. @@ -290,7 +290,7 @@ Proof. + (* in interval *) rewrite IHbst1. rewrite (H1 x). rewrite IHbst2. auto. intros. apply H1; auto. apply Raw.InRight; auto. - apply Raw.IsRoot. reflexivity. auto. auto. + apply Raw.IsRoot. reflexivity. auto. auto. intros. apply H1; auto. apply Raw.InLeft; auto. + (* above interval *) apply IHbst1. intros. apply H1; auto. apply Raw.InLeft; auto. @@ -303,7 +303,7 @@ Theorem for_all_between_iff: for_all_between s = true <-> (forall x, In x s -> above_low_bound x = true -> below_high_bound x = true -> pred x = true). Proof. unfold for_all_between; intros; split; intros. -- eapply raw_for_all_between_1; eauto. apply MSet.is_ok. +- eapply raw_for_all_between_1; eauto. apply MSet.is_ok. - apply raw_for_all_between_2; auto. apply MSet.is_ok. Qed. @@ -337,10 +337,10 @@ Remark In_raw_partition_between_1: Proof. induction m; simpl; intros. - inv H. -- destruct (raw_partition_between m1) as [l1 l2] eqn:LEQ; simpl in *. +- destruct (raw_partition_between m1) as [l1 l2] eqn:LEQ; simpl in *. destruct (raw_partition_between m2) as [r1 r2] eqn:REQ; simpl in *. destruct (above_low_bound t1) eqn:LB; [destruct (below_high_bound t1) eqn: RB | idtac]; simpl in H. - + rewrite Raw.join_spec in H. rewrite Raw.In_node_iff. intuition. + + rewrite Raw.join_spec in H. rewrite Raw.In_node_iff. intuition. + rewrite Raw.In_node_iff. intuition. + rewrite Raw.In_node_iff. intuition. Qed. @@ -351,10 +351,10 @@ Remark In_raw_partition_between_2: Proof. induction m; simpl; intros. - inv H. -- destruct (raw_partition_between m1) as [l1 l2] eqn:LEQ; simpl in *. +- destruct (raw_partition_between m1) as [l1 l2] eqn:LEQ; simpl in *. destruct (raw_partition_between m2) as [r1 r2] eqn:REQ; simpl in *. destruct (above_low_bound t1) eqn:LB; [destruct (below_high_bound t1) eqn: RB | idtac]; simpl in H. - + rewrite Raw.concat_spec in H. rewrite Raw.In_node_iff. intuition. + + rewrite Raw.concat_spec in H. rewrite Raw.In_node_iff. intuition. + rewrite Raw.join_spec in H. rewrite Raw.In_node_iff. intuition. + rewrite Raw.join_spec in H. rewrite Raw.In_node_iff. intuition. Qed. @@ -364,22 +364,22 @@ Lemma raw_partition_between_ok: Proof. induction 1; simpl. - split; constructor. -- destruct IHbst1 as [L1 L2]. destruct IHbst2 as [R1 R2]. - destruct (raw_partition_between l) as [l1 l2] eqn:LEQ; simpl in *. +- destruct IHbst1 as [L1 L2]. destruct IHbst2 as [R1 R2]. + destruct (raw_partition_between l) as [l1 l2] eqn:LEQ; simpl in *. destruct (raw_partition_between r) as [r1 r2] eqn:REQ; simpl in *. destruct (above_low_bound x) eqn:LB; [destruct (below_high_bound x) eqn: RB | idtac]; simpl. + split. apply Raw.join_ok; auto. - red; intros. apply l0. apply In_raw_partition_between_1. rewrite LEQ; auto. + red; intros. apply l0. apply In_raw_partition_between_1. rewrite LEQ; auto. red; intros. apply g. apply In_raw_partition_between_1. rewrite REQ; auto. apply Raw.concat_ok; auto. - intros. transitivity x. - apply l0. apply In_raw_partition_between_2. rewrite LEQ; auto. + intros. transitivity x. + apply l0. apply In_raw_partition_between_2. rewrite LEQ; auto. apply g. apply In_raw_partition_between_2. rewrite REQ; auto. + split. auto. apply Raw.join_ok; auto. - red; intros. apply l0. apply In_raw_partition_between_2. rewrite LEQ; auto. + red; intros. apply l0. apply In_raw_partition_between_2. rewrite LEQ; auto. + split. auto. apply Raw.join_ok; auto. @@ -397,11 +397,11 @@ Remark In_raw_partition_between_3: Proof. induction m; simpl; intros. - inv H. -- destruct (raw_partition_between m1) as [l1 l2] eqn:LEQ; simpl in *. +- destruct (raw_partition_between m1) as [l1 l2] eqn:LEQ; simpl in *. destruct (raw_partition_between m2) as [r1 r2] eqn:REQ; simpl in *. destruct (above_low_bound t1) eqn:LB; [destruct (below_high_bound t1) eqn: RB | idtac]; simpl in H. + rewrite Raw.join_spec in H. intuition. - apply above_monotone with t1; auto. + apply above_monotone with t1; auto. apply below_monotone with t1; auto. + auto. + auto. @@ -414,17 +414,17 @@ Remark In_raw_partition_between_4: Proof. induction 1; simpl; intros. - inv H. -- destruct (raw_partition_between l) as [l1 l2] eqn:LEQ; simpl in *. +- destruct (raw_partition_between l) as [l1 l2] eqn:LEQ; simpl in *. destruct (raw_partition_between r) as [r1 r2] eqn:REQ; simpl in *. destruct (above_low_bound x0) eqn:LB; [destruct (below_high_bound x0) eqn: RB | idtac]; simpl in H. - + simpl in H1. rewrite Raw.concat_spec in H1. intuition. + + simpl in H1. rewrite Raw.concat_spec in H1. intuition. + assert (forall y, X.eq y x0 \/ X.lt x0 y -> below_high_bound y = false). - { intros. destruct (below_high_bound y) eqn:E; auto. + { intros. destruct (below_high_bound y) eqn:E; auto. assert (below_high_bound x0 = true) by (apply below_monotone with y; auto). congruence. } simpl in H1. rewrite Raw.join_spec in H1. intuition. + assert (forall y, X.eq y x0 \/ X.lt y x0 -> above_low_bound y = false). - { intros. destruct (above_low_bound y) eqn:E; auto. + { intros. destruct (above_low_bound y) eqn:E; auto. assert (above_low_bound x0 = true) by (apply above_monotone with y; auto). congruence. } simpl in H1. rewrite Raw.join_spec in H1. intuition. @@ -438,23 +438,23 @@ Remark In_raw_partition_between_5: Proof. induction 1; simpl; intros. - inv H. -- destruct (raw_partition_between l) as [l1 l2] eqn:LEQ; simpl in *. +- destruct (raw_partition_between l) as [l1 l2] eqn:LEQ; simpl in *. destruct (raw_partition_between r) as [r1 r2] eqn:REQ; simpl in *. destruct (above_low_bound x0) eqn:LB; [destruct (below_high_bound x0) eqn: RB | idtac]; simpl in H. - + simpl. rewrite Raw.join_spec. inv H1. + + simpl. rewrite Raw.join_spec. inv H1. auto. - right; left; apply IHbst1; auto. + right; left; apply IHbst1; auto. right; right; apply IHbst2; auto. - + simpl. inv H1. + + simpl. inv H1. assert (below_high_bound x0 = true) by (apply below_monotone with x; auto). congruence. - auto. - assert (below_high_bound x0 = true) by (apply below_monotone with x; auto). + auto. + assert (below_high_bound x0 = true) by (apply below_monotone with x; auto). congruence. - + simpl. inv H1. + + simpl. inv H1. assert (above_low_bound x0 = true) by (apply above_monotone with x; auto). congruence. - assert (above_low_bound x0 = true) by (apply above_monotone with x; auto). + assert (above_low_bound x0 = true) by (apply above_monotone with x; auto). congruence. eauto. Qed. @@ -467,7 +467,7 @@ Remark In_raw_partition_between_6: Proof. induction 1; simpl; intros. - inv H. -- destruct (raw_partition_between l) as [l1 l2] eqn:LEQ; simpl in *. +- destruct (raw_partition_between l) as [l1 l2] eqn:LEQ; simpl in *. destruct (raw_partition_between r) as [r1 r2] eqn:REQ; simpl in *. destruct (above_low_bound x0) eqn:LB; [destruct (below_high_bound x0) eqn: RB | idtac]; simpl in H. + simpl. rewrite Raw.concat_spec. inv H1. @@ -476,11 +476,11 @@ Proof. destruct H2; congruence. left; apply IHbst1; auto. right; apply IHbst2; auto. - + simpl. rewrite Raw.join_spec. inv H1. + + simpl. rewrite Raw.join_spec. inv H1. auto. - right; left; apply IHbst1; auto. + right; left; apply IHbst1; auto. auto. - + simpl. rewrite Raw.join_spec. inv H1. + + simpl. rewrite Raw.join_spec. inv H1. auto. auto. right; right; apply IHbst2; auto. @@ -496,7 +496,7 @@ Theorem partition_between_iff_1: In x (fst (partition_between s)) <-> In x s /\ above_low_bound x = true /\ below_high_bound x = true. Proof. - intros. unfold partition_between, In; simpl. split. + intros. unfold partition_between, In; simpl. split. intros. split. apply In_raw_partition_between_1; auto. eapply In_raw_partition_between_3; eauto. intros [A [B C]]. apply In_raw_partition_between_5; auto. apply MSet.is_ok. Qed. @@ -506,7 +506,7 @@ Theorem partition_between_iff_2: In x (snd (partition_between s)) <-> In x s /\ (above_low_bound x = false \/ below_high_bound x = false). Proof. - intros. unfold partition_between, In; simpl. split. + intros. unfold partition_between, In; simpl. split. intros. split. apply In_raw_partition_between_2; auto. eapply In_raw_partition_between_4; eauto. apply MSet.is_ok. intros [A B]. apply In_raw_partition_between_6; auto. apply MSet.is_ok. Qed. -- cgit