0

かなり単純な型階層を作成しようとしています。最小限の作業例を次に示します。

Record R0 : Type := {
  R0_S :> Type
}.

Record R1 : Type := {
  R1_S   : Type;
  op1    : R1_S -> R1_S
}.

Record R2 : Type := {
  R2_S   : Type;
  op2    : R2_S -> R2_S
}.

Record R12: Type := {
  R12_S   : Type;
  R12_op1 : R12_S -> R12_S;
  R12_op2 : R12_S -> R12_S
}.

Definition R1_0 (r1: R1) := (Build_R0 (R1_S r1)).
Coercion   R1_0 : R1 >-> R0.

Definition R2_0 (r2: R2) := (Build_R0 (R2_S r2)).
Coercion   R2_0 : R2 >-> R0.

Definition R12_1 (r12: R12) := (Build_R1 (R12_S r12) (R12_op1 r12)).
Coercion   R12_1 : R12 >-> R1.

Definition R12_2 (r12: R12) := (Build_R2 (R12_S r12) (R12_op2 r12)).
Coercion   R12_2 : R12 >-> R2.  (* Warning *)

その最後の強制により、次の警告が生成されます。

Ambiguous paths:
[R12_2; R2_0] : R12 >-> R0
[R12_2; R2_0; R0_S] : R12 >-> Sortclass
R12_2 is now a coercion

実際、R12to R0(またはSortclass) からの型強制は 2 つの異なるパスを取ることができます。そして、Coqが一般的なケースでこれを許可しない理由を理解しています. だって...どれが使われるの？

ただし、この場合、両方のパスによる強制がまったく同じR1_0 (R12_1 r12)であることを示すことができます。R2_0 (R12_2 r12)しかし、それでも、次の一見有効な公理を追加することはできません。

Parameter r12 : R12.
Parameter x : r12.
Axiom id1 : (op1 _ x) = x.  (* OK    *)
Axiom id2 : (op2 _ x) = x.  (* Error *)

質問:では、これで問題ないことを Coq に納得させる方法はありますか?

4

1 に答える 1

1

これで問題ないことを Coq に納得させる方法はないと思います。ただし、正規構造や型クラスなどの他の機能を使用することで、同様の効果を得ることができます。これは、例を型クラスで変換する方法です。たとえば、次のようになります。

Class R1 T :=
{
  op1 : T -> T
}.

Class R2 T :=
{
  op2 : T -> T
}.

Class R12 T `{R1 T} `{R2 T} :=
{}.

Section S.

Context T `{R12 T}.
Variable x : T.

Hypothesis id1 : op1 x = x.
Hypothesis id2 : op2 x = x.

End S.

classR12には独自のメソッドがありませんが、 type が と の両方のインスタンスである必要があることにT注意してください。これは道徳的に同じ結果になります。この宣言は、これらの要件のおかげで、Coq が and のインスタンスを自動的に想定することを強制します。R1R2ContextR1R2

編集：

クラスを追加してダイアグラムを完成させようとすると、R0型クラスの推論が失敗した結果、奇妙なエラーが発生する場合があります。1 つの解決策は、 in の自動一般化をオフにしてR12(つまり、逆引用符を削除して)、 と をR1同じインスタンスR2に基づくようにすることです。R0

Class R0 (T : Type) := {}.

Class R1 T `{R0 T} :=
{
  op1 : T -> T
}.

Class R2 T `{R0 T} :=
{
  op2 : T -> T
}.

Class R12 T `{R0 T} {r1:R1 T} {r2:R2 T} :=
{}.

Section S.

Context T `{R12 T}.
Variable x : T.

Hypothesis id1 : op1 x = x.
Hypothesis id2 : op2 x = x.

End S.

残念ながら、型クラスの推論はやや複雑であるため、なぜエラーが発生するのかについて、私には十分な説明がありません。ただ、以前のようなあいまいなパスは実際にはありませんので、最初に抱えていた問題とは関係ないと思います。

于 2013-06-03T14:54:01.253 に答える