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.

ただし、次の理由から、このコードはあまり好きではありません。

モジュラーではありません: アドホックリストデータコンストラクターは、本質的に、先頭と末尾が互換性があるという証明 (タグ) と結合されています。
コードの再利用を好まない: 通常のリスト関数 (リスト連結など) を再定義し、通常のリスト定理 (リスト連結の結合性など) を再証明する必要があります。

私は、次の 3 つのステップからなる別のアプローチを念頭に置いています。

タグ付けされた要素の単一のタイプを定義する (タグ付けされたタイプの要素のファミリとは対照的に):
```
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 で 3 番目のステップを実行するにはどうすればよいですか?

coq - 操作が正当化されるという証拠から、操作されるデータを切り離す

1 に答える 1

Related

Reference