1

私はしばらくの間、問題に行き詰まりました。そのために、より小さなスタンドアロンの例を導き出しました。

Axiom f : nat -> Set.

Goal forall (n : nat) (e : n = n) (x : f n),
  match e in _ = _n return f _n -> Prop with
  | Logic.eq_refl => fun v : f n => v = x
  end x.

を実行しようとするとdestruct e、次のエラー メッセージが表示されます。

Error: Abstracting over the terms "n0" and "e" leads to a term
"fun (n0 : nat) (e : n0 = n0) =>
 forall x : f n0,
 match e in (_ = _n) return (f _n -> Prop) with
 | Logic.eq_refl => fun v : f n0 => v = x
 end x" which is ill-typed.

しばらく頭を悩ませた後、その用語で何がタイプミスなのか理解できませんでした...だから私はこれを試しました：

Definition illt :=
  fun (n : nat) (e : n = n) =>
  forall x : f n,
  match e in _ = _n return f _n -> Prop with
  | Logic.eq_refl => fun v : f n => v = x
  end x.

Coq は type でそれを受け入れますforall n : nat, n = n -> Prop。

では、このエラー メッセージの何が問題なのですか? また、最初の目標をどのように解決/微調整できますか?

ところで、これはすべてcoq8.3です。これが 8.4 で修正されたものである場合は、教えてください。申し訳ありません! :)

編集: Robin Green のコメントに対処するためSet Printing Allに、エラー メッセージのバージョンを次に示します。

Error: Abstracting over the terms "n0" and "e" leads to a term
"fun (n0 : nat) (e : @eq nat n0 n0) =>
 forall x : f n0,
 match e in (@eq _ _ _n) return (f _n -> Prop) with
 | eq_refl => fun v : f n0 => @eq (f n0) v x
 end x" which is ill-typed.

これは適切に型付けされた用語であり、暗黙的なものは何もありません。

4

1 に答える 1

3

問題の考えられる説明を次に示します。パターン マッチング構造を構築するときに何が起こるかは、定理を使用して説明することもできます。これが、あなたのケースで使用されている定理の私の見解です。

Check eq_rect.

eq_rect
 : forall (A : Type) (x : A) (P : A -> Type),
   P x -> forall y : A, x = y -> P y

したがって、等式でパターン マッチングを行う場合は、たまたま に等しいと証明できる任意の値 に対してパラメーター化された数式 P を提供する必要があります。直観的には、パターンマッチング式を で置き換えることができるはずですが、そこに表示されるプロパティ P は、Coq が推測できる範囲を超えています。これは、数式内の のすべての出現が in 型にバインドされており、単にのタイプになります。エラーメッセージにはそうは書かれていませんが、おそらく間違いです。yxapply eq_rectxf nf mm = n

証明を実行するには、等式の証明が特定のクラスの型で一意であり、natそのようなクラスに属しているという事実を使用することをお勧めします。これは Eqdep_dec ファイルで処理されます。

Require Eqdep_dec Arith.

これで、証明は非常に簡単に完了します。

Goal forall n (x : f n) (e : n = n),
  match e in _ = _n return f _n -> Prop with
  | Logic.eq_refl => fun v : f n => v = x
  end x.
intros n x e; replace e with (eq_refl n).
  reflexivity.
apply Eqdep_dec.UIP_dec, eq_nat_dec.
Qed.

さて、この解決策は物足りないと感じるかもしれません。これはどこUIP_decから来たのですか？UIP はID 証明の一意性を表しますが、残念ながら、このプロパティはすべての任意の型に対して保証されているわけではありません。これは、等しいことが決定可能である ( で表されるUIP_dec) すべての型で保証されます。たとえば、natです。

于 2013-02-18T18:14:19.193 に答える