feat: add notion of finite execution for LTS #258
Conversation
|
There are lots of |
There was a problem hiding this comment.
Please include the beginning and ending states of ss among the arguments of LTS.IsExecution. That will make the statements of several theorems shorter and prettier. My personal preference of the argument order is:
lts.IsExecution s1 μs s2 ss
which makes LTS.IsExecution just an extension of LTS.MTr by one additional argument.
Also, this PR will interact with my PRs #241 and #249. So we need to figure out how they are sequenced.
| @[scoped grind =] | ||
| def LTS.IsExecution (lts : LTS State Label) | ||
| (ss : List State) (μs : List Label) : Prop := | ||
| ∃ hlen : ss.length = μs.length + 1, ∀ k, {valid : k < μs.length} → lts.Tr ss[k] μs[k] ss[k + 1] |
There was a problem hiding this comment.
My main comment about this definition is that the beginning state s1 and ending state s2 of ss should be among the arguments of LTS.IsExecution and the constraints ss[0] = s1 and ss[μs.length] = s2 should be included in this definition. The consequence of not doing so is that they have to be repeated again and again in the theorems I pointed out below. It is particularly ugly that the condition ss.length = μs.length + 1 has to be repeated several times below, only because it is needed to discharge the list indexing proof obligations.
Do we really need to give names hlen and valid to the two subexpressions? I've checked that replacing both by _ still works and I can't think of a use case where we actually need those names.
Also, is there any advantage in using {...} instead of (...) for _ : k < μs.length?
There was a problem hiding this comment.
hlen and valid are remnants of a previous version, removed.
Re the start and final states: I'm gonna try a bit to see if I can remove the disadvantage you mention without introducing start and final states in the signature. If possible, I'd like to keep the signature as close as possible to the omega-variant. The only reason for having them is formalisation convenience (which I agree shouldn't be sacrificed too much, but let's see..).
There was a problem hiding this comment.
The reason for {...} is to try and tell Lean that that part should be figured out automatically from the context. We can always revert it if we don't find it very useful.
Ah, now I remember, that one had a valid reason for being called valid (pun intended): it's so that we can instantiate it directly when necessary by using the (valid := ...) syntax.
There was a problem hiding this comment.
I view LTS.IsExecution as a natural extension of LTS.MTr that provides a witness to the execution path. There is no advantage in trying to shoehorn it to match LTS.IsOmegaExecution. It just creates more contorted code.
There was a problem hiding this comment.
Ah, but that (valid := ...) might not be too useful since it's not a formal param of the def... removed for now.
There was a problem hiding this comment.
Ah, seeing it as an extension of MTr kinda makes that signature more palatable to me for some reason. Ok, then, I'll add the params.
Btw, for memory, I've tried using head? and getLast? instead of indexes and it still feels like shoehorning.
|
I think it's pretty usable now and I've integrated the major comments, so we can discuss it again as a proper PR. |
This PR adds a notion of finite execution for LTS analogous to the infinite counterpart.