towokit928 (Jan 02 2022 at 04:48): towokit928 (Jan 02 2022 at 04:48):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)[0]-> (states tr)[0] -(labels tr)[1]-> (states tr)[1] -> ...
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_split gets 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.
Paolo Giarrusso (Jan 02 2022 at 05:21):after 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 is_trace_aux:
Paolo Giarrusso (Jan 02 2022 at 05:22):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.
Paolo Giarrusso (Jan 02 2022 at 05:25):and l1 ++ (q :: l2) = (l1 ++ [q]) ++ l2, so we can take qs1 = l1 ++ [q].
Paolo Giarrusso (Jan 02 2022 at 05:30):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).
Paolo Giarrusso (Jan 02 2022 at 05:33):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)
Paolo Giarrusso (Jan 02 2022 at 05:33):(I’m using last from stdpp: https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/theories/list.v#L179; there might be something similar in the stdlib)
Paolo Giarrusso (Jan 02 2022 at 05:34):sorry, last returns 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.
Paolo Giarrusso (Jan 02 2022 at 05:35):I haven’t checked all the details carefully so I wouldn’t be surprised by off-by-one errors.
Paolo Giarrusso (Jan 02 2022 at 05:37):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
Paolo Giarrusso (Jan 02 2022 at 05:43):in particular, the above proof sketch does _not_ use a single induction on the goal you show.
Paolo Giarrusso (Jan 02 2022 at 05:48):also Hi does not seem necessary here?
towokit928 (Jan 03 2022 at 08:48):Thank you, I really appreciate the advice. Let me work through it and get back to you if I have any questions!
Notification Bot (Jan 03 2022 at 08:48):towokit928 has marked this topic as resolved.
Last updated: Apr 20 2024 at 10:02 UTC