diff options
| -rw-r--r-- | plugins/xml/xmlcommand.ml | 12 | ||||
| -rwxr-xr-x | test-suite/check | 19 | ||||
| -rw-r--r-- | test-suite/misc/berardi_test.v | 155 |
3 files changed, 180 insertions, 6 deletions
diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml index 294f5154d..b3b2e2654 100644 --- a/plugins/xml/xmlcommand.ml +++ b/plugins/xml/xmlcommand.ml @@ -660,23 +660,23 @@ let _ = None -> Buffer.output_buffer stdout theory_buffer ; | Some fn -> - let ch = open_out (fn ^ ".v") in + let ch = open_out (fn ^ ".v") in Buffer.output_buffer ch theory_buffer ; + close_out ch; + (* dummy glob file *) + let ch = open_out (fn ^ ".glob") in close_out ch end ; Option.iter (fun fn -> let coqdoc = Filename.concat (Envars.coqbin ()) ("coqdoc" ^ Coq_config.exec_extension) in let options = " --html -s --body-only --no-index --latin1 --raw-comments" in - let dir = Option.get xml_library_root in let command cmd = if Sys.command cmd <> 0 then Util.anomaly ("Error executing \"" ^ cmd ^ "\"") in - command (coqdoc^options^" -d "^dir^" "^fn^".v"); - let dot = if fn.[0]='/' then "." else "" in - command ("mv "^dir^"/"^dot^"*.html "^fn^".xml "); - command ("rm "^fn^".v"); + command (coqdoc^options^" -o "^fn^".xml "^fn^".v"); + command ("rm "^fn^".v "^fn^".glob"); print_string("\nWriting on file \"" ^ fn ^ ".xml\" was successful\n")) ofn) ;; diff --git a/test-suite/check b/test-suite/check index efac178c0..d0c5790bb 100755 --- a/test-suite/check +++ b/test-suite/check @@ -4,8 +4,10 @@ if [ "$1" = -byte ]; then coqtop="../bin/coqtop.byte -boot -q -batch -I prerequisite" + bincoqc="../bin/coqc -byte -I prerequisite" else coqtop="../bin/coqtop -boot -q -batch -I prerequisite" + bincoqc="../bin/coqc -I prerequisite" fi command="$coqtop -top Top -load-vernac-source" @@ -249,6 +251,21 @@ prepare_tests () { done } +test_misc () { + # Non-standard features + + # Test xml compilation + printf " xml..." + COQ_XML_LIBRARY_ROOT=misc/xml $bincoqc -xml misc/berardi_test > /dev/null 2>&1 + if [ ! -d misc/xml ]; then + printf "failed\n" + else + printf "apparently ok\n" + nbtestsok=`expr $nbtestsok + 1` + rm -r misc/xml + fi +} + # Programme principal echo "Preparing tests" @@ -267,6 +284,8 @@ echo "Interactive tests" test_interactive interactive echo "Micromega tests" test_success micromega +echo "Miscellaneous tests" +test_misc # We give a chance to disable the complexity tests which may cause # random build failures on build farms diff --git a/test-suite/misc/berardi_test.v b/test-suite/misc/berardi_test.v new file mode 100644 index 000000000..5b2f5063b --- /dev/null +++ b/test-suite/misc/berardi_test.v @@ -0,0 +1,155 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id$ i*) + +(** This file formalizes Berardi's paradox which says that in + the calculus of constructions, excluded middle (EM) and axiom of + choice (AC) imply proof irrelevance (PI). + Here, the axiom of choice is not necessary because of the use + of inductive types. +<< +@article{Barbanera-Berardi:JFP96, + author = {F. Barbanera and S. Berardi}, + title = {Proof-irrelevance out of Excluded-middle and Choice + in the Calculus of Constructions}, + journal = {Journal of Functional Programming}, + year = {1996}, + volume = {6}, + number = {3}, + pages = {519-525} +} +>> *) + +Set Implicit Arguments. + +Section Berardis_paradox. + +(** Excluded middle *) +Hypothesis EM : forall P:Prop, P \/ ~ P. + +(** Conditional on any proposition. *) +Definition IFProp (P B:Prop) (e1 e2:P) := + match EM B with + | or_introl _ => e1 + | or_intror _ => e2 + end. + +(** Axiom of choice applied to disjunction. + Provable in Coq because of dependent elimination. *) +Lemma AC_IF : + forall (P B:Prop) (e1 e2:P) (Q:P -> Prop), + (B -> Q e1) -> (~ B -> Q e2) -> Q (IFProp B e1 e2). +Proof. +intros P B e1 e2 Q p1 p2. +unfold IFProp in |- *. +case (EM B); assumption. +Qed. + + +(** We assume a type with two elements. They play the role of booleans. + The main theorem under the current assumptions is that [T=F] *) +Variable Bool : Prop. +Variable T : Bool. +Variable F : Bool. + +(** The powerset operator *) +Definition pow (P:Prop) := P -> Bool. + + +(** A piece of theory about retracts *) +Section Retracts. + +Variables A B : Prop. + +Record retract : Prop := + {i : A -> B; j : B -> A; inv : forall a:A, j (i a) = a}. + +Record retract_cond : Prop := + {i2 : A -> B; j2 : B -> A; inv2 : retract -> forall a:A, j2 (i2 a) = a}. + + +(** The dependent elimination above implies the axiom of choice: *) +Lemma AC : forall r:retract_cond, retract -> forall a:A, j2 r (i2 r a) = a. +Proof. +intros r. +case r; simpl in |- *. +trivial. +Qed. + +End Retracts. + +(** This lemma is basically a commutation of implication and existential + quantification: (EX x | A -> P(x)) <=> (A -> EX x | P(x)) + which is provable in classical logic ( => is already provable in + intuitionnistic logic). *) + +Lemma L1 : forall A B:Prop, retract_cond (pow A) (pow B). +Proof. +intros A B. +destruct (EM (retract (pow A) (pow B))) as [(f0,g0,e) | hf]. + exists f0 g0; trivial. + exists (fun (x:pow A) (y:B) => F) (fun (x:pow B) (y:A) => F); intros; + destruct hf; auto. +Qed. + + +(** The paradoxical set *) +Definition U := forall P:Prop, pow P. + +(** Bijection between [U] and [(pow U)] *) +Definition f (u:U) : pow U := u U. + +Definition g (h:pow U) : U := + fun X => let lX := j2 (L1 X U) in let rU := i2 (L1 U U) in lX (rU h). + +(** We deduce that the powerset of [U] is a retract of [U]. + This lemma is stated in Berardi's article, but is not used + afterwards. *) +Lemma retract_pow_U_U : retract (pow U) U. +Proof. +exists g f. +intro a. +unfold f, g in |- *; simpl in |- *. +apply AC. +exists (fun x:pow U => x) (fun x:pow U => x). +trivial. +Qed. + +(** Encoding of Russel's paradox *) + +(** The boolean negation. *) +Definition Not_b (b:Bool) := IFProp (b = T) F T. + +(** the set of elements not belonging to itself *) +Definition R : U := g (fun u:U => Not_b (u U u)). + + +Lemma not_has_fixpoint : R R = Not_b (R R). +Proof. +unfold R at 1 in |- *. +unfold g in |- *. +rewrite AC with (r := L1 U U) (a := fun u:U => Not_b (u U u)). +trivial. +exists (fun x:pow U => x) (fun x:pow U => x); trivial. +Qed. + + +Theorem classical_proof_irrelevence : T = F. +Proof. +generalize not_has_fixpoint. +unfold Not_b in |- *. +apply AC_IF. +intros is_true is_false. +elim is_true; elim is_false; trivial. + +intros not_true is_true. +elim not_true; trivial. +Qed. + +End Berardis_paradox. |