Non specificare in modo esplicito le istanze di un tipo in coq

Question

Sono interessato a cimentarmi nella costruzione della teoria degli insiemi usando Coq. Vorrei definire un tipo setssenza specificare quali sono i suoi membri e una funzione che mappa due insiemi su una prop

Definition elem (s1 s1 : sets) : Prop.

Farei quindi ipotesi sugli assiomi della teoria degli insiemi ed esprimerei teoremi come (per esempio)

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

Tuttavia, la sintassi di cui sopra non funziona. Questa idea è qualcosa che può essere realizzata in Coq? C'è un modo migliore per raggiungere questo obiettivo in Coq? Sono molto nuovo in Coq, quindi mi scuso se c'è un modo ovvio per farlo che non conosco.

Answer 1

Devi dare nomi ai teoremi. E per postulare cose, usa Parameterand Axiom(che tecnicamente significa la stessa cosa ma puoi usare per distinguere informalmente tra concetti e fatti).

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. *)

In confronto, Definitione Theoremsono usati per definire e dimostrare le cose. Dopo aver postulato gli assiomi ZFC, puoi dimostrare che un insieme non è un elemento di per sé. Il Theoremcomando prende prima il nome di un teorema (usato per riferirsi ad esso in futuro):

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