proposition: Lemma sink1_hObU: forall L k j, weak_heapOrdered_bounded L k j -> match sink1 L j with | (L', None) => heapOrdered_bounded L' k | (L', Some j') => weak_heapOrdered_bounded L' k j' end.
proof: Proof. intros. unfold sink1. assert (Hy : j < left_child j) by apply left_child_inc. assert (Hw : left_child j < right_child j) by apply left_child_lt_right_child. case_eq (nth_error L j). * case_eq (nth_error L (left_child j)). + intros. assert (Hl : left_child j < length L) by (apply nth_error_Some; congruence). case_eq (nth_error L (right_child j)); intros. - assert (Hr: right_child j < length L) by (apply nth_error_Some; congruence). case (a1 <<=? a). 2: (destruct (Aleq_linear a1 a); try contradiction; intros _). ** case (a0 <<=? a1). 2: (destruct (Aleq_linear a0 a1); try contradiction; intros _). ++ repeat intro. case (eq_nat_dec i j). -- intro. subst j. rewrite H0, H2. rewrite H1 in H4. inversion H4. subst a4. clear H4. split; inversion 1; subst; auto. transitivity a1; auto. -- intro. destruct H. apply H; auto. ++ split; intros. -- case (eq_nat_dec i j); intro. *** subst j. rewrite nth_error_exchange in H6; try lia. rewrite nth_error_exchange'; try lia. rewrite nth_error_exchange''; try lia. rewrite H1, H0. rewrite H2 in H6. inversion H6. subst a3. clear H6. split; inversion 1; subst; auto. *** rewrite nth_error_exchange'' in H6; auto. assert (right_child i <> right_child j) by (intro Hq; apply right_child_inj in Hq; auto). destruct H. case (eq_nat_dec j (right_child i)); intro. +++ subst j. rewrite nth_error_exchange; try lia. rewrite H2. split. --- intro. rewrite nth_error_exchange''. intro. specialize (H i a3 H4 n H6). apply H in H9. trivial. generalize (left_child_lt_right_child i). lia. intro. eapply left_child_neq_right_child; eauto. --- inversion 1. subst c. clear H9. apply H8 with (right_child (right_child i)); auto. generalize (right_child_root i). unfold root_idx. lia. rewrite parent_right_child. unfold root_idx. lia. rewrite parent_right_child; auto. rewrite parent_right_child; auto. +++ split. 2: rewrite nth_error_exchange''; auto; apply H; auto. case (eq_nat_dec j (left_child i)); intro. --- subst j. rewrite nth_error_exchange; try lia. rewrite H2. inversion 1. subst b. clear H9. eapply H8. 4: apply H2. generalize (left_child_root i); unfold root_idx; lia. rewrite parent_left_child. trivial. rewrite parent_right_child. trivial. rewrite parent_left_child. trivial. --- rewrite nth_error_exchange''; auto. apply H; auto. generalize (left_child_neq_right_child i j). lia. -- repeat intro. rewrite parent_right_child in H8. rewrite nth_error_exchange in H8; try lia. rewrite H2 in H8. inversion H8. subst a3. clear H8. assert (parent gs < gs). { apply parent_dec. unfold root_idx. assert (gs = 0 \/ gs > 0) by lia. destruct H8; trivial. subst gs. change 0 with root_idx in H6. rewrite parent_root in H6. generalize (right_child_root j). lia. } rewrite nth_error_exchange'' in H7; try lia. destruct H. assert (right_child j <> j) by lia. rewrite parent_right_child in H5. assert (right_child j >= k) by (generalize (right_child_inc j); lia). specialize (H _ _ H11 H10 H2). destruct H. rewrite <- H6 in *. destruct (even_or_odd gs). apply H12. rewrite right_child_parent_even; auto. generalize (left_child_root j); intro. lia. apply H. rewrite left_child_parent_odd; auto. ** case (a0 <<=? a). 2: (destruct (Aleq_linear a0 a); try contradiction; intros _). ++ repeat intro. case (eq_nat_dec i j). -- intro. subst j. rewrite H0, H2. rewrite H1 in H5. inversion H5. subst a3. clear H5. split; inversion 1; subst; auto. transitivity a; auto. -- intro. destruct H. apply H; auto. ++ intros. split; intros. -- case (eq_nat_dec i j); intro. *** subst j. rewrite nth_error_exchange in H7; try lia. rewrite nth_error_exchange'; try lia. rewrite nth_error_exchange''; try lia. rewrite H1, H2. rewrite H0 in H7. inversion H7. subst a2. clear H7. split; inversion 1; subst; auto. *** rewrite nth_error_exchange'' in H7; auto. assert (left_child i <> left_child j) by (intro Hq; apply left_child_inj in Hq; auto). destruct H. case (eq_nat_dec j (left_child i)); intro. +++ subst j. rewrite nth_error_exchange; try lia. rewrite H0. split. --- inversion 1. subst b. clear H10. apply H9 with (left_child (left_child i)); auto. generalize (left_child_root i). lia. 1,2,3: rewrite parent_left_child; auto. --- intro. rewrite nth_error_exchange''. intro. eapply H; eauto. generalize (left_child_lt_right_child i). lia. apply left_child_neq_right_child. +++ rewrite nth_error_exchange''; auto. split. apply H; auto. case (eq_nat_dec j (right_child i)); intro. --- subst j. rewrite nth_error_exchange; try lia. rewrite H0. inversion 1. subst c. clear H10. eapply H9. 4: apply H0. generalize (right_child_root i); lia. 1,3: rewrite parent_right_child; auto. rewrite parent_left_child. trivial. --- rewrite nth_error_exchange''; auto. apply H; auto. apply left_child_neq_right_child. -- repeat intro. rewrite parent_left_child in H9. rewrite nth_error_exchange in H9; try lia. rewrite H0 in H9. inversion H9. subst a2. clear H9. assert (parent gs < gs). { apply parent_dec. unfold root_idx. assert (gs = 0 \/ gs > 0) by lia. destruct H9; trivial. subst gs. change 0 with root_idx in H7. rewrite parent_root in H7. generalize (left_child_root j). lia. } rewrite nth_error_exchange'' in H8; try lia. destruct H. assert (left_child j <> j) by lia. rewrite parent_left_child in H6. assert (left_child j >= k) by (generalize (left_child_inc j); lia). specialize (H _ _ H12 H11 H0). destruct H. rewrite <- H7 in *. destruct (even_or_odd gs). apply H13. rewrite right_child_parent_even; auto. generalize (left_child_root j); intro. lia. apply H. rewrite left_child_parent_odd; auto. - assert (Hr: right_child j >= length L) by (apply nth_error_None in H2; auto). case (a0 <<=? a); repeat intro. ** case (eq_nat_dec i j); intro. ++ subst j. rewrite H1 in H4. inversion H4. subst a2. clear H4. rewrite H0, H2. split; inversion 1. subst b. trivial. ++ destruct H. apply H; auto. ** split; intros. case (eq_nat_dec i j); intro. ++ subst j. rewrite nth_error_exchange in H5; try lia. rewrite nth_error_exchange'; try lia. rewrite nth_error_exchange_oob; try lia. rewrite H1. rewrite H0 in H5. inversion H5. subst a1. clear H5. split; intros; inversion H5. subst a0. destruct (Aleq_linear a b); trivial. contradiction. ++ rewrite nth_error_exchange'' in H5; auto. assert (left_child i <> left_child j) by (intro Hq; apply left_child_inj in Hq; auto). assert (left_child j <> right_child i) by apply left_child_neq_right_child. destruct H. specialize (H _ _ H3 n0 H5). split. -- case (eq_nat_dec j (left_child i)); intro. *** subst j. rewrite nth_error_exchange; try lia. rewrite H0. inversion 1. subst b. clear H9. assert (left_child i <> root_idx) by (generalize (left_child_root i); lia). assert (parent (left_child i) >= k) by (rewrite parent_left_child; auto). apply (H8 H9 H10 (left_child (left_child i))); try rewrite parent_left_child; auto. *** rewrite nth_error_exchange''; auto. destruct H. apply H. -- case (eq_nat_dec j (right_child i)); intro. *** subst j. rewrite nth_error_exchange; try lia. rewrite H0. inversion 1. subst c. clear H9. assert (right_child i <> root_idx) by (generalize (right_child_root i); lia). assert (parent (right_child i) >= k) by (rewrite parent_right_child; auto). eapply (H8 H9 H10 (left_child (right_child i))). rewrite parent_left_child. trivial. trivial. rewrite parent_right_child. trivial. *** rewrite nth_error_exchange''; auto. destruct H. apply H9. ++ repeat intro. rewrite parent_left_child in H7. rewrite nth_error_exchange in H7; try lia. rewrite H0 in H7. inversion H7. subst a1. clear H7. assert (parent gs < gs). { apply parent_dec. unfold root_idx. assert (gs = 0 \/ gs > 0) by lia. destruct H7; trivial. subst gs. change 0 with root_idx in H5. rewrite parent_root in H5. generalize (left_child_root j). lia. } rewrite nth_error_exchange'' in H6; try lia. assert (left_child j <> j) by lia. rewrite parent_left_child in H4. assert (left_child j >= k) by (generalize (left_child_inc j); lia). destruct H. specialize (H _ _ H9 H8 H0). destruct H. rewrite <- H5 in *. destruct (even_or_odd gs). apply H11. rewrite right_child_parent_even; auto. generalize (left_child_root j); intro. lia. apply H. rewrite left_child_parent_odd; auto. + repeat intro. case (eq_nat_dec i j); intro. 2: eapply H; auto. subst j. rewrite H1 in H3; inversion H3. subst a0. clear H3. split; intros. rewrite H0 in H3; inversion H3. apply nth_error_None in H0. assert (right_child i < length L) by (apply nth_error_Some; congruence). lia. * repeat intro. assert (i <> j). intro. subst. rewrite H0 in H2. discriminate. destruct H. eapply H; trivial. Qed.
imports: Psatz List Arith.Div2 Even Relations RelationClasses PeanoNat Peano_dec Recdef Sorting Permutation Multiset