proposition: Lemma initializing_inc_list_inc: forall size capacity, 0 <= size < capacity -> upd_Znth size (initializing_inc_list size capacity) (Vint (Int.repr size)) = initializing_inc_list (size + 1) capacity.
proof: Proof. unfold initializing_inc_list. intros. rewrite upd_Znth_app2. 1,2: rewrite Zlength_map, List_ext.nat_inc_list_Zlength. 2: rewrite (Zlength_default_val_array tuint); lia. rewrite Z2Nat.id. 2: lia. rewrite Z.sub_diag. apply List_ext.list_eq_Znth. rewrite Zlength_app, Zlength_app, Zlength_upd_Znth, Zlength_map, Zlength_map. rewrite (Zlength_default_val_array tuint), (Zlength_default_val_array tuint). rewrite List_ext.nat_inc_list_Zlength, List_ext.nat_inc_list_Zlength. 1,2,3: lia. rewrite Zlength_app, Zlength_upd_Znth, Zlength_map. rewrite List_ext.nat_inc_list_Zlength, (Zlength_default_val_array tuint). 2: lia. replace (Z.of_nat (Z.to_nat size) + (capacity - size)) with capacity by lia. intros. assert (i < size \/ size <= i) by lia. destruct H1. rewrite Znth_app1, Znth_app1. rewrite Znth_map, Znth_map. rewrite List_ext.nat_inc_list_i, List_ext.nat_inc_list_i. trivial. 5,6: rewrite Zlength_map. 3,4,5,6: rewrite List_ext.nat_inc_list_Zlength. 1,2,3,4,5,6: lia. rewrite Znth_app2. 1,2 : rewrite Zlength_map, List_ext.nat_inc_list_Zlength. 2: lia. assert (i = size \/ size < i) by lia. destruct H2. subst i. rewrite Znth_app1. rewrite Znth_map, List_ext.nat_inc_list_i, Z2Nat.id, Z.sub_diag, Znth_upd_Znth_same; trivial. 5: rewrite Zlength_map. 4,5: rewrite List_ext.nat_inc_list_Zlength. rewrite (Zlength_default_val_array tuint). 1,2,3,4,5,6: lia. rewrite Znth_app2. 1,2: rewrite Zlength_map, List_ext.nat_inc_list_Zlength. rewrite Znth_upd_Znth_diff. unfold default_val. simpl. unfold Zrepeat. rewrite Znth_repeat_inrange, Znth_repeat_inrange; trivial. all: lia. Qed.
imports: RelationClasses VST.floyd.proofauto CertiGraph.lib.List_ext CertiGraph.binheap.binary_heap_pro CertiGraph.binheap.binary_heap_malloc_spec CertiGraph.binheap.binary_heap_model CertiGraph.binheap.binary_heap_Zmodel