proposition: Lemma swim1_hO: forall L j, weak_heapOrdered2 L j -> match swim1 L j with | (L', None) => heapOrdered L' | (L', Some j') => weak_heapOrdered2 L' j' end.
proof: Proof. intros. unfold swim1. case_eq (j <=? root_idx); intro. rewrite Nat.leb_le in H0. destruct j. apply weak_heapOrdered2_root. trivial. inversion H0. rename H0 into Hx. case_eq (nth_error L j); case_eq (nth_error L (parent j)); intros. + case (a0 <<=? a). - split; repeat intro. * rename j into child. remember (parent child) as root. rename a into rootval. rename a0 into childval. case (eq_nat_dec i child); intro. ++ subst i. rewrite nth_error_exchange in H3; try (apply nth_error_Some; congruence). rewrite H0 in H3. inversion H3. subst b. clear H3. rewrite <- Heqroot in H4. rewrite nth_error_exchange' in H4; try (apply nth_error_Some; congruence). rewrite H1 in H4. inversion H4. subst a2. trivial. ++ rewrite nth_error_exchange'' in H3; auto. destruct (eq_nat_dec (parent i) root). -- rename i into sibling. rewrite e in H4. rewrite nth_error_exchange' in H4; try (apply nth_error_Some; congruence). rewrite H1 in H4. inversion H4. subst a2. clear H4. destruct H. specialize (H sibling b n H3 rootval). rewrite e in H. specialize (H H0). transitivity rootval; auto. -- destruct (eq_nat_dec (parent i) child). rename i into grandchild. 2: destruct H; specialize (H i b n H3); rewrite nth_error_exchange'' in H4; auto. rewrite e in H4. rewrite nth_error_exchange in H4; try (apply nth_error_Some; congruence). rewrite H0 in H4. inversion H4. subst a2. clear H4. destruct H. rewrite Heqroot in H0. rewrite grandsOk_root in H4. eapply H4; eauto. apply Nat.leb_nle in Hx. lia. * apply Nat.leb_nle in Hx. assert (j > root_idx) by lia. assert (parent j < j) by (apply parent_dec; lia). assert (parent (parent j) < parent j) by (apply parent_dec; unfold root_idx in *; lia). rewrite nth_error_exchange'' in H6; try lia. case (eq_nat_dec j gs); intro. -- subst gs. rewrite nth_error_exchange in H5; try (apply nth_error_Some; congruence). destruct H. eapply H. 3: eapply H6. lia. trivial. -- assert (gs <> parent j). { intro. subst gs. lia. } rewrite nth_error_exchange'' in H5; auto. rewrite <- H4 in *. destruct H. transitivity a; eapply H. 2: apply H0. lia. trivial. 2: apply H5. lia. trivial. - rewrite hOhO2. repeat intro. destruct (eq_nat_dec i j). subst j. assert (E: a0 = b) by congruence. subst. assert (E: a1 = a) by congruence. subst. destruct (Aleq_linear a b); auto. contradiction. destruct H. apply H with i; auto. + assert (parent j <= j) by apply parent_le. destruct (nth_error_le _ _ _ H1 _ H2). congruence. + rewrite hOhO2. repeat intro. destruct H. apply H with i; auto. congruence. + rewrite hOhO2. repeat intro. destruct H. apply H with i; auto. congruence. Qed.
imports: Psatz List Arith.Div2 Even Relations RelationClasses PeanoNat Peano_dec Recdef Sorting Permutation Multiset