7

私の証明スクリプトは、矛盾する目標を解決するために使用する必要がある、nat = boolまたは のようなばかげた型の等価性を与えてくれます。nat = list unit

通常の数学では、これは些細なことです。与えられたセットbool := { true, false }と nat := { 0, 1, 2, ... }私はそれを知っていますtrue ∈ boolがtrue ∉ nat、したがってbool ≠ nat. Coqでは、それをどのように述べればよいかさえわかりませんtrue :̸ nat。

質問

これらの等式が偽であることを示す方法はありますか? それとも、それは不可能ですか？

(編集: 失敗した試行の長いリストを削除しましたが、履歴で引き続き表示できます。)

4

2 に答える 2

8

tl;dr カーディナリティ引数は、型が等しくないことを示す唯一の方法です。確かに、カーディナリティの引数をより効果的に自動化するには、少し熟考する必要があります。さらに先に進みたい場合は、ユニバースを構築して型に構文表現を与え、証明義務が型の意味的不等式ではなく、表現の構文的不等式として組み立てられるようにします。

等式としての同形

Coq の論理は、同形集合が命題的に等しいという公理と一致していると広く信じられています (そして、その証明がどこかにあるかもしれません) 。実際、これはウラジミール・ヴォエヴォツキーの「一価公理」の結果であり、人々は現在この公理をとても楽しんでいます。私が言わなければならないのは、(型ケースがない場合) 一貫性があることは非常にもっともらしいように思われ、任意の時点で必要な同形のコンポーネントを挿入することによって、等しい型間で値を何らかの方法で転送する計算解釈を構築できることです。

そのような公理が一貫していると仮定すると、型同型の存在を反駁するだけで、現状の論理における型の不等式が成り立つことがわかります。その結果、部分的な解決策は、少なくとも原則として、その場所にあります。列挙可能性は、非同型性を示す上でかなり重要です。のステータスがどうなるかnat = (nat -> nat)はわかりませんが、システムの外から見ると、 のすべての住民がnat -> nat正規形を持っており、数え切れないほど多くの正規形があることは明らかです。少なくとも、一貫した公理または反射原理があることはもっともらしいです。ロジックをより内向的にし、その仮説を検証します。

カーディナリティ引数の自動化

現在の状況を改善するためにあなたが取ることができる 2 つのステップを見ることができます。根本的ではない手順は、リフレクションをより適切に使用して、これらのカーディナリティ引数を作成するための一般的なテクノロジを改善することです。一般に、有限集合がより大きな集合とは異なることを示したいと考えているため、あなたはそうするのに理想的な立場にあります。DList Aの異なる要素のリストである の概念があるとしAます。網羅的 DList Aで長い 説明を作成できればDList B、反証できますA = B。

Induction-recursionによる DList の素敵な定義がありますが、Coq には Induction-Recursion がありません。幸いなことに、インデックスを慎重に使用することでシミュレートできる定義の 1 つです。非公式の構文を許してください。

Parameters
  A   : Set
  d   : A -> A -> bool
  dok : forall x y, d x y = true -> x = y -> False

それdは「明確」のためです。セットにすでに決定可能な平等がある場合は、d非常に簡単に装備できます。d大規模なセットには、あまり作業をせずに、目的に適したものを装備できます。実際、これが重要なステップです。SSReflect チームの知恵に従い、ドメインの小ささを利用してboolではなくPropを使用し、コンピューターに重い仕事を任せます。

では、いただきましょう

DListBody : (A -> bool) -> Set

ここで、インデックスはリストの鮮度テストです

dnil  : DListBody (const true)       (* any element is fresh for the empty list *)
dsnoc : forall f, (xs : DListBody f) -> (x : A) -> is_true (f x) ->
          DListBody (fun y => f y /\ d x y)

DListまた、必要に応じて、ラッピングをDListBody実存的に定義することもできます。おそらく、それは実際には必要な情報を隠しているのかもしれません。

Exhaustive (f : A -> bool)(mylist : DListBody f) = forall x : A, is_false (f x)

したがって、有限列挙の DListBody を書き留めることができれば、些細なサブゴールを使用したケース分析だけで、それが網羅的であることを証明できます。

その後、ピジョンホールの議論を 1 回行うだけで済みます。型間の同等性を反証したい場合 ( の適切な候補が既にあると仮定してd)、小さい方を徹底的に列挙し、大きい方から長いリストを示します。それだけです。

宇宙で働く

