aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--plugins/xml/xmlcommand.ml12
-rwxr-xr-xtest-suite/check19
-rw-r--r--test-suite/misc/berardi_test.v155
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.