]> matita.cs.unibo.it Git - helm.git/commitdiff
Many files added. Symbolic links missing. examples and contrib missing due
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 7 Dec 2000 14:33:18 +0000 (14:33 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 7 Dec 2000 14:33:18 +0000 (14:33 +0000)
to lack of space

41 files changed:
helm/EXPORT/export_Utrecht_Ramsey/Makefile [new file with mode: 0644]
helm/EXPORT/export_Utrecht_Ramsey/exporttheories.sh [new file with mode: 0755]
helm/EXPORT/export_Utrecht_Ramsey/prova_Utrecht_Ramsey.v [new file with mode: 0644]
helm/EXPORT/exportcoq/Makefile [new file with mode: 0644]
helm/EXPORT/exportcoq/export_contrib_theory.sh [new file with mode: 0755]
helm/EXPORT/exportcoq/export_theory_theory.sh [new file with mode: 0755]
helm/EXPORT/exportcoq/exporttheories.sh [new file with mode: 0755]
helm/EXPORT/exportcoq/provacoq.v [new file with mode: 0644]
helm/EXPORT/exportcoq/provacoqArith.v [new file with mode: 0644]
helm/EXPORT/exportcoq/provacoqBool.v [new file with mode: 0644]
helm/EXPORT/exportcoq/provacoqInit.v [new file with mode: 0644]
helm/EXPORT/exportcoq/provacoqLists.v [new file with mode: 0644]
helm/EXPORT/exportcoq/provacoqLogic.v [new file with mode: 0644]
helm/EXPORT/exportcoq/provacoqReals.v [new file with mode: 0644]
helm/EXPORT/exportcoq/provacoqRelations.v [new file with mode: 0644]
helm/EXPORT/exportcoq/provacoqSets.v [new file with mode: 0644]
helm/EXPORT/exportcoq/provacoqSorting.v [new file with mode: 0644]
helm/EXPORT/exportcoq/provacoqTrees.v [new file with mode: 0644]
helm/EXPORT/exportcoq/provacoqZArith.v [new file with mode: 0644]
helm/EXPORT/exportcoq/provacoqcontribOmega.v [new file with mode: 0644]
helm/EXPORT/exportcoq/provacoqcontribRing.v [new file with mode: 0644]
helm/EXPORT/exportcsczfc/Makefile [new file with mode: 0644]
helm/EXPORT/exportcsczfc/csc_zfc/csc_eqdep.v [new file with mode: 0644]
helm/EXPORT/exportcsczfc/csc_zfc/csc_zfc.v [new file with mode: 0644]
helm/EXPORT/exportcsczfc/exporttheories.sh [new file with mode: 0755]
helm/EXPORT/exportcsczfc/provacsczfc.v [new file with mode: 0644]
helm/EXPORT/exportprove/Makefile [new file with mode: 0644]
helm/EXPORT/exportprove/exporttheories.sh [new file with mode: 0755]
helm/EXPORT/exportprove/prova.v [new file with mode: 0644]
helm/EXPORT/exportprove/provaCofix.v [new file with mode: 0644]
helm/EXPORT/exportprove/provaFeIota.v [new file with mode: 0644]
helm/EXPORT/exportprove/provaStruct.v [new file with mode: 0644]
helm/EXPORT/exportprove/prove/provaF.v [new file with mode: 0644]
helm/EXPORT/exportprove/prove/provaIota.v [new file with mode: 0644]
helm/EXPORT/exportprove/prove/provacofix.v [new file with mode: 0644]
helm/EXPORT/exportprove/prove/provastruct.v [new file with mode: 0644]
helm/EXPORT/exportprove/prove/provastruct2.v [new file with mode: 0644]
helm/EXPORT/exportprove/prove/provastruct3.v [new file with mode: 0644]
helm/EXPORT/exportprove/prove/provastruct4.v [new file with mode: 0644]
helm/EXPORT/exportprove/prove/provastruct5.v [new file with mode: 0644]
helm/EXPORT/mktheory.pl [new file with mode: 0755]

diff --git a/helm/EXPORT/export_Utrecht_Ramsey/Makefile b/helm/EXPORT/export_Utrecht_Ramsey/Makefile
new file mode 100644 (file)
index 0000000..2015d17
--- /dev/null
@@ -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 (executable)
index 0000000..b2dd5f8
--- /dev/null
@@ -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 (file)
index 0000000..aa0500f
--- /dev/null
@@ -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 (file)
index 0000000..79c7463
--- /dev/null
@@ -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 (executable)
index 0000000..6ebb2ad
--- /dev/null
@@ -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 (executable)
index 0000000..d2e5442
--- /dev/null
@@ -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 (executable)
index 0000000..5fdc473
--- /dev/null
@@ -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 (file)
index 0000000..99b52eb
--- /dev/null
@@ -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 (file)
index 0000000..1fdc4f9
--- /dev/null
@@ -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 (file)
index 0000000..a898237
--- /dev/null
@@ -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 (file)
index 0000000..d40ea3e
--- /dev/null
@@ -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 (file)
index 0000000..91b74ef
--- /dev/null
@@ -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 (file)
index 0000000..e2296a5
--- /dev/null
@@ -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 (file)
index 0000000..445f9f9
--- /dev/null
@@ -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 (file)
index 0000000..c588b30
--- /dev/null
@@ -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 (file)
index 0000000..9502861
--- /dev/null
@@ -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 (file)
index 0000000..ff940fd
--- /dev/null
@@ -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 (file)
index 0000000..a90b041
--- /dev/null
@@ -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 (file)
index 0000000..ff43bbd
--- /dev/null
@@ -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 (file)
index 0000000..04d2994
--- /dev/null
@@ -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 (file)
index 0000000..bfc2633
--- /dev/null
@@ -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 (file)
index 0000000..7016b28
--- /dev/null
@@ -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 (file)
index 0000000..8019c08
--- /dev/null
@@ -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 (file)
index 0000000..a109239
--- /dev/null
@@ -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]<Ens>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 (executable)
index 0000000..419e33d
--- /dev/null
@@ -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 (file)
index 0000000..81737d5
--- /dev/null
@@ -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 (file)
index 0000000..28bb13d
--- /dev/null
@@ -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 (executable)
index 0000000..f7993fe
--- /dev/null
@@ -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 (file)
index 0000000..0d98e57
--- /dev/null
@@ -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 (file)
index 0000000..d0f9729
--- /dev/null
@@ -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 (file)
index 0000000..bc5b2c0
--- /dev/null
@@ -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 (file)
index 0000000..06c9529
--- /dev/null
@@ -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 (file)
index 0000000..072010f
--- /dev/null
@@ -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 (file)
index 0000000..74a510b
--- /dev/null
@@ -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 (file)
index 0000000..199cade
--- /dev/null
@@ -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 (file)
index 0000000..503c7e0
--- /dev/null
@@ -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 (file)
index 0000000..0784e97
--- /dev/null
@@ -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 (file)
index 0000000..d189330
--- /dev/null
@@ -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 (file)
index 0000000..1307f46
--- /dev/null
@@ -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 (file)
index 0000000..952c9d2
--- /dev/null
@@ -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 (executable)
index 0000000..2be018e
--- /dev/null
@@ -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;
+<?xml version="1.0" encoding="ISO-8859-1"?>
+<!DOCTYPE Theory SYSTEM "http://localhost:8081/getdtd?uri=maththeory.dtd">
+
+<Theory uri="cic:/$curi">
+EOT
+
+while (<STDIN>) {
+ chomp;
+ if ($opencom > 0) {
+  $opencom-- if (/\*\)/ && !/\(\*.*\*\)/);
+ } else {
+  if (/\(\*.*\*\)/) { # (* comment *)
+   s/\(\*.*\*\)//;
+  } elsif (/\(\*/) {
+   # (* comment
+   $opencom++;
+   $_ = "";
+  }
+
+  if (/Require /) {
+   s/ *Require *(.*)\..*/$1/;
+   print "$ident<!-- Require $_ -->\n";
+  } elsif (/Goal /) {
+   $opengoal = 1;
+  } elsif (/Section /) {
+   s/ *Section *(.*)\..*/$1/;
+   print "$ident<SECTION uri=\"$1\">\n";
+   $ident = $ident." ";
+  } elsif (/Chapter /) {
+   s/ *Chapter *(.*)\..*/$1/;
+   print "$ident<SECTION uri=\"$1\">\n";
+   $ident = $ident." ";
+  } elsif (/End /) {
+   chop($ident);
+   print "$ident</SECTION>\n";
+  } elsif (/Variable(s?) /) {
+   s/ *Variable(s?) *([^:]*):.*/$2/;
+   s/ //g;
+   @vl = split /,/;
+   foreach (@vl) {
+    print "$ident<VARIABLE uri=\"$_.var$with_types\"/>\n";
+   }
+  } elsif (/Hypothesis /) {
+   s/ *Hypothesis *([^ :]*)( |:).*/$1/;
+   @vl = split /,/;
+   foreach (@vl) {
+    print "$ident<VARIABLE uri=\"$_.var$with_types\"/>\n";
+   }
+  } elsif (/^ *Inductive /) {
+   if (/ *Inductive *[^ :]+ ([^ :]*) :=/) {
+    s/ *Inductive *[^ :]+ ([^ :]*) *:=.*/$1/;
+   } elsif (/ *Inductive *[^ :]*( |:)/) {
+    s/ *Inductive *([^ :\[]*)( |:|\[).*/$1/;
+   }
+   print "$ident<DEFINITION uri=\"$_.ind$with_types\"/>\n";
+  } elsif (/ *CoInductive /) {
+   if (/ *CoInductive *[^ :]+ ([^ :]*) *:=/) {
+    s/ *CoInductive *[^ :]+ ([^ :]*) *:=.*/$1/;
+   } elsif (/ *CoInductive *[^ :]*( |:)/) {
+    s/ *CoInductive *([^ :]*)( |:).*/$1/;
+   }
+   print "$ident<DEFINITION uri=\"$_.ind$with_types\"/>\n";
+  } elsif (/^ *Fixpoint /) {
+   s/ *Fixpoint *([^ \[]*)( |\[).*/$1/;
+   print "$ident<DEFINITION uri=\"$_.con$with_types\"/>\n";
+   $openfix = 1;
+  } elsif (/ *CoFixpoint /) {
+   s/ *CoFixpoint *([^ \[]*)( |\[).*/$1/;
+   print "$ident<DEFINITION uri=\"$_.con$with_types\"/>\n";
+   $openfix = 1;
+  } elsif (/^ *Definition /) {
+   s/ *Definition *([^ :]*)( |:)?.*/$1/;
+   print "$ident<DEFINITION uri=\"$_.con$with_types\"/>\n";
+  } elsif (/Local /) {
+   s/ *Local *([^ :]*)( |:)?.*/$1/;
+   print "$ident<DEFINITION uri=\"$_.con$with_types\"/>\n";
+  } elsif (/Lemma /) {
+   s/ *Lemma *([^ :]*)( |:)?.*/$1/;
+   print "$ident<THEOREM id=\"id$cid\" uri=\"$_.con$with_types\"/>\n";
+   $cid++;
+  } elsif (/Theorem /) {
+   s/ *Theorem *([^ :]+)( |:)?.*/$1/;
+   print "$ident<THEOREM id=\"id$cid\" uri=\"$_.con$with_types\"/>\n";
+   $cid++;
+  } elsif (/Remark /) {
+   s/ *Remark *([^ :]*)( |:)?.*/$1/;
+   print "$ident<THEOREM id=\"id$cid\" uri=\"$_.con$with_types\"/>\n";
+   $cid++;
+  } elsif (/Scheme /) {
+   s/ *Scheme *([^ :]*)( |:)?.*/$1/;
+   print "$ident<THEOREM id=\"id$cid\" uri=\"$_.con$with_types\"/>\n";
+   $cid++;
+   $openscheme = 1;
+  } elsif (/Save / && $opengoal) {
+   s/ *Save *([^ \.]*)( |\.).*/$1/;
+   print "$ident<THEOREM id=\"id$cid\" uri=\"$_.con$with_types\"/>\n";
+   $cid++;
+  } elsif (/with / && $openscheme) {
+   s/ *with *([^ :]*)( |:).*/$1/;
+   print "$ident<THEOREM id=\"id$cid\" uri=\"$_.con$with_types\"/>\n";
+   $cid++;
+  } elsif (/with / && $openfix) {
+   s/ *with *([^ :]*)( |:).*/$1/;
+   print "$ident<DEFINITION uri=\"$_.con$with_types\"/>\n";
+   $cid++;
+  } elsif (/Axiom /) {
+   s/ *Axiom *([^ :]*)( |:).*/$1/;
+   print "$ident<AXIOM id=\"id$cid\" uri=\"$_.con$with_types\"/>\n";
+   $cid++;
+  } elsif (/Parameter /) {
+   s/ *Parameter *([^ :]*)( |:).*/$1/;
+   print "$ident<AXIOM id=\"id$cid\" uri=\"$_.con$with_types\"/>\n";
+   $cid++;
+  } elsif (/Record /) {
+   s/ *Record *([^ :]*)( |:).*/$1/;
+   print "$ident<DEFINITION uri=\"$_.ind$with_types\"/>\n";
+   $cid++;
+  }
+
+  if ($openscheme && (/\./)) {
+   $openscheme = 0;
+  } elsif ($openfix && (/\./)) {
+   $openfix = 0;
+  }
+
+ }
+}
+
+print "</Theory>\n";