Ajout infos de débogage de "universe inconsistency" quand option Set

  Printing Universes est active.
Ajout de l'option "using" à la tactique non documentée "auto decomp".
Ajout de la base "extcore" pour étendre "auto decomp" avec des
  principes élémentaires tels que le dépliage de "iff".
Quelques extensions/raffinements dans ChoiceFacts et ClassicalFacts.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10156 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 69 insertions, 5 deletions

diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index bdc8f9de68..8deb362cd9 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -89,6 +89,8 @@ Theorem iff_sym : forall A B:Prop, (A <-> B) -> (B <-> A).
 
 End Equivalence.
 
+Hint Unfold iff: extcore.
+
 (** [(IF_then_else P Q R)], written [IF P then Q else R] denotes
     either [P] and [Q], or [~P] and [Q] *)
 
diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v
index 75043c4229..488da63b68 100644
--- a/theories/Logic/ChoiceFacts.v
+++ b/theories/Logic/ChoiceFacts.v
@@ -95,9 +95,9 @@ Section ChoiceSchemes.
 
 Variables A B :Type.
 
-Variables P:A->Prop.
+Variable P:A->Prop.
 
-Variables R:A->B->Prop.
+Variable R:A->B->Prop.
 
 (** ** Constructive choice and description *)
 
@@ -396,6 +396,16 @@ Proof.
   intro x; apply IndPrem; eauto.
 Qed.
 
+Lemma fun_choice_and_indep_general_prem_iff_guarded_fun_choice :
+  FunctionalChoiceOnInhabitedSet /\ IndependenceOfGeneralPremises
+  <-> GuardedFunctionalChoice.
+Proof.
+  auto decomp using
+    guarded_fun_choice_imp_indep_of_general_premises,
+    guarded_fun_choice_imp_fun_choice,
+    fun_choice_and_indep_general_prem_imp_guarded_fun_choice.
+Qed.
+
 (** AC_fun + Drinker = OAC_fun *)
 
 (** This was already observed by Bell [Bell] *)
@@ -427,6 +437,16 @@ Proof.
   exists f; assumption.
 Qed.
 
+Lemma fun_choice_and_small_drinker_iff_omniscient_fun_choice :
+  FunctionalChoiceOnInhabitedSet /\ SmallDrinker'sParadox 
+  <-> OmniscientFunctionalChoice.
+Proof.
+  auto decomp using 
+    omniscient_fun_choice_imp_small_drinker,
+    omniscient_fun_choice_imp_fun_choice,
+    fun_choice_and_small_drinker_imp_omniscient_fun_choice.
+Qed.
+
 (** OAC_fun = GAC_fun *)
 
 (** This is derivable from the intuitionistic equivalence between IGP and Drinker
@@ -614,6 +634,14 @@ Proof.
   destruct Heq using eq_indd; trivial.
 Qed.
 
+Theorem dep_iff_non_dep_functional_rel_reification : 
+  FunctionalRelReification <-> DependentFunctionalRelReification.
+Proof.
+  auto decomp using
+    non_dep_dep_functional_rel_reification,
+    dep_non_dep_functional_rel_reification.
+Qed.
+
 (**********************************************************************)
 (** * Non contradiction of constructive descriptions wrt functional axioms of choice *)
 
@@ -649,10 +677,10 @@ Qed.
 (** ** Non contradiction of definite description *)
 
 Lemma relative_non_contradiction_of_definite_descr :
-  (ConstructiveDefiniteDescription -> False)
-  -> (FunctionalRelReification -> False).
+  forall C:Prop, (ConstructiveDefiniteDescription -> C)
+  -> (FunctionalRelReification -> C).
 Proof.
-  intros H FunReify.
+  intros C H FunReify.
   assert (DepFunReify := non_dep_dep_functional_rel_reification FunReify).
   pose (A0 := { A:Type & { P:A->Prop & exists! x, P x }}).
   pose (B0 := fun x:A0 => projT1 x).
@@ -675,6 +703,19 @@ Proof.
   apply (proj2_sig (DefDescr B (R x) (H x))).
 Qed.
 
+(** Remark, the following lemma morally holds:
+
+Definition In_propositional_context (A:Type) := forall C:Prop, (A -> C) -> C.
+
+Lemma constructive_definite_descr_in_prop_context_iff_fun_reification :
+   In_propositional_context ConstructiveDefiniteDescription
+   <-> FunctionalRelReification.
+
+but expecting [FunctionalRelReification] to be applied on the same
+Type universes on both sides of the equivalence breaks the
+stratification of universes.
+*)
+
 (**********************************************************************)
 (** * Excluded-middle + definite description => computational excluded-middle *)
 
diff --git a/theories/Logic/ClassicalFacts.v b/theories/Logic/ClassicalFacts.v
index ad91718439..f3f177a734 100644
--- a/theories/Logic/ClassicalFacts.v
+++ b/theories/Logic/ClassicalFacts.v
@@ -91,6 +91,17 @@ Proof.
     right; apply (Ext A False); split; [ exact H | apply False_ind ].
 Qed.
 
+(** A weakest form of propositional extensionality: extensionality for
+    provable propositions only *)
+
+Definition provable_prop_extensionality := forall A:Prop, A -> A = True.
+
+Lemma provable_prop_ext :
+  prop_extensionality -> provable_prop_extensionality.
+Proof.
+  intros Ext A Ha; apply Ext; split; trivial.
+Qed.
+
 (************************************************************************)
 (** * Classical logic and proof-irrelevance *)
 
@@ -105,6 +116,7 @@ Qed.
         (just take the identity), which
      implies the existence of a fixpoint operator in [A]
         (e.g. take the Y combinator of lambda-calculus)
+
 *)
 
 Definition inhabited (A:Prop) := A.
@@ -143,6 +155,10 @@ Proof.
   reflexivity.
 Qed.
 
+(** Remark: [prop_extensionality] can be replaced in lemma [ext_prop_fixpoint]
+    by the weakest property [provable_prop_extensionality].
+*)
+
 (************************************************************************)
 (** ** CC |- prop_ext /\ dep elim on bool -> proof-irrelevance  *)
 
@@ -230,6 +246,11 @@ Section Proof_irrelevance_Prop_Ext_CC.
 
 End Proof_irrelevance_Prop_Ext_CC.
 
+(** Remark: [prop_extensionality] can be replaced in lemma
+    [ext_prop_dep_proof_irrel_gen] by the weakest property
+    [provable_prop_extensionality].  
+*)
+
 (************************************************************************)
 (** ** CIC |- prop. ext. -> proof-irrelevance                   *)