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:
- I know the empty list is a sublist of all lists.
- All lists are sublists of themselves.
- 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
- 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?
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?