proposition: Lemma data_at_tarray_fold: forall sh n n1 p t (v v' v1 v2: list (reptype t)), 0 <= n1 <= n -> n <= Zlength v' -> v = sublist 0 n v' -> v1 = sublist 0 n1 v' -> v2 = sublist n1 n v' -> complete_legal_cosu_type t = true -> data_at sh (tarray t n1) v1 p * data_at sh (tarray t (n - n1)) v2 (offset_val (sizeof t * n1) p) |-- data_at sh (tarray t n) v p.
proof: Proof. intros. rewrite (split2_data_at_Tarray sh t n n1 v v' v1 v2); [|assumption..]. entailer!. unfold field_address0. rewrite if_true. - simpl nested_field_offset. entailer!!. - pose proof (field_compatible_tarray_join n _ p _ H H4 H5 H7). clear -H1 H. red in H1. red. simpl in *. tauto. Qed.
imports: VST.veric.compcert_rmaps VST.msl.shares VST.msl.wand_frame VST.concurrency.conclib CertiGraph.lib.List_ext CertiGraph.msl_ext.log_normalize CertiGraph.msl_ext.ramification_lemmas CertiGraph.graph.graph_model CertiGraph.CertiGC.GCGraph CertiGraph.CertiGC.env_graph_gc CertiGraph.msl_ext.iter_sepcon Coq.Lists.List