1

ID と構成を提供するクラスを定義しようとしています。他の便利なインスタンス (nil と連結を含むリスト; ID と合成との関係 ;-) ) に加えて、関数のインスタンスが必要です。

与えられた

Class Cat (C0 : Type) (C1 : C0 -> C0 -> Type) :=
  {   identity : forall a, C1 a a
  ;   compose : forall {a b c : C0}, C1 b c -> C1 a b -> C1 a c
  (*  snip: some laws  *)
  }.

のようなものを定義できるようにしたい

Instance Cat (->) := { ... }.

しかし、Coq の演算子はそのようには機能しません。最初->は表記だと思いLocate "_ -> _".ましたが、これはUnknown notation. ちょっとうまくいきfun a b => a -> bますが、後で型がおかしく見えます。

> Check (identity nat).
identity nat
     : (fun a b : Type => a -> b) nat nat

(同じことが にEval compute inも当てはまります。型を単純化していないようです。)より読みやすいidentity nat : nat -> nat. （現在、私がやっていることの型は読めなくなります。）

「生」を取得する方法、->または少なくともCoqにもっと良い型を与えるよう説得する方法はありますか?

補足: 私はInductive評価セマンティクスを表す多くの を構築しています。私の目標は、「通常の」プログラミング言語のサブセットを Coq にマッピングして戻し、セキュリティ制約を転送し、魔法をかけることです。私は同じことを異なるコンストラクターで何度も何度も証明することを余儀なくされています。これにより、一度だけ証明できるようになることを願っています。カテゴリはこれを抽象化する正しい方法だと思います。私が間違っている場合に備えて、このメモをここに含めます->。問題全体を回避するより良い方法があるかもしれません。

4

1 に答える 1

2

質問の一部しか答えられません。はandの->ような表記ではなく、パーサーに組み込まれています。構文はwhen is not free inと同等です (すべての状況で同等かどうかはわかりません。 で発生できない用途があり、 を使用する必要がある場合があります)。+exists{ ... | ... }foralla -> bforall x:a, bxbxb->

その理由は、関数の抽象化と適用、およびそれらの型の強化が Coq の基本であり、より原始的な概念から派生したものではないからです。fun、アプリケーション、->またはを直接いじることはできませんforall。これらはファーストクラスのオブジェクトではないためです。

そうは言っても、型クラスは、特にアプリケーションをいじる方法です。私はそれらに精通していないので、あなたがやろうとしていることを行う方法があるかどうかわかりません.

于 2012-08-31T15:10:24.957 に答える