coq-contribs / zfc Goto Github PK
View Code? Open in Web Editor NEWAn encoding of Zermelo-Fraenkel Set Theory in Coq
License: GNU Lesser General Public License v2.1
An encoding of Zermelo-Fraenkel Set Theory in Coq
License: GNU Lesser General Public License v2.1
Contribution Rocq/ZF ==================== This directory contains: - An encoding of Zermelo-Fraenkel Set Theory in Coq Author & Date: Benjamin WERNER INRIA-Rocquencourt October 1996 Installation procedure: ----------------------- To get this contribution compiled, type make or make opt Which will compile the proof file. Description: ------------ The encoding of Zermelo-Fraenkel Set Theory is largely inspired by Peter Aczel's work dating back to the eighties. A type Ens is defined, which represents sets. Two predicates IN and EQ stand for membership and extensional equality between sets. The axioms of ZFC are then proved and thus appear as theorems in the development. A main motivation for this work is the comparison of the respective expressive power of Coq and ZFC. A non-computational type-theoretical axiom of choice is necessary to prove the replacement schemata and the set-theoretical AC. The main difference between this work and Peter Aczel's, is that propositions are defined on the impredicative level Prop. Since the definition of Ens is, however, still unchanged, I also added most of Peter Aczel's definition. The main advantage of Aczel's approach, is a more constructive vision of the existential quantifier (which gives the set-theoretical axiom of choice for free). Further information on this contribution: ----------------------------------------- See "The encoding of Zermelo-Fraenkel Set Theory in Coq", in the Proceedings of TACS'97.
I think that it is common now to use "exists" instead "EXType". Shall I rename it in the whole repository?
It is also possible to use "Defined." instead of "Qed."
https://gmalecha.github.io/reflections/2017/qed-considered-harmful
Will it be approved?
Due to uncertainty in using the raw (Ens->Prop) expression as a type of classes, I propose the next definition of the class with built-in soundness proof:
(* 'class' is the type of well-defined classes. *)
Record class := {
prty :> Ens->Prop;
sound : forall (a b : Ens), EQ a b -> (prty a <-> prty b);
}.
Definition EQC (A B:class) := forall z:Ens, A z <-> B z.
(* set to class *)
Definition stoc : Ens -> class.
Proof.
intro x.
unshelve eapply Build_class.
+ intro y. exact (IN y x).
+ intros a b aeqb. split.
- apply IN_sound_left. exact aeqb.
- apply IN_sound_left. apply EQ_sym. exact aeqb.
Defined.
Coercion stoc : Ens >-> class.
It is mentioned in the README that Peter Aczel's book was used. Which one so I can follow along?
According to
it is good practice to add "From ZFC " to every "Require Import", rename filename "Make" to "_CoqProject" everywhere, and deleting the first line "-R . ZFC".
By the way, usual name is "zfc", not "ZFC".
I think we may
a)change the name of github repository to "ZFC" (which is more reasonable variant, but something may go wrong, for example for my fork. Or may not.)
b)or change everywhere name to "zfc". "From zfc Require ...". (not very good solution, (a) is better).
Shall "make clean" command clean .aux files? It doesn't.
A declarative, efficient, and flexible JavaScript library for building user interfaces.
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. ๐๐๐
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google โค๏ธ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.