After spending quite some time to automatically prove the field_compatible premise of Lemma field_at_app in all cases I found that this premise it is not required at all. The proof of the lemma runs through unmodified if the premise is removed as in:
Lemma field_at_app' {cs: compspecs}: forall sh t gfs1 gfs2 v v' p,
(* field_compatible t [] p -> *)
JMeq v v'
-> field_at sh t (gfs1++gfs2) v p = field_at sh (nested_field_type t gfs2) gfs1 v' (field_address t gfs2 p).
Proof.
intros.
rewrite !field_at_data_at.
rewrite (data_at_type_changeable sh
(nested_field_type t (gfs1 ++ gfs2))
(nested_field_type (nested_field_type t gfs2) gfs1) v v'); auto.
f_equal.
apply field_address_app.
symmetry; apply nested_field_type_nested_field_type.
Qed.
The premise is theoretically trivial to prove, but in practice requires a lot of book keeping, since it requires to prove something about the complete structure when reasoning about address arithmetic for a field - usually at this point the context is reduced such that information for the complete field is not available. Floyd asks the user to prove this upfront - which makes it hard to automate. I think this usually happens when a forward_call is done over arguments with nested structures.
After spending quite some time to automatically prove the
field_compatiblepremise ofLemma field_at_appin all cases I found that this premise it is not required at all. The proof of the lemma runs through unmodified if the premise is removed as in:The premise is theoretically trivial to prove, but in practice requires a lot of book keeping, since it requires to prove something about the complete structure when reasoning about address arithmetic for a field - usually at this point the context is reduced such that information for the complete field is not available. Floyd asks the user to prove this upfront - which makes it hard to automate. I think this usually happens when a forward_call is done over arguments with nested structures.