coqで型のインスタンスを明示的に指定しない

Aug 21 2020

Coqを使って集合論を構築することに興味があります。setsメンバーが何であるかを指定せずに型を定義し、2つのセットをプロップにマッピングする関数を定義したい

Definition elem (s1 s1 : sets) : Prop.

次に、集合論仮説の公理を作成し、定理を(たとえば)として表現します。

Theorem : ZFC -> (forall s : sets, ~ elem s s).

ただし、上記の構文は機能しません。このアイデアはCoqで実行できるものですか?Coqでこの目標を達成するためのより良い方法はありますか?私はCoqに非常に慣れていないので、私が知らないこれを行う明白な方法がある場合はお詫び申し上げます。

回答

3 Li-yaoXia Aug 21 2020 at 21:13

定理に名前を付ける必要があります。そして、物事を仮定するために、とを使用ParameterしますAxiom(これは技術的には同じことを意味しますが、概念と事実を非公式に区別するために使用できます)。

Parameter set : Type.
Parameter elem : set -> set -> Prop.

Axiom set_extensionality : forall x y, (forall z, elem z x <-> elem z y) -> x = y.
(* etc. *)

比較するとDefinitionTheoremは、物事を定義および証明するために使用されます。ZFC公理を仮定すると、集合がそれ自体の要素ではないことを証明できます。Theoremコマンドは、(将来的には、それを参照するために使用される)最初の定理名を取ります。

Theorem no_self_elem : forall x, ~ elem x x.
Proof.
  (* tactics here. *)
Qed.