proposition: Lemma body_pq_emp: semax_body Vprog (@Gprog size inf _) f_pq_emp (@pq_emp_spec size inf _).
proof: Proof. start_function. forward_for_simple_bound size (EX i : Z, PROP (@isEmpty inf (sublist 0 i priq_contents) = Vone) LOCAL (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. assert_PROP (Zlength priq_contents = size). { entailer!. repeat rewrite Zlength_map; auto. } forward; forward_if; forward; entailer!. + rewrite (isEmpty_in priq_contents (Znth i priq_contents)); trivial. 1: apply Znth_In; lia. pose proof (sublist.Forall_Znth _ _ i H3 H); simpl in H9. rewrite Int.signed_repr in H6; lia. + rewrite (sublist_split 0 i (i+1)); try lia. rewrite isEmpty_Vone_app; split; trivial. rewrite sublist_one; try lia. simpl. destruct (Z_lt_dec (Znth i priq_contents) (inf + 1)); trivial. exfalso. rewrite Int.signed_repr in H6; try lia. apply (sublist.Forall_Znth _ _ i H3) in H; simpl in H; rep_lia. - forward. entailer!. rewrite sublist_same in H3; trivial. 2: repeat rewrite Zlength_map; trivial. replace (Vint (Int.repr 1)) with Vone by now unfold Vone, Int.one. symmetry; trivial. Qed.
imports: VST.floyd.proofauto CertiGraph.lib.find_lemmas CertiGraph.priq.priq_arr_specs CertiGraph.priq.is_empty_lemmas CertiGraph.priq.priq_arr