Отсутствие явного указания экземпляров типа в coq

Мне интересно попробовать свои силы в построении теории множеств с помощью Coq. Я хотел бы определить тип sets без указания его членов, а функцию, отображающую два набора в Prop

Definition elem (s1 s1 : sets) : Prop.

Затем я бы сформулировал аксиомы гипотез теории множеств и выразил теоремы как (например)

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

Однако приведенный выше синтаксис не работает. Можно ли реализовать эту идею в Coq? Есть ли лучший способ достичь этой цели в Coq? Я новичок в Coq, поэтому прошу прощения, если есть очевидный способ сделать это, которого я не знаю.


coq set-theory
person Abe    schedule 21.08.2020    source источник

Ответы (1)


arrow_upward
3
arrow_downward

Вам нужно дать названия теоремам. А для постулирования вещей используйте 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.
person Li-yao Xia    schedule 21.08.2020
comment
Большое тебе спасибо! - person Abe; 21.08.2020