coq에서 유형의 인스턴스를 명시 적으로 지정하지 않음

Question

Coq를 사용하여 집합 이론을 구성하는 데 관심이 있습니다. sets멤버가 무엇인지 지정하지 않고 유형을 정의하고 두 세트를 Prop에 매핑하는 함수 를 정의하고 싶습니다.

Definition elem (s1 s1 : sets) : Prop.

그런 다음 집합 이론 가설의 공리를 만들고 정리를 다음과 같이 표현합니다 (예 :

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

그러나 위의 구문은 작동하지 않습니다. 이 아이디어는 Coq에서 할 수있는 일입니까? Coq에서이 목표를 달성하는 더 좋은 방법이 있습니까? 저는 Coq을 처음 접했기 때문에이 일을하는 명백한 방법이 있는지 모르겠지만 사과드립니다.

Answer 1

정리에 이름을 붙여야합니다. 그리고 사물을 가정하려면 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. *)

비교, Definition그리고 Theorem정의하고 일을 증명하는 데 사용됩니다. ZFC 공리를 가정하면 세트가 그 자체의 요소가 아님을 증명할 수 있습니다. 이 Theorem명령은 정리 이름을 먼저 사용합니다 (향후 참조에 사용됨).

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