より根本的な代替案は、そもそもなぜこれらの目標を達成しているのか、そしてそれが本当にあなたが望んでいることを意味するのかを疑問視することです. 型とは、実際にはどのようなものであるべきでしょうか? その質問には複数の可能な答えがありますが、少なくともそれらが何らかの意味で「カーディナリティ」であることは明らかです。型をより具体的で構文的であると考えたい場合、それらが別個の構造によって構築されている場合は別個であると考えたい場合は、ユニバースで作業することにより、より具体的な表現を型に装備する必要がある場合があります。型の「名前」の帰納的なデータ型を定義し、名前を型としてデコードする手段とともに、名前の観点から開発を再構築します。名前の不等式は、通常のコンストラクターの識別に従っていることがわかります。

問題は、ここでも帰納再帰がサポートされていないため、Coq ではユニバースの構築が少しトリッキーになる可能性があることです。どのタイプを考慮する必要があるかによって大きく異なります。帰納的にいくつかを定義してU : Setから、再帰的なデコーダーを実装できるかもしれませんT : U -> Set。これは、単純な型の宇宙では確かにもっともらしいです。依存型のユニバースが必要な場合は、少し面倒です。最低でもこれくらいはできる

U : Type   (* note that we've gone up a size *)
NAT : U
PI : forall (A : Set), (A -> U) -> U

T : U -> Set
T NAT = nat
T (PI A B) = forall (a : A), T (B a)

ただし、 のドメインはではなく でPIエンコードされていないことに注意してください。帰納再帰アグダンはこれを乗り越え、定義と同時にSetUUT

U : Set   (* nice and small *)
NAT : U
PI : forall (A : U), (T A -> U) -> U   (* note the use of T *)

T : U -> Set
T NAT = nat
T (PI A B) = forall (a : T A), T (B a)

しかし、Coqにはそれがありません。繰り返しになりますが、回避策はインデックス作成を使用することです。ここでのコストはU必然的に大きくなります。

U : Set -> Type
NAT : U nat
PI : forall (A : Set)(B : A -> Set),
       U A -> (forall a, U (B a)) -> U (forall a, B a)

しかし、そのように構築された宇宙で多くのことを成し遂げることができます。たとえば、そのような宇宙に計算上有効な拡張等式を装備することができます。

于 2012-09-07T09:22:10.893 に答える
1

拡張部分解

参考までに、ここに の私の証明を示しnat = bool -> Falseます。(かなり長いですが、この証明の一般的な構造を簡単に理解できれば幸いです。)

Goal nat = bool -> False.
  (* For any two types, if they are actually identical, the identity is an
     isomorphism. *)
  assert (forall (T U : Set), T = U ->
              exists (f : T -> U) (g : U -> T),
              (forall t, (g (f t)) = t) /\ (forall u, (f (g u)) = u))
          as Hiso
  by (intros T U H; rewrite H; exists (@id U); exists (@id U);
          split; intro; reflexivity).
  (* our nat = bool *)
  intro HC.
  (* combining the facts gives an iso between nat and bool *)
  pose proof (Hiso nat bool HC); clear HC Hiso.
  inversion H as [phi [phi_inv [Hl Hr]]]; clear H Hr.
  (* this breaks because ||bool|| = 2 while ||nat|| > 2 -- we get collisions *)
  assert (forall m n o,
              phi m = phi n \/ phi n = phi o \/ phi m = phi o)
   by (intros m n o;
        case (phi m); case (phi n); case (phi o); clear; tauto).
  (* building the collision for 0, 1 and 2 *)
  pose proof (H 0 1 2) as HC; clear H.
  (* (false) identity preservation for 0, 1, 2 *)
  pose proof (Hl 0) as H0; pose proof (Hl 1) as H1;
  pose proof (Hl 2) as H2; clear Hl.
  (* case analysis on phi calls yields equalities on non-equal numbers... *)
  destruct (phi 0); destruct (phi 1); destruct (phi 2);
  (* ...rewriting leads to an equality '0 = 2' or '0 = 1' or '1 = 2'... *)
  try (rewrite H2 in H0); try (rewrite H1 in H0); try (rewrite H2 in H1);
  (* ...which can be used to solve by constructor inequality *)
  try inversion H0; inversion H1.
Qed.

ご覧のとおり、これは (自動化されたとしても) 大規模な有限型には実際には使用できません。項が大きすぎます。これに関する改善は素晴らしいでしょう。

于 2012-09-01T01:59:53.323 に答える