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/Heaps.v | 76 ++++++++++++++++++++++++++++++------------------------------- 1 file changed, 38 insertions(+), 38 deletions(-) (limited to 'lib/Heaps.v') diff --git a/lib/Heaps.v b/lib/Heaps.v index 0ee07a58..65334a38 100644 --- a/lib/Heaps.v +++ b/lib/Heaps.v @@ -152,7 +152,7 @@ Lemma le_lt_trans: Proof. unfold le; intros; intuition. destruct (E.compare x1 x3). - auto. + auto. elim (@E.lt_not_eq x2 x3). auto. apply E.eq_trans with x1. apply E.eq_sym; auto. auto. elim (@E.lt_not_eq x2 x1). eapply E.lt_trans; eauto. apply E.eq_sym; auto. eapply E.lt_trans; eauto. @@ -163,7 +163,7 @@ Lemma lt_le_trans: Proof. unfold le; intros; intuition. destruct (E.compare x1 x3). - auto. + auto. elim (@E.lt_not_eq x1 x2). auto. apply E.eq_trans with x3. auto. apply E.eq_sym; auto. elim (@E.lt_not_eq x3 x2). eapply E.lt_trans; eauto. apply E.eq_sym; auto. eapply E.lt_trans; eauto. @@ -172,7 +172,7 @@ Qed. Lemma le_trans: forall x1 x2 x3, le x1 x2 -> le x2 x3 -> le x1 x3. Proof. - intros. destruct H. destruct H0. red; left; eapply E.eq_trans; eauto. + intros. destruct H. destruct H0. red; left; eapply E.eq_trans; eauto. red. right. eapply le_lt_trans; eauto. red; auto. red. right. eapply lt_le_trans; eauto. Qed. @@ -181,7 +181,7 @@ Lemma lt_heap_trans: forall x y, le x y -> forall h, lt_heap h x -> lt_heap h y. Proof. - induction h; simpl; intros. + induction h; simpl; intros. auto. intuition. eapply lt_le_trans; eauto. Qed. @@ -190,7 +190,7 @@ Lemma gt_heap_trans: forall x y, le y x -> forall h, gt_heap h x -> gt_heap h y. Proof. - induction h; simpl; intros. + induction h; simpl; intros. auto. intuition. eapply le_lt_trans; eauto. Qed. @@ -205,12 +205,12 @@ Proof. - tauto. - tauto. - rewrite e3 in *; simpl in *; intuition. -- intuition. elim NEQ. eapply E.eq_trans; eauto. +- intuition. elim NEQ. eapply E.eq_trans; eauto. - rewrite e3 in *; simpl in *; intuition. -- intuition. elim NEQ. eapply E.eq_trans; eauto. -- intuition. +- intuition. elim NEQ. eapply E.eq_trans; eauto. +- intuition. - rewrite e3 in *; simpl in *; intuition. -- intuition. elim NEQ. eapply E.eq_trans; eauto. +- intuition. elim NEQ. eapply E.eq_trans; eauto. - rewrite e3 in *; simpl in *; intuition. Qed. @@ -224,7 +224,7 @@ Proof. - rewrite e3 in *; simpl in *; tauto. - rewrite e3 in *; simpl in *; tauto. Qed. - + Lemma partition_gt: forall x pivot h, gt_heap h x -> gt_heap (fst (partition pivot h)) x /\ gt_heap (snd (partition pivot h)) x. @@ -249,18 +249,18 @@ Proof. - intuition. eapply lt_heap_trans; eauto. red; auto. eapply lt_heap_trans; eauto. red; auto. - eapply gt_heap_trans with y; eauto. red. left. apply E.eq_sym; auto. + eapply gt_heap_trans with y; eauto. red. left. apply E.eq_sym; auto. - rewrite e3 in *; simpl in *; intuition. eapply lt_heap_trans; eauto. red; auto. eapply gt_heap_trans with y; eauto. red; auto. -- intuition. +- intuition. eapply lt_heap_trans; eauto. red; auto. eapply gt_heap_trans; eauto. red; auto. -- intuition. eapply gt_heap_trans; eauto. red; auto. +- intuition. eapply gt_heap_trans; eauto. red; auto. - rewrite e3 in *; simpl in *. intuition. eapply lt_heap_trans with y; eauto. red; auto. eapply gt_heap_trans; eauto. red; auto. -- intuition. +- intuition. eapply lt_heap_trans with y; eauto. red; auto. eapply gt_heap_trans; eauto. red; auto. eapply gt_heap_trans with x; eauto. red; auto. @@ -275,16 +275,16 @@ Lemma partition_bst: bst (fst (partition pivot h)) /\ bst (snd (partition pivot h)). Proof. intros pivot h0. functional induction (partition pivot h0); simpl; try tauto. -- rewrite e3 in *; simpl in *. intuition. +- rewrite e3 in *; simpl in *. intuition. apply lt_heap_trans with x; auto. red; auto. generalize (partition_gt y pivot b2 H7). rewrite e3; simpl. tauto. -- rewrite e3 in *; simpl in *. intuition. +- rewrite e3 in *; simpl in *. intuition. generalize (partition_gt x pivot b1 H3). rewrite e3; simpl. tauto. generalize (partition_lt y pivot b1 H4). rewrite e3; simpl. tauto. - rewrite e3 in *; simpl in *. intuition. generalize (partition_gt y pivot a2 H6). rewrite e3; simpl. tauto. generalize (partition_lt x pivot a2 H8). rewrite e3; simpl. tauto. -- rewrite e3 in *; simpl in *. intuition. +- rewrite e3 in *; simpl in *. intuition. generalize (partition_lt y pivot a1 H3). rewrite e3; simpl. tauto. apply gt_heap_trans with x; auto. red; auto. Qed. @@ -294,8 +294,8 @@ Qed. Lemma insert_bst: forall x h, bst h -> bst (insert x h). Proof. - intros. - unfold insert. case_eq (partition x h). intros a b EQ; simpl. + intros. + unfold insert. case_eq (partition x h). intros a b EQ; simpl. generalize (partition_bst x h H). generalize (partition_split x h H). rewrite EQ; simpl. tauto. @@ -305,13 +305,13 @@ Lemma In_insert: forall x h y, bst h -> (In y (insert x h) <-> E.eq y x \/ In y h). Proof. intros. unfold insert. - case_eq (partition x h). intros a b EQ; simpl. + case_eq (partition x h). intros a b EQ; simpl. assert (E.eq y x \/ ~E.eq y x). destruct (E.compare y x); auto. right; red; intros. elim (E.lt_not_eq l). apply E.eq_sym; auto. destruct H0. tauto. - generalize (In_partition y x H0 h H). rewrite EQ; simpl. tauto. + generalize (In_partition y x H0 h H). rewrite EQ; simpl. tauto. Qed. (** Properties of [findMin] and [deleteMin] *) @@ -324,7 +324,7 @@ Opaque deleteMin. auto. tauto. tauto. - intuition. apply IHh. simpl. tauto. + intuition. apply IHh. simpl. tauto. Qed. Lemma deleteMin_bst: @@ -336,8 +336,8 @@ Proof. tauto. intuition. apply IHh. simpl; auto. - apply deleteMin_lt; auto. simpl; auto. - apply gt_heap_trans with y; auto. red; auto. + apply deleteMin_lt; auto. simpl; auto. + apply gt_heap_trans with y; auto. red; auto. Qed. Lemma In_deleteMin: @@ -347,16 +347,16 @@ Lemma In_deleteMin: Proof. Transparent deleteMin. intros y x h0. functional induction (deleteMin h0); simpl; intros. - discriminate. + discriminate. + inv H. tauto. inv H. tauto. - inv H. tauto. destruct _x. inv H. simpl. tauto. generalize (IHh H). simpl. tauto. Qed. Lemma gt_heap_In: forall x y h, gt_heap h x -> In y h -> E.lt x y. Proof. - induction h; simpl; intros. + induction h; simpl; intros. contradiction. intuition. apply lt_le_trans with x0; auto. red. left. apply E.eq_sym; auto. Qed. @@ -373,7 +373,7 @@ Proof. assert (le x x1). apply IHh1; auto. tauto. simpl. right; left; apply E.eq_refl. intuition. - apply le_trans with x1. auto. apply le_trans with x0. simpl in H4. red; tauto. + apply le_trans with x1. auto. apply le_trans with x0. simpl in H4. red; tauto. red; left; apply E.eq_sym; auto. apply le_trans with x1. auto. apply le_trans with x0. simpl in H4. red; tauto. red; right. eapply gt_heap_In; eauto. @@ -396,8 +396,8 @@ Opaque deleteMax. intros x h0. functional induction (deleteMax h0); simpl; intros. auto. tauto. - tauto. - intuition. apply IHh. simpl. tauto. + tauto. + intuition. apply IHh. simpl. tauto. Qed. Lemma deleteMax_bst: @@ -410,7 +410,7 @@ Proof. intuition. apply IHh. simpl; auto. apply lt_heap_trans with x; auto. red; auto. - apply deleteMax_gt; auto. simpl; auto. + apply deleteMax_gt; auto. simpl; auto. Qed. Lemma In_deleteMax: @@ -422,14 +422,14 @@ Transparent deleteMax. intros y x h0. functional induction (deleteMax h0); simpl; intros. congruence. inv H. tauto. - inv H. tauto. + inv H. tauto. destruct _x1. inv H. simpl. tauto. generalize (IHh H). simpl. tauto. Qed. Lemma lt_heap_In: forall x y h, lt_heap h x -> In y h -> E.lt y x. Proof. - induction h; simpl; intros. + induction h; simpl; intros. contradiction. intuition. apply le_lt_trans with x0; auto. red. left. apply E.eq_sym; auto. Qed. @@ -448,7 +448,7 @@ Proof. intuition. apply le_trans with x1; auto. apply le_trans with x0. red; right. eapply lt_heap_In; eauto. - simpl in H6. red; tauto. + simpl in H6. red; tauto. apply le_trans with x1; auto. apply le_trans with x0. red; auto. simpl in H6. red; tauto. @@ -511,8 +511,8 @@ Qed. Lemma findMin_empty: forall h y, findMin h = None -> ~In y h. Proof. - unfold findMin, In; intros; simpl. - destruct (proj1_sig h). + unfold findMin, In; intros; simpl. + destruct (proj1_sig h). simpl. tauto. exploit R.findMin_empty; eauto. congruence. Qed. @@ -540,8 +540,8 @@ Qed. Lemma findMax_empty: forall h y, findMax h = None -> ~In y h. Proof. - unfold findMax, In; intros; simpl. - destruct (proj1_sig h). + unfold findMax, In; intros; simpl. + destruct (proj1_sig h). simpl. tauto. exploit R.findMax_empty; eauto. congruence. Qed. -- cgit