coq - Coq 中子列表的归纳命题

Question

我正在努力提出一个列表子列表的概念，它是通过删除列表中的元素创建的（以便保留顺序）。我需要提出一个归纳命题来确定 l1 是否是 l2 的子列表。

至今：

1. 我知道空列表是所有列表的子列表。
2. 所有列表都是它们自己的子列表。
3. 如果已知 l1 是 l2 的子列表，则将相同列表附加到 l1 和 l2 的头部或尾部的列表将导致前者成为后者的子列表
4. 现在是困难的部分。如何提供证据证明 ["x";"y"] 之类的列表是 ["a";"x";"z";"y"] 的子列表？

语法类似于 Inductive Sublist {X : Type} : list X -> list X -> Prop := ..

有人可以帮我吗？

Answer 1

你会怎么做非正式的？仅使用您的三个规则。如果您无法管理，则意味着您的定义可能过于复杂/不完整。

我认为与其试图考虑所有那些复杂的示例，不如专注于您的示例，同时牢记列表的构建方式。为什么是[ x ; y ]一个子列表[ a ; x ; y ; z ]？因为（没有第二个列表的头部）[ x ; y ]是 的子列表[ x ; y ; z ]，那是因为[ y ]是 的子列表[ y ; z ]，这是因为[]是[ z ]始终成立的子列表。

你看到一个模式吗？