Remove duplicate of ko_at_kheap_upd_id#972
Conversation
michaelmcinerney
added
the
MCS
michaelmcinerney
force-pushed
the
michaelm-unbundle_lemma
branch
from
437ed41 to
86fb501
Compare
| by (wpsimp wp: update_sched_context_wp) | ||
| apply (wpsimp wp: update_sched_context_wp) | ||
| apply (clarsimp simp: ko_at_kheap_upd_id) | ||
| done |
There was a problem hiding this comment.
Would by (wpsimp wp: update_sched_context_wp simp: ko_at_kheap_upd_id) work?
There was a problem hiding this comment.
It does work. I am never sure where the dividing line should be between the wp steps and the simp steps. I guess it's pretty much harmless here. I think the case I'm thinking of is where we unfold low level things like obj_at within a wpsimp. If we're not upsetting the wp rules by performing the simp, I guess it should all just go in together. Is that right, or is there another reason?
There was a problem hiding this comment.
The main reason I would put it in here is that it was in there before -- when it was declared [simp] wpsimp was using it implicitly.
Generally I'd not put not too much into wpsimp if you have multiple steps anyway, but if you can turn the entire proof into a single method invocation without making it a monster, I would usually go for that.
| apply (wpsimp wp: update_sched_context_wp) | ||
| apply (simp add: ko_at_kheap_upd_id) | ||
| done |
There was a problem hiding this comment.
(same as the other location -- if we can put the simp rule directly into wpsimp, we can keep it a one-liner)
michaelmcinerney
force-pushed
the
michaelm-ko_at_kheap_upd_id
branch
from
80d8964 to
08c30b8
Compare
Remove duplicate of ko_at_kheap_upd_id, and since the duplicate was added to [simp], update proofs that require this rule to be locally added to simp. Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
michaelmcinerney
force-pushed
the
michaelm-ko_at_kheap_upd_id
branch
from
08c30b8 to
7c686e3
Compare
2 participants
No description provided.