Stream: Coq users

Topic: ✔ Help with induction proof


view this post on Zulip 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.

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.

view this post on Zulip 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:

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Jan 02 2022 at 05:25):

and l1 ++ (q :: l2) = (l1 ++ [q]) ++ l2, so we can take qs1 = l1 ++ [q].

view this post on Zulip 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).

view this post on Zulip 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)

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Jan 02 2022 at 05:48):

also Hi does not seem necessary here?

view this post on Zulip 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!

view this post on Zulip Notification Bot (Jan 03 2022 at 08:48):

towokit928 has marked this topic as resolved.


Last updated: Feb 01 2023 at 11:04 UTC