proposition: Lemma body_popMin: semax_body Vprog (@Gprog size inf _) f_popMin (@popMin_spec size inf _).
proof: Proof. start_function. assert_PROP (Zlength priq_contents = size). { entailer!. repeat rewrite Zlength_map; auto. } assert (0 <= 0 < Zlength (map Int.repr priq_contents)). { rewrite Zlength_map. rewrite H4. lia. } forward. forward. forward_for_simple_bound size (EX i : Z, PROP () LOCAL (temp _minWeight (Vint (Int.repr (fold_right Z.min (Znth 0 priq_contents) (sublist 0 i priq_contents)))); temp _minVertex (Vint (Int.repr (find priq_contents (fold_right Z.min (Znth 0 priq_contents) (sublist 0 i priq_contents)) 0))); temp _size (Vint (Int.repr size)); temp _inf (Vint (Int.repr inf)); temp _pq pq) SEP (data_at Tsh (tarray tint size) (map Vint (map Int.repr priq_contents)) pq)). - entailer!. simpl. rewrite find_index. trivial. lia. simpl. unfold not. lia. - forward. assert (0 <= i < Zlength priq_contents) by lia. assert (Int.min_signed <= fold_right Z.min (Znth 0 priq_contents) (sublist 0 i priq_contents) <= Int.max_signed). { apply Forall_fold_min. - apply sublist.Forall_Znth; [lia|]. rewrite Forall_forall. intros. rewrite In_Znth_iff in H8. destruct H8 as [? [? ?]]. rewrite <- H9. pose proof (sublist.Forall_Znth _ _ x0 H8 H). simpl in H10. split; [lia|]. apply Z.le_trans with (m := inf + 1); lia. - rewrite Forall_forall. intros. rewrite In_Znth_iff in H8. destruct H8 as [? [? ?]]. rewrite <- H9. apply (Forall_sublist _ 0 i _) in H. apply (sublist.Forall_Znth _ _ _ H8) in H. simpl in H. split; [lia|]. apply Z.le_trans with (m := inf + 1); lia. } assert (Int.min_signed <= Znth i priq_contents <= Int.max_signed). { apply (sublist.Forall_Znth _ _ _ H7) in H; simpl in H. rep_lia. } forward_if. + forward. forward. entailer!. rewrite (sublist_split 0 i (i+1)) by lia. rewrite (sublist_one i (i+1) priq_contents) by lia. rewrite fold_min_another. rewrite Z.min_r; [|lia]. split; trivial. f_equal. rewrite find_index; trivial. apply min_not_in_prev; trivial. + forward. entailer!. rewrite (sublist_split 0 i (i+1)) by lia. rewrite (sublist_one i (i+1) priq_contents) by lia. rewrite fold_min_another. rewrite Z.min_l; [|lia]. split; trivial. - rewrite sublist_same; [|lia..]. assert (0 <= find priq_contents (fold_right Z.min (Znth 0 priq_contents) priq_contents) 0 < Zlength priq_contents). { apply find_range. apply min_in_list; [apply incl_refl | apply Znth_In; lia]. } forward. forward. Exists (find priq_contents (fold_right Z.min (hd 0 priq_contents) priq_contents) 0). entailer!. destruct priq_contents; simpl; auto. Qed.
imports: VST.floyd.proofauto CertiGraph.lib.find_lemmas CertiGraph.priq.priq_arr_specs CertiGraph.priq.is_empty_lemmas CertiGraph.priq.priq_arr