Hi, I'm stuck with a proof and would very much appreciate if someone could point me in the right direction.
A: Type Q: Type ts: Transition_System Q A tr: Trace Q A q: Q Hc: is_trace_aux ts (start tr) (states tr) (labels tr) Hi: initial ts (start tr) H: In q (states tr) --------------------------- exists n : nat, ts |- start tr ~>^ n q
Intuitively, is_trace_aux is an inductive relation which means a given transition system has a trace
(start tr) -(labels tr)-> (states tr) -(labels tr)-> (states tr) -> ...
The goal says something similar: that from the start of the trace, we can take n steps to reach some state q, and we have to show this given H: that q is a state in the trace.
Informally this seems quite obvious, however I'm stuck trying to prove this formally.
in_splitgets us the fact that
(states tr) = l1 ++ (q :: l2)
(states tr), and using that as n via
exists (S (length (states tr)))..
I guess the problem is how to get the length n from an inductive relation that doesn't say anything about lengths.
The details don't really matter as I just need advice on the high-level approach, but full definitions are here: https://lara.epfl.ch/w/fv20/labs04, with this being
in_trace_reachable. I'm not from EPFL, just working through this on my own, to get familiar with transition system and simulation proofs. If anyone knows other introductory material on this topic I would also appreciate pointers.
in_split, I think you can do
exists (S (length l1)). At that point, I think you need to prove something analogous to
in_split but for
lemma 1: namely, for all
q0 qs1 qs2 ls,
is_trace_aux q0 (qs1 ++ qs2) ls implies
is_trace_aux q0 qs1 (firstn (length qs1) ls). This needs to be proven via a separate induction; a separate lemma is likely to be simpler to prove.
l1 ++ (q :: l2) = (l1 ++ [q]) ++ l2, so we can take
qs1 = l1 ++ [q].
Applying lemma 1 should get you something like
is_trace_aux ts (start tr) (l1 ++ [q]) (firstn (length (l1 ++ [q])) ls), where
length (l1 ++ [q]) = S (length l1).
to conclude, you need to prove lemma 2 by induction, saying that
forall ts q0 qs ls, is_trace_aux ts q0 qs ls -> ts |- q0 ~>^ (length qs) (last qs)
last from stdpp: https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/theories/list.v#L179; there might be something similar in the stdlib)
option, so make lemma 2
forall ts q0 q qs ls, is_trace_aux ts q0 (qs ++ [q]) ls -> ts |- q0 ~>^ (S (length qs)) q.
I haven’t checked all the details carefully so I wouldn’t be surprised by off-by-one errors.
this proof seems far from trivial so you probably should try to work out the details carefully enough on paper before you try convincing Coq of those — or at least when you get stuck
in particular, the above proof sketch does _not_ use a single induction on the goal you show.
Hi does not seem necessary here?
Thank you, I really appreciate the advice. Let me work through it and get back to you if I have any questions!
towokit928 has marked this topic as resolved.
Last updated: Feb 01 2023 at 11:04 UTC