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.

- I know we need to somehow make use of H to get the length of the trace before q, so that we can supply that as n.
- Applying
`in_split`

gets us the fact that`(states tr) = l1 ++ (q :: l2)`

- I then tried induction on l1. However I then get stuck in the inductive case and don't know how to convert the IH into a form that is useful.
- I also tried induction on the trace
`(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.

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`

:

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.

and `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)`

(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)

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`

.

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.

also `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: Jun 16 2024 at 01:42 UTC