Search code examples
verifiable-c

Using sep_apply in a semax context with VST

Nika Pona asked this question on vst-user, and I have the same question:

I have a goal of the form semax _ PROP()LOCAL()SEP(a;b;c;d) and a lemma of the form a*c |-- k or a*c = k. How do I get form SEP(a;b;c;d) to SEP(k;b;d)?

I've fiddled around with the sep_apply tactic but so far I've failed to get it to apply in this context.

Solution

  • sep_apply should work, but you may need to fully instantiate the arguments of the lemma, e.g., sep_apply (my_lemma a c k)