proposition: Lemma harray_split: forall sh L1 L2 ptr, harray sh (L1 ++ L2) ptr = ((harray sh L1 ptr) * (harray sh L2 (field_address0 (tarray t_struct_edge (Zlength (L1 ++ L2))) [ArraySubsc (Zlength L1)] ptr)))%logic.
proof: Proof. intros. unfold harray. rewrite map_app. rewrite (split2_data_at_Tarray_app (Zlength L1) (Zlength (L1 ++ L2)) sh t_struct_edge (map heap_item_rep L1) (map heap_item_rep L2)). 2: rewrite Zlength_map; reflexivity. 2: rewrite Zlength_app, Zlength_map; lia. rewrite Zlength_app. replace (Zlength L1 + Zlength L2 - Zlength L1) with (Zlength L2) by lia. trivial. Qed.
imports: VST.floyd.proofauto Coq.ZArith.ZArith CertiGraph.floyd_ext.closed_lemmas CertiGraph.kruskal.kruskal_edgelist RelationClasses CertiGraph.binheap.binary_heap_model CertiGraph.binheap.binary_heap_Zmodel