coq - 将要操作的数据与操作合理的证据分离

Question

我有一种列表，其头部和尾部必须在某种意义上“兼容”:

Inductive tag := A | B. (* Just an example *)

Inductive element : tag -> tag -> Set :=
  | AA : element A A
  | AB : element A B
  | BB : element B B. (* Also just an example *)

Inductive estack : tag -> tag -> Set :=
  | ENil  : forall     t,                              estack t t
  | ECons : forall r s t, element r s -> estack s t -> estack r t.

但是，我不是很喜欢这段代码，原因如下:

1. 它不是模块化的:临时列表数据构造器本质上与头部和尾部兼容的证明 - 标签相结合。
2. 它不利于代码重用:我不得不重新定义常用的列表函数(例如列表连接)并重新证明通常的列表定理(例如列表连接的结合性)。

我有一个不同的方法，它包括三个步骤:

1. 定义单一类型的标记元素(相对于一系列标记类型的元素):

   Inductive taggedElement := Tagged : forall t1 t2, element t1 t2 -> taggedElement.
   

2. 定义标记元素的任意(即有效或无效)列表的类型:

   Definition taggedElementStack := list taggedElement.
   

3. 将标记元素的有效列表定义为元组，其元素是标记元素的任意列表和元素与相邻元素兼容的证明

   (* I have no idea how to do this in Coq, hence the question!
    * 
    * I am going to use pseudomathematical notation. I am not well versed in either
    * mathematics or theoretical computer science, so please do not beat me with a
    * stick if I say something that is completely bogus!
    * 
    * I want to construct the type
    * 
    *     (tes : taggedElementStack, b : proof that P(tes) holds)
    * 
    * where P(tes) is a predicate that is only true when, for every sublist of tes,
    * including tes itself, the heads and tails are compatible.
    *)
   

我将如何在 Coq 中执行第三步？

Answer 1

看看你的estack，它做了什么？概括! element 只是一个关系(A -> A -> Set)，tag 只是一个Set。你得到了什么？

Inductive RTList {I : Set} (X : Rel I) : Rel I :=
  | RTNil  : forall {i : I}, RTList X i i
  | RTCons : forall {i j k : I},    X i j -> RTList X j k -> RTList X i k.

(Rel 只是一个定义 Rel I = I -> I -> Set。)

自反传递闭包! 是通用的、可重用的和模块化的。或者你会这么想。

我在 Coq 的库中找到的唯一实现是在 Coq.Relations.Relation_Operators 中，名为 clos_refl_trans , 不同的结构和锁定到 Prop (所有根据文档，没试过)。

您可能必须重新实现它或在某处找到一个库。至少，您只需执行一次(对于 Set、Prop 和 Type 最多执行三次)。

---

您的其他想法可能更难管理。看NoDup对于与您的描述相似的内容，您可以重用该模式。如果你真的想要那个。 NoDup使用 In ，这是一个检查元素是否在列表中的函数。上次尝试使用它时，我发现解决涉及 In 的证明要困难得多。你不能只是 destruct 但必须应用辅助引理，你必须小心地展开 $n 级别，折叠起来很困难等等。我建议除非真的有必要，否则你' d 最好坚持使用 Prop 的数据类型。