5

これは簡単な質問です。私はCoqが初めてです。

私は排他的な or in Coq を定義したいと思っています（私の知る限り、これは事前定義されていません）。重要な部分は、複数の命題 (Xor ABCD など) を許可することです。

次の 2 つのプロパティも必要です。

(Xor A1 A2 ... An)/\~A1 -> Xor A2... An
(Xor A1 A2 ... An)/\A1 -> ~A2/\.../\~An

現在、定義されていない数の変数に対して関数を定義するのに問題があります。2 つ、3 つ、4 つ、5 つの変数 (必要な数) に対して手動で定義しようとしました。しかし、プロパティを証明するのは苦痛であり、非常に非効率的です。

4

2 に答える 2

4

さて、2つの引数についてXorから始めて、そのプロパティを証明することをお勧めします。

次に、それを一般化したい場合は、引数のリストを使用してXorを定義できます。これを定義し、2引数のXorを使用してそのプロパティを証明できるはずです。

もう少し詳しく説明することもできますが、自分でやるほうが楽しいと思います。どうなるか教えてください:)。

于 2011-07-20T19:05:37.160 に答える
4

あなたの 2 番目のプロパティを考えると、排他的またはより高いアリティでのあなたの定義は、「これらの命題の正確に 1 つが真である」(「これらの命題の奇数個が真である」または「これらの命題の少なくとも 1 つが真であり、少なくとも 1 つは偽である」などの一般化の可能性があります)。

この排他的 or は結合プロパティではありません。つまり、アリティの高い xor を xor(A1,…,An)=xor(A1,xor(A2,…)) として定義することはできません。グローバル定義が必要です。これは、型コンストラクターが引数のリスト (または他のデータ構造ですが、リストが最も明白な選択肢です) を受け取る必要があることを意味します。

Inductive xor : list Prop -> Prop := …

ここで、合理的な選択肢が 2 つあります。第一原理から帰納的に xor の定義を作成するか、リスト述語を呼び出します。リストの述語は、「この述語に一致するリストに一意の要素があります」になります。標準リスト ライブラリはこの述語を定義しておらず、定義するのは xor を定義するよりも少し難しいため、帰納的に xor を構築します。

引数はリストなので、ケースを分類してみましょう:

  • 空のリストの xor は常に false です。
  • (cons A L)次の 2 つの条件のいずれかが満たされている場合 、リストの xorは true です。
    • A は真であり、L のどの要素も真ではありません。
    • A は false で、L の要素の 1 つだけが true です。

nandこれは、間違った命題のリストを特徴付ける、命題のリスト の補助述語を定義する必要があることを意味します。ここには多くの可能性があります:/\演算子を折りたたむ、手動で誘導する、またはリスト述語を呼び出す (これも標準リスト ライブラリにはありません)。手で導入しますが、折り畳み/\も合理的な選択です。

Require Import List.
Inductive nand : list Prop -> Prop :=
  | nand_nil : nand nil
  | nand_cons : forall (A:Prop) L, ~A -> nand L -> nand (A::L).
Inductive xor : list Prop -> Prop :=
  | xor_t : forall (A:Prop) L, A -> nand L -> xor (A::L)
  | xor_f : forall (A:Prop) L, ~A -> xor L -> xor (A::L).
Hint Constructors nand xor.

証明したいプロパティは、反転プロパティの単純な結果です: 構築された型が与えられた場合、可能性を分解します ( がある場合、それは aまたは axorのいずれかです)。これが最初の手動証明です。2番目は非常に似ています。xor_txor_f

Lemma xor_tail : forall A L, xor (A::L) -> ~A -> xor L.
Proof.
  intros. inversion_clear H.
    contradiction.
    assumption.
Qed.

必要になる可能性が高いプロパティの別のセットは、nandと 組み込みの接続詞の間の同等性です。nand (A::nil)例として、と同等の証明を次に示し~Aます。nand (A::B::nil)それが同等であることの証明~A/\~Bなどは、単に同じです。順方向では、これは再び反転プロパティです (nand型の可能なコンストラクターを分析します)。逆方向では、これはコンストラクターの単純なアプリケーションです。

Lemma nand1 : forall A, nand (A::nil) <-> ~A.
Proof.
  split; intros.
    inversion_clear H. assumption.
    constructor. assumption. constructor.
Qed.

また、ある時点で、置換および再配置のプロパティが必要になる可能性があります。以下に、証明したい重要な補題をいくつか示します (これらはそれほど難しいものではありません。適切なものを導入するだけです)。

  • forall A1 B2 L, (A1<->A2) -> (xor (A1::L) <-> xor (A2::L))
  • forall K L1 L2, (xor L1 <-> xor L2) -> (xor (K++L1) <-> xor (K++L2))
  • forall K A B L, xor (K++A::B::L) <-> xor (K::B::A::L)
  • forall K L M N, xor (K++L++M++N) <-> xor (K++M++L++N)
于 2011-07-21T01:24:31.080 に答える