proposition: Lemma field_compatible_tarray_join: forall (n n1 : Z) (p : val) (t: type), 0 <= n1 <= n -> complete_legal_cosu_type t = true -> field_compatible (tarray t n1) [] p -> field_compatible (tarray t (n - n1)) [] (offset_val (sizeof t * n1) p) -> field_compatible (tarray t n) [] p.
proof: Proof. intros. unfold field_compatible. simpl. destruct H1 as [? [_ [? [? _]]]]. destruct H2 as [_ [_ [? [? _]]]]. destruct p; try contradiction. clear H1. simpl isptr. inv_int i. unfold size_compatible in *. simpl in H2. simpl sizeof in *. rewrite Z.max_r in * by lia. pose proof (Ctypes.sizeof_pos t). unfold sizeof in H2. remember (Ctypes.sizeof t) as S. rewrite ptrofs_add_repr in H2. rewrite Ptrofs.unsigned_repr in * by rep_lia. assert (0 <= ofs + S * n1 <= Ptrofs.max_unsigned). { destruct H, H6. split. 2: rep_lia. apply Z.add_nonneg_nonneg. 1: lia. apply Z.mul_nonneg_nonneg; lia. } rewrite Ptrofs.unsigned_repr in * by assumption. assert (forall i, ofs + S * n1 + S * (i - n1) = ofs + S * i). { intros. rewrite <- Z.add_assoc. rewrite <- Z.mul_add_distr_l. do 2 f_equal. lia. } rewrite H8 in H2. do 4 (split; auto). constructor. intros. unfold tarray in *. inversion H4; subst. 1: simpl in H10; inversion H10. inversion H5; subst. 1: simpl in H10; inversion H10. unfold sizeof in *. remember (Ctypes.sizeof t) as S. rewrite ptrofs_add_repr in H15. rewrite Ptrofs.unsigned_repr in * by rep_lia. assert (0 <= i < n1 \/ n1 <= i < n) by lia. destruct H10. 1: apply H14; assumption. assert (0 <= i - n1 < n - n1) by lia. specialize (H15 _ H11). rewrite H8 in H15. assumption. 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