Coqに構文型の不等式を証明させるにはどうすればよいですか？
私はこの質問への答えを読みました。これは、一価性を仮定する場合、型の不等式を証明する唯一の方法はカーディナリティの引数を使用することであることを示唆しています。
私の理解では、Coqの論理が一価性と一致している場合、それは一価性の否定とも一致しているはずです。私はunivalenceの否定が本当にいることになることを得る一方で、いくつかの同型タイプは非同一である、私はいることを表現することが可能なはずであると信じていない（同一ではありません）同型タイプを同じです。
事実上、私はCoqに型と型コンストラクターを帰納的定義として扱いinversion、私の2つの非常に明確に異なる型は等しくないと言う典型的なスタイルの議論をしたいと思います。
それはできますか？これは次のようにする必要があります。
それは一貫性を保つのに十分弱いと私は思います。
私はポリモーフィックな判断（事実上、パラメーターを持つ帰納型forall X : Type, x -> Prop）を持っており、その選択Xは判断のコンストラクターによって決定されます。
X（たとえばX = nat）特定の選択に対するすべての判断について、いくつかのプロパティが保持されることを証明したいのですが、を使用しようとするとinversion、一部のコンストラクターはnat = string（たとえば）のような仮説を立てます。これらの型の同等性の仮説は、同じカーディナリティを持つタイプに対しても表示されるため、矛盾を生成するためにカーディナリティの引数を作成することはできません（そしてしたくありません）。
Inductive気になるタイプのクローズドワールドエンコーディングを作成し、それを上記の判断のポリモーフィック変数にする必要がありますか？
型の不等式を使用したい場合、あなたができる最善のことは、関心のある型のすべてのペアに対して公理を仮定することだと思います。
Axiom nat_not_string : nat <> string.
Axiom nat_not_pair : forall A B, nat <> A * B.
(* ... *)
Coqでは、帰納的に定義された型の名前について話す一流の方法がないので、単一の仮定でこの公理のファミリーを述べる方法があるべきではありません。当然、OCamlでCoqプラグインを記述して、帰納型が定義されるたびにこれらの公理を自動的に生成できる場合があります。しかし、必要な公理の数はタイプの数で二次関数的に増加するので、すぐに手に負えなくなると思います。
この場合、実際には、「考えられない」アプローチがおそらく最も便利です。
（Nit：「Coqの論理が一価性と一致している場合、それは一価性の否定とも一致している必要があります」。はい。ただし、Coqが一価性を証明できないためです。）
この記事はインターネットから収集されたものであり、転載の際にはソースを示してください。
侵害の場合は、連絡してください[email protected]
コメントを追加