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.

但是，我不太喜欢这段代码，原因如下：

它不是模块化的：ad-hoc 列表数据构造器本质上与头部和尾部兼容的证明 - 标记相结合。
它不利于代码重用：我被迫重新定义通常的列表函数（例如列表连接）并重新证明通常的列表定理（例如列表连接的关联性）。

我想到了一种不同的方法，它包括三个步骤：

定义单一类型的标记元素（而不是一系列标记类型的元素）：

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

定义标记元素的任意（即有效或无效）列表的类型：
```
Definition taggedElementStack := list taggedElement.
```

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

(* 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 中执行第三步？

score 2 · Accepted Answer

看看你的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 的库中找到的唯一实现是 in Coq.Relations.Relation_Operators、 named clos_refl_trans、不同的结构和锁定Prop（全部根据文档，没有尝试过）。

您可能必须重新实现它或在某个地方找到一个库。至少，您只需执行一次（或最多执行 3 次Set,Prop和Type）。

Your other idea will probably be harder to manage. Look at NoDup for something that's similar to your description, you might be able to reuse the pattern. If you really want that. NoDup uses In, which is a function that checks if an element is in a list. The last time I tried using it, I found it considerably harder to solve proofs involving In. You can't just destruct but have to apply helper lemmas, you have to carefully unfold exactly $n levels, folding back is hard etc. etc. I'd suggest that unless it's truly necessary, you'd better stick with data types for Props.

coq - 将要操作的数据与操作合理的证明脱钩

1 回答 1

Related

Reference