From: Claudio Sacerdoti Coen Date: Thu, 7 Dec 2000 14:33:18 +0000 (+0000) Subject: Many files added. Symbolic links missing. examples and contrib missing due X-Git-Tag: nogzip~103 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5cc1f56f25e23f8132b578f9ad46ac9e27979cb4;p=helm.git Many files added. Symbolic links missing. examples and contrib missing due to lack of space --- diff --git a/helm/EXPORT/export_Utrecht_Ramsey/Makefile b/helm/EXPORT/export_Utrecht_Ramsey/Makefile new file mode 100644 index 000000000..2015d1755 --- /dev/null +++ b/helm/EXPORT/export_Utrecht_Ramsey/Makefile @@ -0,0 +1,11 @@ +all: objects theories + +objects: + coqc -R Ramsey Utrecht.Ramsey Ramsey/*.v + echo "Load Verbose prova_Utrecht_Ramsey." | ~/V7/bin/coqtop.byte -R Ramsey Utrecht.Ramsey + +theories: + ./exporttheories.sh + +clean: + rm -f *.vo Ramsey/*.vo diff --git a/helm/EXPORT/export_Utrecht_Ramsey/exporttheories.sh b/helm/EXPORT/export_Utrecht_Ramsey/exporttheories.sh new file mode 100755 index 000000000..b2dd5f8aa --- /dev/null +++ b/helm/EXPORT/export_Utrecht_Ramsey/exporttheories.sh @@ -0,0 +1,10 @@ +#!/bin/bash + +echo "Exporting theory $1"; + +for i in Ramsey/*.v + do + basename=$(basename $i | sed s/\\.v//) + cat $i | ../mktheory.pl "Utrecht/Ramsey/$basename" > \ + examples/Utrecht/Ramsey/$basename.theory.xml + done diff --git a/helm/EXPORT/export_Utrecht_Ramsey/prova_Utrecht_Ramsey.v b/helm/EXPORT/export_Utrecht_Ramsey/prova_Utrecht_Ramsey.v new file mode 100644 index 000000000..aa0500f15 --- /dev/null +++ b/helm/EXPORT/export_Utrecht_Ramsey/prova_Utrecht_Ramsey.v @@ -0,0 +1,5 @@ +Require Export Xml. + +Require Ramsey. + +Print XML Module Disk "examples" Ramsey. diff --git a/helm/EXPORT/exportcoq/Makefile b/helm/EXPORT/exportcoq/Makefile new file mode 100644 index 000000000..79c7463a0 --- /dev/null +++ b/helm/EXPORT/exportcoq/Makefile @@ -0,0 +1,7 @@ +all: objects theories + +objects: + echo "Load Verbose provacoq." | ~/V7/bin/coqtop.byte + +theories: + ./exporttheories.sh diff --git a/helm/EXPORT/exportcoq/export_contrib_theory.sh b/helm/EXPORT/exportcoq/export_contrib_theory.sh new file mode 100755 index 000000000..6ebb2ad28 --- /dev/null +++ b/helm/EXPORT/exportcoq/export_contrib_theory.sh @@ -0,0 +1,12 @@ +#!/bin/bash + +echo "Exporting theory $1"; + +for i in ~/V7/contrib/$1/*.v + do + basename=$(basename $i | sed s/\\.v//) + cat $i | ../mktheory.pl "Coq/$1/$basename" 0 > \ + examples/Coq/$1/$basename.theory.xml +# cat $i | ../mktheory.pl "Coq/$1/$basename" 1 > \ +# examples/Coq/$1/"$basename"_with_types.theory.xml + done diff --git a/helm/EXPORT/exportcoq/export_theory_theory.sh b/helm/EXPORT/exportcoq/export_theory_theory.sh new file mode 100755 index 000000000..d2e5442bd --- /dev/null +++ b/helm/EXPORT/exportcoq/export_theory_theory.sh @@ -0,0 +1,12 @@ +#!/bin/bash + +echo "Exporting theory $1"; + +for i in ~/V7/theories/$1/*.v + do + basename=$(basename $i | sed s/\\.v//) + cat $i | ../mktheory.pl "Coq/$1/$basename" 0 > \ + examples/Coq/$1/$basename.theory.xml +# cat $i | ../mktheory.pl "Coq/$1/$basename" 1 > \ +# examples/Coq/$1/"$basename"_with_types.theory.xml + done diff --git a/helm/EXPORT/exportcoq/exporttheories.sh b/helm/EXPORT/exportcoq/exporttheories.sh new file mode 100755 index 000000000..5fdc47378 --- /dev/null +++ b/helm/EXPORT/exportcoq/exporttheories.sh @@ -0,0 +1,17 @@ +#!/bin/bash + +./export_theory_theory.sh Arith +./export_theory_theory.sh Bool +./export_theory_theory.sh Init +./export_theory_theory.sh Lists +./export_theory_theory.sh Logic +./export_theory_theory.sh Reals +./export_theory_theory.sh Relations +./export_theory_theory.sh Sets +#./export_theory_theory.sh SORTING +#./export_theory_theory.sh TREES +./export_theory_theory.sh Wellfounded +./export_theory_theory.sh Zarith + +./export_contrib_theory.sh omega +./export_contrib_theory.sh ring diff --git a/helm/EXPORT/exportcoq/provacoq.v b/helm/EXPORT/exportcoq/provacoq.v new file mode 100644 index 000000000..99b52ebc7 --- /dev/null +++ b/helm/EXPORT/exportcoq/provacoq.v @@ -0,0 +1,14 @@ +Load Verbose provacoqArith. +Load Verbose provacoqBool. +Load Verbose provacoqInit. +Load Verbose provacoqLists. +Load Verbose provacoqLogic. +Load Verbose provacoqReals. +Load Verbose provacoqRelations. +Load Verbose provacoqSets. +(*Load Verbose provacoqSorting.*) +(*Load Verbose provacoqTrees.*) +Load Verbose provacoqZArith. + +Load Verbose provacoqcontribRing. +Load Verbose provacoqcontribOmega. diff --git a/helm/EXPORT/exportcoq/provacoqArith.v b/helm/EXPORT/exportcoq/provacoqArith.v new file mode 100644 index 000000000..1fdc4f943 --- /dev/null +++ b/helm/EXPORT/exportcoq/provacoqArith.v @@ -0,0 +1,31 @@ +Require Export Xml. + +Require Arith. +Require Compare. +Require Compare_dec. +(*Require Div.*) +Require Div2. +Require EqNat. +Require Euclid_def. +Require Euclid_proof. +Require Peano_dec. + +Print XML Module Disk "examples" Arith. +Print XML Module Disk "examples" Between. +Print XML Module Disk "examples" Compare. +Print XML Module Disk "examples" Compare_dec. +(*Print XML Module Disk "examples" Div.*) +Print XML Module Disk "examples" Div2. +Print XML Module Disk "examples" EqNat. +Print XML Module Disk "examples" Euclid_def. +Print XML Module Disk "examples" Euclid_proof. +Print XML Module Disk "examples" Even. +Print XML Module Disk "examples" Gt. +Print XML Module Disk "examples" Le. +Print XML Module Disk "examples" Lt. +Print XML Module Disk "examples" Min. +Print XML Module Disk "examples" Minus. +Print XML Module Disk "examples" Mult. +Print XML Module Disk "examples" Peano_dec. +Print XML Module Disk "examples" Plus. +Print XML Module Disk "examples" Wf_nat. diff --git a/helm/EXPORT/exportcoq/provacoqBool.v b/helm/EXPORT/exportcoq/provacoqBool.v new file mode 100644 index 000000000..a898237be --- /dev/null +++ b/helm/EXPORT/exportcoq/provacoqBool.v @@ -0,0 +1,13 @@ +Require Export Xml. + +Require Bool. +Require DecBool. +Require IfProp. +Require Sumbool. +Require Zerob. + +Print XML Module Disk "examples" Bool. +Print XML Module Disk "examples" DecBool. +Print XML Module Disk "examples" IfProp. +Print XML Module Disk "examples" Sumbool. +Print XML Module Disk "examples" Zerob. diff --git a/helm/EXPORT/exportcoq/provacoqInit.v b/helm/EXPORT/exportcoq/provacoqInit.v new file mode 100644 index 000000000..d40ea3ee5 --- /dev/null +++ b/helm/EXPORT/exportcoq/provacoqInit.v @@ -0,0 +1,13 @@ +Require Export Xml. + +Print XML Module Disk "examples" Datatypes. +Print XML Module Disk "examples" DatatypesSyntax. +Print XML Module Disk "examples" Logic. +Print XML Module Disk "examples" LogicSyntax. +Print XML Module Disk "examples" Specif. +Print XML Module Disk "examples" SpecifSyntax. +Print XML Module Disk "examples" Peano. +Print XML Module Disk "examples" Wf. +Print XML Module Disk "examples" Prelude. +Print XML Module Disk "examples" Logic_Type. +Print XML Module Disk "examples" Logic_TypeSyntax. diff --git a/helm/EXPORT/exportcoq/provacoqLists.v b/helm/EXPORT/exportcoq/provacoqLists.v new file mode 100644 index 000000000..91b74ef0a --- /dev/null +++ b/helm/EXPORT/exportcoq/provacoqLists.v @@ -0,0 +1,15 @@ +Require Export Xml. + +Require List. +Require ListSet. +Require PolyList. +(*Require PolyListSyntax.*) +Require Streams. +Require TheoryList. + +Print XML Module Disk "examples" List. +Print XML Module Disk "examples" ListSet. +Print XML Module Disk "examples" PolyList. +(*Print XML Module Disk "examples" PolyListSyntax.*) +Print XML Module Disk "examples" Streams. +Print XML Module Disk "examples" TheoryList. diff --git a/helm/EXPORT/exportcoq/provacoqLogic.v b/helm/EXPORT/exportcoq/provacoqLogic.v new file mode 100644 index 000000000..e2296a51f --- /dev/null +++ b/helm/EXPORT/exportcoq/provacoqLogic.v @@ -0,0 +1,17 @@ +Require Export Xml. + +Require Classical. +Require Classical_Pred_Set. +Require Classical_Pred_Type. +Require Classical_Prop. +Require Classical_Type. +Require Eqdep. +Require Eqdep_dec. + +Print XML Module Disk "examples" Classical. +Print XML Module Disk "examples" Classical_Pred_Set. +Print XML Module Disk "examples" Classical_Pred_Type. +Print XML Module Disk "examples" Classical_Prop. +Print XML Module Disk "examples" Classical_Type. +Print XML Module Disk "examples" Eqdep. +Print XML Module Disk "examples" Eqdep_dec. diff --git a/helm/EXPORT/exportcoq/provacoqReals.v b/helm/EXPORT/exportcoq/provacoqReals.v new file mode 100644 index 000000000..445f9f988 --- /dev/null +++ b/helm/EXPORT/exportcoq/provacoqReals.v @@ -0,0 +1,23 @@ +Require Export Xml. + +Require R_Ifp. +Require Raxioms. +Require Rdefinitions. +Require Rbase. +Require Rbasic_fun. +Require Rderiv. +Require Reals. +Require Rfunctions. +Require Rlimit. +Require TypeSyntax. + +Print XML Module Disk "examples" R_Ifp. +Print XML Module Disk "examples" Raxioms. +Print XML Module Disk "examples" Rdefinitions. +Print XML Module Disk "examples" Rbase. +Print XML Module Disk "examples" Rbasic_fun. +Print XML Module Disk "examples" Rderiv. +Print XML Module Disk "examples" Reals. +Print XML Module Disk "examples" Rfunctions. +Print XML Module Disk "examples" Rlimit. +Print XML Module Disk "examples" TypeSyntax. diff --git a/helm/EXPORT/exportcoq/provacoqRelations.v b/helm/EXPORT/exportcoq/provacoqRelations.v new file mode 100644 index 000000000..c588b30f3 --- /dev/null +++ b/helm/EXPORT/exportcoq/provacoqRelations.v @@ -0,0 +1,33 @@ +Require Export Xml. + +Require Newman. +Require Operators_Properties. +Require Relation_Definitions. +Require Relation_Operators. +Require Relations. +Require Rstar. +(*Require Disjoint_Union.*) +(*Require Inclusion.*) +(*Require Inverse_Image.*) +(*Require Lexicographic_Exponentiation.*) +(*Require Lexicographic_Product.*) +(*Require Transitive_Closure.*) +(*Require Union.*) +(*Require Well_Ordering.*) +(*Require Wellfounded.*) + +Print XML Module Disk "examples" Newman. +Print XML Module Disk "examples" Operators_Properties. +Print XML Module Disk "examples" Relation_Definitions. +Print XML Module Disk "examples" Relation_Operators. +Print XML Module Disk "examples" Relations. +Print XML Module Disk "examples" Rstar. +(*Print XML Module Disk "examples/WELLFOUNDED" Disjoint_Union.*) +(*Print XML Module Disk "examples/WELLFOUNDED" Inclusion.*) +(*Print XML Module Disk "examples/WELLFOUNDED" Inverse_Image.*) +(*Print XML Module Disk "examples/WELLFOUNDED" Lexicographic_Exponentiation.*) +(*Print XML Module Disk "examples/WELLFOUNDED" Lexicographic_Product.*) +(*Print XML Module Disk "examples/WELLFOUNDED" Transitive_Closure.*) +(*Print XML Module Disk "examples/WELLFOUNDED" Union.*) +(*Print XML Module Disk "examples/WELLFOUNDED" Well_Ordering.*) +(*Print XML Module Disk "examples/WELLFOUNDED" Wellfounded.*) diff --git a/helm/EXPORT/exportcoq/provacoqSets.v b/helm/EXPORT/exportcoq/provacoqSets.v new file mode 100644 index 000000000..9502861b0 --- /dev/null +++ b/helm/EXPORT/exportcoq/provacoqSets.v @@ -0,0 +1,48 @@ +Require Export Xml. + +Require Classical_sets. +Require Constructive_sets. +Require Cpo. +Require Ensembles. +Require Finite_sets. +Require Finite_sets_facts. +Require Image. +Require Infinite_sets. +Require Integers. +Require Multiset. +Require Partial_Order. +Require Permut. +(*Require CSCPermut.*) +Require Powerset. +Require Powerset_Classical_facts. +Require Powerset_facts. +Require Relations_1. +Require Relations_1_facts. +Require Relations_2. +Require Relations_2_facts. +Require Relations_3. +Require Relations_3_facts. +Require Uniset. + +Print XML Module Disk "examples" Classical_sets. +Print XML Module Disk "examples" Constructive_sets. +Print XML Module Disk "examples" Cpo. +Print XML Module Disk "examples" Ensembles. +Print XML Module Disk "examples" Finite_sets. +Print XML Module Disk "examples" Finite_sets_facts. +Print XML Module Disk "examples" Image. +Print XML Module Disk "examples" Infinite_sets. +Print XML Module Disk "examples" Integers. +Print XML Module Disk "examples" Multiset. +Print XML Module Disk "examples" Partial_Order. +Print XML Module Disk "examples" Permut. +Print XML Module Disk "examples" Powerset. +Print XML Module Disk "examples" Powerset_Classical_facts. +Print XML Module Disk "examples" Powerset_facts. +Print XML Module Disk "examples" Relations_1. +Print XML Module Disk "examples" Relations_1_facts. +Print XML Module Disk "examples" Relations_2. +Print XML Module Disk "examples" Relations_2_facts. +Print XML Module Disk "examples" Relations_3. +Print XML Module Disk "examples" Relations_3_facts. +Print XML Module Disk "examples" Uniset. diff --git a/helm/EXPORT/exportcoq/provacoqSorting.v b/helm/EXPORT/exportcoq/provacoqSorting.v new file mode 100644 index 000000000..ff940fd22 --- /dev/null +++ b/helm/EXPORT/exportcoq/provacoqSorting.v @@ -0,0 +1,13 @@ +(* +Require Export Xml. + +Require Generic. +Require Heap. +Require Permutation. +Require Sorting. + +Print XML Module Disk "examples" Generic. +Print XML Module Disk "examples" Heap. +Print XML Module Disk "examples" Permutation. +Print XML Module Disk "examples" Sorting. +*) diff --git a/helm/EXPORT/exportcoq/provacoqTrees.v b/helm/EXPORT/exportcoq/provacoqTrees.v new file mode 100644 index 000000000..a90b04122 --- /dev/null +++ b/helm/EXPORT/exportcoq/provacoqTrees.v @@ -0,0 +1,7 @@ +(* +Require Export Xml. + +Require Btree. + +Print XML Module Disk "examples" Btree. +*) diff --git a/helm/EXPORT/exportcoq/provacoqZArith.v b/helm/EXPORT/exportcoq/provacoqZArith.v new file mode 100644 index 000000000..ff43bbd23 --- /dev/null +++ b/helm/EXPORT/exportcoq/provacoqZArith.v @@ -0,0 +1,19 @@ +Require Export Xml. + +Require Wf_Z. +Require ZArith. +Require ZArith_dec. +Require Zmisc. +Require Zsyntax. +Require auxiliary. +Require fast_integer. +Require zarith_aux. + +Print XML Module Disk "examples" Wf_Z. +Print XML Module Disk "examples" ZArith. +Print XML Module Disk "examples" ZArith_dec. +Print XML Module Disk "examples" Zmisc. +Print XML Module Disk "examples" Zsyntax. +Print XML Module Disk "examples" auxiliary. +Print XML Module Disk "examples" fast_integer. +Print XML Module Disk "examples" zarith_aux. diff --git a/helm/EXPORT/exportcoq/provacoqcontribOmega.v b/helm/EXPORT/exportcoq/provacoqcontribOmega.v new file mode 100644 index 000000000..04d299423 --- /dev/null +++ b/helm/EXPORT/exportcoq/provacoqcontribOmega.v @@ -0,0 +1,11 @@ +Require Export Xml. + +Require Omega. +Require Zlogarithm. +Require OmegaSyntax. +Require Zpower. + +Print XML Module Disk "examples" Omega. +Print XML Module Disk "examples" Zlogarithm. +Print XML Module Disk "examples" OmegaSyntax. +Print XML Module Disk "examples" Zpower. diff --git a/helm/EXPORT/exportcoq/provacoqcontribRing.v b/helm/EXPORT/exportcoq/provacoqcontribRing.v new file mode 100644 index 000000000..bfc2633be --- /dev/null +++ b/helm/EXPORT/exportcoq/provacoqcontribRing.v @@ -0,0 +1,17 @@ +Require Export Xml. + +Require ArithRing. +Require Quote. +Require Ring. +Require Ring_abstract. +Require Ring_normalize. +Require Ring_theory. +Require ZArithRing. + +Print XML Module Disk "examples" ArithRing. +Print XML Module Disk "examples" Quote. +Print XML Module Disk "examples" Ring. +Print XML Module Disk "examples" Ring_abstract. +Print XML Module Disk "examples" Ring_normalize. +Print XML Module Disk "examples" Ring_theory. +Print XML Module Disk "examples" ZArithRing. diff --git a/helm/EXPORT/exportcsczfc/Makefile b/helm/EXPORT/exportcsczfc/Makefile new file mode 100644 index 000000000..7016b2865 --- /dev/null +++ b/helm/EXPORT/exportcsczfc/Makefile @@ -0,0 +1,11 @@ +all: objects theories + +objects: + coqc -R csc_zfc csc_zfc csc_zfc/*.v + echo "Load Verbose provacsczfc." | ~/V7/bin/coqtop.byte -R csc_zfc csc_zfc + +theories: + ./exporttheories.sh + +clean: + rm -f *.vo csc_zfc/*.vo diff --git a/helm/EXPORT/exportcsczfc/csc_zfc/csc_eqdep.v b/helm/EXPORT/exportcsczfc/csc_zfc/csc_eqdep.v new file mode 100644 index 000000000..8019c08b3 --- /dev/null +++ b/helm/EXPORT/exportcsczfc/csc_zfc/csc_eqdep.v @@ -0,0 +1,9 @@ +Section Dependent_equality. + +Variable U:Type. +Variable P:U->Type. + +Inductive eq_depT [p:U;x:(P p)] : (q:U)(P q)->Prop := + eq_depT_intro : (eq_depT p x p x). + +End Dependent_equality. diff --git a/helm/EXPORT/exportcsczfc/csc_zfc/csc_zfc.v b/helm/EXPORT/exportcsczfc/csc_zfc/csc_zfc.v new file mode 100644 index 000000000..a109239c0 --- /dev/null +++ b/helm/EXPORT/exportcsczfc/csc_zfc/csc_zfc.v @@ -0,0 +1,1566 @@ +(******************************************************************************) +(* Zermelo Set Theory + atomic sets *) +(* *) +(* Claudio Sacerdoti Coen *) +(* *) +(* Based on *) +(* *) +(* Zermolo Set Theory *) +(* *) +(* Benjamin Werner *) +(* *) +(******************************************************************************) + +(* This is an extension of Benjamin's encoding of usual Set Theory where I *) +(* assume the existence of exactly one atomic set for each object t of type T *) +(* where T is a Type in Coq: if (t:T) and (T:Type) then ((atom T t):Ens) *) +(* The usual axioms of set theory are modified so that they work in the *) +(* usual way if applied to "normal" sets, and in a reasonable way when *) +(* applied to atomic sets (for example (Union (atom T t) E) is equal to E for *) +(* each non-atomic set E) *) +(* All this has been already studied by Fraenkel and Mostowski in the '40, *) +(* but with totally different goals (in order to proove some independence *) +(* results in set theory) *) + +(* This is the introduction to the original encoding of Benjamin: *) +(* This is an encoding of usual Set Theory, simillar to Peter Aczel's work *) +(* in the early 80's. The main difference is that the propositions here *) +(* live in the impredicative world of "Prop". Thus, priority is given to *) +(* expressivity against constructivity. *) +(* *) +(* Since the definition of Sets is the same for both approaches, I added *) +(* most of Aczel's encoding of CZF at the end of the file. Many *) +(* definitions are common to both aproaches. *) + +(* In this work only the encoding of ZFC (and not that of CZF) has been *) +(* developed, but it should be straightforward to do. *) + +Require csc_eqdep. + +(******************************************************************************) +(* Useful data types *) +(******************************************************************************) + +Inductive Set F := . + +Inductive Set Un := void : Un. + +(* Existential quantification *) +Inductive EXType [P:Type; Q:P->Prop]: Prop := + EXTypei : (x:P)(Q x)->(EXType P Q). + +(* Sigma types -- i.e. computational existentials *) +Inductive sig [A:Type;P:A->Prop] : Type := + exist : (x:A)(P x)->(sig A P). + +(* Existential on the Type level *) +Inductive depprod [A:Type; P : A->Type] : Type := + dep_i : (x:A)(P x)->(depprod A P). + +(* Cartesian product in Type *) +Inductive prod_t [A,B:Type] : Type := + pair_t : A->B->(prod_t A B). + +(******************************************************************************) +(* Definition of Ens, EQ, IN *) +(******************************************************************************) + +(* The type representing sets (Ensemble = french for set) *) +Inductive Ens : Type := + sup : (A:Type)(A->Ens)->Ens + | atom : (A:Type)A->Ens. + +(* Recursive Definition of the extentional equality on sets *) +Definition EQ : Ens -> Ens -> Prop. +Induction 1. +Intros A f eq1. +Induction 1. +Intros B g eq2. +Apply and. +Exact (x:A) + (EXType ? [y:B](eq1 x (g y))). +Exact (y:B) + (EXType ? [x:A](eq1 x (g y))). + +Intros A' a'. +Exact False. + +Intros A a. +Induction 1. +Intros A' f eq1. +Exact False. + +Intros. +(*Exact (X == X0).*) +Exact (eq_depT Type [A:Type]A A a A0 y). +Save. + +Transparent EQ. + +(* Membership on sets *) +Definition IN: Ens -> Ens -> Prop := +[E1,E2:Ens] + Cases E2 of + (sup A f) => (EXType ? [y:A](EQ E1 (f y))) + | (atom A a) => False + end. +Transparent IN. + + +(******************************************************************************) +(* INCLUSION *) +(******************************************************************************) + +Definition INC : Ens -> Ens -> Prop := + [E1,E2:Ens] + Cases E1 E2 of + (sup A f) (sup B g) => (E:Ens)(IN E E1)->(IN E E2) + | (sup A f) (atom B b) => False + | (atom A a) (sup B g) => False (* ??? or True? *) + | (atom A a) (atom B b) => (EQ E1 E2) (* ??? or False? *) + end. + +(* EQ is an equivalence relation *) + +Theorem EQ_refl : (E:Ens)(EQ E E). +Induction E. +Intros; Split; Simpl; Intro. +Exists x; Exact (H x). +Exists y; Exact (H y). +Intros; Simpl; Constructor 1. +Qed. + +Theorem EQ_tran : (E1,E2,E3:Ens)(EQ E1 E2)->(EQ E2 E3)->(EQ E1 E3). +Induction E1; [Intros A1 f1 r1 | Intros A1 a1] ; +Induction E2; [Intros A2 f2 r2 | Intros A2 a2 | Intros A2 f2 r2 | Intros A2 a2]; +Induction E3; [Intros A3 f3 r3 | Auto | Contradiction | Auto | + Auto | Contradiction | Auto | Intros A3 a3]. +Simpl; Intros e1 e2; Split; Elim e1; Intros I1 I2; Elim e2; Intros I3 I4; + [ Intros a1; Elim (I1 a1) ; Intros a2 ; Elim (I3 a2) ; Intros a3 ; Exists a3 | + Intros a3; Elim (I4 a3) ; Intros a2 ; Elim (I2 a2) ; Intros a1 ; Exists a1 ]; + Apply r1 with (f2 a2); Assumption. + +Simpl ; Intros; Inversion H; Inversion H0; Assumption. +Qed. + +Theorem EQ_sym : (E1,E2:Ens)(EQ E1 E2)->(EQ E2 E1). +Induction E1 ; [ Intros A1 f1 r1 | Intros A1 a1 ]; +Induction E2 ; [Intros A2 f2 r2 | Contradiction | Contradiction |Intros A2 a2]. + +Induction 1; Intros e1 e2; Split; + [ Intros a2; Elim (e2 a2); Intros a1 H1; Exists a1 | + Intros a1; Elim (e1 a1); Intros a2 H2; Exists a2 ] ; Apply r1; Assumption. +Destruct 1; Apply EQ_refl. +Qed. + +Theorem EQ_INC : (E,E':Ens)(EQ E E')->(INC E E'). +Induction E ; [Intros A f r | Intros A a] ; Induction E' ; + [Intros A' f' r' | Contradiction | Contradiction | Intros A' a']. +Simpl; Destruct 1; Intros e1 e2. +Intros C; Induction 1; Intros a ea; Elim (e1 a); Intros a' ea'; Exists a'. +Apply EQ_tran with (f a); Assumption. +Destruct 1; Hnf; Constructor 1. +Qed. + +Hints Resolve EQ_sym EQ_refl EQ_INC : zfc. + +Theorem INC_EQ : (E,E':Ens)(INC E E')->(INC E' E)->(EQ E E'). +Induction E ; [Intros A f r | Intros A a] ; Induction E' ; + [Intros A' f' r' | Auto | Auto | Auto]. +Unfold INC; Simpl; Intros I1 I2; Split. +Intros a; Apply I1; Exists a; Apply EQ_refl. +Intros a'; Cut (EXType A [x:A](EQ (f' a')(f x))). +Induction 1; Intros a ea; Exists a; Apply EQ_sym; Exact ea. +Apply I2; Exists a'; Apply EQ_refl. +Qed. + +Hints Resolve INC_EQ : zfc. + +(* Membership is extentional (i.e. is stable w.r.t. EQ) *) + +Theorem IN_sound_left : + (E,E',E'':Ens) + (EQ E E')->(IN E E'')->(IN E' E''). +Induction E''; [Intros A'' f'' r'' e | Intros A'' a'' e]; Simpl. +Induction 1; Intros a'' p; Exists a''; Apply EQ_tran with E; + [Apply EQ_sym; Assumption | Assumption]. + +Intro; Assumption. +Qed. + +Theorem IN_sound_right : + (E,E',E'':Ens) + (EQ E' E'')->(IN E E')->(IN E E''). +Induction E'; [Intros A' f' r' | Intros A' a']; Induction E''; + [Intros A'' f'' r'' | Intros A'' a'' | Intros A'' f'' r'' | Intros A'' a'']; + Simpl. +Induction 1; Intros e1 e2; Induction 1; Intros a' e'; Elim (e1 a'); + Intros a'' e''; Exists a''; Apply EQ_tran with (f' a'); Assumption. +Intros; Assumption. +Intros; Elim H. +Intros; Assumption. +Qed. + +(* Inclusion is reflexive, transitive, extentional *) + +Theorem INC_refl : (E:Ens)(INC E E). +Induction E; Auto with zfc. +Qed. + +Theorem INC_tran : (E,E',E'':Ens)(INC E E')->(INC E' E'')->(INC E E''). +Induction E; Induction E'; Induction E''; Simpl; + Auto Orelse Contradiction Orelse (Intros; Elim H0; Assumption). +Qed. + +Theorem INC_sound_left : + (E,E',E'':Ens) + (EQ E E')->(INC E E'')->(INC E' E''). +Induction E; [Intros A f r | Intros A a]; Induction E'; + [Intros A' f' r' | Intros A' a' | Intros A' f' r' | Intros A' a']; + Induction E''; [Intros A'' f'' r'' | Contradiction | Contradiction | + Contradiction | Contradiction | Contradiction | Contradiction | + Intros A'' a'']. +Unfold INC; Intros; Apply H0; Apply IN_sound_right with (sup A' f'); + Auto with zfc. +Destruct 1; Auto. +Qed. + +Theorem INC_sound_right : + (E,E',E'':Ens) + (EQ E' E'')->(INC E E')->(INC E E''). +Induction E; [Intros A f r | Intros A a]; Induction E'; + [Intros A' f' r' | Intros A' a' | Intros A' f' r' | Intros A' a']; + Induction E''; [Intros A'' f'' r'' | Contradiction | Contradiction | + Contradiction | Contradiction | Contradiction | Contradiction | + Intros A'' a'']. +Unfold INC; Intros; Apply IN_sound_right with (sup A' f'); + [Assumption | Apply H0; Assumption]. +Destruct 1; Auto. +Qed. + +(******************************************************************************) +(* THE EMPTY SET *) +(******************************************************************************) + +(* The empty set (vide = french for empty) *) +Definition Vide : Ens := + (sup F [f:F]Cases f of end). + +Theorem Vide_est_vide : (E:Ens)(IN E Vide)->F. +Unfold Vide; Simpl; Intros E H; Cut False. +Induction 1. +Elim H; Intros x; Elim x. +Qed. + +(* CSC: This is different from Werner *) +Theorem tout_vide_est_Vide : + (A:Type)(f:A->Ens)((E':Ens)(IN E' (sup A f))->F)->(EQ (sup A f) Vide). +Intros; Hnf; Split. +Intro; Cut F. +Destruct 1. +Apply H with (f x); Unfold IN; Exists x; Apply EQ_refl. +Destruct y. +Qed. + +(******************************************************************************) +(* PAIRE *) +(******************************************************************************) + +Definition Paire : Ens -> Ens -> Ens := + [E1,E2:Ens] (sup bool [b:bool]Cases b of true => E1 | false => E2 end). + +(* The pair construction is extentional *) + +Theorem Paire_sound_left : (A,A',B:Ens) + (EQ A A')->(EQ (Paire A B)(Paire A' B)). +Unfold Paire . +Simpl. +(Intros; Split). +Induction x. +(Exists true; Auto with zfc). + +(Exists false; Auto with zfc). + +(Induction y; Simpl). +(Exists true; Auto with zfc). + +(Exists false; Auto with zfc). +Qed. + +Theorem Paire_sound_right : (A,B,B':Ens) + (EQ B B')->(EQ (Paire A B)(Paire A B')). +Unfold Paire; Simpl; Intros; Split. +Induction x. +(Exists true; Auto with zfc). +Exists false; Auto with zfc. +Induction y. +(Exists true; Auto with zfc). +Exists false; Auto with zfc. +Qed. + +Hints Resolve Paire_sound_right Paire_sound_left : zfc. + +Theorem IN_Paire_left : (E,E':Ens)(IN E (Paire E E')). +Unfold Paire; Exists true; Apply EQ_refl. +Qed. + +Theorem IN_Paire_right : (E,E':Ens)(IN E' (Paire E E')). +Unfold Paire; Exists false; Apply EQ_refl. +Qed. + +Theorem Paire_IN : (E,E',A:Ens)(IN A (Paire E E'))->(EQ A E)\/(EQ A E'). +Unfold Paire; Simpl. +Induction 1; Intros b; Elim b; Auto with zfc. +Save. + +Hints Resolve IN_Paire_left IN_Paire_right Vide_est_vide : zfc. + +(******************************************************************************) +(* SINGLETON *) +(******************************************************************************) + +(* CSC: This is different from Benjamin only because I like it more; *) +(* theorems are also simpler *) +(* In Benjamin's encoding (Sing E) was defined as (Paire E E) *) +Definition Sing : Ens -> Ens := + [E:Ens] (sup Un [x:Un]Cases x of void => E end). + +Theorem IN_Sing : (E:Ens)(IN E (Sing E)). +Simpl; Exists void; Apply EQ_refl. +Qed. + +Theorem IN_Sing_EQ : (E,E':Ens)(IN E (Sing E'))->(EQ E E'). +Simpl; Intros; Elim H; Destruct x; Trivial. +Qed. + +Hints Resolve IN_Sing IN_Sing_EQ : zfc. + +Theorem Sing_sound : (A,A':Ens)(EQ A A')->(EQ (Sing A)(Sing A')). +Intros; Hnf; Split; [Destruct x | Destruct y]; Exists void; Assumption. +Qed. + +Hints Resolve Sing_sound : zfc. + +Theorem EQ_Sing_EQ : (E1,E2:Ens)(EQ (Sing E1)(Sing E2))->(EQ E1 E2). +Intros; Hnf in H; Elim H; Intros; Elim (H0 void); Destruct x; Trivial. +Qed. + +Hints Resolve EQ_Sing_EQ : zfc. + +(******************************************************************************) +(* COMPREHENSION (OR SEPARATION) *) +(******************************************************************************) + +Definition Comp: Ens -> (Ens -> Prop) -> Ens. +Induction 1. +Intros A f fr P. +Apply (sup {x:A|(P (f x))}). +Induction 1; Intros x p; Exact (f x). +Intros. Exact X. +Qed. + +Transparent Comp. + +Theorem Comp_INC : (E:Ens)(P:Ens->Prop)(INC (Comp E P) E). +Destruct E. +Intros A f P; Simpl; Destruct E0; [Intros A' f' H | Intros A' a' H]; + Elim H; Destruct x; Intros x0 p eq; Exists x0; Exact eq. +Auto with zfc. +Qed. + +Theorem IN_Comp_P : + (E,A:Ens) + (P:Ens->Prop)((w1,w2:Ens)(P w1)->(EQ w1 w2)->(P w2))-> + (IN A (Comp E P))->(P A). +Induction E. +Simpl; Intros B f Hr A P H i; Elim i; Destruct x; Simpl; Intro b; Intros; + Apply H with (f b); Auto with zfc. +Contradiction. +Qed. + +Theorem IN_P_Comp : + (E,A:Ens) + (P:Ens ->Prop)((w1,w2:Ens)(P w1)->(EQ w1 w2)->(P w2))-> + (IN A E)->(P A)->(IN A (Comp E P)). +Induction E. +Simpl; Intros B f HR A P H i; Elim i; Simpl; Intros; Cut (P (f x)). +Intros Pf. +Exists (exist B [x:B](P (f x)) x Pf); Simpl; Auto with zfc. +Apply H with A; Auto with zfc. +Contradiction. +Qed. + +(* Again, extentionality is not stated, but easy *) + +(******************************************************************************) +(* UNION *) +(******************************************************************************) + +(* Projections of a set: *) +(* 1: its base type, F for atoms *) + +Definition pi1: Ens -> Type. +Induction 1. +Intros A f r. +Exact A. +Intros. +Exact F. +Save. + +Transparent pi1. + +(* 2: the function, [_:F]Vide for atoms *) + +Definition pi2 : (E:Ens)(pi1 E)->Ens. +Induction E. +Intros A f r. +Exact f. +Intros. +Exact Vide. +Save. + +Transparent pi2. + +Definition Union : (E:Ens)Ens. +Induction 1. +Intros A f r. +Apply (sup (depprod A [x:A](pi1 (f x)))). +Induction 1; Intros a b. +Exact (pi2 (f a) b). +Intros. +Exact Vide. +Save. + +Transparent Union. + +Theorem EQ_EXType : (E,E':Ens) + (EQ E E') + ->(a:(pi1 E)) + (EXType (pi1 E') [b:(pi1 E')](EQ (pi2 E a) (pi2 E' b))). +Induction E; [Intros A f r | Intros A a]; Induction E'; + [Intros A' f' r' | Intros A' a' | Intros A' f' r' | Intros A' a']. +Simpl; Destruct 1; Intros e1 e2 a; Apply e1. +Contradiction. +Contradiction. +Simpl; Destruct 2. +Qed. + +Transparent EQ_EXType. + +Theorem IN_EXType: (E,E':Ens)(IN E' E)-> + (EXType (pi1 E) [a:(pi1 E)](EQ E' (pi2 E a))). +Induction E. +Simpl; Intros A f r; Induction 1; Intros; Exists x; Assumption. +Destruct 1. +Qed. + +Theorem IN_Union : (E,E',E'':Ens) + (IN E' E)->(IN E'' E')->(IN E'' (Union E)). +Induction E. +2: Destruct 1. +Intros A f r. +Intros; Simpl. +Elim (IN_EXType (sup A f) E' H). +Intros x e. +Cut (EQ (pi2 (sup A f) x) E'). +2: Auto with zfc v62. +Intros e1. +Cut (IN E'' (pi2 (sup A f) x)). +Intros i1. +Elim (IN_EXType ? ? i1). +Intros x0 e2. +Simpl in x0. +Exists (dep_i A [x:A](pi1 (f x)) x x0). +Simpl. +Exact e2. +Apply IN_sound_right with E'; Assumption. +Qed. + +(* CSC: This is different from Benjamin *) +Theorem IN_INC_Union : + (A:Type)(f:A->Ens)(E:Ens)(IN (sup A f) E)->(INC (sup A f) (Union E)). +Induction E. +Intros A f r H; Hnf; Hnf in H; Intros; Elim H; Intros x e. +Cut (IN E0 (f0 x)). +Intro in_E0_f0x; Apply IN_Union with (f0 x). +Hnf; Split with x; Auto with zfc. + +Auto with zfc. +Apply IN_sound_right with (sup A f); Trivial. + +(Simpl; Destruct 2; Destruct x). +Qed. + +Theorem Union_IN : (E,E':Ens)(IN E' (Union E))-> + (EXType ? [E1:Ens](IN E1 E)/\(IN E' E1)). +Induction E. +2: (Simpl; Destruct 2; Destruct x). +Unfold Union ; Simpl; Intros A f r. +Induction 1. +Induction x. +(Intros a b; Simpl). +Intros. +Exists (f a). +Split. +(Exists a; Auto with zfc v62). + +(Apply IN_sound_left with (pi2 (f a) b); Auto with zfc v62). +Simpl. +(Generalize b ; Elim (f a); Simpl). +Intros. +(Exists b0; Auto with zfc v62). + +Destruct 2. +Qed. + +(* extentionality of union *) + +Theorem Union_sound + : (E,E':Ens)(EQ E E')->(EQ (Union E) (Union E')). +Unfold Union. +Induction E ; [Intros A f r | Intros A a] ; Induction E' ; + [Intros A' f' r' | Intros A' a' | Intros A' f' r' | Intros A' a']. + +Simpl; Induction 1; Intros e1 e2; Split. +Intros x; Elim x; Intros a aa; Elim (e1 a); Intros a' ea. +Elim (EQ_EXType (f a)(f' a') ea aa); Intros aa' eaa. +Exists (dep_i A' [x:A'](pi1 (f' x)) a' aa'); Simpl; Auto with zfc v62. +Intros c'; Elim c'; Intros a' aa'; Elim (e2 a'); Intros a ea. +Cut (EQ (f' a')(f a)). +2 : Auto with zfc v62. +Intros ea'; Elim (EQ_EXType (f' a')(f a) ea' aa'); Intros aa eaa. +Exists (dep_i A [x:A](pi1 (f x)) a aa); Auto with zfc v62. + +Contradiction. +Contradiction. +Destruct 1; Apply EQ_refl. +Qed. + +(* The union construction is monotone w.r.t. inclusion *) + +Theorem Union_mon : (E,E':Ens)(INC E E')->(INC (Union E)(Union E')). +Induction E ; [Intros A f r | Intros A a] ; Induction E'; + [Intros A' f' r' | Contradiction | Contradiction | Intros A' a']. +2: Auto with zfc. +Intro; Cut (E:Ens)(IN E (sup A f))->(IN E (sup A' f')). +2: Auto. +Intro XXX; Cut ((E:Ens)(IN E (Union (sup A f)))->(IN E (Union (sup A' f')))) + ->(INC (Union (sup A f)) (Union (sup A' f'))). +2: Auto. +Intros X; Apply X; Intros E0 Y; (Elim (Union_IN (sup A f) E0); Auto with zfc). +Destruct 1; Intros; Cut (IN x (sup A' f')). +2: Auto. +Intro; (Apply IN_Union with x; Auto). +Qed. + +(******************************************************************************) +(* INTERSECTION *) +(******************************************************************************) + +Definition Inter : (E:Ens)Ens := +[E:Ens] + Cases E of + (sup A f) => + (sup ? + [c:(depprod A + [a:A](depprod ? [b:(pi1 (f a))](x:A)(IN (pi2 (f a) b)(f x))) + ) + ] + Cases c of + (dep_i a (dep_i b p)) => (pi2 (f a) b) + end + ) + | (atom A a) => Vide + end. + +Theorem IN_Inter_all : (E,E':Ens) + (IN E' (Inter E))-> + (E'':Ens)(IN E'' E)->(IN E' E''). +Induction E; [Intros A f r | Contradiction]; Intros E'. +Induction 1; Intros c; Elim c; Intros a ca; Elim ca; Intros aa paa. +Intros e E'' e''. +Elim e''; Intros a1 ea1. +Apply IN_sound_right with (f a1); Auto with zfc v62. +Apply IN_sound_left with (pi2 (f a) aa); Auto with zfc v62. +Qed. + +Theorem all_IN_Inter : (E,E',E'':Ens) + (IN E'' E)-> + ((E'':Ens)(IN E'' E)->(IN E' E''))-> + (IN E' (Inter E)). +(Induction E; [Intros A f r | Contradiction]). +Intros E' E'' i H. +Elim (IN_EXType (sup A f) E'' i). +(Intros a e; Simpl in a). +Simpl in e. +(Cut (IN E' E''); Auto with zfc v62). +Intros i'. +(Cut (IN E' (f a)); Auto with zfc v62). +Intros i0. +Elim (IN_EXType (f a) E' i0). +Intros b e'. +Simpl. +Cut (x:A)(IN (pi2 (f a) b) (f x)). +Intros. +Exists (dep_i A + [a:A] + (depprod (pi1 (f a)) + [b:(pi1 (f a))](x:A)(IN (pi2 (f a) b) (f x))) + a + (dep_i (pi1 (f a)) + [b:(pi1 (f a))](x:A)(IN (pi2 (f a) b) (f x)) b H0)). +Simpl. +Auto with zfc v62. +Auto with zfc v62. +Intros. +Apply IN_sound_left with E'. +Auto with zfc v62. +Apply H. +Auto with zfc v62. +Simpl. +(Exists x; Auto with zfc v62). +(Apply IN_sound_right with E''; Auto with zfc v62). +Qed. + +(******************************************************************************) +(* POWERSET *) +(******************************************************************************) + +Definition Power : Ens -> Ens := +[E:Ens] + Cases E of + (sup A f) => + (sup ? + [P:A->Prop] + (sup ? + [c:(depprod A [a:A](P a))] + Cases c of + (dep_i a p) => (f a) + end + ) + ) + | (atom A a) => (Sing (atom A a)) (* ??? or Vide? *) + end. + +Theorem IN_Power_INC : (E,E':Ens)(IN E' (Power E))->(INC E' E). +Induction E. +Intros A f r; Unfold INC ; Simpl. +Intros E'; Induction 1; Intros P. +Elim E'. +Simpl. +Intros A' f' r'. +Induction 1; Intros HA HB. +Intros E''; Induction 1; Intros a' e. +Elim (HA a'). +Induction x; Intros a p. +Intros; Exists a. +Apply EQ_tran with (f' a'); Auto with zfc v62. +Contradiction. +Auto with zfc. +Qed. + +(* CSC: This is different from Benjamin *) +Theorem INC_IN_Power : (E,E':Ens)(INC E' E)->(IN E' (Power E)). +Induction E. +2: Induction E'. +2: Contradiction. +2: (Destruct 1; Unfold Power; Auto with zfc). +Intros A f r; Unfold INC; Simpl; Induction E'. +2: Contradiction. +Intros A' f' r' i. +Exists [a:A](IN (f a) (sup A' f')). +Simpl. +Split. +Intros. +Elim (i (f' x)). +Intros a e. +(Cut (EQ (f a) (f' x)); Auto with zfc v62). +Intros e1. +Exists (dep_i A [a:A](EXType A' [y:A'](EQ (f a) (f' y))) a + (EXTypei A' [y:A'](EQ (f a) (f' y)) x e1)). +Auto with zfc v62. +Simpl. +(Exists x; Auto with zfc v62). +Induction y; Induction 1; Intros. +(Exists x0; Auto with zfc v62). +Qed. + +Theorem Power_mon : (E,E':Ens)(INC E E')->(INC (Power E)(Power E')). +Induction E; [Intros A f r | Intros A a]; Induction E'; + [Intros A' f' r' | Contradiction | Contradiction | Destruct 1; Auto with zfc]. +Intro. +Hnf in H. +Cut ((E:Ens)(IN E (Power (sup A f)))->(IN E (Power (sup A' f')))) + ->(INC (Power (sup A f)) (Power (sup A' f'))). +2: Auto. +Intros. +Apply H0. +Intros. +Cut (INC E0 (sup A f)). +2: (Apply IN_Power_INC; Auto). +Intro. +Cut (INC E0 (sup A' f')). +Intro. +Apply INC_IN_Power. +Assumption. + +Generalize H2. +Elim E0. +Unfold INC. +Auto with zfc. + +Auto with zfc. +Qed. + +Theorem Power_sound : (E,E':Ens)(EQ E E')->(EQ (Power E)(Power E')). +Induction E; [Intros A f r | Intros A a]; Induction E'; + [Intros A' f' r' | Contradiction | Contradiction | Destruct 1; Auto with zfc]. +Intro. +Apply INC_EQ. +Cut ((E:Ens)(IN E (Power (sup A f)))->(IN E (Power (sup A' f')))) + ->(INC (Power (sup A f)) (Power (sup A' f'))). +2: Auto. +Intros; Apply H0; Clear H0; Intros; Cut (INC E0 (sup A f)). +2: (Apply IN_Power_INC; Auto with zfc). +Clear H0; Intro; Apply INC_IN_Power. +(Apply INC_sound_right with (sup A f); Auto). + +(* Using simmetry *) +Cut ((E:Ens)(IN E (Power (sup A' f')))->(IN E (Power (sup A f)))) + ->(INC (Power (sup A' f')) (Power (sup A f))). +2: Auto. +Intros; Apply H0; Clear H0; Intros; Cut (INC E0 (sup A' f')). +2: (Apply IN_Power_INC; Auto with zfc). +Clear H0; Intro; Apply INC_IN_Power. +(Apply INC_sound_right with (sup A' f'); Auto with zfc). +Qed. + +(******************************************************************************) +(* ORDERED COUPLES *) +(******************************************************************************) + +(* small lemmas *) + +Theorem not_EQ_Sing_Vide : (E:Ens)(EQ (Sing E) Vide)->F. +Intros E e; Cut False. +Induction 1. +Cut (IN E Vide). +Simpl; Induction 1; Intros xx; Elim xx; Induction 1. +Apply IN_sound_right with (Sing E); Auto with zfc v62. +Qed. + +Theorem not_EQ_Vide_Sing : (E:Ens)(EQ Vide (Sing E))->F. +Intros E e; Cut False. +Induction 1. +Cut (IN E Vide). +Simpl; Induction 1; Intros xx; Elim xx; Induction 1. +Apply IN_sound_right with (Sing E); Auto with zfc v62. +Qed. + +(* This definition of the ordered pair is slightly different from *) +(* the usual one, since we want it to work in an intuisionistic *) +(* setting. Works the same, neitherless. The soundness proofs are *) +(* unpleasant. *) + +Definition Couple := [E,E': Ens](Paire (Sing E) (Paire Vide (Sing E'))). + +Theorem Couple_inj_left : (A,A',B,B':Ens) + (EQ (Couple A A')(Couple B B'))->(EQ A B). +(Unfold Couple; Simpl); Induction 1; (Intros HA HB; Elim (HA true)). +(Intros x; Elim x; Simpl; Induction 1; Intros H3 H4; Elim (H3 void); + Simpl; Destruct x0). +Trivial. + +Elim (H4 false); Destruct x1; Intros; Cut (EQ (Sing B') Vide). +Simpl; Induction 1; Intros yy; Elim (yy void); Destruct x2. + +Apply EQ_tran with A. +Auto with zfc. + +Assumption. + +Intros; Cut (EQ (Sing B') Vide). +Simpl; Induction 1; Intros yy; Elim (yy void); Destruct x1. + +Apply EQ_tran with A. +Auto with zfc. + +Elim (H4 true); Destruct x1; Trivial. +Qed. + +Theorem Couple_inj_right : (A,A',B,B':Ens) + (EQ (Couple A A')(Couple B B'))->(EQ A' B'). +Unfold Couple; Simpl. +Induction 1; Intros H1 H2. +Elim (H1 false). +Intros bb1; Elim bb1. +Intros HF. +Change (EQ (Paire Vide (Sing A'))(Sing B)) in HF. +Cut F. +Induction 1. +Apply (not_EQ_Vide_Sing A'). +Apply EQ_tran with B. +Apply IN_Sing_EQ; Apply IN_sound_right with (Paire Vide (Sing A')); + Auto with zfc v62. +Apply EQ_sym; Apply IN_Sing_EQ; + Apply IN_sound_right with (Paire Vide (Sing A')); Auto with zfc v62. +Change (EQ (Paire Vide (Sing A'))(Paire Vide (Sing B')))->(EQ A' B'). +Intros HP; Cut (EQ (Sing A') (Sing B')). +Intros; Auto with zfc v62. +Cut (IN (Sing A')(Paire Vide (Sing B'))). +Intros HI; Elim (Paire_IN Vide (Sing B')(Sing A') HI). +Intros; Cut F. +Induction 1. +Apply not_EQ_Sing_Vide with A'; Assumption. +Trivial with zfc v62. +Apply IN_sound_right with (Paire Vide (Sing A')); Auto with zfc v62. +Qed. + +(******************************************************************************) +(* POWERSET *) +(******************************************************************************) + +(* Here we cheat. It is easier to define the cartesian product using *) +(* the type theoretical product, i.e. we here use non set-theoretical *) +(* constructions. We could however use the usual definitions. *) + +Definition Prod : Ens -> Ens -> Ens := +[E,E':Ens] + Cases E E' of + (sup A f) (sup A' f') => + (sup ? + [c:(prod_t A A')] + Cases c of + (pair_t a a') => (Couple (f a) (f' a')) + end + ) + | _ _ => Vide + end. + +Hints Resolve Paire_sound_left Paire_sound_right : zfc. + +Theorem Couple_sound_left : + (A,A',B:Ens)(EQ A A')->(EQ (Couple A B)(Couple A' B)). + Unfold Couple;Intros; Auto with zfc v62. +Save. + +Theorem Couple_sound_right: + (A,B,B':Ens)(EQ B B')->(EQ (Couple A B)(Couple A B')). + Unfold Couple;Intros; Auto with zfc v62. +Save. + +Theorem Couple_IN_Prod : (E1,E2,E1',E2':Ens) + (IN E1' E1)->(IN E2' E2)-> + (IN (Couple E1' E2')(Prod E1 E2)). +Induction E1; [Intros A1 f1 r1 | Contradiction]. +Induction E2; [Intros A2 f2 r2 | Contradiction]. +Intros E1' E2' i1 i2. +Elim (IN_EXType (sup A1 f1) E1'). +(Intros x e1; Simpl in x). +Elim (IN_EXType (sup A2 f2) E2'). +(Intros x0 e2; Simpl in x). +Apply IN_sound_left with (Couple (pi2 (sup A1 f1) x) (pi2 (sup A2 f2) x0)). +Apply EQ_tran with (Couple (pi2 (sup A1 f1) x) E2'). +Apply Couple_sound_right. +Auto with zfc v62. + +(Apply Couple_sound_left; Auto with zfc v62). + +Simpl. +Exists (pair_t ? ? x x0). +Simpl. +Split. + +Induction x1. +Exists true; Auto with zfc. +Exists false; Auto with zfc. + +Induction y. +Exists true; Auto with zfc. +Exists false; Auto with zfc. +Assumption. +Assumption. +Qed. + +Theorem Couple_Prod_IN : (E1,E2,E1',E2':Ens) + (IN (Couple E1' E2')(Prod E1 E2))-> + (IN E1' E1)/\(IN E2' E2). +Induction E1; [Intros A1 f1 r1 | Destruct 1; Destruct x]. +Induction E2; [Intros A2 f2 r2 | Destruct 1; Destruct x]. +Intros E1' E2' i. +Elim (IN_EXType (Prod (sup A1 f1) (sup A2 f2)) (Couple E1' E2') i). +Destruct x; Intros a1 a2 e. +Change (EQ (Couple E1' E2') (Couple (f1 a1) (f2 a2))) in e. +Cut (EQ E1' (f1 a1)). +Cut (EQ E2' (f2 a2)). +Intros e1 e2. +Split. +Apply IN_sound_left with (f1 a1); Auto with zfc v62; Simpl; Exists a1; + Auto with zfc v62. +Apply IN_sound_left with (f2 a2); Auto with zfc v62; Simpl; Exists a2; + Auto with zfc v62. +Apply Couple_inj_right with A:=E1' B:=(f1 a1); Auto with zfc v62. +Apply Couple_inj_left with E2' (f2 a2); Auto with zfc v62. +Qed. + +Theorem IN_Prod_EXType : (E,E',E'':Ens)(IN E'' (Prod E E'))-> + (EXType ? [A:Ens](EXType ? [B:Ens](EQ (Couple A B) E''))). +Induction E ; [Intros A f r | Destruct 1; Destruct x]. +Induction E'; [Intros A' f' r' | Destruct 1; Destruct x]. +Intros; Elim (IN_EXType (Prod (sup A f) (sup A' f')) E''). +Induction x. +Intros; Exists (f y); Exists (f' y0); Auto with zfc v62. +Auto with zfc v62. +Qed. + +(******************************************************************************) +(* ORDINALS *) +(******************************************************************************) + +Definition Succ := [E:Ens](Union (Paire E (Sing E))). + +Inductive Ord : Ens -> Prop := + Oo : (Ord Vide) +| So : (E:Ens)(Ord E)->(Ord (Succ E)) +| Lo : (E:Ens)((e:Ens)(IN e E)->(Ord e))->(Ord (Union E)) +| Eo : (E,E':Ens)(Ord E)->(EQ E E')->(Ord E'). + +Hints Resolve Oo So Lo : zfc. + +Definition Nat : nat ->Ens. +Induction 1; Intros. +Exact Vide. +Exact (Succ X). +Save. + +Transparent Nat. + +Theorem Nat_Ord : (n:nat)(Ord (Nat n)). +Induction n; Simpl; Auto with zfc v62. +Save. + +Definition Omega : Ens := + (sup nat Nat). + +Theorem IN_Succ : (E:Ens)(IN E (Succ E)). +Intros E; Unfold Succ; Apply IN_Union with (Sing E); Auto with zfc v62. +Qed. + +(* CSC: This is different from Werner *) +Theorem INC_Succ : (A:Type)(f:A->Ens)(INC (sup A f) (Succ (sup A f))). +Intros; Cut ((E:Ens)(IN E (sup A f))->(IN E (Succ (sup A f)))) + ->(INC (sup A f) (Succ (sup A f))). +Intros; Apply H; Unfold Succ; Intros. +Apply IN_Union with (sup A f); Auto with zfc. + +Intros; Exact H. +Qed. + +Hints Resolve IN_Succ INC_Succ : zfc. + +Theorem IN_Succ_or : (E,E':Ens)(IN E' (Succ E))->(EQ E E')\/(IN E' E). +Intros E E' i. +Unfold Succ in i. +Elim (Union_IN (Paire E (Sing E)) E' i). +Intros E1; Induction 1; Intros i1 i2. +Elim (Paire_IN E (Sing E) E1 i1). +Intros; Right; Apply IN_sound_right with E1; Auto with zfc v62. +Intros; Left; Cut (IN E' (Sing E)). +Auto with zfc v62. +Apply IN_sound_right with E1; Auto with zfc v62. +Qed. + +Theorem E_not_IN_E : (E:Ens)(IN E E)->F. +Induction E. +Intros A f r i. +Cut False. +Induction 1. +Elim (IN_EXType (sup A f) (sup A f) i); Intros a e. + +Simpl in a. +Change (EQ (sup A f) (f a)) in e. +Elim (r a). +Apply IN_sound_right with (sup A f); Auto with zfc v62. +Exists a; Auto with zfc v62. +Intros; Cut False; Contradiction. +Qed. + +Theorem Nat_IN_Omega : (n:nat)(IN (Nat n) Omega). +Intros; Simpl; Exists n; Auto with zfc v62. +Qed. +Hints Resolve Nat_IN_Omega : zfc. + +Theorem IN_Omega_EXType : (E:Ens)(IN E Omega)->(EXType ? [n:nat](EQ (Nat n) E)). +(Simpl; Induction 1). +Intros n e. +(Exists n; Auto with zfc v62). +Qed. + +Theorem IN_Nat_EXType : (n:nat)(E:Ens)(IN E (Nat n))->(EXType ? [p:nat](EQ E (Nat p))). +Induction n. +Simpl. +Induction 1. +Induction x. + +Intros. +Change (IN E (Succ (Nat n0))) in H0. +Elim (IN_Succ_or (Nat n0) E H0). +(Intros; Exists n0). +Auto with zfc v62. + +Intros. +(Elim (H E); Auto with zfc v62). +Qed. + +Theorem Omega_EQ_Union : (EQ Omega (Union Omega)). +Apply INC_EQ. +Cut ((E:Ens)(IN E Omega)->(IN E (Union Omega))) + ->(INC Omega (Union Omega)). +Intros; Apply H. +Clear H. +Intros. +Elim (IN_Omega_EXType E H). +Intros n e. +Apply IN_Union with (Nat (S n)). +Auto with zfc v62. + +Apply IN_sound_left with (Nat n). +Auto with zfc v62. + +(Change (IN (Nat n) (Succ (Nat n))); Auto with zfc v62). + +Intros. +Exact H. + +Cut ((E:Ens)(IN E (Union Omega))->(IN E Omega)) + ->(INC (Union Omega) Omega). +Intros; Apply H; Clear H. +Intros. +Elim (Union_IN Omega E H). +Intros e h. +Elim h. +Intros i1 i2. +Elim (IN_Omega_EXType e i1). +Intros n e1. +Cut (IN E (Nat n)). +Intros. +(Elim (IN_Nat_EXType n E H0); Intros). +(Apply IN_sound_left with (Nat x); Auto with zfc v62). + +(Apply IN_sound_right with e; Auto with zfc v62). + +Intros. +Exact H. +Qed. + +Theorem Omega_Ord : (Ord Omega). +Apply Eo with (Union Omega). +Apply Lo. +Intros. +Elim (IN_Omega_EXType e H). +Intros n ee. +Apply Eo with (Nat n); Auto with zfc v62. +Elim n. +Auto with zfc v62. +Auto with zfc v62. +Intros. +Change (Ord (Succ (Nat n0))); Auto with zfc v62. +Apply EQ_sym; Auto with zfc v62. +Apply Omega_EQ_Union. +Qed. + +Definition Alpha : Ens->Ens. +Induction 1. +Intros A f r. +Apply Union. +Apply (sup A). +Intros a. +Exact (Power (r a)). +Intros A a; Exact (atom A a). (* ??? or Vide? *) +Save. + +Transparent Alpha. + +(******************************************************************************) +(* AXIOM OF CHOICE *) +(******************************************************************************) + +(* A Type-theoretical axiom of choice gives us the collection axiom *) + +Definition collection := + (P:Ens->Ens->Prop) + ((x,x',y:Ens)(EQ x x')->(P x y)->(P x' y))-> + ((E:Ens)(EXType ? (P E)))-> + (E:Ens)(EXType ? [A:Ens](x:Ens)(IN x E)-> + (EXType ? [y:Ens](IN y A)/\(P x y))). + + +Definition choice := + (A,B:Type)(P:A->B->Prop) + ((a:A)(EXType ? [b:B](P a b)))-> + (EXType ? [f:A->B]((a:A)(P a (f a)))). + +Theorem Choice_Collection : choice -> collection. +Intro; Unfold collection; Intros P comp G E; + Cut (EXType ? [f:(Ens->Ens)](B:Ens)(P B (f B))). +Induction 1; Intros f Pf; Elim E. +Intros A g hr; Split with (sup A [a:A](f (g a))). +Simpl; Intros X i; Elim i; Intros a ea; Split with (f (g a)). +Split. +Exists a; Auto with zfc. + +Apply comp with (g a); Auto with zfc. + +Auto with zfc. + +Intros; Split with Vide; Contradiction. + +Unfold choice in H; Apply H; Intros; Elim (G a); Intros b hb; Exists b; + Assumption. +Qed. + +(* If we also assume the excluded middle, we can derive *) +(* the usual replacement schemata. *) + +Definition functional := + [P:Ens->Ens->Prop](x,y,y':Ens) + (P x y)->(P x y')->(EQ y y'). +Definition replacement := + (P:Ens->Ens->Prop) + (functional P)-> + ((x,y,y':Ens)(EQ y y')->(P x y)->(P x y'))-> + ((x,x',y:Ens)(EQ x x')->(P x y)->(P x' y))-> + (X:Ens)(EXType ? [Y:Ens](y:Ens) + (((IN y Y)->(EXType ? [x:Ens](IN x X)/\(P x y))) + /\((EXType ? [x:Ens](IN x X)/\(P x y))->(IN y Y)))). + +Theorem classical_Collection_Replacement : + ((S:Prop)S\/(S->False))-> + collection -> + replacement. +Unfold replacement; Intros EM Collection P fp comp_r comp_l X. +Cut (EXType ? [Y:Ens](y:Ens)((EXType ? [x:Ens](IN x X)/\(P x y))->(IN y Y))). +Induction 1; Intros Y HY. +Exists (Comp Y [y:Ens](EXType ? [x:Ens](IN x X)/\(P x y))). +Intros y; Split. +Intros HC. +Apply (IN_Comp_P Y y [y0:Ens](EXType Ens [x:Ens](IN x X)/\(P x y0))); Auto with zfc v62. +Intros w1 w2; Induction 1; Intros x; Induction 1; Intros Ix Px e. +Exists x; Split; Auto with zfc v62. +Apply comp_r with w1; Auto with zfc v62. +Intros He. +Apply IN_P_Comp. + +Intros w1 w2; Induction 1; Intros x; Induction 1; Intros Ix Px e. +Exists x; Split; Auto with zfc v62. +Apply comp_r with w1; Auto with zfc v62. +Apply HY; Auto with zfc v62. +Auto with zfc v62. + +Elim (Collection [x,y:Ens]((P x y)\/(((y':Ens)(P x y')->False)/\(EQ y Vide)))) + with X. +Intros Y HY. +Elim (EM (EXType ? [x:Ens](IN x X)/\(P x Vide))). +Intros Hvide; Elim Hvide; Intros xv Hxv; Exists Y. +Intros y; Induction 1; Intros x; Induction 1; Intros Hx1 Hx2. +Elim (HY x Hx1). +Intros y'; Induction 1; Intros Hy'1 Hy'2. +Elim Hy'2. +Intros Hy'3; Apply IN_sound_left with y'; Auto with zfc v62. +Apply fp with x; Auto with zfc v62. +Induction 1; Intros Hy'3 Hy'4. +Elim (Hy'3 y Hx2). +Intros HP; Exists (Comp Y [y:Ens]((EQ y Vide)->False)). +Intros y; Induction 1; Intros x; Induction 1; Intros Hx1 Hx2. +Apply IN_P_Comp. +Intros w1 w2 Hw1 Hw Hw2; Apply Hw1; Apply EQ_tran with w2; Auto with zfc v62. +Elim (HY x). +Intros y'; Induction 1; Intros Hy'1 Hy'2. +Elim Hy'2; Intros Hy'3. +Apply IN_sound_left with y'; Auto with zfc v62. +Apply fp with x; Auto with zfc v62. +Elim Hy'3; Intros Hy'4 Hy'5. +Elim (Hy'4 y); Auto with zfc v62. +Assumption. +Intros e; Apply HP; Exists x; Split; Auto with zfc v62; + Apply comp_r with y; Auto with zfc v62; Apply fp; Auto with zfc v62. +Intros x x' y e Hx; Elim Hx; Intros Hx1. +Left; Apply comp_l with x; Auto with zfc v62. +Right; Elim Hx1; Intros Hx2 Hx3; Split. +2 : Assumption. +Intros y' Hy'; Apply (Hx2 y'); Apply comp_l with x'; Auto with zfc v62. +Intros x; Elim (EM (EXType ? [y:Ens](P x y))); Intros Hx. +Elim Hx; Intros x0 Hx0; Exists x0; Left; Assumption. +Exists Vide; Right; Split; Auto with zfc v62. +Intros y Hy; Elim Hx; Exists y; Auto with zfc v62. +Qed. + +(******************************************************************************) +(* SMALL SETS AND THE BIG SET OF SMALL SETS *) +(******************************************************************************) + +(* Some definitions replicated on another type level *) + +Inductive EXType' [P:Type; Q:P->Prop]: Prop := + EXTypei' : (x:P)(Q x)->(EXType' P Q). + +Inductive prod_t' [A,B:Type] : Type := + pair_t' : A->B->(prod_t' A B). + +Inductive depprod'' [A:Type; P : A->Type] : Type := + dep_i'' : (x:A)(P x)->(depprod'' A P). + +(* The small sets *) +Inductive Ens' : Type := + sup' : (A:Type)(A->Ens')->Ens' + | atom' : (A:Type)A->Ens'. + +(* Equality on small sets *) +Definition EQ' : Ens' -> Ens' -> Prop. +Induction 1. +Intros A f eq1. +Induction 1. +Intros B g eq2. +Apply and. +Exact (x:A) + (EXType' ? [y:B](eq1 x (g y))). +Exact (y:B) + (EXType' ? [x:A](eq1 x (g y))). + +Intros A' a'. +Exact False. + +Intros A a. +Induction 1. +Intros A' f eq1. +Exact False. + +Intros. +(*Exact (X == X0).*) +Exact (eq_depT Type [A:Type]A A a A0 y). +Save. + +Transparent EQ'. + +(* small sets can be injected into big sets *) +Definition inj : Ens'->Ens. +Induction 1; [Intros A f fr ; Exact (sup A fr) | Intros A a ; Exact (atom A a)]. +Qed. + +Transparent inj. + +Theorem inj_sound : (E1,E2:Ens')(EQ' E1 E2)->(EQ (inj E1)(inj E2)). +Induction E1; [Intros A1 f1 r1 | Intros A a] ; Induction E2; + [Intros A2 f2 r2 | Contradiction | Contradiction | Intros A' a']. +(Induction 1; Intros HR1 HR2; Split). +(Intros a1; Elim (HR1 a1); Intros a2 Ha2; Exists a2; Auto with zfc v62). +(Intros a2; Elim (HR2 a2); Intros a1 Ha1; Exists a1; Auto with zfc v62). + +Auto with zfc. +Qed. + +Definition Sing' : Ens' -> Ens' := + [E:Ens'] (sup' Un [x:Un]Cases x of void => E end). + +Definition Power' : Ens' -> Ens' := +[E:Ens'] + Cases E of + (sup' A f) => + (sup' ? + [P:A->Prop] + (sup' ? + [c:(depprod'' A [a:A](P a))] + Cases c of + (dep_i'' a p) => (f a) + end + ) + ) + | (atom' A a) => (Sing' (atom' A a)) (* ??? or Vide? *) + end. + +Theorem Power_sound_inj : (E:Ens')(EQ (inj (Power' E))(Power (inj E))). +Induction E; [Intros A f HR | Intros A a]. +Simpl; Split. +Intros P; Exists P; Split. +Intros c; Elim c; Intros a p. +Exists (dep_i A [a0:A](P a0) a p); Simpl; Auto with zfc v62. +Intros c; Elim c; Intros a p. +Exists (dep_i'' A [a0:A](P a0) a p); Simpl; Auto with zfc v62. +Intros P; Exists P; Split. +Intros c; Elim c; Intros a p. +Exists (dep_i A [a0:A](P a0) a p); Simpl; Auto with zfc v62. +Intros c; Elim c; Intros a p. +Exists (dep_i'' A [a0:A](P a0) a p); Simpl; Auto with zfc v62. + +Simpl; Split. +Destruct x; Exists void; Auto with zfc. +Destruct y; Exists void; Auto with zfc. +Qed. + +(* The set of small sets *) +Definition Big := (sup Ens' inj). + +Theorem Big_is_big : (E:Ens')(IN (inj E) Big). +Intros E; Unfold Big; Simpl; Exists E; Auto with zfc. +Qed. + +Theorem IN_Big_small : (E:Ens)(IN E Big)->(EXType' ? [E':Ens'](EQ E (inj E'))). +Unfold Big; Simpl; Induction 1; Intros E' HE'; Exists E'; Assumption. +Qed. + +Theorem IN_small_small : (E:Ens)(E':Ens')(IN E (inj E'))-> + (EXType' ? [E1:Ens'](EQ E (inj E1))). +Induction E'; [Intros A' f' HR' | Contradiction]; Simpl; + Induction 1; Intros a' e'; Exists (f' a'); Assumption. +Qed. + +Theorem Big_closed_for_power : (E:Ens)(IN E Big)->(IN (Power E) Big). +Unfold Big; Simpl; Intros E; Induction 1; Intros E' HE'; Exists (Power' E'). +Apply EQ_tran with (Power (inj E')). +Apply Power_sound; Assumption. +Apply EQ_sym; Apply Power_sound_inj. +Qed. + +(******************************************************************************) +(* NO SET OF ALL SETS *) +(******************************************************************************) + +(* Just for fun : a proof that there is no set of all sets, using *) +(* Russell's paradox construction *) +(* There, of course, are other proofs (foundation, etc) *) + +Theorem Russell : (E:Ens)((E':Ens)(IN E' E))->False. +Intros U HU. +Cut ([x:Ens](IN x x)->False (Comp U [x:Ens](IN x x)->False)). +Intros HR. +Apply HR. +(Apply IN_P_Comp; Auto with zfc v62). +(Intros w1 w2 HF e i; Apply HF; Apply IN_sound_left with w2; Auto with zfc v62; + Apply IN_sound_right with w2; Auto with zfc v62). +Intros H. +Cut (IN (Comp U [x:Ens](IN x x)->False) (Comp U [x:Ens](IN x x)->False)). +Change ([x:Ens](IN x x)->False (Comp U [x:Ens](IN x x)->False)). +Cut (w1,w2:Ens)((IN w1 w1)->False)->(EQ w1 w2)->(IN w2 w2)->False. +Intros ww. +Exact (IN_Comp_P U (Comp U [x:Ens](IN x x)->False) + [x:Ens](IN x x)->False ww H). +(Intros w1 w2 HF e i; Apply HF; Apply IN_sound_left with w2; Auto with zfc v62; + Apply IN_sound_right with w2; Auto with zfc v62). +Assumption. +Qed. + +(******************************************************************************) +(* SOME AXIOMS AND STRANGE THINGS ;-( *) +(* *) +(* The need for axioms is due to the usage of dependent equality, or to my *) +(* ignorance about it ;-) *) +(* *) +(******************************************************************************) + +Axiom a_de_pi2 : + (T:Type)(n,m:T)(existT Type [A:Type]A T n)==(existT Type [A:Type]A T m)->n==m. + +(* The main consequence of the previous axiom *) +Theorem a_pi2 : (T:Type)(n,m:T)(atom T n)==(atom T m)->n==m. +Intros; Inversion H; Apply a_de_pi2; Assumption. +Qed. + +(* This theorem is really strange: I can prove this in general, but I can't *) +(* prove any of it's instance: for example I can't prove *) +(* ~(nat==bool)->~(atom nat O)==(atom bool true) due to an internal error of *) +(* Coq *) +Theorem a_npi1 : (T1,T2:Type)(t1:T1)(t2:T2)~T1==T2->~(atom T1 t1)==(atom T2 t2). +Unfold not; Intros; Apply H; Inversion H0; Reflexivity. +Qed. + +(******************************************************************************) +(* MAPPING A TYPE TO THE SET OF IT'S ELEMENTS *) +(******************************************************************************) + +(* (Ens_of_t T t) is thought as the coercion from an element (t:T) to a set *) +Definition Ens_of_t : (T:Type)T->Ens := + [T:Type][t:T](atom T t). + +(* (Ens_of_T T) is thought as the set of the elements of type T ... *) +Definition Ens_of_T : Type -> Ens := + [T:Type] (sup T [t:T](Ens_of_t T t)). + +(* ... and (Prop_on_Ens_of_Prop T P) is thought as the proposition on Ens *) +(* that is true only for (atom T t) where (t:T) and (P t) is true. *) +Inductive Prop_on_Ens_of_Prop [T:Type; P:T->Prop] : Ens->Prop := + cons : (t:T)(P t)->(Prop_on_Ens_of_Prop T P (atom T t)). + +Theorem Prop_on_Ens_of_Prop_atom_Prop : + (T:Type; P:(T->Prop); t:T)(Prop_on_Ens_of_Prop T P (atom T t))->(P t). +Intros; Inversion H; Replace t with t0. +Assumption. + +Apply a_de_pi2; Assumption. +Qed. + +Theorem Prop_on_Ens_of_Prop_t : + (T:Type; P:(T->Prop); E:Ens) + (Prop_on_Ens_of_Prop T P E) + ->(EXType T [t:T]E==(atom T t)/\(P t)). +Intros. +Inversion H. +Split with t. +Auto. +Qed. + +Lemma EQ_atom: (T:Type)(t:T)(E:Ens)(EQ (atom T t) E)->(atom T t)==E. +Destruct E. +Contradiction. + +Intros. +Inversion H. +Reflexivity. +Qed. + + +Theorem Prop_on_Ens_of_Prop_sound : + (E1,E2:Ens)(T:Type)(P:T->Prop) + (EQ E1 E2) + -> (Prop_on_Ens_of_Prop T P E1) + -> (Prop_on_Ens_of_Prop T P E2). +Intros. +Cut (EXType ? [t:T]E1==(atom T t)/\(P t)). +Destruct 1; Destruct 1. +Intros. +Rewrite H3 in H. +Cut (atom T x)==E2. +Intros. +Rewrite <- H5. +Constructor 1. +Assumption. + +Apply EQ_atom. +Assumption. + +Apply Prop_on_Ens_of_Prop_t. +Assumption. +Qed. + + +(******************************************************************************) +(* EXAMPLES OF USAGE *) +(******************************************************************************) + +(* We could define an implicit coercion from nat to Ens using Ens_of_t *) +Coercion Ens_of_nat := [n:nat](Ens_of_t nat n). + +(* CNat is the set of the natural numbers of Coq ... *) +Definition CNat : Ens := + (Ens_of_T nat). + +Mutual Inductive + is_even : nat->Prop := + is_even_O : (is_even O) + | is_even_S : (n:nat)(is_odd n)->(is_even (S n)) +with + is_odd : nat->Prop := + id_ood_S : (n:nat)(is_even n)->(is_odd (S n)). + +Lemma not_even_odd: (n:nat)(is_even n)->(is_odd n)->False. +Induction n. +Intros; Inversion H0. + +Intros; Apply H; [Inversion H1 | Inversion H0]; Assumption. +Qed. + +Definition Cis_even : Ens -> Prop := + (Prop_on_Ens_of_Prop nat is_even). + +Definition Cis_odd : Ens -> Prop := + (Prop_on_Ens_of_Prop nat is_odd). + +(* ... and CEven and COdd are the sets of even/odd natural numbers of Coq *) + +Definition CEven := (Comp CNat Cis_even). + +Definition COdd := (Comp CNat Cis_odd). + +(* And now an easy fact: the intersection of CEven with COdd is empty *) +Fact COdd_Inter_CEven_EQ_Vide: (EQ (Inter (Paire CEven COdd)) Vide). +Apply INC_EQ. +Cut (E:Ens)(IN E (Inter (Paire CEven COdd)))->(IN E Vide). +Auto. + +Intros. +Cut False. +Contradiction. + +Cut (IN E CEven)/\(IN E COdd). +Destruct 1. +Intros. +Unfold CEven in H1. +Cut (Cis_even E). +Unfold COdd in H2. +Cut (Cis_odd E). +Intros. +Inversion H3. +Inversion H4. +Rewrite <- H6 in H8. +Cut t0==t. +Intro. +Rewrite H9 in H7. +Apply not_even_odd with t; Assumption. + +Apply a_pi2; Assumption. + +Apply IN_Comp_P with CNat. +Intros. +Unfold Cis_odd. +Apply Prop_on_Ens_of_Prop_sound with w1; Assumption. + +Assumption. + +Apply IN_Comp_P with CNat. +Intros. +Unfold Cis_even. +Apply Prop_on_Ens_of_Prop_sound with w1; Assumption. + +Assumption. + +Split. +Apply IN_Inter_all with (Paire CEven COdd). +Assumption. + +Auto with zfc. + +Apply IN_Inter_all with (Paire CEven COdd). +Assumption. + +Auto with zfc. + +Simpl. +Destruct 1. +Destruct x. +Qed. + +(* Another easy fact: O is not in COdd *) +Fact O_not_IN_COdd : ~(IN O COdd). +Unfold not; Intro. +Cut (Cis_odd O). +Intro. +Inversion H0. +Simpl in H1. +Cut t==O. +Intro. +Rewrite H3 in H2. +Inversion H2. + +Apply a_de_pi2. +Assumption. + +Unfold COdd in H. +Apply IN_Comp_P with CNat. +Intros. +Unfold Cis_odd. +Apply Prop_on_Ens_of_Prop_sound with w1. +Assumption. + +Exact H0. + +Assumption. +Qed. diff --git a/helm/EXPORT/exportcsczfc/exporttheories.sh b/helm/EXPORT/exportcsczfc/exporttheories.sh new file mode 100755 index 000000000..419e33d53 --- /dev/null +++ b/helm/EXPORT/exportcsczfc/exporttheories.sh @@ -0,0 +1,10 @@ +#!/bin/bash + +echo "Exporting theory $1"; + +for i in csc_eqdep.v csc_zfc.v + do + basename=$(basename $i | sed s/\\.v//) + cat $i | ../mktheory.pl "csczfc/$basename" > \ + examples/csczfc/$1/$basename.theory.xml + done diff --git a/helm/EXPORT/exportcsczfc/provacsczfc.v b/helm/EXPORT/exportcsczfc/provacsczfc.v new file mode 100644 index 000000000..81737d5a9 --- /dev/null +++ b/helm/EXPORT/exportcsczfc/provacsczfc.v @@ -0,0 +1,6 @@ +Require Xml. +Require csc_eqdep. +Require csc_zfc. + +Print XML Dir Disk "examples/csczfc" csc_eqdep. +Print XML Dir Disk "examples/csczfc" csc_zfc. diff --git a/helm/EXPORT/exportprove/Makefile b/helm/EXPORT/exportprove/Makefile new file mode 100644 index 000000000..28bb13d8a --- /dev/null +++ b/helm/EXPORT/exportprove/Makefile @@ -0,0 +1,14 @@ +all: objects theories + +objects: + coqc -R prove prove prove/*.v + echo "Load Verbose provaStruct." | ~/V7/bin/coqtop.byte -R prove prove + echo "Load Verbose provaFeIota." | ~/V7/bin/coqtop.byte -R prove prove + echo "Load Verbose provaCofix." | ~/V7/bin/coqtop.byte -R prove prove + echo "Load Verbose prova." | ~/V7/bin/coqtop.byte -R prove prove + +theories: + ./exporttheories.sh + +clean: + rm -f *.vo prove/*.vo diff --git a/helm/EXPORT/exportprove/exporttheories.sh b/helm/EXPORT/exportprove/exporttheories.sh new file mode 100755 index 000000000..f7993fe62 --- /dev/null +++ b/helm/EXPORT/exportprove/exporttheories.sh @@ -0,0 +1,10 @@ +#!/bin/bash + +echo "Exporting theory $1"; + +for i in prove/*.v + do + basename=$(basename $i | sed s/\\.v//) + cat $i | ../mktheory.pl "prove/$basename" > \ + examples/prove/$1/$basename.theory.xml + done diff --git a/helm/EXPORT/exportprove/prova.v b/helm/EXPORT/exportprove/prova.v new file mode 100644 index 000000000..0d98e5769 --- /dev/null +++ b/helm/EXPORT/exportprove/prova.v @@ -0,0 +1,34 @@ +Require Export Xml. + +Section prova. + +Inductive + tree : Set := node : forest -> tree +with + forest : Set := leaf : forest | cons : tree -> forest -> forest. + +Fixpoint tree_size [t:tree] : nat := + Cases t of (node f) => (S (forest_size f)) end +with forest_size [f:forest] : nat := + Cases f of leaf => (S O) | (cons t f') => (plus (tree_size t) (forest_size f')) + end. + +Theorem a_ab_b: (A,B:Prop)A->(A->B)->B. +Auto. +Qed. + +Axiom dummy_axiom: (n,m:nat)(le n m)\/(gt n m). + +End prova. + +Print XML Section Disk "examples/prove" prova. + +Theorem ab_ac_abc: (A,B,C:Prop)(A->B)->(A->C)->A->B/\C. +Intros A B C AB AC A1. +Split. + +Show XML File "examples/ab_ac_abc.xml" Proof. + +Auto. +Auto. +Qed. diff --git a/helm/EXPORT/exportprove/provaCofix.v b/helm/EXPORT/exportprove/provaCofix.v new file mode 100644 index 000000000..d0f97294b --- /dev/null +++ b/helm/EXPORT/exportprove/provaCofix.v @@ -0,0 +1,4 @@ +Require Xml. +Require provacofix. + +Print XML Module Disk "examples" provacofix. diff --git a/helm/EXPORT/exportprove/provaFeIota.v b/helm/EXPORT/exportprove/provaFeIota.v new file mode 100644 index 000000000..bc5b2c022 --- /dev/null +++ b/helm/EXPORT/exportprove/provaFeIota.v @@ -0,0 +1,6 @@ +Require Xml. +Require provaF. +Require provaIota. + +Print XML Module Disk "examples" provaF. +Print XML Module Disk "examples" provaIota. diff --git a/helm/EXPORT/exportprove/provaStruct.v b/helm/EXPORT/exportprove/provaStruct.v new file mode 100644 index 000000000..06c952970 --- /dev/null +++ b/helm/EXPORT/exportprove/provaStruct.v @@ -0,0 +1,16 @@ +Require Export Xml. + +Require provastruct. +Print XML Module Disk "examples" provastruct. + +Require provastruct2. +Print XML Module Disk "examples" provastruct2. + +Require provastruct3. +Print XML Module Disk "examples" provastruct3. + +Require provastruct4. +Print XML Module Disk "examples" provastruct4. + +Require provastruct5. +Print XML Module Disk "examples" provastruct5. diff --git a/helm/EXPORT/exportprove/prove/provaF.v b/helm/EXPORT/exportprove/prove/provaF.v new file mode 100644 index 000000000..072010f0c --- /dev/null +++ b/helm/EXPORT/exportprove/prove/provaF.v @@ -0,0 +1,33 @@ +Definition int := (A:Prop)(A->A)->A->A. + +Definition O := [A:Prop][s:A->A][o:A]o. + +Definition S := [n:int][A:Prop][s:A->A][o:A](s (n A s o)). + +Definition Uno := [A:Prop][s:A->A][o:A](s o). + +Definition Due := [A:Prop][s:A->A][o:A](s (s o)). + +Definition Tre := [A:Prop][s:A->A][o:A](s (s (s o))). + +Definition id := [A:Prop][x:A]x. + +Definition id_Due := (id int Due). + +Definition difficult := ((S Due) (int -> int) (id (int -> int)) (id int)). + +Definition is_Zero := [n:int](n int [_:int]Uno O). + +Definition couple := [A:Prop][x:A][y:A][z:A->A->A](z x y). + +Definition Couple := [A:Prop](z:A->A->A)A. + +Definition fst := [A:Prop][x:A][y:A]x. + +Definition snd := [A:Prop][x:A][y:A]y. + +Definition next : (Couple int) -> (Couple int) := [x:(Couple int)](couple int (x (snd int)) (S (x (snd int)))). + +Definition pred := [n:int]((n (Couple int) next (couple int O O))(fst int)). + +Definition test := (((pred Tre) (int -> int))(id (int->int)) (id int)). diff --git a/helm/EXPORT/exportprove/prove/provaIota.v b/helm/EXPORT/exportprove/prove/provaIota.v new file mode 100644 index 000000000..74a510b5d --- /dev/null +++ b/helm/EXPORT/exportprove/prove/provaIota.v @@ -0,0 +1,53 @@ +Inductive bool : Set := true : bool | false : bool. +Inductive nat : Set := O : nat | S : nat -> nat. + +Fixpoint plus [n:nat] : nat -> nat := + [m:nat] + Cases n of + O => m + | (S n) => (S (plus n m)) + end. + +Fixpoint mult [n:nat] : nat -> nat := + [m:nat] + Cases n of + O => O + | (S n) => (plus m (mult n m)) + end. + +Fixpoint fact [n:nat] : nat := + Cases n of + O => (S O) + | (S n) => (mult (S n) (fact n)) + end. + +Definition bnot := + [b:bool] + Cases b of + true => false + | false => true + end. + +Fixpoint is_even [n:nat] : bool := + Cases n of + O => true + | (S n) => (bnot (bnot (is_odd n))) + end +with is_odd [n:nat] : bool := + Cases n of + O => false + | (S n) => (bnot (bnot (is_even n))) + end +. + +Fixpoint idn [n:nat] : nat := + Cases n of + O => O + | (S n) => (S (idn n)) + end. + +Definition test1 := (is_even (S (S O))). +Definition test2 := (is_even (S (S (S O)))). +Definition test3 := (idn (idn (S O))). +Definition test4 := (is_odd (fact (S (S (O))))). +Definition test5 := (is_odd (fact (S (S (S (S (S (S O)))))))). diff --git a/helm/EXPORT/exportprove/prove/provacofix.v b/helm/EXPORT/exportprove/prove/provacofix.v new file mode 100644 index 000000000..199cadeb6 --- /dev/null +++ b/helm/EXPORT/exportprove/prove/provacofix.v @@ -0,0 +1,45 @@ +(* Let's define an infinite tree whose nodes are made of natural value and an *) +(* infinite forest of infinite trees whose nodes ... *) + +(* (obbrobrio_tree n) is used to build such a tree whose root value is n and *) +(* root forest is made of the corecursively defined tress whose roots values *) +(* are (n+1), (n+2), ... *) + +(* To finish, we provide also some destructors and a funny (?!?) theorem *) + +CoInductive tree : Set := + node : nat -> forest -> tree +with forest : Set := + nil : forest + | cons : tree -> forest -> forest. + +CoFixpoint obbrobrio_tree : nat -> tree := + [n:nat] + (node n (obbrobrio_forest (S n) nil)) +with obbrobrio_forest : nat -> forest -> forest := + [n:nat][f:forest] + (cons (obbrobrio_tree n) (obbrobrio_forest (S n) f)). + +Definition root_value : tree -> nat := + [t:tree] + Cases t of + (node n _) => n + end. + +Definition root_forest : tree -> forest := + [t:tree] + Cases t of + (node _ f) => f + end. + +Definition root_tree : forest -> tree := + [f:forest] + Cases f of + nil => (obbrobrio_tree (S (S (S O)))) + | (cons t _) => t + end. + +Theorem easy : (root_value (root_tree (root_forest (obbrobrio_tree O))))=(S O). +Proof. + Trivial. +Qed. diff --git a/helm/EXPORT/exportprove/prove/provastruct.v b/helm/EXPORT/exportprove/prove/provastruct.v new file mode 100644 index 000000000..503c7e0ac --- /dev/null +++ b/helm/EXPORT/exportprove/prove/provastruct.v @@ -0,0 +1,22 @@ +Require Export Xml. + +Section a. + Variable A:Prop. + Section b1. + Variable B:Prop. + Axiom axiom: A -> (A -> B) ->B. + Theorem th1: A -> (A -> B) -> A/\B. + Intros A' H. + Split. + Assumption. + Apply axiom; Assumption. + Qed. + End b1. + Section b2. + Variable B:Set. + Axiom axiom': (A:Prop)A->A. + End b2. + Theorem th1': (A:Prop)A->A. + Auto. + Qed. +End a. diff --git a/helm/EXPORT/exportprove/prove/provastruct2.v b/helm/EXPORT/exportprove/prove/provastruct2.v new file mode 100644 index 000000000..0784e9794 --- /dev/null +++ b/helm/EXPORT/exportprove/prove/provastruct2.v @@ -0,0 +1,42 @@ +Section init. +Section a. + Section a1. + Section a11. + Section a111. + Local uno := (S O). + End a111. + Section a112. + End a112. + Section a113. + End a113. + End a11. + Local uno := (S O). + End a1. + Section a2. + Section a21. + Local uno := (S O). + End a21. + Section a22. + Section a221. + End a221. + End a22. + Section a23. + Section a231. + Section a2311. + Local uno := (S O). + End a2311. + Section a2312. + End a2312. + Section a2313. + End a2313. + End a231. + Section a232. + Section a2321. + End a2321. + End a232. + End a23. + Local uno := (S O). + End a2. + Definition uno := (S O). +End a. +End init. diff --git a/helm/EXPORT/exportprove/prove/provastruct3.v b/helm/EXPORT/exportprove/prove/provastruct3.v new file mode 100644 index 000000000..d18933010 --- /dev/null +++ b/helm/EXPORT/exportprove/prove/provastruct3.v @@ -0,0 +1,11 @@ +Section a. + Section a1. + Variable A : Prop. + Variable B : Prop. + Inductive t1 : Set := k1 : A -> t1. + End a1. + + Inductive t2 [B:Set] : Set := k2 : (t2 B). + + Variable A : Prop. +End a. diff --git a/helm/EXPORT/exportprove/prove/provastruct4.v b/helm/EXPORT/exportprove/prove/provastruct4.v new file mode 100644 index 000000000..1307f46e5 --- /dev/null +++ b/helm/EXPORT/exportprove/prove/provastruct4.v @@ -0,0 +1,8 @@ +Section a. + Variables N,M:nat. + Section b. + Variable P:Prop. + Local SN := (S N). + Axiom A : N = M. + End b. +End a. diff --git a/helm/EXPORT/exportprove/prove/provastruct5.v b/helm/EXPORT/exportprove/prove/provastruct5.v new file mode 100644 index 000000000..952c9d21a --- /dev/null +++ b/helm/EXPORT/exportprove/prove/provastruct5.v @@ -0,0 +1,11 @@ +Section a. + Variable A:Prop. + Theorem easy:(B:Prop)B->B. + Exact ([H:Prop][B:Prop][b:B]b A). + Qed. + Section b. + Theorem easy':(B:Prop)B->B. + Exact easy. + Qed. + End b. +End a. diff --git a/helm/EXPORT/mktheory.pl b/helm/EXPORT/mktheory.pl new file mode 100755 index 000000000..2be018e98 --- /dev/null +++ b/helm/EXPORT/mktheory.pl @@ -0,0 +1,151 @@ +#!/usr/bin/perl + +# Assumptions: +# Comments on one line are stripped +# Comments on many lines: +# nothing after *) (end of command) +# Commands could be nested (but see previous assumption) +# Commands don't span on several lines +# If a line is commented, the comment must begin at the begin of line and end +# at the end of line +# In a line, before a command only spaces are allowed + +$curi = $ARGV[0]; +$with_types = ($ARGV[1] ? ".types" : ""); +$ident = " "; +$cid = 1; +$opencom = 0; +$openscheme = 0; +$openfix = 0; +$opengoal = 0; + +print < + + + +EOT + +while () { + chomp; + if ($opencom > 0) { + $opencom-- if (/\*\)/ && !/\(\*.*\*\)/); + } else { + if (/\(\*.*\*\)/) { # (* comment *) + s/\(\*.*\*\)//; + } elsif (/\(\*/) { + # (* comment + $opencom++; + $_ = ""; + } + + if (/Require /) { + s/ *Require *(.*)\..*/$1/; + print "$ident\n"; + } elsif (/Goal /) { + $opengoal = 1; + } elsif (/Section /) { + s/ *Section *(.*)\..*/$1/; + print "$ident
\n"; + $ident = $ident." "; + } elsif (/Chapter /) { + s/ *Chapter *(.*)\..*/$1/; + print "$ident
\n"; + $ident = $ident." "; + } elsif (/End /) { + chop($ident); + print "$ident
\n"; + } elsif (/Variable(s?) /) { + s/ *Variable(s?) *([^:]*):.*/$2/; + s/ //g; + @vl = split /,/; + foreach (@vl) { + print "$ident\n"; + } + } elsif (/Hypothesis /) { + s/ *Hypothesis *([^ :]*)( |:).*/$1/; + @vl = split /,/; + foreach (@vl) { + print "$ident\n"; + } + } elsif (/^ *Inductive /) { + if (/ *Inductive *[^ :]+ ([^ :]*) :=/) { + s/ *Inductive *[^ :]+ ([^ :]*) *:=.*/$1/; + } elsif (/ *Inductive *[^ :]*( |:)/) { + s/ *Inductive *([^ :\[]*)( |:|\[).*/$1/; + } + print "$ident\n"; + } elsif (/ *CoInductive /) { + if (/ *CoInductive *[^ :]+ ([^ :]*) *:=/) { + s/ *CoInductive *[^ :]+ ([^ :]*) *:=.*/$1/; + } elsif (/ *CoInductive *[^ :]*( |:)/) { + s/ *CoInductive *([^ :]*)( |:).*/$1/; + } + print "$ident\n"; + } elsif (/^ *Fixpoint /) { + s/ *Fixpoint *([^ \[]*)( |\[).*/$1/; + print "$ident\n"; + $openfix = 1; + } elsif (/ *CoFixpoint /) { + s/ *CoFixpoint *([^ \[]*)( |\[).*/$1/; + print "$ident\n"; + $openfix = 1; + } elsif (/^ *Definition /) { + s/ *Definition *([^ :]*)( |:)?.*/$1/; + print "$ident\n"; + } elsif (/Local /) { + s/ *Local *([^ :]*)( |:)?.*/$1/; + print "$ident\n"; + } elsif (/Lemma /) { + s/ *Lemma *([^ :]*)( |:)?.*/$1/; + print "$ident\n"; + $cid++; + } elsif (/Theorem /) { + s/ *Theorem *([^ :]+)( |:)?.*/$1/; + print "$ident\n"; + $cid++; + } elsif (/Remark /) { + s/ *Remark *([^ :]*)( |:)?.*/$1/; + print "$ident\n"; + $cid++; + } elsif (/Scheme /) { + s/ *Scheme *([^ :]*)( |:)?.*/$1/; + print "$ident\n"; + $cid++; + $openscheme = 1; + } elsif (/Save / && $opengoal) { + s/ *Save *([^ \.]*)( |\.).*/$1/; + print "$ident\n"; + $cid++; + } elsif (/with / && $openscheme) { + s/ *with *([^ :]*)( |:).*/$1/; + print "$ident\n"; + $cid++; + } elsif (/with / && $openfix) { + s/ *with *([^ :]*)( |:).*/$1/; + print "$ident\n"; + $cid++; + } elsif (/Axiom /) { + s/ *Axiom *([^ :]*)( |:).*/$1/; + print "$ident\n"; + $cid++; + } elsif (/Parameter /) { + s/ *Parameter *([^ :]*)( |:).*/$1/; + print "$ident\n"; + $cid++; + } elsif (/Record /) { + s/ *Record *([^ :]*)( |:).*/$1/; + print "$ident\n"; + $cid++; + } + + if ($openscheme && (/\./)) { + $openscheme = 0; + } elsif ($openfix && (/\./)) { + $openfix = 0; + } + + } +} + +print "\n";