proposition: Lemma list_append: forall {dsh psh: share} {ls : listspec list_structid list_link list_token} (hd mid tl:val) ct1 ct2 P, (forall tl', lseg_cell ls dsh psh (vund ls) tl tl' * P tl |-- FF) -> (lseg ls dsh psh ct1 hd mid) * lseg ls dsh psh ct2 mid tl * P tl|-- (lseg ls dsh psh (ct1 ++ ct2) hd tl) * P tl.
proof: Proof. intros. unfold lseg. revert hd; induction ct1; simpl; intros; auto. * normalize. * normalize. progress (autorewrite with subst norm1 norm2); normalize. apply exp_right with y. apply andp_right. + apply not_prop_right; intro. apply ptr_eq_e in H1; subst hd. clear IHct1. specialize (H y). unfold lseg_cell in H. rewrite prop_true_andp in H by auto. change (LsegGeneral.lseg ls dsh psh (map (fun v : val => (v, vund ls)) ct1)) with (lseg ls dsh psh ct1). change (LsegGeneral.lseg ls dsh psh (map (fun v : val => (v, vund ls)) ct2)) with (lseg ls dsh psh ct2). apply derives_trans with (lseg ls dsh psh ct1 y mid * lseg ls dsh psh ct2 mid tl * FF). cancel. auto. rewrite sepcon_FF; auto. + normalize. specialize (IHct1 y). clear H. do 2 rewrite sepcon_assoc. eapply derives_trans. apply sepcon_derives. apply derives_refl. rewrite <- !sepcon_assoc; eassumption. cancel. Qed.
imports: VST.floyd.base2 VST.floyd.client_lemmas VST.floyd.closed_lemmas VST.floyd.nested_pred_lemmas VST.floyd.nested_field_lemmas VST.floyd.efield_lemmas VST.floyd.mapsto_memory_block VST.floyd.reptype_lemmas VST.floyd.data_at_rec_lemmas VST.floyd.field_at VST.floyd.nested_loadstore VST.floyd.entailer