Updated PR by removing whitespaces. Bug 17450.

1 files changed, 38 insertions, 38 deletions

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.