## Stream: Coq users

### Topic: ✔ Help with induction proof

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

• 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.

#### 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: Oct 03 2023 at 20:01 UTC