I think that's perfectly acceptable for the trace monad (not using monad_eq). Did you gain an impression on whether it would be feasible to update monad_eq in a way that would make sense for the trace monad? It's not used that much in the main refinement proofs, so it wouldn't be big loss, but if the work sparked an insight, it'd be good to know.

I think it might be doable but it would be complicated.

The main issue is that for the nondet monad, equality can be nicely separated into in_monad style set membership and equality of the failure flag, both of which are resolved by rules we want anyway.

However, the trace monad version of in_monad only handles completed monad results, it doesn't say anything about the trace that leads to the result or about Failed or Incomplete results. My guess is that with lemmas about those as well then we could update monad_eq to work for the trace monad, but there's a good chance that that would end up being more effort than it saves.

Ok, we should definitely defer until we know we want this then, esp since monad_eq is not used that often.

Not sure if we did this before, but it'd be nice to have that triv_refinement is a partial order, i.e. reflexive, transitive, and and antisymmetric. We could even instantiate it into the order class which would make a bunch of consequences of that available. Not that we are likely to need it much, but it'd be a nice setup.

Edit: let me retract the bit about the order class -- if we made it a class instance (if that even works for the type), we would be declaring < globally for programs. We don't really want that. What would make sense though, is interpreting the order locale for it. That should only make theorems available.

I'm also almost tempted to rename this into trace_refinement if that name is still available. Because it's not trivial at all, it is actually the classical version of refinement on traces (it's just not data refinement).

It's interesting that this doesn't fall out easily. It's one of the fundamental properties of refinement. We don't make explicit use of it, but it's a good sanity check and it could be a sign that our definition of data refinement is still a bit too complex. No need to resolve this in the short term, but maybe there is a tweak or two yet to be discovered that might make things easier in the future. (It's not unexpected that there would be side conditions since the type for programs is a lot tighter in the nondet monad, whereas for the trace monad there are many traces that don't really make sense as programs. So maybe it's just a reflection of that).

This was one of the things I tried to prove pretty early on in the process of working on all this, so it might be easier now that I have a better understanding of the prefix_refinement definition. I was sort of thinking to leave it though, until we have a chance to put more thought into how we want to handle failure. Currently it is very different to how corres handles it.

Having played around with this a bit more, it's actually a bit more complicated than I was previously thinking. The current definition allows us to show refinement between a non-failing abstract function and a failing concrete function, as long as all of the failing traces in the concrete function do not satisfy the rely.

It is almost definitely possible to resolve this, it will just require a bit of thought and possible some worked examples to find the nicest way off expressing things.

No need to do this now. As long as it's flagged we can do this at any time later.

Depends on how this is used. If it is used with instantiation, then having them separate is better. If it is used by matching against a current goal to extract P, then a single name is better. We could get both but providing two separate names and a lemmas statement for the collection.

It looks like the corres version is used both ways, so I've split this up and added lemmas prefix_refinement_gen_asms = ... like you suggested.

That would be really good to add to corres. We always unfold unless_def for no good reason.

same as above: good to add to corres

Good to remove this section -- even if they were easy to prove, it'd be better not to introduce this temptation for prefix refinement.

Could we want non-simp rules for use when the return relation is already instantiated?

It'd be better to provide the intro version of those. If those exist, then it doesn't harm to have the equality as well, but if we have only the equality, people will just use it with simp anyway.

It really should be using \<top>\<top>. Would it be hard to remove?

Very easy to remove, the only concern is that I'm not sure why it was added in the first place.

Esp as an input abbreviation, there is really no point introducing it -- maybe to make it look more familiar. I'd actually rather get rid of dc as well, it has been the source of much annoyance.