proposition: Lemma unfold_lseg_neq (ls: listspec list_structid list_link list_token): forall P Q1 Q R (v v2: val) sh (s: list (elemtype ls)), PROPx P (LOCALx (Q1::Q) (SEPx (lseg ls sh s v v2 :: R))) |-- !! (ptr_neq v v2) -> PROPx P (LOCALx (Q1::Q) (SEPx (lseg ls sh s v v2 :: R))) |-- EX hryp: elemtype ls * list (elemtype ls) * val, match hryp with (h,r,y) => !! (s=h::r /\ is_pointer_or_null y) && PROPx P (LOCALx Q (SEPx (list_token sh v :: list_cell ls sh h v:: field_at sh list_struct (StructField list_link :: nil) (valinject (nested_field_type list_struct (StructField list_link :: nil)) y) v :: lseg ls sh r y v2 :: R))) end.
proof: Proof. intros. apply derives_trans with (PROPx P (LOCALx (Q1::Q) (SEPx (lseg_cons ls sh s v v2 :: R)))). apply derives_trans with (!! (ptr_neq v v2) && PROPx P (LOCALx (Q1::Q) (SEPx (lseg ls sh s v v2 :: R)))). apply andp_right; auto. intro rho; unfold PROPx,LOCALx,SEPx,local,tc_expr,tc_lvalue; unfold_lift; simpl. unfold lift1; simpl. repeat (apply derives_extract_prop; intro). rewrite prop_true_andp by auto. rewrite prop_true_andp by auto. apply sepcon_derives; auto. rewrite lseg_neq; auto. intro rho; unfold PROPx,LOCALx,SEPx,local,tc_expr,tc_lvalue,lift2,lift1,lift0; simpl. unfold_lift. unfold lseg_cons. simpl. apply derives_extract_prop; intro. apply derives_extract_prop; intros [? ?]. rewrite sepcon_andp_prop'. apply derives_extract_prop; intro. rewrite exp_sepcon1; apply exp_left; intro h. rewrite exp_sepcon1; apply exp_left; intro r. rewrite exp_sepcon1; apply exp_left; intro y. repeat rewrite sepcon_andp_prop'. apply derives_extract_prop; intros [? ?]. subst. apply exp_right with (h,r,y). repeat rewrite prop_true_andp by auto. repeat rewrite sepcon_assoc. auto. 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