Inductive proposition for sublists in Coq

Question

I am struggling with coming up with a notion of sublist of a list, which is created by deleting elements in the list (so that the order is preserved). I need to come up with an inductive proposition that decides if l1 is a sublist of l2.

So far:

1. I know the empty list is a sublist of all lists.
2. All lists are sublists of themselves.
3. If it is known that l1 is a sublist of l2, then lists resulting from appending the same list to both l1 and l2 at the head or tail would result in the former being a sublist of the latter
4. Now is the hard part. How to provide evidence that a list like ["x";"y"] is a sublist of ["a";"x";"z";"y"]?

The syntax is something like Inductive Sublist {X : Type} : list X -> list X -> Prop := ..

Can someone please help me with it?

Answer 1

How would you do informally already? Using just your three rules. If you can't manage it means that you have perhaps a too complicated / incomplete definition.

I think instead of trying to think of all those complicated examples you could focus on your example(s) while keeping in mind how lists are constructed. Why is [ x ; y ] a sublist of [ a ; x ; y ; z ]? Because (without the head of the second list) [ x ; y ] is a sublist of [ x ; y ; z ], and that's because [ y ] is a sublist of [ y ; z ], which is because [] is a sublist of [ z ] which always holds.

Do you see a pattern?